Library Sets
Section sets.
Variable A : Type.
Variable decA : ∀ 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) := ∀ (x:A), P x ↔ Q x.
Implicit Arguments full [].
Implicit Arguments empty [].
Lemma eqset_refl : ∀ P:set, eqset P P.
Lemma eqset_sym : ∀ P Q:set, eqset P Q → eqset Q P.
Lemma eqset_trans : ∀ 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 : ∀ P:set, eqset P P.
Lemma eqset_sym : ∀ P Q:set, eqset P Q → eqset Q P.
Lemma eqset_trans : ∀ 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 :
∀ P1 Q P2,
eqset P1 P2 → eqset (union P1 Q) (union P2 Q).
Lemma eqset_union_right :
∀ 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 : ∀ (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 :
∀ P1 Q P2,
eqset P1 P2 → eqset (union P1 Q) (union P2 Q).
Lemma eqset_union_right :
∀ 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 : ∀ (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 : ∀ (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 : ∀ (x:A)(P:set),
¬ P x → finite P → finite (add x P).
Lemma fin_eqset: ∀ (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 : ∀ P, finite P → {isempty P}+{notempty P}.
Definition notempty (P:set) := not (eqset P empty).
Lemma isempty_dec : ∀ 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 : ∀ 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 : ∀ P Q (f:finite P) (e:eqset P Q),
(size (fin_eqset e f)) = (size f).
Definition incl (P Q:set) := ∀ x, P x → Q x.
Lemma incl_refl : ∀ (P:set), incl P P.
Lemma incl_trans : ∀ (P Q R:set),
incl P Q → incl Q R → incl P R.
Lemma eqset_incl : ∀ (P Q : set), eqset P Q → incl P Q.
Lemma eqset_incl_sym : ∀ (P Q : set), eqset P Q → incl Q P.
Lemma eqset_incl_intro :
∀ (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 : ∀ (P:set), incl P P.
Lemma incl_trans : ∀ (P Q R:set),
incl P Q → incl Q R → incl P R.
Lemma eqset_incl : ∀ (P Q : set), eqset P Q → incl P Q.
Lemma eqset_incl_sym : ∀ (P Q : set), eqset P Q → incl Q P.
Lemma eqset_incl_intro :
∀ (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 : ∀ P, incl empty P.
Lemma incl_empty_false : ∀ P a, incl P empty → ¬ P a.
Lemma incl_add_empty : ∀ (a:A) (P:set), ¬ incl (add a P) empty.
Lemma eqset_empty_false : ∀ P a, eqset P empty → P a → False.
Hint Immediate incl_empty_false eqset_empty_false incl_add_empty.
Lemma incl_rem_stable : ∀ a P Q, incl P Q → incl (rem a P) (rem a Q).
Lemma incl_add_stable : ∀ a P Q, incl P Q → incl (add a P) (add a Q).
Lemma incl_rem_add_iff :
∀ a P Q, incl (rem a P) Q ↔ incl P (add a Q).
Lemma incl_rem_add:
∀ (a:A) (P Q:set),
(P a) → incl Q (rem a P) → incl (add a Q) P.
Lemma incl_add_rem :
∀ (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 :
∀ (a:A) (P Q:set),
(P a) → eqset Q (rem a P) → eqset (add a Q) P.
Lemma eqset_add_rem :
∀ (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 :
∀ x (P:set), eqset (add x (rem x P)) (add x P).
Lemma add_rem_diff_eqset :
∀ x y (P:set),
x<>y → eqset (add x (rem y P)) (rem y (add x P)).
Lemma add_eqset_in :
∀ 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 :
∀ x (P:set), P x → eqset (add x (rem x P)) P.
Hint Resolve add_rem_eqset_in.
Lemma rem_add_eq_eqset :
∀ x (P:set), eqset (rem x (add x P)) (rem x P).
Lemma rem_add_diff_eqset :
∀ x y (P:set),
x<>y → eqset (rem x (add y P)) (add y (rem x P)).
Lemma rem_eqset_notin :
∀ 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 :
∀ x (P:set), ¬P x → eqset (rem x (add x P)) P.
Hint Resolve rem_add_eqset_notin.
Lemma rem_not_in : ∀ x (P:set), ¬ rem x P x.
Lemma add_in : ∀ x (P:set), add x P x.
Lemma add_in_eq : ∀ x y P, x=y → add x P y.
Lemma add_intro : ∀ x (P:set) y, P y → add x P y.
Lemma add_incl : ∀ x (P:set), incl P (add x P).
Lemma add_incl_intro : ∀ x (P Q:set), (Q x) → (incl P Q) → (incl (add x P) Q).
Lemma rem_incl : ∀ x (P:set), incl (rem x P) P.
Hint Resolve rem_not_in add_in rem_incl add_incl.
Lemma union_sym : ∀ P Q : set,
eqset (union P Q) (union Q P).
Lemma union_empty_left : ∀ P : set,
eqset P (union P empty).
Lemma union_empty_right : ∀ P : set,
eqset P (union empty P).
Lemma union_add_left : ∀ (a:A) (P Q: set),
eqset (add a (union P Q)) (union P (add a Q)).
Lemma union_add_right : ∀ (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 : ∀ P Q, incl P (union P Q).
Lemma union_incl_right : ∀ P Q, incl Q (union P Q).
Lemma union_incl_intro : ∀ 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 : ∀ 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 : ∀ P Q : set,
eqset (inter P Q) (inter Q P).
Lemma inter_empty_left : ∀ P : set,
eqset empty (inter P empty).
Lemma inter_empty_right : ∀ P : set,
eqset empty (inter empty P).
Lemma inter_add_left_in : ∀ (a:A) (P Q: set),
(P a) → eqset (add a (inter P Q)) (inter P (add a Q)).
Lemma inter_add_left_out : ∀ (a:A) (P Q: set),
¬ P a → eqset (inter P Q) (inter P (add a Q)).
Lemma inter_add_right_in : ∀ (a:A) (P Q: set),
Q a → eqset (add a (inter P Q)) (inter (add a P) Q).
Lemma inter_add_right_out : ∀ (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 : ∀ I (F:I→set) i, incl (F i) (gunion F).
Lemma gunion_elim : ∀ I (F:I→set) (P:set), (∀ i, incl (F i) P) → incl (gunion F) P.
Lemma gunion_monotonic : ∀ I (F G : I → set),
(∀ i, incl (F i) (G i))-> incl (gunion F) (gunion G).
Lemma gunion_intro : ∀ I (F:I→set) i, incl (F i) (gunion F).
Lemma gunion_elim : ∀ I (F:I→set) (P:set), (∀ i, incl (F i) P) → incl (gunion F) P.
Lemma gunion_monotonic : ∀ I (F G : I → set),
(∀ i, incl (F i) (G i))-> incl (gunion F) (gunion G).
Lemma finite_rem : ∀ (P:set) (a:A),
finite P → finite (rem a P).
Lemma size_finite_rem:
∀ (P:set) (a:A) (f:finite P),
(P a) → size f = S (size (finite_rem a f)).
Require Import Arith.
Lemma size_incl :
∀ (P:set)(f:finite P) (Q:set)(g:finite Q),
(incl P Q)-> size f ≤ size g.
Lemma size_unique :
∀ (P:set)(f:finite P) (Q:set)(g:finite Q),
(eqset P Q)-> size f = size g.
Definition dec (P:set) := ∀ x, {P x}+{¬ P x}.
Lemma finite_incl : ∀ P:set,
finite P → ∀ Q:set, dec Q → incl Q P → finite Q.
Lemma finite_dec : ∀ P:set, finite P → dec P.
Lemma fin_add_in : ∀ (a:A) (P:set), finite P → finite (add a P).
Lemma finite_union :
∀ P Q, finite P → finite Q → finite (union P Q).
Lemma finite_full_dec : ∀ P:set, finite full → dec P → finite P.
Require Import Lt.
Lemma finite_incl : ∀ P:set,
finite P → ∀ Q:set, dec Q → incl Q P → finite Q.
Lemma finite_dec : ∀ P:set, finite P → dec P.
Lemma fin_add_in : ∀ (a:A) (P:set), finite P → finite (add a P).
Lemma finite_union :
∀ P Q, finite P → finite Q → finite (union P Q).
Lemma finite_full_dec : ∀ P:set, finite full → dec P → finite P.
Require Import Lt.
Lemma finite_inter : ∀ P Q, dec P → finite Q → finite (inter P Q).
Lemma size_inter_empty : ∀ P Q (decP:dec P) (e:eqset Q empty),
size (finite_inter decP (fin_eq_empty e))=O.
Lemma size_inter_add_in :
∀ 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 :
∀ 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 : ∀ 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 : ∀ (P:set), finite P → notempty P → sigT P.
Lemma select_diff : ∀ (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.