Require Export Setoid.
Require Omega.

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.

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.

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

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

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

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.