(****************************************************************************)
(*                                                                          *)
(*                         Naive Set Theory in Coq                          *)
(*                                                                          *)
(*                     INRIA                        INRIA                   *)
(*              Rocquencourt                        Sophia-Antipolis        *)
(*                                                                          *)
(*                                 Coq V6.1                                 *)
(*									    *)
(*			         Gilles Kahn 				    *)
(*				 Gerard Huet				    *)
(*									    *)
(*									    *)
(*                                                                          *)
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks  *)
(* to the Newton Institute for providing an exceptional work environment    *)
(* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
(****************************************************************************)

Require Export Ensembles.

Section Ensembles_facts.
Variable U: Type.

Lemma Extension: (B, C: (Ensemble U)) B == C -> (Same_set U B C).
Proof.
Intros B C H'; Rewrite H'; Auto.
Qed.

Lemma Noone_in_empty: (x: U) ~ (In U (Empty_set U) x).
Proof.
Intro x; Red; Induction 1.
Qed.
Hint Noone_in_empty.

Lemma Included_Empty: (A: (Ensemble U))(Included U (Empty_set U) A).
Proof.
Intro; Red.
Intros x H; Elim (Noone_in_empty x); Auto.
Qed.
Hint Included_Empty.

Lemma Add_intro1:
  (A: (Ensemble U)) (x, y: U) (In U A y) -> (In U (Add U A x) y).
Proof.
Unfold 1 Add; Auto.
Qed.
Hint Add_intro1.

Lemma Add_intro2: (A: (Ensemble U)) (x: U) (In U (Add U A x) x).
Proof.
Unfold 1 Add; Auto.
Qed.
Hint Add_intro2.

Lemma Inhabited_add: (A: (Ensemble U)) (x: U) (Inhabited U (Add U A x)).
Proof.
Intros A x.
Apply Inhabited_intro with x := x; Auto.
Qed.
Hint Inhabited_add.

Lemma Inhabited_not_empty:
  (X: (Ensemble U)) (Inhabited U X) -> ~ X == (Empty_set U).
Proof.
Intros X H'; Elim H'.
Intros x H'0; Red; Intro H'1.
Absurd (In U X x); Auto.
Rewrite H'1; Auto.
Qed.
Hint Inhabited_not_empty.

Lemma Add_not_Empty :
 (A: (Ensemble U)) (x: U) ~ (Add U A x) == (Empty_set U).
Proof.
Auto.
Qed.
Hint Add_not_Empty.

Lemma not_Empty_Add :
 (A: (Ensemble U)) (x: U) ~ (Empty_set U) == (Add U A x).
Proof.
Intros; Red; Intro H; Generalize (Add_not_Empty A x); Auto.
Qed.
Hint not_Empty_Add.

Lemma Singleton_inv: (x, y: U) (In U (Singleton U x) y) -> x == y.
Proof.
Intros x y H'; Elim H'; Trivial.
Qed.
Hint Singleton_inv.

Lemma Singleton_intro: (x, y: U) x == y -> (In U (Singleton U x) y).
Proof.
Intros x y H'; Rewrite H'; Trivial.
Qed.
Hint Singleton_intro.

Lemma Union_inv:  (B, C: (Ensemble U)) (x: U) 
  (In U (Union U B C) x) -> (In U B x) \/ (In U C x).
Proof.
Intros B C x H'; Elim H'; Auto.
Qed.

Lemma Add_inv:
  (A: (Ensemble U)) (x, y: U) (In U (Add U A x) y) -> (In U A y) \/ x == y.
Proof.
Intros A x y H'; Elim H'; Auto.
Qed.

Lemma Intersection_inv:
  (B, C: (Ensemble U)) (x: U) (In U (Intersection U B C) x) ->
   (In U B x) /\ (In U C x).
Proof.
Intros B C x H'; Elim H'; Auto.
Qed.
Hint Intersection_inv.

Lemma Couple_inv: (x, y, z: U) (In U (Couple U x y) z) -> z == x \/ z == y.
Proof.
Intros x y z H'; Elim H'; Auto.
Qed.
Hint Couple_inv.

Lemma Setminus_intro:
  (A, B: (Ensemble U)) (x: U) (In U A x) -> ~ (In U B x) ->
   (In U (Setminus U A B) x).
Proof.
Unfold 1 Setminus; Red; Auto.
Qed.
Hint Setminus_intro.
 
Lemma Strict_Included_intro:
  (X, Y: (Ensemble U)) (Included U X Y) /\ ~ X == Y -> 
                       (Strict_Included U X Y).
Proof.
Auto.
Qed.
Hint Strict_Included_intro.

Lemma Strict_Included_strict: (X: (Ensemble U)) ~ (Strict_Included U X X).
Proof.
Intro X; Red; Intro H'; Elim H'.
Intros H'0 H'1; Elim H'1; Auto.
Qed.
Hint Strict_Included_strict.

End Ensembles_facts.

Hint Singleton_inv.
Hint Singleton_intro.
Hint Add_intro1.
Hint Add_intro2.
Hint Intersection_inv.
Hint Couple_inv.
Hint Setminus_intro.
Hint Strict_Included_intro.
Hint Strict_Included_strict.
Hint Noone_in_empty.
Hint Inhabited_not_empty.
Hint Add_not_Empty.
Hint not_Empty_Add.
Hint Inhabited_add.
Hint Included_Empty.

(* $Id: Constructive_sets.v,v 1.2 1996/09/26 14:03:17 jcfillia Exp $ *)
