+++ /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 / blobdiff