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.