Library Sets

Require Export Setoid.
Require Omega.

Sets.v: Definition of sets as predicates over a type A

Section sets.
Variable A : Type.
Variable decA : x y :A, {x=y}+{x<>y}.

Definition set := AProp.
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 Qeqset Q P.

Lemma eqset_trans : P Q R:set,
   eqset P Qeqset Q Reqset P R.

Hint Resolve eqset_refl.
Hint Immediate eqset_sym.

Setoid structure

Lemma set_setoid : Setoid_Theory set eqset.

Add Setoid set eqset set_setoid as Set_setoid.

Add Morphism add : eqset_add.

Add Morphism rem : eqset_rem.
Hint Resolve eqset_add eqset_rem.

Add Morphism union : eqset_union.
Hint Immediate eqset_union.

Lemma eqset_union_left :
   P1 Q P2,
   eqset P1 P2eqset (union P1 Q) (union P2 Q).

Lemma eqset_union_right :
   P Q1 Q2 ,
   eqset Q1 Q2eqset (union P Q1) (union P Q2).

Hint Resolve eqset_union_left eqset_union_right.

Add Morphism inter : eqset_inter.
Hint Immediate eqset_inter.

Add Morphism compl : eqset_compl.
Hint Resolve eqset_compl.

Lemma eqset_add_empty : (a:A) (P:set), ¬eqset (add a P) empty.

Finite sets given as an enumeration of elements

Inductive finite (P: set) : Type :=
   fin_eq_empty : eqset P emptyfinite P
 | fin_eq_add : (x:A)(Q:set),
             ¬ Q xfinite Qeqset P (add x Q) → finite P.
Hint Constructors finite.

Lemma fin_empty : (finite empty).

Lemma fin_add : (x:A)(P:set),
             ¬ P xfinite Pfinite (add x P).

Lemma fin_eqset: (P Q : set), (eqset P Q)->(finite P)->(finite Q).

Hint Resolve fin_empty fin_add.

Emptyness is decidable for finite sets

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}.

Size of a finite set

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')

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 xQ x.

Lemma incl_refl : (P:set), incl P P.

Lemma incl_trans : (P Q R:set),
incl P Qincl Q Rincl P R.

Lemma eqset_incl : (P Q : set), eqset P Qincl P Q.

Lemma eqset_incl_sym : (P Q : set), eqset P Qincl Q P.

Lemma eqset_incl_intro :
(P Q : set), incl P Qincl Q Peqset P Q.

Hint Resolve incl_refl incl_trans eqset_incl_intro.
Hint Immediate eqset_incl eqset_incl_sym.

Properties of operations on sets

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 emptyP aFalse.

Hint Immediate incl_empty_false eqset_empty_false incl_add_empty.

Lemma incl_rem_stable : a P Q, incl P Qincl (rem a P) (rem a Q).

Lemma incl_add_stable : a P Q, incl P Qincl (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 aincl (add a Q) Pincl 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 aeqset (add a Q) Peqset 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<>yeqset (add x (rem y P)) (rem y (add x P)).

Lemma add_eqset_in :
   x (P:set), P xeqset (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 xeqset (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<>yeqset (rem x (add y P)) (add y (rem x P)).

Lemma rem_eqset_notin :
   x (P:set), ¬P xeqset (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 xeqset (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=yadd x P y.

Lemma add_intro : x (P:set) y, P yadd 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 Rincl Q Rincl (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 P2incl Q1 Q2incl (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 aeqset (inter P Q) (inter P (add a Q)).

Lemma inter_add_right_in : (a:A) (P Q: set),
      Q aeqset (add a (inter P Q)) (inter (add a P) Q).

Lemma inter_add_right_out : (a:A) (P Q: set),
      ¬ Q aeqset (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.

Generalized union

Definition gunion (I:Type)(F:Iset) : set := fun zexists i, F i z.

Lemma gunion_intro : I (F:Iset) i, incl (F i) (gunion F).

Lemma gunion_elim : I (F:Iset) (P:set), ( i, incl (F i) P) → incl (gunion F) P.

Lemma gunion_monotonic : I (F G : Iset),
      ( i, incl (F i) (G i))-> incl (gunion F) (gunion G).

Removing an element from a finite set

Lemma finite_rem : (P:set) (a:A),
   finite Pfinite (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.

Decidable sets

Definition dec (P:set) := x, {P x}+{¬ P x}.

Lemma finite_incl : P:set,
   finite P Q:set, dec Qincl Q Pfinite Q.

Lemma finite_dec : P:set, finite Pdec P.

Lemma fin_add_in : (a:A) (P:set), finite Pfinite (add a P).

Lemma finite_union :
      P Q, finite Pfinite Qfinite (union P Q).

Lemma finite_full_dec : P:set, finite fulldec Pfinite P.

Require Import Lt.

Filter operation

Lemma finite_inter : P Q, dec Pfinite Qfinite (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 xsize (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 xsize (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.

Selecting elements in a finite set

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
                Ofun ex
         | (S k1) ⇒ fun (e:S k1<S (size fq)) ⇒ nth_finite fq (lt_S_n k1 (size fq) e)

A set with size > 1 contains at least 2 different elements

Lemma select_non_empty : (P:set), finite Pnotempty PsigT P.

Lemma select_diff : (P:set) (FP:finite P),
     (1 < size FP)%natsigT (fun xsigT (fun yP 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
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.