Library Weight


Require Import Nat.
Require Import List.
Require Import Decidable.
Require Import Omega.
Require Import Permutation.

Require Import Tact.
Require Import Decide.

Definition sumweight {T : Type} (f : T -> nat) (l : list T) : nat
  :=
  fold_right (fun x m => f x + m) 0 l.

Lemma sumweight_cons :
  forall (T : Type) (f : T -> nat) (x : T) (l : list T),
    sumweight f (cons x l) = f x + sumweight f l.

Lemma sumweight_app :
  forall (T : Type) (f : T -> nat) (p q : list T),
    sumweight f (p ++ q) = sumweight f p + sumweight f q.
Lemma NoDup_app :
  forall (T : Type) (p q : list T),
    NoDup p
    -> NoDup q
    -> (forall x, In x p -> In x q -> False)
    -> NoDup (p ++ q).
Lemma permutation_weight :
  forall (T : Type) (f : T -> nat) (p q : list T),
    Permutation p q
    -> sumweight f p = sumweight f q.
Lemma permutation_weight' :
  forall (T : Type) (f : T -> nat) (p q : list T),
    NoDup p
    -> NoDup q
    -> (forall x, In x p <-> In x q)
    -> sumweight f p = sumweight f q.

Lemma incl_weight :
  forall (T : Type) (f : T -> nat) (p q : list T),
    NoDup p
    -> NoDup q
    -> List.incl p q
    -> sumweight f p <= sumweight f q.
Lemma inclusion_exclusion :
  forall T (f : T -> nat) (p q u : list T),
    (forall (x y : T), decidable (x = y))
    -> NoDup p
    -> NoDup q
    -> NoDup u
    -> List.incl p u
    -> List.incl q u
    -> exists r,
         NoDup r
         /\ List.incl r p
         /\ List.incl r q
         /\ sumweight f r >= sumweight f p + sumweight f q - sumweight f u.
Lemma enumerate_subset :
  forall T (P : T -> Prop) (u : list T),
    (forall x, In x u -> decidable (P x))
    -> NoDup u
    -> exists p,
         NoDup p
         /\ forall x, In x p <-> (P x /\ In x u).
Lemma deduplicate :
  forall T (l : list T),
    (forall (x y : T), decidable (x = y))
    -> exists l',
         NoDup l'
         /\ (forall x, In x l <-> In x l').
Definition weight {T : Type} (f : T -> nat) (P : T -> Prop) (n : nat) : Prop
  :=
  exists l,
    NoDup l
    /\ (forall x, P x <-> In x l)
    /\ sumweight f l = n.

Lemma weight_empty :
  forall T f, weight f (fun (x : T) => False) 0.

Lemma weight_singleton :
  forall (T : Type) (f : T -> nat) (x : T),
    weight f (fun y => y = x) (f x).

Lemma weight_In :
  forall (T : Type) (f : T -> nat) (l : list T),
    NoDup l
    -> weight f (fun x => In x l) (sumweight f l).

Lemma weight_fun :
  forall (T : Type) (f : T -> nat) (P : T -> Prop) n n',
    weight f P n
    -> weight f P n'
    -> n = n'.

Lemma weight_iff :
  forall (T : Type) (f : T -> nat) (P Q : T -> Prop) n,
    (forall x, P x <-> Q x)
    -> weight f P n
    -> weight f Q n.

Lemma weight_empty' :
  forall T (f : T -> nat) (P : T -> Prop),
    (forall x, ~ P x)
    -> weight f P 0.
Lemma weight_nonempty :
  forall T (f : T -> nat) (P : T -> Prop) p,
    weight f P p
    -> p > 0
    -> exists x, P x.

Lemma weight_subset :
  forall (T : Type) (f : T -> nat) (P Q : T -> Prop) n,
    (forall x, Q x -> decidable (P x))
    -> incl P Q
    -> weight f Q n
    -> exists m,
         weight f P m
         /\ m <= n.

Lemma weight_subset' :
  forall (T : Type) (f : T -> nat) (P Q : T -> Prop) m n,
    (forall x, Q x -> decidable (P x))
    -> incl P Q
    -> weight f P m
    -> weight f Q n
    -> m <= n.

Lemma weight_sum :
  forall T (f : T -> nat) (A B : T -> Prop) a b,
    weight f A a
    -> weight f B b
    -> (forall x, A x -> B x -> False)
    -> weight f (fun x => A x \/ B x) (a + b).

Lemma NoDup_weight_incl :
  forall T (f : T -> nat) (l l' : list T),
    NoDup l
    -> (forall x, In x l' -> f x > 0)
    -> sumweight f l' <= sumweight f l
    -> List.incl l l'
    -> List.incl l' l.

Lemma weight_partition :
  forall T (f : T -> nat) (A B U : T -> Prop) a b,
    incl A U
    -> incl B U
    -> (forall x, U x -> f x > 0)
    -> weight f U (a + b)
    -> weight f A a
    -> weight f B b
    -> (forall x, A x -> B x -> False)
    -> forall x, U x -> A x \/ B x.

Lemma weight_difference :
  forall T (f : T -> nat) (A B : T -> Prop) a b,
    (forall (x y : T), decidable (x = y))
    -> weight f A a
    -> weight f B b
    -> a < b
    -> exists x, ~ A x /\ B x.
Lemma weight_corr_le :
  forall S T (f : S -> nat) (g : T -> nat) (P : S -> Prop) (Q : T -> Prop) (R : S -> T -> Prop) p q,
    (forall x x' y, P x -> P x' -> Q y -> R x y -> R x' y -> x = x')
    -> (forall x, P x -> exists y, R x y /\ Q y /\ f x <= g y)
    -> weight f P p
    -> weight g Q q
    -> p <= q.
Lemma weight_corr_eq :
  forall S T (f : S -> nat) (g : T -> nat) (P : S -> Prop) (Q : T -> Prop) (R : S -> T -> Prop) p q,
    (forall x x' y, P x -> P x' -> Q y -> R x y -> R x' y -> x = x')
    -> (forall x y y', P x -> Q y -> Q y' -> R x y -> R x y' -> y = y')
    -> (forall x, P x -> exists y, R x y /\ Q y /\ f x = g y)
    -> (forall y, Q y -> exists x, R x y /\ P x /\ f x = g y)
    -> weight f P p
    -> weight g Q q
    -> p = q.

Lemma weight_map_inj :
  forall S T (g : S -> nat) (h : T -> nat) (P : S -> Prop) (Q : T -> Prop) (f : S -> T) p q,
    (forall x, P x -> Q (f x) /\ g x <= h (f x))
    -> (forall x y, P x -> P y -> f x = f y -> x = y)
    -> weight g P p
    -> weight h Q q
    -> p <= q.

Lemma weight_map_surj :
  forall S T (g : S -> nat) (h : T -> nat) (P : S -> Prop) (Q : T -> Prop) (f : T -> S) p q,
    (forall x, Q x -> P (f x) /\ g (f x) <= h x)
    -> (forall x, P x -> exists y, Q y /\ x = f y)
    -> weight g P p
    -> weight h Q q
    -> p <= q.

Lemma weight_incl :
  forall T (f : T -> nat) (P Q : T -> Prop) p q,
    incl P Q
    -> weight f P p
    -> weight f Q q
    -> p <= q.


Lemma fold_right_map :
  forall S T U (f : S -> T) (g : T -> U -> U) (l : list S) (x : U),
    fold_right g x (map f l) = fold_right (fun y z => g (f y) z) x l.

Lemma fold_right_ext_in :
  forall T U (f f' : T -> U -> U) (l : list T) (x : U),
    (forall y z, In y l -> f y z = f' y z)
    -> fold_right f x l = fold_right f' x l.

Lemma weight_image :
  forall S T (g : S -> nat) (h : T -> nat) (P : S -> Prop) (f : S -> T) n,
    (forall x, P x -> g x = h (f x))
    -> (forall x y, P x -> P y -> f x = f y -> x = y)
    -> weight g P n
    -> weight h (fun x => exists y, x = f y /\ P y) n.

Lemma weight_finite :
  forall T (f : T -> nat) (P : T -> Prop) n, weight f P n -> finite P.

Lemma finite_weight :
  forall T (f : T -> nat) (P : T -> Prop),
    (forall (x y : T), decidable (x = y))
    -> finite P
    -> exists n, weight f P n.

Lemma weight_gt_decide :
  forall (T : Type) (f : T -> nat) (P U : T -> Prop) n n',
    (forall x, decidable (P x))
    -> incl P U
    -> weight f U n
    -> decidable (exists p, weight f P p /\ p > n').

Definition weight_lt {T : Type} (f : T -> nat) (P : T -> Prop) (n : nat) : Prop
  :=
  ~ exists l,
      NoDup l
      /\ (forall x, In x l -> P x)
      /\ sumweight f l >= n.

Lemma weight_impl_weight_lt :
  forall T (f : T -> nat) (P : T -> Prop) m n,
    m < n
    -> weight f P m
    -> weight_lt f P n.

Lemma weight_lt_increase :
  forall T (f : T -> nat) (P : T -> Prop) m n,
    m <= n
    -> weight_lt f P m
    -> weight_lt f P n.

Lemma weight_lt_impl_lt :
  forall T (f : T -> nat) (P Q : T -> Prop) p q,
    incl P Q
    -> weight f P p
    -> weight_lt f Q q
    -> p < q.

Lemma weight_lt_by_contradiction :
  forall T (f : T -> nat) (P : T -> Prop) p,
    (forall Q q, incl Q P -> weight f Q q -> q >= p -> False)
    -> weight_lt f P p.