--- /dev/null
+(******************************************************************************)
+(* Zermelo Set Theory + atomic sets *)
+(* *)
+(* Claudio Sacerdoti Coen *)
+(* *)
+(* Based on *)
+(* *)
+(* Zermolo Set Theory *)
+(* *)
+(* Benjamin Werner *)
+(* *)
+(******************************************************************************)
+
+(* This is an extension of Benjamin's encoding of usual Set Theory where I *)
+(* assume the existence of exactly one atomic set for each object t of type T *)
+(* where T is a Type in Coq: if (t:T) and (T:Type) then ((atom T t):Ens) *)
+(* The usual axioms of set theory are modified so that they work in the *)
+(* usual way if applied to "normal" sets, and in a reasonable way when *)
+(* applied to atomic sets (for example (Union (atom T t) E) is equal to E for *)
+(* each non-atomic set E) *)
+(* All this has been already studied by Fraenkel and Mostowski in the '40, *)
+(* but with totally different goals (in order to proove some independence *)
+(* results in set theory) *)
+
+(* This is the introduction to the original encoding of Benjamin: *)
+(* This is an encoding of usual Set Theory, simillar to Peter Aczel's work *)
+(* in the early 80's. The main difference is that the propositions here *)
+(* live in the impredicative world of "Prop". Thus, priority is given to *)
+(* expressivity against constructivity. *)
+(* *)
+(* Since the definition of Sets is the same for both approaches, I added *)
+(* most of Aczel's encoding of CZF at the end of the file. Many *)
+(* definitions are common to both aproaches. *)
+
+(* In this work only the encoding of ZFC (and not that of CZF) has been *)
+(* developed, but it should be straightforward to do. *)
+
+Require csc_eqdep.
+
+(******************************************************************************)
+(* Useful data types *)
+(******************************************************************************)
+
+Inductive Set F := .
+
+Inductive Set Un := void : Un.
+
+(* Existential quantification *)
+Inductive EXType [P:Type; Q:P->Prop]: Prop :=
+ EXTypei : (x:P)(Q x)->(EXType P Q).
+
+(* Sigma types -- i.e. computational existentials *)
+Inductive sig [A:Type;P:A->Prop] : Type :=
+ exist : (x:A)(P x)->(sig A P).
+
+(* Existential on the Type level *)
+Inductive depprod [A:Type; P : A->Type] : Type :=
+ dep_i : (x:A)(P x)->(depprod A P).
+
+(* Cartesian product in Type *)
+Inductive prod_t [A,B:Type] : Type :=
+ pair_t : A->B->(prod_t A B).
+
+(******************************************************************************)
+(* Definition of Ens, EQ, IN *)
+(******************************************************************************)
+
+(* The type representing sets (Ensemble = french for set) *)
+Inductive Ens : Type :=
+ sup : (A:Type)(A->Ens)->Ens
+ | atom : (A:Type)A->Ens.
+
+(* Recursive Definition of the extentional equality on sets *)
+Definition EQ : Ens -> Ens -> Prop.
+Induction 1.
+Intros A f eq1.
+Induction 1.
+Intros B g eq2.
+Apply and.
+Exact (x:A)
+ (EXType ? [y:B](eq1 x (g y))).
+Exact (y:B)
+ (EXType ? [x:A](eq1 x (g y))).
+
+Intros A' a'.
+Exact False.
+
+Intros A a.
+Induction 1.
+Intros A' f eq1.
+Exact False.
+
+Intros.
+(*Exact (X == X0).*)
+Exact (eq_depT Type [A:Type]A A a A0 y).
+Save.
+
+Transparent EQ.
+
+(* Membership on sets *)
+Definition IN: Ens -> Ens -> Prop :=
+[E1,E2:Ens]
+ Cases E2 of
+ (sup A f) => (EXType ? [y:A](EQ E1 (f y)))
+ | (atom A a) => False
+ end.
+Transparent IN.
+
+
+(******************************************************************************)
+(* INCLUSION *)
+(******************************************************************************)
+
+Definition INC : Ens -> Ens -> Prop :=
+ [E1,E2:Ens]
+ Cases E1 E2 of
+ (sup A f) (sup B g) => (E:Ens)(IN E E1)->(IN E E2)
+ | (sup A f) (atom B b) => False
+ | (atom A a) (sup B g) => False (* ??? or True? *)
+ | (atom A a) (atom B b) => (EQ E1 E2) (* ??? or False? *)
+ end.
+
+(* EQ is an equivalence relation *)
+
+Theorem EQ_refl : (E:Ens)(EQ E E).
+Induction E.
+Intros; Split; Simpl; Intro.
+Exists x; Exact (H x).
+Exists y; Exact (H y).
+Intros; Simpl; Constructor 1.
+Qed.
+
+Theorem EQ_tran : (E1,E2,E3:Ens)(EQ E1 E2)->(EQ E2 E3)->(EQ E1 E3).
+Induction E1; [Intros A1 f1 r1 | Intros A1 a1] ;
+Induction E2; [Intros A2 f2 r2 | Intros A2 a2 | Intros A2 f2 r2 | Intros A2 a2];
+Induction E3; [Intros A3 f3 r3 | Auto | Contradiction | Auto |
+ Auto | Contradiction | Auto | Intros A3 a3].
+Simpl; Intros e1 e2; Split; Elim e1; Intros I1 I2; Elim e2; Intros I3 I4;
+ [ Intros a1; Elim (I1 a1) ; Intros a2 ; Elim (I3 a2) ; Intros a3 ; Exists a3 |
+ Intros a3; Elim (I4 a3) ; Intros a2 ; Elim (I2 a2) ; Intros a1 ; Exists a1 ];
+ Apply r1 with (f2 a2); Assumption.
+
+Simpl ; Intros; Inversion H; Inversion H0; Assumption.
+Qed.
+
+Theorem EQ_sym : (E1,E2:Ens)(EQ E1 E2)->(EQ E2 E1).
+Induction E1 ; [ Intros A1 f1 r1 | Intros A1 a1 ];
+Induction E2 ; [Intros A2 f2 r2 | Contradiction | Contradiction |Intros A2 a2].
+
+Induction 1; Intros e1 e2; Split;
+ [ Intros a2; Elim (e2 a2); Intros a1 H1; Exists a1 |
+ Intros a1; Elim (e1 a1); Intros a2 H2; Exists a2 ] ; Apply r1; Assumption.
+Destruct 1; Apply EQ_refl.
+Qed.
+
+Theorem EQ_INC : (E,E':Ens)(EQ E E')->(INC E E').
+Induction E ; [Intros A f r | Intros A a] ; Induction E' ;
+ [Intros A' f' r' | Contradiction | Contradiction | Intros A' a'].
+Simpl; Destruct 1; Intros e1 e2.
+Intros C; Induction 1; Intros a ea; Elim (e1 a); Intros a' ea'; Exists a'.
+Apply EQ_tran with (f a); Assumption.
+Destruct 1; Hnf; Constructor 1.
+Qed.
+
+Hints Resolve EQ_sym EQ_refl EQ_INC : zfc.
+
+Theorem INC_EQ : (E,E':Ens)(INC E E')->(INC E' E)->(EQ E E').
+Induction E ; [Intros A f r | Intros A a] ; Induction E' ;
+ [Intros A' f' r' | Auto | Auto | Auto].
+Unfold INC; Simpl; Intros I1 I2; Split.
+Intros a; Apply I1; Exists a; Apply EQ_refl.
+Intros a'; Cut (EXType A [x:A](EQ (f' a')(f x))).
+Induction 1; Intros a ea; Exists a; Apply EQ_sym; Exact ea.
+Apply I2; Exists a'; Apply EQ_refl.
+Qed.
+
+Hints Resolve INC_EQ : zfc.
+
+(* Membership is extentional (i.e. is stable w.r.t. EQ) *)
+
+Theorem IN_sound_left :
+ (E,E',E'':Ens)
+ (EQ E E')->(IN E E'')->(IN E' E'').
+Induction E''; [Intros A'' f'' r'' e | Intros A'' a'' e]; Simpl.
+Induction 1; Intros a'' p; Exists a''; Apply EQ_tran with E;
+ [Apply EQ_sym; Assumption | Assumption].
+
+Intro; Assumption.
+Qed.
+
+Theorem IN_sound_right :
+ (E,E',E'':Ens)
+ (EQ E' E'')->(IN E E')->(IN E E'').
+Induction E'; [Intros A' f' r' | Intros A' a']; Induction E'';
+ [Intros A'' f'' r'' | Intros A'' a'' | Intros A'' f'' r'' | Intros A'' a''];
+ Simpl.
+Induction 1; Intros e1 e2; Induction 1; Intros a' e'; Elim (e1 a');
+ Intros a'' e''; Exists a''; Apply EQ_tran with (f' a'); Assumption.
+Intros; Assumption.
+Intros; Elim H.
+Intros; Assumption.
+Qed.
+
+(* Inclusion is reflexive, transitive, extentional *)
+
+Theorem INC_refl : (E:Ens)(INC E E).
+Induction E; Auto with zfc.
+Qed.
+
+Theorem INC_tran : (E,E',E'':Ens)(INC E E')->(INC E' E'')->(INC E E'').
+Induction E; Induction E'; Induction E''; Simpl;
+ Auto Orelse Contradiction Orelse (Intros; Elim H0; Assumption).
+Qed.
+
+Theorem INC_sound_left :
+ (E,E',E'':Ens)
+ (EQ E E')->(INC E E'')->(INC E' E'').
+Induction E; [Intros A f r | Intros A a]; Induction E';
+ [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a'];
+ Induction E''; [Intros A'' f'' r'' | Contradiction | Contradiction |
+ Contradiction | Contradiction | Contradiction | Contradiction |
+ Intros A'' a''].
+Unfold INC; Intros; Apply H0; Apply IN_sound_right with (sup A' f');
+ Auto with zfc.
+Destruct 1; Auto.
+Qed.
+
+Theorem INC_sound_right :
+ (E,E',E'':Ens)
+ (EQ E' E'')->(INC E E')->(INC E E'').
+Induction E; [Intros A f r | Intros A a]; Induction E';
+ [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a'];
+ Induction E''; [Intros A'' f'' r'' | Contradiction | Contradiction |
+ Contradiction | Contradiction | Contradiction | Contradiction |
+ Intros A'' a''].
+Unfold INC; Intros; Apply IN_sound_right with (sup A' f');
+ [Assumption | Apply H0; Assumption].
+Destruct 1; Auto.
+Qed.
+
+(******************************************************************************)
+(* THE EMPTY SET *)
+(******************************************************************************)
+
+(* The empty set (vide = french for empty) *)
+Definition Vide : Ens :=
+ (sup F [f:F]<Ens>Cases f of end).
+
+Theorem Vide_est_vide : (E:Ens)(IN E Vide)->F.
+Unfold Vide; Simpl; Intros E H; Cut False.
+Induction 1.
+Elim H; Intros x; Elim x.
+Qed.
+
+(* CSC: This is different from Werner *)
+Theorem tout_vide_est_Vide :
+ (A:Type)(f:A->Ens)((E':Ens)(IN E' (sup A f))->F)->(EQ (sup A f) Vide).
+Intros; Hnf; Split.
+Intro; Cut F.
+Destruct 1.
+Apply H with (f x); Unfold IN; Exists x; Apply EQ_refl.
+Destruct y.
+Qed.
+
+(******************************************************************************)
+(* PAIRE *)
+(******************************************************************************)
+
+Definition Paire : Ens -> Ens -> Ens :=
+ [E1,E2:Ens] (sup bool [b:bool]Cases b of true => E1 | false => E2 end).
+
+(* The pair construction is extentional *)
+
+Theorem Paire_sound_left : (A,A',B:Ens)
+ (EQ A A')->(EQ (Paire A B)(Paire A' B)).
+Unfold Paire .
+Simpl.
+(Intros; Split).
+Induction x.
+(Exists true; Auto with zfc).
+
+(Exists false; Auto with zfc).
+
+(Induction y; Simpl).
+(Exists true; Auto with zfc).
+
+(Exists false; Auto with zfc).
+Qed.
+
+Theorem Paire_sound_right : (A,B,B':Ens)
+ (EQ B B')->(EQ (Paire A B)(Paire A B')).
+Unfold Paire; Simpl; Intros; Split.
+Induction x.
+(Exists true; Auto with zfc).
+Exists false; Auto with zfc.
+Induction y.
+(Exists true; Auto with zfc).
+Exists false; Auto with zfc.
+Qed.
+
+Hints Resolve Paire_sound_right Paire_sound_left : zfc.
+
+Theorem IN_Paire_left : (E,E':Ens)(IN E (Paire E E')).
+Unfold Paire; Exists true; Apply EQ_refl.
+Qed.
+
+Theorem IN_Paire_right : (E,E':Ens)(IN E' (Paire E E')).
+Unfold Paire; Exists false; Apply EQ_refl.
+Qed.
+
+Theorem Paire_IN : (E,E',A:Ens)(IN A (Paire E E'))->(EQ A E)\/(EQ A E').
+Unfold Paire; Simpl.
+Induction 1; Intros b; Elim b; Auto with zfc.
+Save.
+
+Hints Resolve IN_Paire_left IN_Paire_right Vide_est_vide : zfc.
+
+(******************************************************************************)
+(* SINGLETON *)
+(******************************************************************************)
+
+(* CSC: This is different from Benjamin only because I like it more; *)
+(* theorems are also simpler *)
+(* In Benjamin's encoding (Sing E) was defined as (Paire E E) *)
+Definition Sing : Ens -> Ens :=
+ [E:Ens] (sup Un [x:Un]Cases x of void => E end).
+
+Theorem IN_Sing : (E:Ens)(IN E (Sing E)).
+Simpl; Exists void; Apply EQ_refl.
+Qed.
+
+Theorem IN_Sing_EQ : (E,E':Ens)(IN E (Sing E'))->(EQ E E').
+Simpl; Intros; Elim H; Destruct x; Trivial.
+Qed.
+
+Hints Resolve IN_Sing IN_Sing_EQ : zfc.
+
+Theorem Sing_sound : (A,A':Ens)(EQ A A')->(EQ (Sing A)(Sing A')).
+Intros; Hnf; Split; [Destruct x | Destruct y]; Exists void; Assumption.
+Qed.
+
+Hints Resolve Sing_sound : zfc.
+
+Theorem EQ_Sing_EQ : (E1,E2:Ens)(EQ (Sing E1)(Sing E2))->(EQ E1 E2).
+Intros; Hnf in H; Elim H; Intros; Elim (H0 void); Destruct x; Trivial.
+Qed.
+
+Hints Resolve EQ_Sing_EQ : zfc.
+
+(******************************************************************************)
+(* COMPREHENSION (OR SEPARATION) *)
+(******************************************************************************)
+
+Definition Comp: Ens -> (Ens -> Prop) -> Ens.
+Induction 1.
+Intros A f fr P.
+Apply (sup {x:A|(P (f x))}).
+Induction 1; Intros x p; Exact (f x).
+Intros. Exact X.
+Qed.
+
+Transparent Comp.
+
+Theorem Comp_INC : (E:Ens)(P:Ens->Prop)(INC (Comp E P) E).
+Destruct E.
+Intros A f P; Simpl; Destruct E0; [Intros A' f' H | Intros A' a' H];
+ Elim H; Destruct x; Intros x0 p eq; Exists x0; Exact eq.
+Auto with zfc.
+Qed.
+
+Theorem IN_Comp_P :
+ (E,A:Ens)
+ (P:Ens->Prop)((w1,w2:Ens)(P w1)->(EQ w1 w2)->(P w2))->
+ (IN A (Comp E P))->(P A).
+Induction E.
+Simpl; Intros B f Hr A P H i; Elim i; Destruct x; Simpl; Intro b; Intros;
+ Apply H with (f b); Auto with zfc.
+Contradiction.
+Qed.
+
+Theorem IN_P_Comp :
+ (E,A:Ens)
+ (P:Ens ->Prop)((w1,w2:Ens)(P w1)->(EQ w1 w2)->(P w2))->
+ (IN A E)->(P A)->(IN A (Comp E P)).
+Induction E.
+Simpl; Intros B f HR A P H i; Elim i; Simpl; Intros; Cut (P (f x)).
+Intros Pf.
+Exists (exist B [x:B](P (f x)) x Pf); Simpl; Auto with zfc.
+Apply H with A; Auto with zfc.
+Contradiction.
+Qed.
+
+(* Again, extentionality is not stated, but easy *)
+
+(******************************************************************************)
+(* UNION *)
+(******************************************************************************)
+
+(* Projections of a set: *)
+(* 1: its base type, F for atoms *)
+
+Definition pi1: Ens -> Type.
+Induction 1.
+Intros A f r.
+Exact A.
+Intros.
+Exact F.
+Save.
+
+Transparent pi1.
+
+(* 2: the function, [_:F]Vide for atoms *)
+
+Definition pi2 : (E:Ens)(pi1 E)->Ens.
+Induction E.
+Intros A f r.
+Exact f.
+Intros.
+Exact Vide.
+Save.
+
+Transparent pi2.
+
+Definition Union : (E:Ens)Ens.
+Induction 1.
+Intros A f r.
+Apply (sup (depprod A [x:A](pi1 (f x)))).
+Induction 1; Intros a b.
+Exact (pi2 (f a) b).
+Intros.
+Exact Vide.
+Save.
+
+Transparent Union.
+
+Theorem EQ_EXType : (E,E':Ens)
+ (EQ E E')
+ ->(a:(pi1 E))
+ (EXType (pi1 E') [b:(pi1 E')](EQ (pi2 E a) (pi2 E' b))).
+Induction E; [Intros A f r | Intros A a]; Induction E';
+ [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a'].
+Simpl; Destruct 1; Intros e1 e2 a; Apply e1.
+Contradiction.
+Contradiction.
+Simpl; Destruct 2.
+Qed.
+
+Transparent EQ_EXType.
+
+Theorem IN_EXType: (E,E':Ens)(IN E' E)->
+ (EXType (pi1 E) [a:(pi1 E)](EQ E' (pi2 E a))).
+Induction E.
+Simpl; Intros A f r; Induction 1; Intros; Exists x; Assumption.
+Destruct 1.
+Qed.
+
+Theorem IN_Union : (E,E',E'':Ens)
+ (IN E' E)->(IN E'' E')->(IN E'' (Union E)).
+Induction E.
+2: Destruct 1.
+Intros A f r.
+Intros; Simpl.
+Elim (IN_EXType (sup A f) E' H).
+Intros x e.
+Cut (EQ (pi2 (sup A f) x) E').
+2: Auto with zfc v62.
+Intros e1.
+Cut (IN E'' (pi2 (sup A f) x)).
+Intros i1.
+Elim (IN_EXType ? ? i1).
+Intros x0 e2.
+Simpl in x0.
+Exists (dep_i A [x:A](pi1 (f x)) x x0).
+Simpl.
+Exact e2.
+Apply IN_sound_right with E'; Assumption.
+Qed.
+
+(* CSC: This is different from Benjamin *)
+Theorem IN_INC_Union :
+ (A:Type)(f:A->Ens)(E:Ens)(IN (sup A f) E)->(INC (sup A f) (Union E)).
+Induction E.
+Intros A f r H; Hnf; Hnf in H; Intros; Elim H; Intros x e.
+Cut (IN E0 (f0 x)).
+Intro in_E0_f0x; Apply IN_Union with (f0 x).
+Hnf; Split with x; Auto with zfc.
+
+Auto with zfc.
+Apply IN_sound_right with (sup A f); Trivial.
+
+(Simpl; Destruct 2; Destruct x).
+Qed.
+
+Theorem Union_IN : (E,E':Ens)(IN E' (Union E))->
+ (EXType ? [E1:Ens](IN E1 E)/\(IN E' E1)).
+Induction E.
+2: (Simpl; Destruct 2; Destruct x).
+Unfold Union ; Simpl; Intros A f r.
+Induction 1.
+Induction x.
+(Intros a b; Simpl).
+Intros.
+Exists (f a).
+Split.
+(Exists a; Auto with zfc v62).
+
+(Apply IN_sound_left with (pi2 (f a) b); Auto with zfc v62).
+Simpl.
+(Generalize b ; Elim (f a); Simpl).
+Intros.
+(Exists b0; Auto with zfc v62).
+
+Destruct 2.
+Qed.
+
+(* extentionality of union *)
+
+Theorem Union_sound
+ : (E,E':Ens)(EQ E E')->(EQ (Union E) (Union E')).
+Unfold Union.
+Induction E ; [Intros A f r | Intros A a] ; Induction E' ;
+ [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a'].
+
+Simpl; Induction 1; Intros e1 e2; Split.
+Intros x; Elim x; Intros a aa; Elim (e1 a); Intros a' ea.
+Elim (EQ_EXType (f a)(f' a') ea aa); Intros aa' eaa.
+Exists (dep_i A' [x:A'](pi1 (f' x)) a' aa'); Simpl; Auto with zfc v62.
+Intros c'; Elim c'; Intros a' aa'; Elim (e2 a'); Intros a ea.
+Cut (EQ (f' a')(f a)).
+2 : Auto with zfc v62.
+Intros ea'; Elim (EQ_EXType (f' a')(f a) ea' aa'); Intros aa eaa.
+Exists (dep_i A [x:A](pi1 (f x)) a aa); Auto with zfc v62.
+
+Contradiction.
+Contradiction.
+Destruct 1; Apply EQ_refl.
+Qed.
+
+(* The union construction is monotone w.r.t. inclusion *)
+
+Theorem Union_mon : (E,E':Ens)(INC E E')->(INC (Union E)(Union E')).
+Induction E ; [Intros A f r | Intros A a] ; Induction E';
+ [Intros A' f' r' | Contradiction | Contradiction | Intros A' a'].
+2: Auto with zfc.
+Intro; Cut (E:Ens)(IN E (sup A f))->(IN E (sup A' f')).
+2: Auto.
+Intro XXX; Cut ((E:Ens)(IN E (Union (sup A f)))->(IN E (Union (sup A' f'))))
+ ->(INC (Union (sup A f)) (Union (sup A' f'))).
+2: Auto.
+Intros X; Apply X; Intros E0 Y; (Elim (Union_IN (sup A f) E0); Auto with zfc).
+Destruct 1; Intros; Cut (IN x (sup A' f')).
+2: Auto.
+Intro; (Apply IN_Union with x; Auto).
+Qed.
+
+(******************************************************************************)
+(* INTERSECTION *)
+(******************************************************************************)
+
+Definition Inter : (E:Ens)Ens :=
+[E:Ens]
+ Cases E of
+ (sup A f) =>
+ (sup ?
+ [c:(depprod A
+ [a:A](depprod ? [b:(pi1 (f a))](x:A)(IN (pi2 (f a) b)(f x)))
+ )
+ ]
+ Cases c of
+ (dep_i a (dep_i b p)) => (pi2 (f a) b)
+ end
+ )
+ | (atom A a) => Vide
+ end.
+
+Theorem IN_Inter_all : (E,E':Ens)
+ (IN E' (Inter E))->
+ (E'':Ens)(IN E'' E)->(IN E' E'').
+Induction E; [Intros A f r | Contradiction]; Intros E'.
+Induction 1; Intros c; Elim c; Intros a ca; Elim ca; Intros aa paa.
+Intros e E'' e''.
+Elim e''; Intros a1 ea1.
+Apply IN_sound_right with (f a1); Auto with zfc v62.
+Apply IN_sound_left with (pi2 (f a) aa); Auto with zfc v62.
+Qed.
+
+Theorem all_IN_Inter : (E,E',E'':Ens)
+ (IN E'' E)->
+ ((E'':Ens)(IN E'' E)->(IN E' E''))->
+ (IN E' (Inter E)).
+(Induction E; [Intros A f r | Contradiction]).
+Intros E' E'' i H.
+Elim (IN_EXType (sup A f) E'' i).
+(Intros a e; Simpl in a).
+Simpl in e.
+(Cut (IN E' E''); Auto with zfc v62).
+Intros i'.
+(Cut (IN E' (f a)); Auto with zfc v62).
+Intros i0.
+Elim (IN_EXType (f a) E' i0).
+Intros b e'.
+Simpl.
+Cut (x:A)(IN (pi2 (f a) b) (f x)).
+Intros.
+Exists (dep_i A
+ [a:A]
+ (depprod (pi1 (f a))
+ [b:(pi1 (f a))](x:A)(IN (pi2 (f a) b) (f x)))
+ a
+ (dep_i (pi1 (f a))
+ [b:(pi1 (f a))](x:A)(IN (pi2 (f a) b) (f x)) b H0)).
+Simpl.
+Auto with zfc v62.
+Auto with zfc v62.
+Intros.
+Apply IN_sound_left with E'.
+Auto with zfc v62.
+Apply H.
+Auto with zfc v62.
+Simpl.
+(Exists x; Auto with zfc v62).
+(Apply IN_sound_right with E''; Auto with zfc v62).
+Qed.
+
+(******************************************************************************)
+(* POWERSET *)
+(******************************************************************************)
+
+Definition Power : Ens -> Ens :=
+[E:Ens]
+ Cases E of
+ (sup A f) =>
+ (sup ?
+ [P:A->Prop]
+ (sup ?
+ [c:(depprod A [a:A](P a))]
+ Cases c of
+ (dep_i a p) => (f a)
+ end
+ )
+ )
+ | (atom A a) => (Sing (atom A a)) (* ??? or Vide? *)
+ end.
+
+Theorem IN_Power_INC : (E,E':Ens)(IN E' (Power E))->(INC E' E).
+Induction E.
+Intros A f r; Unfold INC ; Simpl.
+Intros E'; Induction 1; Intros P.
+Elim E'.
+Simpl.
+Intros A' f' r'.
+Induction 1; Intros HA HB.
+Intros E''; Induction 1; Intros a' e.
+Elim (HA a').
+Induction x; Intros a p.
+Intros; Exists a.
+Apply EQ_tran with (f' a'); Auto with zfc v62.
+Contradiction.
+Auto with zfc.
+Qed.
+
+(* CSC: This is different from Benjamin *)
+Theorem INC_IN_Power : (E,E':Ens)(INC E' E)->(IN E' (Power E)).
+Induction E.
+2: Induction E'.
+2: Contradiction.
+2: (Destruct 1; Unfold Power; Auto with zfc).
+Intros A f r; Unfold INC; Simpl; Induction E'.
+2: Contradiction.
+Intros A' f' r' i.
+Exists [a:A](IN (f a) (sup A' f')).
+Simpl.
+Split.
+Intros.
+Elim (i (f' x)).
+Intros a e.
+(Cut (EQ (f a) (f' x)); Auto with zfc v62).
+Intros e1.
+Exists (dep_i A [a:A](EXType A' [y:A'](EQ (f a) (f' y))) a
+ (EXTypei A' [y:A'](EQ (f a) (f' y)) x e1)).
+Auto with zfc v62.
+Simpl.
+(Exists x; Auto with zfc v62).
+Induction y; Induction 1; Intros.
+(Exists x0; Auto with zfc v62).
+Qed.
+
+Theorem Power_mon : (E,E':Ens)(INC E E')->(INC (Power E)(Power E')).
+Induction E; [Intros A f r | Intros A a]; Induction E';
+ [Intros A' f' r' | Contradiction | Contradiction | Destruct 1; Auto with zfc].
+Intro.
+Hnf in H.
+Cut ((E:Ens)(IN E (Power (sup A f)))->(IN E (Power (sup A' f'))))
+ ->(INC (Power (sup A f)) (Power (sup A' f'))).
+2: Auto.
+Intros.
+Apply H0.
+Intros.
+Cut (INC E0 (sup A f)).
+2: (Apply IN_Power_INC; Auto).
+Intro.
+Cut (INC E0 (sup A' f')).
+Intro.
+Apply INC_IN_Power.
+Assumption.
+
+Generalize H2.
+Elim E0.
+Unfold INC.
+Auto with zfc.
+
+Auto with zfc.
+Qed.
+
+Theorem Power_sound : (E,E':Ens)(EQ E E')->(EQ (Power E)(Power E')).
+Induction E; [Intros A f r | Intros A a]; Induction E';
+ [Intros A' f' r' | Contradiction | Contradiction | Destruct 1; Auto with zfc].
+Intro.
+Apply INC_EQ.
+Cut ((E:Ens)(IN E (Power (sup A f)))->(IN E (Power (sup A' f'))))
+ ->(INC (Power (sup A f)) (Power (sup A' f'))).
+2: Auto.
+Intros; Apply H0; Clear H0; Intros; Cut (INC E0 (sup A f)).
+2: (Apply IN_Power_INC; Auto with zfc).
+Clear H0; Intro; Apply INC_IN_Power.
+(Apply INC_sound_right with (sup A f); Auto).
+
+(* Using simmetry *)
+Cut ((E:Ens)(IN E (Power (sup A' f')))->(IN E (Power (sup A f))))
+ ->(INC (Power (sup A' f')) (Power (sup A f))).
+2: Auto.
+Intros; Apply H0; Clear H0; Intros; Cut (INC E0 (sup A' f')).
+2: (Apply IN_Power_INC; Auto with zfc).
+Clear H0; Intro; Apply INC_IN_Power.
+(Apply INC_sound_right with (sup A' f'); Auto with zfc).
+Qed.
+
+(******************************************************************************)
+(* ORDERED COUPLES *)
+(******************************************************************************)
+
+(* small lemmas *)
+
+Theorem not_EQ_Sing_Vide : (E:Ens)(EQ (Sing E) Vide)->F.
+Intros E e; Cut False.
+Induction 1.
+Cut (IN E Vide).
+Simpl; Induction 1; Intros xx; Elim xx; Induction 1.
+Apply IN_sound_right with (Sing E); Auto with zfc v62.
+Qed.
+
+Theorem not_EQ_Vide_Sing : (E:Ens)(EQ Vide (Sing E))->F.
+Intros E e; Cut False.
+Induction 1.
+Cut (IN E Vide).
+Simpl; Induction 1; Intros xx; Elim xx; Induction 1.
+Apply IN_sound_right with (Sing E); Auto with zfc v62.
+Qed.
+
+(* This definition of the ordered pair is slightly different from *)
+(* the usual one, since we want it to work in an intuisionistic *)
+(* setting. Works the same, neitherless. The soundness proofs are *)
+(* unpleasant. *)
+
+Definition Couple := [E,E': Ens](Paire (Sing E) (Paire Vide (Sing E'))).
+
+Theorem Couple_inj_left : (A,A',B,B':Ens)
+ (EQ (Couple A A')(Couple B B'))->(EQ A B).
+(Unfold Couple; Simpl); Induction 1; (Intros HA HB; Elim (HA true)).
+(Intros x; Elim x; Simpl; Induction 1; Intros H3 H4; Elim (H3 void);
+ Simpl; Destruct x0).
+Trivial.
+
+Elim (H4 false); Destruct x1; Intros; Cut (EQ (Sing B') Vide).
+Simpl; Induction 1; Intros yy; Elim (yy void); Destruct x2.
+
+Apply EQ_tran with A.
+Auto with zfc.
+
+Assumption.
+
+Intros; Cut (EQ (Sing B') Vide).
+Simpl; Induction 1; Intros yy; Elim (yy void); Destruct x1.
+
+Apply EQ_tran with A.
+Auto with zfc.
+
+Elim (H4 true); Destruct x1; Trivial.
+Qed.
+
+Theorem Couple_inj_right : (A,A',B,B':Ens)
+ (EQ (Couple A A')(Couple B B'))->(EQ A' B').
+Unfold Couple; Simpl.
+Induction 1; Intros H1 H2.
+Elim (H1 false).
+Intros bb1; Elim bb1.
+Intros HF.
+Change (EQ (Paire Vide (Sing A'))(Sing B)) in HF.
+Cut F.
+Induction 1.
+Apply (not_EQ_Vide_Sing A').
+Apply EQ_tran with B.
+Apply IN_Sing_EQ; Apply IN_sound_right with (Paire Vide (Sing A'));
+ Auto with zfc v62.
+Apply EQ_sym; Apply IN_Sing_EQ;
+ Apply IN_sound_right with (Paire Vide (Sing A')); Auto with zfc v62.
+Change (EQ (Paire Vide (Sing A'))(Paire Vide (Sing B')))->(EQ A' B').
+Intros HP; Cut (EQ (Sing A') (Sing B')).
+Intros; Auto with zfc v62.
+Cut (IN (Sing A')(Paire Vide (Sing B'))).
+Intros HI; Elim (Paire_IN Vide (Sing B')(Sing A') HI).
+Intros; Cut F.
+Induction 1.
+Apply not_EQ_Sing_Vide with A'; Assumption.
+Trivial with zfc v62.
+Apply IN_sound_right with (Paire Vide (Sing A')); Auto with zfc v62.
+Qed.
+
+(******************************************************************************)
+(* POWERSET *)
+(******************************************************************************)
+
+(* Here we cheat. It is easier to define the cartesian product using *)
+(* the type theoretical product, i.e. we here use non set-theoretical *)
+(* constructions. We could however use the usual definitions. *)
+
+Definition Prod : Ens -> Ens -> Ens :=
+[E,E':Ens]
+ Cases E E' of
+ (sup A f) (sup A' f') =>
+ (sup ?
+ [c:(prod_t A A')]
+ Cases c of
+ (pair_t a a') => (Couple (f a) (f' a'))
+ end
+ )
+ | _ _ => Vide
+ end.
+
+Hints Resolve Paire_sound_left Paire_sound_right : zfc.
+
+Theorem Couple_sound_left :
+ (A,A',B:Ens)(EQ A A')->(EQ (Couple A B)(Couple A' B)).
+ Unfold Couple;Intros; Auto with zfc v62.
+Save.
+
+Theorem Couple_sound_right:
+ (A,B,B':Ens)(EQ B B')->(EQ (Couple A B)(Couple A B')).
+ Unfold Couple;Intros; Auto with zfc v62.
+Save.
+
+Theorem Couple_IN_Prod : (E1,E2,E1',E2':Ens)
+ (IN E1' E1)->(IN E2' E2)->
+ (IN (Couple E1' E2')(Prod E1 E2)).
+Induction E1; [Intros A1 f1 r1 | Contradiction].
+Induction E2; [Intros A2 f2 r2 | Contradiction].
+Intros E1' E2' i1 i2.
+Elim (IN_EXType (sup A1 f1) E1').
+(Intros x e1; Simpl in x).
+Elim (IN_EXType (sup A2 f2) E2').
+(Intros x0 e2; Simpl in x).
+Apply IN_sound_left with (Couple (pi2 (sup A1 f1) x) (pi2 (sup A2 f2) x0)).
+Apply EQ_tran with (Couple (pi2 (sup A1 f1) x) E2').
+Apply Couple_sound_right.
+Auto with zfc v62.
+
+(Apply Couple_sound_left; Auto with zfc v62).
+
+Simpl.
+Exists (pair_t ? ? x x0).
+Simpl.
+Split.
+
+Induction x1.
+Exists true; Auto with zfc.
+Exists false; Auto with zfc.
+
+Induction y.
+Exists true; Auto with zfc.
+Exists false; Auto with zfc.
+Assumption.
+Assumption.
+Qed.
+
+Theorem Couple_Prod_IN : (E1,E2,E1',E2':Ens)
+ (IN (Couple E1' E2')(Prod E1 E2))->
+ (IN E1' E1)/\(IN E2' E2).
+Induction E1; [Intros A1 f1 r1 | Destruct 1; Destruct x].
+Induction E2; [Intros A2 f2 r2 | Destruct 1; Destruct x].
+Intros E1' E2' i.
+Elim (IN_EXType (Prod (sup A1 f1) (sup A2 f2)) (Couple E1' E2') i).
+Destruct x; Intros a1 a2 e.
+Change (EQ (Couple E1' E2') (Couple (f1 a1) (f2 a2))) in e.
+Cut (EQ E1' (f1 a1)).
+Cut (EQ E2' (f2 a2)).
+Intros e1 e2.
+Split.
+Apply IN_sound_left with (f1 a1); Auto with zfc v62; Simpl; Exists a1;
+ Auto with zfc v62.
+Apply IN_sound_left with (f2 a2); Auto with zfc v62; Simpl; Exists a2;
+ Auto with zfc v62.
+Apply Couple_inj_right with A:=E1' B:=(f1 a1); Auto with zfc v62.
+Apply Couple_inj_left with E2' (f2 a2); Auto with zfc v62.
+Qed.
+
+Theorem IN_Prod_EXType : (E,E',E'':Ens)(IN E'' (Prod E E'))->
+ (EXType ? [A:Ens](EXType ? [B:Ens](EQ (Couple A B) E''))).
+Induction E ; [Intros A f r | Destruct 1; Destruct x].
+Induction E'; [Intros A' f' r' | Destruct 1; Destruct x].
+Intros; Elim (IN_EXType (Prod (sup A f) (sup A' f')) E'').
+Induction x.
+Intros; Exists (f y); Exists (f' y0); Auto with zfc v62.
+Auto with zfc v62.
+Qed.
+
+(******************************************************************************)
+(* ORDINALS *)
+(******************************************************************************)
+
+Definition Succ := [E:Ens](Union (Paire E (Sing E))).
+
+Inductive Ord : Ens -> Prop :=
+ Oo : (Ord Vide)
+| So : (E:Ens)(Ord E)->(Ord (Succ E))
+| Lo : (E:Ens)((e:Ens)(IN e E)->(Ord e))->(Ord (Union E))
+| Eo : (E,E':Ens)(Ord E)->(EQ E E')->(Ord E').
+
+Hints Resolve Oo So Lo : zfc.
+
+Definition Nat : nat ->Ens.
+Induction 1; Intros.
+Exact Vide.
+Exact (Succ X).
+Save.
+
+Transparent Nat.
+
+Theorem Nat_Ord : (n:nat)(Ord (Nat n)).
+Induction n; Simpl; Auto with zfc v62.
+Save.
+
+Definition Omega : Ens :=
+ (sup nat Nat).
+
+Theorem IN_Succ : (E:Ens)(IN E (Succ E)).
+Intros E; Unfold Succ; Apply IN_Union with (Sing E); Auto with zfc v62.
+Qed.
+
+(* CSC: This is different from Werner *)
+Theorem INC_Succ : (A:Type)(f:A->Ens)(INC (sup A f) (Succ (sup A f))).
+Intros; Cut ((E:Ens)(IN E (sup A f))->(IN E (Succ (sup A f))))
+ ->(INC (sup A f) (Succ (sup A f))).
+Intros; Apply H; Unfold Succ; Intros.
+Apply IN_Union with (sup A f); Auto with zfc.
+
+Intros; Exact H.
+Qed.
+
+Hints Resolve IN_Succ INC_Succ : zfc.
+
+Theorem IN_Succ_or : (E,E':Ens)(IN E' (Succ E))->(EQ E E')\/(IN E' E).
+Intros E E' i.
+Unfold Succ in i.
+Elim (Union_IN (Paire E (Sing E)) E' i).
+Intros E1; Induction 1; Intros i1 i2.
+Elim (Paire_IN E (Sing E) E1 i1).
+Intros; Right; Apply IN_sound_right with E1; Auto with zfc v62.
+Intros; Left; Cut (IN E' (Sing E)).
+Auto with zfc v62.
+Apply IN_sound_right with E1; Auto with zfc v62.
+Qed.
+
+Theorem E_not_IN_E : (E:Ens)(IN E E)->F.
+Induction E.
+Intros A f r i.
+Cut False.
+Induction 1.
+Elim (IN_EXType (sup A f) (sup A f) i); Intros a e.
+
+Simpl in a.
+Change (EQ (sup A f) (f a)) in e.
+Elim (r a).
+Apply IN_sound_right with (sup A f); Auto with zfc v62.
+Exists a; Auto with zfc v62.
+Intros; Cut False; Contradiction.
+Qed.
+
+Theorem Nat_IN_Omega : (n:nat)(IN (Nat n) Omega).
+Intros; Simpl; Exists n; Auto with zfc v62.
+Qed.
+Hints Resolve Nat_IN_Omega : zfc.
+
+Theorem IN_Omega_EXType : (E:Ens)(IN E Omega)->(EXType ? [n:nat](EQ (Nat n) E)).
+(Simpl; Induction 1).
+Intros n e.
+(Exists n; Auto with zfc v62).
+Qed.
+
+Theorem IN_Nat_EXType : (n:nat)(E:Ens)(IN E (Nat n))->(EXType ? [p:nat](EQ E (Nat p))).
+Induction n.
+Simpl.
+Induction 1.
+Induction x.
+
+Intros.
+Change (IN E (Succ (Nat n0))) in H0.
+Elim (IN_Succ_or (Nat n0) E H0).
+(Intros; Exists n0).
+Auto with zfc v62.
+
+Intros.
+(Elim (H E); Auto with zfc v62).
+Qed.
+
+Theorem Omega_EQ_Union : (EQ Omega (Union Omega)).
+Apply INC_EQ.
+Cut ((E:Ens)(IN E Omega)->(IN E (Union Omega)))
+ ->(INC Omega (Union Omega)).
+Intros; Apply H.
+Clear H.
+Intros.
+Elim (IN_Omega_EXType E H).
+Intros n e.
+Apply IN_Union with (Nat (S n)).
+Auto with zfc v62.
+
+Apply IN_sound_left with (Nat n).
+Auto with zfc v62.
+
+(Change (IN (Nat n) (Succ (Nat n))); Auto with zfc v62).
+
+Intros.
+Exact H.
+
+Cut ((E:Ens)(IN E (Union Omega))->(IN E Omega))
+ ->(INC (Union Omega) Omega).
+Intros; Apply H; Clear H.
+Intros.
+Elim (Union_IN Omega E H).
+Intros e h.
+Elim h.
+Intros i1 i2.
+Elim (IN_Omega_EXType e i1).
+Intros n e1.
+Cut (IN E (Nat n)).
+Intros.
+(Elim (IN_Nat_EXType n E H0); Intros).
+(Apply IN_sound_left with (Nat x); Auto with zfc v62).
+
+(Apply IN_sound_right with e; Auto with zfc v62).
+
+Intros.
+Exact H.
+Qed.
+
+Theorem Omega_Ord : (Ord Omega).
+Apply Eo with (Union Omega).
+Apply Lo.
+Intros.
+Elim (IN_Omega_EXType e H).
+Intros n ee.
+Apply Eo with (Nat n); Auto with zfc v62.
+Elim n.
+Auto with zfc v62.
+Auto with zfc v62.
+Intros.
+Change (Ord (Succ (Nat n0))); Auto with zfc v62.
+Apply EQ_sym; Auto with zfc v62.
+Apply Omega_EQ_Union.
+Qed.
+
+Definition Alpha : Ens->Ens.
+Induction 1.
+Intros A f r.
+Apply Union.
+Apply (sup A).
+Intros a.
+Exact (Power (r a)).
+Intros A a; Exact (atom A a). (* ??? or Vide? *)
+Save.
+
+Transparent Alpha.
+
+(******************************************************************************)
+(* AXIOM OF CHOICE *)
+(******************************************************************************)
+
+(* A Type-theoretical axiom of choice gives us the collection axiom *)
+
+Definition collection :=
+ (P:Ens->Ens->Prop)
+ ((x,x',y:Ens)(EQ x x')->(P x y)->(P x' y))->
+ ((E:Ens)(EXType ? (P E)))->
+ (E:Ens)(EXType ? [A:Ens](x:Ens)(IN x E)->
+ (EXType ? [y:Ens](IN y A)/\(P x y))).
+
+
+Definition choice :=
+ (A,B:Type)(P:A->B->Prop)
+ ((a:A)(EXType ? [b:B](P a b)))->
+ (EXType ? [f:A->B]((a:A)(P a (f a)))).
+
+Theorem Choice_Collection : choice -> collection.
+Intro; Unfold collection; Intros P comp G E;
+ Cut (EXType ? [f:(Ens->Ens)](B:Ens)(P B (f B))).
+Induction 1; Intros f Pf; Elim E.
+Intros A g hr; Split with (sup A [a:A](f (g a))).
+Simpl; Intros X i; Elim i; Intros a ea; Split with (f (g a)).
+Split.
+Exists a; Auto with zfc.
+
+Apply comp with (g a); Auto with zfc.
+
+Auto with zfc.
+
+Intros; Split with Vide; Contradiction.
+
+Unfold choice in H; Apply H; Intros; Elim (G a); Intros b hb; Exists b;
+ Assumption.
+Qed.
+
+(* If we also assume the excluded middle, we can derive *)
+(* the usual replacement schemata. *)
+
+Definition functional :=
+ [P:Ens->Ens->Prop](x,y,y':Ens)
+ (P x y)->(P x y')->(EQ y y').
+Definition replacement :=
+ (P:Ens->Ens->Prop)
+ (functional P)->
+ ((x,y,y':Ens)(EQ y y')->(P x y)->(P x y'))->
+ ((x,x',y:Ens)(EQ x x')->(P x y)->(P x' y))->
+ (X:Ens)(EXType ? [Y:Ens](y:Ens)
+ (((IN y Y)->(EXType ? [x:Ens](IN x X)/\(P x y)))
+ /\((EXType ? [x:Ens](IN x X)/\(P x y))->(IN y Y)))).
+
+Theorem classical_Collection_Replacement :
+ ((S:Prop)S\/(S->False))->
+ collection ->
+ replacement.
+Unfold replacement; Intros EM Collection P fp comp_r comp_l X.
+Cut (EXType ? [Y:Ens](y:Ens)((EXType ? [x:Ens](IN x X)/\(P x y))->(IN y Y))).
+Induction 1; Intros Y HY.
+Exists (Comp Y [y:Ens](EXType ? [x:Ens](IN x X)/\(P x y))).
+Intros y; Split.
+Intros HC.
+Apply (IN_Comp_P Y y [y0:Ens](EXType Ens [x:Ens](IN x X)/\(P x y0))); Auto with zfc v62.
+Intros w1 w2; Induction 1; Intros x; Induction 1; Intros Ix Px e.
+Exists x; Split; Auto with zfc v62.
+Apply comp_r with w1; Auto with zfc v62.
+Intros He.
+Apply IN_P_Comp.
+
+Intros w1 w2; Induction 1; Intros x; Induction 1; Intros Ix Px e.
+Exists x; Split; Auto with zfc v62.
+Apply comp_r with w1; Auto with zfc v62.
+Apply HY; Auto with zfc v62.
+Auto with zfc v62.
+
+Elim (Collection [x,y:Ens]((P x y)\/(((y':Ens)(P x y')->False)/\(EQ y Vide))))
+ with X.
+Intros Y HY.
+Elim (EM (EXType ? [x:Ens](IN x X)/\(P x Vide))).
+Intros Hvide; Elim Hvide; Intros xv Hxv; Exists Y.
+Intros y; Induction 1; Intros x; Induction 1; Intros Hx1 Hx2.
+Elim (HY x Hx1).
+Intros y'; Induction 1; Intros Hy'1 Hy'2.
+Elim Hy'2.
+Intros Hy'3; Apply IN_sound_left with y'; Auto with zfc v62.
+Apply fp with x; Auto with zfc v62.
+Induction 1; Intros Hy'3 Hy'4.
+Elim (Hy'3 y Hx2).
+Intros HP; Exists (Comp Y [y:Ens]((EQ y Vide)->False)).
+Intros y; Induction 1; Intros x; Induction 1; Intros Hx1 Hx2.
+Apply IN_P_Comp.
+Intros w1 w2 Hw1 Hw Hw2; Apply Hw1; Apply EQ_tran with w2; Auto with zfc v62.
+Elim (HY x).
+Intros y'; Induction 1; Intros Hy'1 Hy'2.
+Elim Hy'2; Intros Hy'3.
+Apply IN_sound_left with y'; Auto with zfc v62.
+Apply fp with x; Auto with zfc v62.
+Elim Hy'3; Intros Hy'4 Hy'5.
+Elim (Hy'4 y); Auto with zfc v62.
+Assumption.
+Intros e; Apply HP; Exists x; Split; Auto with zfc v62;
+ Apply comp_r with y; Auto with zfc v62; Apply fp; Auto with zfc v62.
+Intros x x' y e Hx; Elim Hx; Intros Hx1.
+Left; Apply comp_l with x; Auto with zfc v62.
+Right; Elim Hx1; Intros Hx2 Hx3; Split.
+2 : Assumption.
+Intros y' Hy'; Apply (Hx2 y'); Apply comp_l with x'; Auto with zfc v62.
+Intros x; Elim (EM (EXType ? [y:Ens](P x y))); Intros Hx.
+Elim Hx; Intros x0 Hx0; Exists x0; Left; Assumption.
+Exists Vide; Right; Split; Auto with zfc v62.
+Intros y Hy; Elim Hx; Exists y; Auto with zfc v62.
+Qed.
+
+(******************************************************************************)
+(* SMALL SETS AND THE BIG SET OF SMALL SETS *)
+(******************************************************************************)
+
+(* Some definitions replicated on another type level *)
+
+Inductive EXType' [P:Type; Q:P->Prop]: Prop :=
+ EXTypei' : (x:P)(Q x)->(EXType' P Q).
+
+Inductive prod_t' [A,B:Type] : Type :=
+ pair_t' : A->B->(prod_t' A B).
+
+Inductive depprod'' [A:Type; P : A->Type] : Type :=
+ dep_i'' : (x:A)(P x)->(depprod'' A P).
+
+(* The small sets *)
+Inductive Ens' : Type :=
+ sup' : (A:Type)(A->Ens')->Ens'
+ | atom' : (A:Type)A->Ens'.
+
+(* Equality on small sets *)
+Definition EQ' : Ens' -> Ens' -> Prop.
+Induction 1.
+Intros A f eq1.
+Induction 1.
+Intros B g eq2.
+Apply and.
+Exact (x:A)
+ (EXType' ? [y:B](eq1 x (g y))).
+Exact (y:B)
+ (EXType' ? [x:A](eq1 x (g y))).
+
+Intros A' a'.
+Exact False.
+
+Intros A a.
+Induction 1.
+Intros A' f eq1.
+Exact False.
+
+Intros.
+(*Exact (X == X0).*)
+Exact (eq_depT Type [A:Type]A A a A0 y).
+Save.
+
+Transparent EQ'.
+
+(* small sets can be injected into big sets *)
+Definition inj : Ens'->Ens.
+Induction 1; [Intros A f fr ; Exact (sup A fr) | Intros A a ; Exact (atom A a)].
+Qed.
+
+Transparent inj.
+
+Theorem inj_sound : (E1,E2:Ens')(EQ' E1 E2)->(EQ (inj E1)(inj E2)).
+Induction E1; [Intros A1 f1 r1 | Intros A a] ; Induction E2;
+ [Intros A2 f2 r2 | Contradiction | Contradiction | Intros A' a'].
+(Induction 1; Intros HR1 HR2; Split).
+(Intros a1; Elim (HR1 a1); Intros a2 Ha2; Exists a2; Auto with zfc v62).
+(Intros a2; Elim (HR2 a2); Intros a1 Ha1; Exists a1; Auto with zfc v62).
+
+Auto with zfc.
+Qed.
+
+Definition Sing' : Ens' -> Ens' :=
+ [E:Ens'] (sup' Un [x:Un]Cases x of void => E end).
+
+Definition Power' : Ens' -> Ens' :=
+[E:Ens']
+ Cases E of
+ (sup' A f) =>
+ (sup' ?
+ [P:A->Prop]
+ (sup' ?
+ [c:(depprod'' A [a:A](P a))]
+ Cases c of
+ (dep_i'' a p) => (f a)
+ end
+ )
+ )
+ | (atom' A a) => (Sing' (atom' A a)) (* ??? or Vide? *)
+ end.
+
+Theorem Power_sound_inj : (E:Ens')(EQ (inj (Power' E))(Power (inj E))).
+Induction E; [Intros A f HR | Intros A a].
+Simpl; Split.
+Intros P; Exists P; Split.
+Intros c; Elim c; Intros a p.
+Exists (dep_i A [a0:A](P a0) a p); Simpl; Auto with zfc v62.
+Intros c; Elim c; Intros a p.
+Exists (dep_i'' A [a0:A](P a0) a p); Simpl; Auto with zfc v62.
+Intros P; Exists P; Split.
+Intros c; Elim c; Intros a p.
+Exists (dep_i A [a0:A](P a0) a p); Simpl; Auto with zfc v62.
+Intros c; Elim c; Intros a p.
+Exists (dep_i'' A [a0:A](P a0) a p); Simpl; Auto with zfc v62.
+
+Simpl; Split.
+Destruct x; Exists void; Auto with zfc.
+Destruct y; Exists void; Auto with zfc.
+Qed.
+
+(* The set of small sets *)
+Definition Big := (sup Ens' inj).
+
+Theorem Big_is_big : (E:Ens')(IN (inj E) Big).
+Intros E; Unfold Big; Simpl; Exists E; Auto with zfc.
+Qed.
+
+Theorem IN_Big_small : (E:Ens)(IN E Big)->(EXType' ? [E':Ens'](EQ E (inj E'))).
+Unfold Big; Simpl; Induction 1; Intros E' HE'; Exists E'; Assumption.
+Qed.
+
+Theorem IN_small_small : (E:Ens)(E':Ens')(IN E (inj E'))->
+ (EXType' ? [E1:Ens'](EQ E (inj E1))).
+Induction E'; [Intros A' f' HR' | Contradiction]; Simpl;
+ Induction 1; Intros a' e'; Exists (f' a'); Assumption.
+Qed.
+
+Theorem Big_closed_for_power : (E:Ens)(IN E Big)->(IN (Power E) Big).
+Unfold Big; Simpl; Intros E; Induction 1; Intros E' HE'; Exists (Power' E').
+Apply EQ_tran with (Power (inj E')).
+Apply Power_sound; Assumption.
+Apply EQ_sym; Apply Power_sound_inj.
+Qed.
+
+(******************************************************************************)
+(* NO SET OF ALL SETS *)
+(******************************************************************************)
+
+(* Just for fun : a proof that there is no set of all sets, using *)
+(* Russell's paradox construction *)
+(* There, of course, are other proofs (foundation, etc) *)
+
+Theorem Russell : (E:Ens)((E':Ens)(IN E' E))->False.
+Intros U HU.
+Cut ([x:Ens](IN x x)->False (Comp U [x:Ens](IN x x)->False)).
+Intros HR.
+Apply HR.
+(Apply IN_P_Comp; Auto with zfc v62).
+(Intros w1 w2 HF e i; Apply HF; Apply IN_sound_left with w2; Auto with zfc v62;
+ Apply IN_sound_right with w2; Auto with zfc v62).
+Intros H.
+Cut (IN (Comp U [x:Ens](IN x x)->False) (Comp U [x:Ens](IN x x)->False)).
+Change ([x:Ens](IN x x)->False (Comp U [x:Ens](IN x x)->False)).
+Cut (w1,w2:Ens)((IN w1 w1)->False)->(EQ w1 w2)->(IN w2 w2)->False.
+Intros ww.
+Exact (IN_Comp_P U (Comp U [x:Ens](IN x x)->False)
+ [x:Ens](IN x x)->False ww H).
+(Intros w1 w2 HF e i; Apply HF; Apply IN_sound_left with w2; Auto with zfc v62;
+ Apply IN_sound_right with w2; Auto with zfc v62).
+Assumption.
+Qed.
+
+(******************************************************************************)
+(* SOME AXIOMS AND STRANGE THINGS ;-( *)
+(* *)
+(* The need for axioms is due to the usage of dependent equality, or to my *)
+(* ignorance about it ;-) *)
+(* *)
+(******************************************************************************)
+
+Axiom a_de_pi2 :
+ (T:Type)(n,m:T)(existT Type [A:Type]A T n)==(existT Type [A:Type]A T m)->n==m.
+
+(* The main consequence of the previous axiom *)
+Theorem a_pi2 : (T:Type)(n,m:T)(atom T n)==(atom T m)->n==m.
+Intros; Inversion H; Apply a_de_pi2; Assumption.
+Qed.
+
+(* This theorem is really strange: I can prove this in general, but I can't *)
+(* prove any of it's instance: for example I can't prove *)
+(* ~(nat==bool)->~(atom nat O)==(atom bool true) due to an internal error of *)
+(* Coq *)
+Theorem a_npi1 : (T1,T2:Type)(t1:T1)(t2:T2)~T1==T2->~(atom T1 t1)==(atom T2 t2).
+Unfold not; Intros; Apply H; Inversion H0; Reflexivity.
+Qed.
+
+(******************************************************************************)
+(* MAPPING A TYPE TO THE SET OF IT'S ELEMENTS *)
+(******************************************************************************)
+
+(* (Ens_of_t T t) is thought as the coercion from an element (t:T) to a set *)
+Definition Ens_of_t : (T:Type)T->Ens :=
+ [T:Type][t:T](atom T t).
+
+(* (Ens_of_T T) is thought as the set of the elements of type T ... *)
+Definition Ens_of_T : Type -> Ens :=
+ [T:Type] (sup T [t:T](Ens_of_t T t)).
+
+(* ... and (Prop_on_Ens_of_Prop T P) is thought as the proposition on Ens *)
+(* that is true only for (atom T t) where (t:T) and (P t) is true. *)
+Inductive Prop_on_Ens_of_Prop [T:Type; P:T->Prop] : Ens->Prop :=
+ cons : (t:T)(P t)->(Prop_on_Ens_of_Prop T P (atom T t)).
+
+Theorem Prop_on_Ens_of_Prop_atom_Prop :
+ (T:Type; P:(T->Prop); t:T)(Prop_on_Ens_of_Prop T P (atom T t))->(P t).
+Intros; Inversion H; Replace t with t0.
+Assumption.
+
+Apply a_de_pi2; Assumption.
+Qed.
+
+Theorem Prop_on_Ens_of_Prop_t :
+ (T:Type; P:(T->Prop); E:Ens)
+ (Prop_on_Ens_of_Prop T P E)
+ ->(EXType T [t:T]E==(atom T t)/\(P t)).
+Intros.
+Inversion H.
+Split with t.
+Auto.
+Qed.
+
+Lemma EQ_atom: (T:Type)(t:T)(E:Ens)(EQ (atom T t) E)->(atom T t)==E.
+Destruct E.
+Contradiction.
+
+Intros.
+Inversion H.
+Reflexivity.
+Qed.
+
+
+Theorem Prop_on_Ens_of_Prop_sound :
+ (E1,E2:Ens)(T:Type)(P:T->Prop)
+ (EQ E1 E2)
+ -> (Prop_on_Ens_of_Prop T P E1)
+ -> (Prop_on_Ens_of_Prop T P E2).
+Intros.
+Cut (EXType ? [t:T]E1==(atom T t)/\(P t)).
+Destruct 1; Destruct 1.
+Intros.
+Rewrite H3 in H.
+Cut (atom T x)==E2.
+Intros.
+Rewrite <- H5.
+Constructor 1.
+Assumption.
+
+Apply EQ_atom.
+Assumption.
+
+Apply Prop_on_Ens_of_Prop_t.
+Assumption.
+Qed.
+
+
+(******************************************************************************)
+(* EXAMPLES OF USAGE *)
+(******************************************************************************)
+
+(* We could define an implicit coercion from nat to Ens using Ens_of_t *)
+Coercion Ens_of_nat := [n:nat](Ens_of_t nat n).
+
+(* CNat is the set of the natural numbers of Coq ... *)
+Definition CNat : Ens :=
+ (Ens_of_T nat).
+
+Mutual Inductive
+ is_even : nat->Prop :=
+ is_even_O : (is_even O)
+ | is_even_S : (n:nat)(is_odd n)->(is_even (S n))
+with
+ is_odd : nat->Prop :=
+ id_ood_S : (n:nat)(is_even n)->(is_odd (S n)).
+
+Lemma not_even_odd: (n:nat)(is_even n)->(is_odd n)->False.
+Induction n.
+Intros; Inversion H0.
+
+Intros; Apply H; [Inversion H1 | Inversion H0]; Assumption.
+Qed.
+
+Definition Cis_even : Ens -> Prop :=
+ (Prop_on_Ens_of_Prop nat is_even).
+
+Definition Cis_odd : Ens -> Prop :=
+ (Prop_on_Ens_of_Prop nat is_odd).
+
+(* ... and CEven and COdd are the sets of even/odd natural numbers of Coq *)
+
+Definition CEven := (Comp CNat Cis_even).
+
+Definition COdd := (Comp CNat Cis_odd).
+
+(* And now an easy fact: the intersection of CEven with COdd is empty *)
+Fact COdd_Inter_CEven_EQ_Vide: (EQ (Inter (Paire CEven COdd)) Vide).
+Apply INC_EQ.
+Cut (E:Ens)(IN E (Inter (Paire CEven COdd)))->(IN E Vide).
+Auto.
+
+Intros.
+Cut False.
+Contradiction.
+
+Cut (IN E CEven)/\(IN E COdd).
+Destruct 1.
+Intros.
+Unfold CEven in H1.
+Cut (Cis_even E).
+Unfold COdd in H2.
+Cut (Cis_odd E).
+Intros.
+Inversion H3.
+Inversion H4.
+Rewrite <- H6 in H8.
+Cut t0==t.
+Intro.
+Rewrite H9 in H7.
+Apply not_even_odd with t; Assumption.
+
+Apply a_pi2; Assumption.
+
+Apply IN_Comp_P with CNat.
+Intros.
+Unfold Cis_odd.
+Apply Prop_on_Ens_of_Prop_sound with w1; Assumption.
+
+Assumption.
+
+Apply IN_Comp_P with CNat.
+Intros.
+Unfold Cis_even.
+Apply Prop_on_Ens_of_Prop_sound with w1; Assumption.
+
+Assumption.
+
+Split.
+Apply IN_Inter_all with (Paire CEven COdd).
+Assumption.
+
+Auto with zfc.
+
+Apply IN_Inter_all with (Paire CEven COdd).
+Assumption.
+
+Auto with zfc.
+
+Simpl.
+Destruct 1.
+Destruct x.
+Qed.
+
+(* Another easy fact: O is not in COdd *)
+Fact O_not_IN_COdd : ~(IN O COdd).
+Unfold not; Intro.
+Cut (Cis_odd O).
+Intro.
+Inversion H0.
+Simpl in H1.
+Cut t==O.
+Intro.
+Rewrite H3 in H2.
+Inversion H2.
+
+Apply a_de_pi2.
+Assumption.
+
+Unfold COdd in H.
+Apply IN_Comp_P with CNat.
+Intros.
+Unfold Cis_odd.
+Apply Prop_on_Ens_of_Prop_sound with w1.
+Assumption.
+
+Exact H0.
+
+Assumption.
+Qed.
projects / helm.git / commitdiff