Library ALEA.Sets
Section sets.
Variable A : Type.
Variable decA : forall x y :A, {x=y}+{x<>y}.
Definition set := A -> Prop.
Definition full : set := fun (x:A) => True.
Definition empty : set := fun (x:A) => False.
Definition add (a:A) (P:set) : set := fun (x:A) => x=a \/ (P x).
Definition singl (a:A) :set := fun (x:A) => x=a.
Definition union (P Q:set) :set := fun (x:A) => (P x) \/ (Q x).
Definition compl (P:set) :set := fun (x:A) => ~P x.
Definition inter (P Q:set) :set := fun (x:A) => (P x) /\ (Q x).
Definition rem (a:A) (P:set) :set := fun (x:A) => x<>a /\ (P x).
Definition eqset (P Q:set) := forall (x:A), P x <-> Q x.
Implicit Arguments full [].
Implicit Arguments empty [].
Lemma eqset_refl : forall P:set, eqset P P.
Lemma eqset_sym : forall P Q:set, eqset P Q -> eqset Q P.
Lemma eqset_trans : forall P Q R:set,
eqset P Q -> eqset Q R -> eqset P R.
Hint Resolve eqset_refl.
Hint Immediate eqset_sym.
Implicit Arguments full [].
Implicit Arguments empty [].
Lemma eqset_refl : forall P:set, eqset P P.
Lemma eqset_sym : forall P Q:set, eqset P Q -> eqset Q P.
Lemma eqset_trans : forall P Q R:set,
eqset P Q -> eqset Q R -> eqset P R.
Hint Resolve eqset_refl.
Hint Immediate eqset_sym.
Lemma set_setoid : Setoid_Theory set eqset.
Add Setoid set eqset set_setoid as Set_setoid.
Add Morphism add : eqset_add.
Save.
Add Morphism rem : eqset_rem.
Save.
Hint Resolve eqset_add eqset_rem.
Add Morphism union : eqset_union.
Save.
Hint Immediate eqset_union.
Lemma eqset_union_left :
forall P1 Q P2,
eqset P1 P2 -> eqset (union P1 Q) (union P2 Q).
Lemma eqset_union_right :
forall P Q1 Q2 ,
eqset Q1 Q2 -> eqset (union P Q1) (union P Q2).
Hint Resolve eqset_union_left eqset_union_right.
Add Morphism inter : eqset_inter.
Save.
Hint Immediate eqset_inter.
Add Morphism compl : eqset_compl.
Save.
Hint Resolve eqset_compl.
Lemma eqset_add_empty : forall (a:A) (P:set), ~eqset (add a P) empty.
Add Setoid set eqset set_setoid as Set_setoid.
Add Morphism add : eqset_add.
Save.
Add Morphism rem : eqset_rem.
Save.
Hint Resolve eqset_add eqset_rem.
Add Morphism union : eqset_union.
Save.
Hint Immediate eqset_union.
Lemma eqset_union_left :
forall P1 Q P2,
eqset P1 P2 -> eqset (union P1 Q) (union P2 Q).
Lemma eqset_union_right :
forall P Q1 Q2 ,
eqset Q1 Q2 -> eqset (union P Q1) (union P Q2).
Hint Resolve eqset_union_left eqset_union_right.
Add Morphism inter : eqset_inter.
Save.
Hint Immediate eqset_inter.
Add Morphism compl : eqset_compl.
Save.
Hint Resolve eqset_compl.
Lemma eqset_add_empty : forall (a:A) (P:set), ~eqset (add a P) empty.
Inductive finite (P: set) : Type :=
fin_eq_empty : eqset P empty -> finite P
| fin_eq_add : forall (x:A)(Q:set),
~ Q x-> finite Q -> eqset P (add x Q) -> finite P.
Hint Constructors finite.
Lemma fin_empty : (finite empty).
Lemma fin_add : forall (x:A)(P:set),
~ P x -> finite P -> finite (add x P).
Lemma fin_eqset: forall (P Q : set), (eqset P Q)->(finite P)->(finite Q).
Hint Resolve fin_empty fin_add.
Definition isempty (P:set) := eqset P empty.
Definition notempty (P:set) := not (eqset P empty).
Lemma isempty_dec : forall P, finite P -> {isempty P}+{notempty P}.
Definition notempty (P:set) := not (eqset P empty).
Lemma isempty_dec : forall P, finite P -> {isempty P}+{notempty P}.
Fixpoint size (P:set) (f:finite P) {struct f}: nat :=
match f with fin_eq_empty _ => 0%nat
| fin_eq_add _ Q _ f' _ => S (size f')
end.
Lemma size_eqset : forall P Q (f:finite P) (e:eqset P Q),
(size (fin_eqset e f)) = (size f).
match f with fin_eq_empty _ => 0%nat
| fin_eq_add _ Q _ f' _ => S (size f')
end.
Lemma size_eqset : forall P Q (f:finite P) (e:eqset P Q),
(size (fin_eqset e f)) = (size f).
Definition incl (P Q:set) := forall x, P x -> Q x.
Lemma incl_refl : forall (P:set), incl P P.
Lemma incl_trans : forall (P Q R:set),
incl P Q -> incl Q R -> incl P R.
Lemma eqset_incl : forall (P Q : set), eqset P Q -> incl P Q.
Lemma eqset_incl_sym : forall (P Q : set), eqset P Q -> incl Q P.
Lemma eqset_incl_intro :
forall (P Q : set), incl P Q -> incl Q P -> eqset P Q.
Hint Resolve incl_refl incl_trans eqset_incl_intro.
Hint Immediate eqset_incl eqset_incl_sym.
Lemma incl_refl : forall (P:set), incl P P.
Lemma incl_trans : forall (P Q R:set),
incl P Q -> incl Q R -> incl P R.
Lemma eqset_incl : forall (P Q : set), eqset P Q -> incl P Q.
Lemma eqset_incl_sym : forall (P Q : set), eqset P Q -> incl Q P.
Lemma eqset_incl_intro :
forall (P Q : set), incl P Q -> incl Q P -> eqset P Q.
Hint Resolve incl_refl incl_trans eqset_incl_intro.
Hint Immediate eqset_incl eqset_incl_sym.
Lemma incl_empty : forall P, incl empty P.
Lemma incl_empty_false : forall P a, incl P empty -> ~ P a.
Lemma incl_add_empty : forall (a:A) (P:set), ~ incl (add a P) empty.
Lemma eqset_empty_false : forall P a, eqset P empty -> P a -> False.
Hint Immediate incl_empty_false eqset_empty_false incl_add_empty.
Lemma incl_rem_stable : forall a P Q, incl P Q -> incl (rem a P) (rem a Q).
Lemma incl_add_stable : forall a P Q, incl P Q -> incl (add a P) (add a Q).
Lemma incl_rem_add_iff :
forall a P Q, incl (rem a P) Q <-> incl P (add a Q).
Lemma incl_rem_add:
forall (a:A) (P Q:set),
(P a) -> incl Q (rem a P) -> incl (add a Q) P.
Lemma incl_add_rem :
forall (a:A) (P Q:set),
~ Q a -> incl (add a Q) P -> incl Q (rem a P) .
Hint Immediate incl_rem_add incl_add_rem.
Lemma eqset_rem_add :
forall (a:A) (P Q:set),
(P a) -> eqset Q (rem a P) -> eqset (add a Q) P.
Lemma eqset_add_rem :
forall (a:A) (P Q:set),
~ Q a -> eqset (add a Q) P -> eqset Q (rem a P).
Hint Immediate eqset_rem_add eqset_add_rem.
Lemma add_rem_eq_eqset :
forall x (P:set), eqset (add x (rem x P)) (add x P).
Lemma add_rem_diff_eqset :
forall x y (P:set),
x<>y -> eqset (add x (rem y P)) (rem y (add x P)).
Lemma add_eqset_in :
forall x (P:set), P x -> eqset (add x P) P.
Hint Resolve add_rem_eq_eqset add_rem_diff_eqset add_eqset_in.
Lemma add_rem_eqset_in :
forall x (P:set), P x -> eqset (add x (rem x P)) P.
Hint Resolve add_rem_eqset_in.
Lemma rem_add_eq_eqset :
forall x (P:set), eqset (rem x (add x P)) (rem x P).
Lemma rem_add_diff_eqset :
forall x y (P:set),
x<>y -> eqset (rem x (add y P)) (add y (rem x P)).
Lemma rem_eqset_notin :
forall x (P:set), ~P x -> eqset (rem x P) P.
Hint Resolve rem_add_eq_eqset rem_add_diff_eqset rem_eqset_notin.
Lemma rem_add_eqset_notin :
forall x (P:set), ~P x -> eqset (rem x (add x P)) P.
Hint Resolve rem_add_eqset_notin.
Lemma rem_not_in : forall x (P:set), ~ rem x P x.
Lemma add_in : forall x (P:set), add x P x.
Lemma add_in_eq : forall x y P, x=y -> add x P y.
Lemma add_intro : forall x (P:set) y, P y -> add x P y.
Lemma add_incl : forall x (P:set), incl P (add x P).
Lemma add_incl_intro : forall x (P Q:set), (Q x) -> (incl P Q) -> (incl (add x P) Q).
Lemma rem_incl : forall x (P:set), incl (rem x P) P.
Hint Resolve rem_not_in add_in rem_incl add_incl.
Lemma union_sym : forall P Q : set,
eqset (union P Q) (union Q P).
Lemma union_empty_left : forall P : set,
eqset P (union P empty).
Lemma union_empty_right : forall P : set,
eqset P (union empty P).
Lemma union_add_left : forall (a:A) (P Q: set),
eqset (add a (union P Q)) (union P (add a Q)).
Lemma union_add_right : forall (a:A) (P Q: set),
eqset (add a (union P Q)) (union (add a P) Q).
Hint Resolve union_sym union_empty_left union_empty_right
union_add_left union_add_right.
Lemma union_incl_left : forall P Q, incl P (union P Q).
Lemma union_incl_right : forall P Q, incl Q (union P Q).
Lemma union_incl_intro : forall P Q R, incl P R -> incl Q R -> incl (union P Q) R.
Hint Resolve union_incl_left union_incl_right union_incl_intro.
Lemma incl_union_stable : forall P1 P2 Q1 Q2,
incl P1 P2 -> incl Q1 Q2 -> incl (union P1 Q1) (union P2 Q2).
Hint Immediate incl_union_stable.
Lemma inter_sym : forall P Q : set,
eqset (inter P Q) (inter Q P).
Lemma inter_empty_left : forall P : set,
eqset empty (inter P empty).
Lemma inter_empty_right : forall P : set,
eqset empty (inter empty P).
Lemma inter_add_left_in : forall (a:A) (P Q: set),
(P a) -> eqset (add a (inter P Q)) (inter P (add a Q)).
Lemma inter_add_left_out : forall (a:A) (P Q: set),
~ P a -> eqset (inter P Q) (inter P (add a Q)).
Lemma inter_add_right_in : forall (a:A) (P Q: set),
Q a -> eqset (add a (inter P Q)) (inter (add a P) Q).
Lemma inter_add_right_out : forall (a:A) (P Q: set),
~ Q a -> eqset (inter P Q) (inter (add a P) Q).
Hint Resolve inter_sym inter_empty_left inter_empty_right
inter_add_left_in inter_add_left_out inter_add_right_in inter_add_right_out.
Definition gunion (I:Type)(F:I->set) : set := fun z => exists i, F i z.
Lemma gunion_intro : forall I (F:I->set) i, incl (F i) (gunion F).
Lemma gunion_elim : forall I (F:I->set) (P:set), (forall i, incl (F i) P) -> incl (gunion F) P.
Lemma gunion_monotonic : forall I (F G : I -> set),
(forall i, incl (F i) (G i))-> incl (gunion F) (gunion G).
Lemma gunion_intro : forall I (F:I->set) i, incl (F i) (gunion F).
Lemma gunion_elim : forall I (F:I->set) (P:set), (forall i, incl (F i) P) -> incl (gunion F) P.
Lemma gunion_monotonic : forall I (F G : I -> set),
(forall i, incl (F i) (G i))-> incl (gunion F) (gunion G).
Definition dec (P:set) := forall x, {P x}+{ ~ P x}.
Definition dec2bool (P:set) : dec P -> A -> bool :=
fun p x => if p x then true else false.
Lemma compl_dec : forall P, dec P -> dec (compl P).
Lemma inter_dec : forall P Q, dec P -> dec Q -> dec (inter P Q).
Lemma union_dec : forall P Q, dec P -> dec Q -> dec (union P Q).
Hint Resolve compl_dec inter_dec union_dec.
Definition dec2bool (P:set) : dec P -> A -> bool :=
fun p x => if p x then true else false.
Lemma compl_dec : forall P, dec P -> dec (compl P).
Lemma inter_dec : forall P Q, dec P -> dec Q -> dec (inter P Q).
Lemma union_dec : forall P Q, dec P -> dec Q -> dec (union P Q).
Hint Resolve compl_dec inter_dec union_dec.
Lemma finite_rem : forall (P:set) (a:A),
finite P -> finite (rem a P).
Lemma size_finite_rem:
forall (P:set) (a:A) (f:finite P),
(P a) -> size f = S (size (finite_rem a f)).
Require Import Arith.
Lemma size_incl :
forall (P:set)(f:finite P) (Q:set)(g:finite Q),
(incl P Q)-> size f <= size g.
Lemma size_unique :
forall (P:set)(f:finite P) (Q:set)(g:finite Q),
(eqset P Q)-> size f = size g.
Lemma finite_incl : forall P:set,
finite P -> forall Q:set, dec Q -> incl Q P -> finite Q.
Lemma finite_dec : forall P:set, finite P -> dec P.
Lemma fin_add_in : forall (a:A) (P:set), finite P -> finite (add a P).
Lemma finite_union :
forall P Q, finite P -> finite Q -> finite (union P Q).
Lemma finite_full_dec : forall P:set, finite full -> dec P -> finite P.
Require Import Lt.
Lemma finite_inter : forall P Q, dec P -> finite Q -> finite (inter P Q).
Lemma size_inter_empty : forall P Q (decP:dec P) (e:eqset Q empty),
size (finite_inter decP (fin_eq_empty e))=O.
Lemma size_inter_add_in :
forall P Q R (decP:dec P)(x:A)(nq:~Q x)(FQ:finite Q)(e:eqset R (add x Q)),
P x ->size (finite_inter decP (fin_eq_add nq FQ e))=S (size (finite_inter decP FQ)).
Lemma size_inter_add_notin :
forall P Q R (decP:dec P)(x:A)(nq:~Q x)(FQ:finite Q)(e:eqset R (add x Q)),
~ P x -> size (finite_inter decP (fin_eq_add nq FQ e))=size (finite_inter decP FQ).
Lemma size_inter_incl : forall P Q (decP:dec P)(FP:finite P)(FQ:finite Q),
(incl P Q) -> size (finite_inter decP FQ)=size FP.
Fixpoint nth_finite (P:set) (k:nat) (PF : finite P) {struct PF}: (k < size PF) -> A :=
match PF as F return (k < size F) -> A with
fin_eq_empty H => (fun (e : k<0) => match lt_n_O k e with end)
| fin_eq_add x Q nqx fq eqq =>
match k as k0 return k0<S (size fq)->A with
O => fun e => x
| (S k1) => fun (e:S k1<S (size fq)) => nth_finite fq (lt_S_n k1 (size fq) e)
end
end.
A set with size > 1 contains at least 2 different elements
Lemma select_non_empty : forall (P:set), finite P -> notempty P -> sigT P.
Lemma select_diff : forall (P:set) (FP:finite P),
(1 < size FP)%nat -> sigT (fun x => sigT (fun y => P x /\ P y /\ x<>y)).
End sets.
Hint Resolve eqset_refl.
Hint Resolve eqset_add eqset_rem.
Hint Immediate eqset_sym finite_dec finite_full_dec eqset_incl eqset_incl_sym eqset_incl_intro.
Hint Resolve incl_refl.
Hint Immediate incl_union_stable.
Hint Resolve union_incl_left union_incl_right union_incl_intro incl_empty rem_incl
incl_rem_stable incl_add_stable.
Hint Constructors finite.
Hint Resolve add_in add_in_eq add_intro add_incl add_incl_intro union_sym union_empty_left union_empty_right
union_add_left union_add_right finite_union eqset_union_left
eqset_union_right.
Implicit Arguments full [].
Implicit Arguments empty [].
Add Parametric Relation (A:Type) : (set A) (eqset (A:=A))
reflexivity proved by (eqset_refl (A:=A))
symmetry proved by (eqset_sym (A:=A))
transitivity proved by (eqset_trans (A:=A))
as eqset_rel.
Add Parametric Relation (A:Type) : (set A) (incl (A:=A))
reflexivity proved by (incl_refl (A:=A))
transitivity proved by (incl_trans (A:=A))
as incl_rel.