helm/EXPORT/exportcsczfc/csc_zfc/csc_zfc.v

   1 (******************************************************************************)
   2 (*                      Zermelo Set Theory + atomic sets                      *)
   3 (*                                                                            *)
   4 (*                           Claudio Sacerdoti Coen                           *)
   5 (*                                                                            *)
   6 (*    Based on                                                                *)
   7 (*                                                                            *)
   8 (*                            Zermolo Set Theory                              *)
   9 (*                                                                            *)
  10 (*                              Benjamin Werner                               *)
  11 (*                                                                            *)
  12 (******************************************************************************)
  13
  14 (* This is an extension of Benjamin's encoding of usual Set Theory where I    *)
  15 (* assume the existence of exactly one atomic set for each object t of type T *)
  16 (* where T is a Type in Coq: if (t:T) and (T:Type) then ((atom T t):Ens)      *)
  17 (* The usual axioms of set theory are modified so that they work in the       *)
  18 (* usual way if applied to "normal" sets, and in a reasonable way when        *)
  19 (* applied to atomic sets (for example (Union (atom T t) E) is equal to E for *)
  20 (* each non-atomic set E)                                                     *)
  21 (* All this has been already studied by Fraenkel and Mostowski in the '40,    *)
  22 (* but with totally different goals (in order to proove some independence     *)
  23 (* results in set theory)                                                     *)
  24
  25 (* This is the introduction to the original encoding of Benjamin:             *)
  26 (*    This is an encoding of usual Set Theory, simillar to Peter Aczel's work *)
  27 (*    in the early 80's. The main difference is that the propositions here    *)
  28 (*    live in the impredicative world of "Prop". Thus, priority is given to   *)
  29 (*    expressivity against constructivity.                                    *)
  30 (*                                                                            *)
  31 (*    Since the definition of Sets is the same for both approaches, I added   *)
  32 (*    most  of Aczel's encoding of CZF at the end of the file. Many           *)
  33 (*    definitions are common to both aproaches.                               *)
  34
  35 (* In this work only the encoding of ZFC (and not that of CZF) has been       *)
  36 (* developed, but it should be straightforward to do.                         *)
  37
  38 Require csc_eqdep.
  39
  40 (******************************************************************************)
  41 (*                          Useful data types                                 *)
  42 (******************************************************************************)
  43
  44 Inductive Set F := .
  45
  46 Inductive Set Un := void : Un.
  47
  48 (* Existential quantification *)
  49 Inductive EXType [P:Type; Q:P->Prop]: Prop :=
  50  EXTypei : (x:P)(Q x)->(EXType P Q).
  51
  52 (* Sigma types -- i.e. computational existentials *)
  53 Inductive sig [A:Type;P:A->Prop] : Type :=
  54  exist : (x:A)(P x)->(sig A P).
  55
  56 (* Existential on the Type level *)
  57 Inductive depprod [A:Type; P : A->Type] : Type :=
  58  dep_i : (x:A)(P x)->(depprod A P).
  59
  60 (* Cartesian product in Type *)
  61 Inductive prod_t [A,B:Type] : Type :=
  62  pair_t : A->B->(prod_t A B).
  63
  64 (******************************************************************************)
  65 (*                         Definition of Ens, EQ, IN                          *)
  66 (******************************************************************************)
  67
  68 (* The type representing sets  (Ensemble = french for set) *)
  69 Inductive Ens : Type :=
  70    sup : (A:Type)(A->Ens)->Ens
  71  | atom : (A:Type)A->Ens.
  72
  73 (* Recursive Definition of the extentional equality on sets *)
  74 Definition EQ : Ens -> Ens -> Prop.
  75 Induction 1.
  76 Intros A f eq1.
  77 Induction 1.
  78 Intros B g eq2.
  79 Apply and.
  80 Exact (x:A)
  81         (EXType ? [y:B](eq1 x (g y))).
  82 Exact (y:B)
  83         (EXType ? [x:A](eq1 x (g y))).
  84
  85 Intros A' a'.
  86 Exact False.
  87
  88 Intros A a.
  89 Induction 1.
  90 Intros A' f eq1.
  91 Exact False.
  92
  93 Intros.
  94 (*Exact (X == X0).*)
  95 Exact (eq_depT Type [A:Type]A A a A0 y).
  96 Save.
  97
  98 Transparent EQ.
  99
 100 (* Membership on sets *)
 101 Definition IN: Ens -> Ens -> Prop :=
 102 [E1,E2:Ens]
 103   Cases E2 of
 104     (sup A f) => (EXType ? [y:A](EQ E1 (f y)))
 105   | (atom A a) => False
 106   end.
 107 Transparent IN.
 108
 109
 110 (******************************************************************************)
 111 (*                                  INCLUSION                                 *)
 112 (******************************************************************************)
 113
 114 Definition INC : Ens -> Ens -> Prop :=
 115  [E1,E2:Ens]
 116  Cases E1 E2 of
 117    (sup A f)  (sup B g)  => (E:Ens)(IN E E1)->(IN E E2)
 118  | (sup A f)  (atom B b) => False
 119  | (atom A a) (sup B g)  => False      (* ??? or True?  *)
 120  | (atom A a) (atom B b) => (EQ E1 E2) (* ??? or False? *)
 121  end.
 122
 123 (* EQ is an equivalence relation  *)
 124
 125 Theorem EQ_refl : (E:Ens)(EQ E E).
 126 Induction E.
 127 Intros; Split; Simpl; Intro.
 128 Exists x; Exact (H x).
 129 Exists y; Exact (H y).
 130 Intros; Simpl; Constructor 1.
 131 Qed.
 132
 133 Theorem EQ_tran : (E1,E2,E3:Ens)(EQ E1 E2)->(EQ E2 E3)->(EQ E1 E3).
 134 Induction E1; [Intros A1 f1 r1 | Intros A1 a1]  ;
 135 Induction E2; [Intros A2 f2 r2 | Intros A2 a2 | Intros A2 f2 r2 | Intros A2 a2];
 136 Induction E3; [Intros A3 f3 r3 | Auto | Contradiction | Auto |
 137  Auto | Contradiction | Auto | Intros A3 a3].
 138 Simpl; Intros e1 e2; Split; Elim e1; Intros I1 I2; Elim e2; Intros I3 I4;
 139  [ Intros a1; Elim (I1 a1) ; Intros a2 ; Elim (I3 a2) ; Intros a3 ; Exists a3 |
 140    Intros a3; Elim (I4 a3) ; Intros a2 ; Elim (I2 a2) ; Intros a1 ; Exists a1 ];
 141  Apply r1 with (f2 a2); Assumption.
 142
 143 Simpl ; Intros; Inversion H; Inversion H0; Assumption.
 144 Qed.
 145
 146 Theorem EQ_sym : (E1,E2:Ens)(EQ E1 E2)->(EQ E2 E1).
 147 Induction E1 ; [ Intros A1 f1 r1 | Intros A1 a1 ];
 148 Induction E2 ; [Intros A2 f2 r2 | Contradiction | Contradiction |Intros A2 a2].
 149
 150 Induction 1; Intros e1 e2; Split;
 151  [ Intros a2; Elim (e2 a2); Intros a1 H1; Exists a1 |
 152    Intros a1; Elim (e1 a1); Intros a2 H2; Exists a2 ] ; Apply r1; Assumption.
 153 Destruct 1; Apply EQ_refl.
 154 Qed.
 155
 156 Theorem EQ_INC : (E,E':Ens)(EQ E E')->(INC E E').
 157 Induction E ; [Intros A f r | Intros A a] ; Induction E' ;
 158  [Intros A' f' r' | Contradiction | Contradiction | Intros A' a'].
 159 Simpl; Destruct 1; Intros e1 e2.
 160 Intros C; Induction 1; Intros a ea; Elim (e1 a); Intros a' ea'; Exists a'.
 161 Apply EQ_tran with (f a); Assumption.
 162 Destruct 1; Hnf; Constructor 1.
 163 Qed.
 164
 165 Hints Resolve EQ_sym EQ_refl EQ_INC : zfc.
 166
 167 Theorem INC_EQ : (E,E':Ens)(INC E E')->(INC E' E)->(EQ E E').
 168 Induction E ; [Intros A f r | Intros A a] ; Induction E' ;
 169  [Intros A' f' r' | Auto | Auto | Auto].
 170 Unfold INC; Simpl; Intros I1 I2; Split.
 171 Intros a; Apply I1; Exists a; Apply EQ_refl.
 172 Intros a'; Cut (EXType A [x:A](EQ (f' a')(f x))).
 173 Induction 1; Intros a ea; Exists a; Apply EQ_sym; Exact ea.
 174 Apply I2; Exists a'; Apply EQ_refl.
 175 Qed.
 176
 177 Hints Resolve INC_EQ : zfc.
 178
 179 (* Membership is extentional (i.e. is stable w.r.t. EQ)   *)
 180
 181 Theorem IN_sound_left :
 182                 (E,E',E'':Ens)
 183                   (EQ E E')->(IN E E'')->(IN E' E'').
 184 Induction E''; [Intros A'' f'' r'' e | Intros A'' a'' e]; Simpl.
 185 Induction 1; Intros a'' p; Exists a''; Apply EQ_tran with E;
 186  [Apply EQ_sym; Assumption | Assumption].
 187
 188 Intro; Assumption.
 189 Qed.
 190
 191 Theorem IN_sound_right :
 192                 (E,E',E'':Ens)
 193                    (EQ E' E'')->(IN E E')->(IN E E'').
 194 Induction E'; [Intros A' f' r' | Intros A' a']; Induction E'';
 195  [Intros A'' f'' r'' | Intros A'' a'' | Intros A'' f'' r'' | Intros A'' a''];
 196  Simpl.
 197 Induction 1; Intros e1 e2; Induction 1; Intros a' e'; Elim (e1 a');
 198  Intros a'' e''; Exists a''; Apply EQ_tran with (f' a'); Assumption.
 199 Intros; Assumption.
 200 Intros; Elim H.
 201 Intros; Assumption.
 202 Qed.
 203
 204 (* Inclusion is reflexive, transitive, extentional *)
 205
 206 Theorem INC_refl : (E:Ens)(INC E E).
 207 Induction E; Auto with zfc.
 208 Qed.
 209
 210 Theorem INC_tran : (E,E',E'':Ens)(INC E E')->(INC E' E'')->(INC E E'').
 211 Induction E; Induction E'; Induction E''; Simpl;
 212  Auto Orelse Contradiction Orelse (Intros; Elim H0; Assumption).
 213 Qed.
 214
 215 Theorem INC_sound_left :
 216                (E,E',E'':Ens)
 217                   (EQ E E')->(INC E E'')->(INC E' E'').
 218 Induction E; [Intros A f r | Intros A a]; Induction E';
 219  [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a'];
 220  Induction E''; [Intros A'' f'' r'' | Contradiction | Contradiction |
 221  Contradiction | Contradiction | Contradiction | Contradiction |
 222  Intros A'' a''].
 223 Unfold INC; Intros; Apply H0; Apply IN_sound_right with (sup A' f');
 224  Auto with zfc.
 225 Destruct 1; Auto.
 226 Qed.
 227
 228 Theorem INC_sound_right :
 229                (E,E',E'':Ens)
 230                  (EQ E' E'')->(INC E E')->(INC E E'').
 231 Induction E; [Intros A f r | Intros A a]; Induction E';
 232  [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a'];
 233  Induction E''; [Intros A'' f'' r'' | Contradiction | Contradiction |
 234  Contradiction | Contradiction | Contradiction | Contradiction |
 235  Intros A'' a''].
 236 Unfold INC; Intros;  Apply IN_sound_right with (sup A' f');
 237  [Assumption | Apply H0; Assumption].
 238 Destruct 1; Auto.
 239 Qed.
 240
 241 (******************************************************************************)
 242 (*                                THE EMPTY SET                               *)
 243 (******************************************************************************)
 244
 245 (* The empty set  (vide = french for empty)   *)
 246 Definition Vide : Ens :=
 247  (sup F [f:F]<Ens>Cases f of end).
 248
 249 Theorem Vide_est_vide : (E:Ens)(IN E Vide)->F.
 250 Unfold Vide; Simpl; Intros E H; Cut False.
 251 Induction 1.
 252 Elim H; Intros x; Elim x.
 253 Qed.
 254
 255 (* CSC: This is different from Werner *)
 256 Theorem tout_vide_est_Vide :
 257  (A:Type)(f:A->Ens)((E':Ens)(IN E' (sup A f))->F)->(EQ (sup A f) Vide).
 258 Intros; Hnf; Split.
 259 Intro; Cut F.
 260 Destruct 1.
 261 Apply H with (f x); Unfold IN; Exists x; Apply EQ_refl.
 262 Destruct y.
 263 Qed.
 264
 265 (******************************************************************************)
 266 (*                                    PAIRE                                   *)
 267 (******************************************************************************)
 268
 269 Definition Paire : Ens -> Ens -> Ens :=
 270  [E1,E2:Ens] (sup bool [b:bool]Cases b of true => E1 | false => E2 end).
 271
 272 (* The pair construction is extentional *)
 273
 274 Theorem Paire_sound_left : (A,A',B:Ens)
 275                         (EQ A A')->(EQ (Paire A B)(Paire A' B)).
 276 Unfold Paire .
 277 Simpl.
 278 (Intros; Split).
 279 Induction x.
 280 (Exists  true; Auto with zfc).
 281
 282 (Exists  false; Auto with zfc).
 283
 284 (Induction y; Simpl).
 285 (Exists  true; Auto with zfc).
 286
 287 (Exists  false; Auto with zfc).
 288 Qed.
 289
 290 Theorem Paire_sound_right : (A,B,B':Ens)
 291                 (EQ B B')->(EQ (Paire A B)(Paire A B')).
 292 Unfold Paire; Simpl; Intros; Split.
 293 Induction x.
 294 (Exists true; Auto with zfc).
 295 Exists false; Auto with zfc.
 296 Induction y.
 297 (Exists true; Auto with zfc).
 298 Exists false; Auto with zfc.
 299 Qed.
 300
 301 Hints Resolve Paire_sound_right Paire_sound_left : zfc.
 302
 303 Theorem IN_Paire_left : (E,E':Ens)(IN E (Paire E E')).
 304 Unfold Paire; Exists true; Apply EQ_refl.
 305 Qed.
 306
 307 Theorem IN_Paire_right : (E,E':Ens)(IN E' (Paire E E')).
 308 Unfold Paire; Exists false; Apply EQ_refl.
 309 Qed.
 310
 311 Theorem Paire_IN : (E,E',A:Ens)(IN A (Paire E E'))->(EQ A E)\/(EQ A E').
 312 Unfold Paire; Simpl.
 313 Induction 1; Intros b; Elim b; Auto with zfc.
 314 Save.
 315
 316 Hints Resolve IN_Paire_left IN_Paire_right Vide_est_vide : zfc.
 317
 318 (******************************************************************************)
 319 (*                                  SINGLETON                                 *)
 320 (******************************************************************************)
 321
 322 (* CSC: This is different from Benjamin only because I like it more; *)
 323 (*      theorems are also simpler                                    *)
 324 (*      In Benjamin's encoding (Sing E) was defined as (Paire E E)   *)
 325 Definition Sing : Ens -> Ens :=
 326  [E:Ens] (sup Un [x:Un]Cases x of void => E end).
 327
 328 Theorem IN_Sing : (E:Ens)(IN E (Sing E)).
 329 Simpl; Exists void; Apply EQ_refl.
 330 Qed.
 331
 332 Theorem IN_Sing_EQ : (E,E':Ens)(IN E (Sing E'))->(EQ E E').
 333 Simpl; Intros; Elim H; Destruct x; Trivial.
 334 Qed.
 335
 336 Hints Resolve IN_Sing IN_Sing_EQ : zfc.
 337
 338 Theorem Sing_sound : (A,A':Ens)(EQ A A')->(EQ (Sing A)(Sing A')).
 339 Intros; Hnf; Split; [Destruct x | Destruct y]; Exists void; Assumption.
 340 Qed.
 341
 342 Hints Resolve Sing_sound : zfc.
 343
 344 Theorem EQ_Sing_EQ : (E1,E2:Ens)(EQ (Sing E1)(Sing E2))->(EQ E1 E2).
 345 Intros; Hnf in H; Elim H; Intros; Elim (H0 void); Destruct x; Trivial.
 346 Qed.
 347
 348 Hints Resolve EQ_Sing_EQ : zfc.
 349
 350 (******************************************************************************)
 351 (*                       COMPREHENSION (OR SEPARATION)                        *)
 352 (******************************************************************************)
 353
 354 Definition Comp: Ens -> (Ens -> Prop) -> Ens.
 355 Induction 1.
 356 Intros A f fr P.
 357 Apply (sup {x:A|(P (f x))}).
 358 Induction 1; Intros x p; Exact (f x).
 359 Intros. Exact X.
 360 Qed.
 361
 362 Transparent Comp.
 363
 364 Theorem Comp_INC : (E:Ens)(P:Ens->Prop)(INC (Comp E P) E).
 365 Destruct E.
 366 Intros A f P; Simpl; Destruct E0; [Intros A' f' H | Intros A' a' H];
 367  Elim H; Destruct x; Intros x0 p eq; Exists x0; Exact eq.
 368 Auto with zfc.
 369 Qed.
 370
 371 Theorem IN_Comp_P :
 372            (E,A:Ens)
 373                (P:Ens->Prop)((w1,w2:Ens)(P w1)->(EQ w1 w2)->(P w2))->
 374                   (IN A (Comp E P))->(P A).
 375 Induction E.
 376 Simpl; Intros B f Hr A P H i; Elim i; Destruct x; Simpl; Intro b; Intros;
 377  Apply H with (f b); Auto with zfc.
 378 Contradiction.
 379 Qed.
 380
 381 Theorem IN_P_Comp :
 382      (E,A:Ens)
 383         (P:Ens ->Prop)((w1,w2:Ens)(P w1)->(EQ w1 w2)->(P w2))->
 384                 (IN A E)->(P A)->(IN A (Comp E P)).
 385 Induction E.
 386 Simpl; Intros B f HR A P H i; Elim i; Simpl; Intros; Cut (P (f x)).
 387 Intros Pf.
 388 Exists (exist B [x:B](P (f x)) x Pf); Simpl; Auto with zfc.
 389 Apply H with A; Auto with zfc.
 390 Contradiction.
 391 Qed.
 392
 393 (* Again, extentionality is not stated, but easy *)
 394
 395 (******************************************************************************)
 396 (*                                    UNION                                   *)
 397 (******************************************************************************)
 398
 399 (* Projections of a set: *)
 400 (*  1: its base type, F for atoms *)
 401
 402 Definition pi1: Ens -> Type.
 403 Induction 1.
 404 Intros A f r.
 405 Exact A.
 406 Intros.
 407 Exact F.
 408 Save.
 409
 410 Transparent pi1.
 411
 412 (*  2: the function, [_:F]Vide for atoms *)
 413
 414 Definition pi2 : (E:Ens)(pi1 E)->Ens.
 415 Induction E.
 416 Intros A f r.
 417 Exact f.
 418 Intros.
 419 Exact Vide.
 420 Save.
 421
 422 Transparent pi2.
 423
 424 Definition Union : (E:Ens)Ens.
 425 Induction 1.
 426 Intros A f r.
 427 Apply (sup (depprod A [x:A](pi1 (f x)))).
 428 Induction 1; Intros a b.
 429 Exact (pi2 (f a) b).
 430 Intros.
 431 Exact Vide.
 432 Save.
 433
 434 Transparent Union.
 435
 436 Theorem EQ_EXType : (E,E':Ens)
 437         (EQ E E')
 438          ->(a:(pi1 E))
 439             (EXType (pi1 E') [b:(pi1 E')](EQ (pi2 E a) (pi2 E' b))).
 440 Induction E; [Intros A f r | Intros A a]; Induction E';
 441  [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a'].
 442 Simpl; Destruct 1; Intros e1 e2 a; Apply e1.
 443 Contradiction.
 444 Contradiction.
 445 Simpl; Destruct 2.
 446 Qed.
 447
 448 Transparent EQ_EXType.
 449
 450 Theorem IN_EXType: (E,E':Ens)(IN E' E)->
 451                         (EXType (pi1 E) [a:(pi1 E)](EQ E' (pi2 E a))).
 452 Induction E.
 453 Simpl; Intros A f r; Induction 1; Intros; Exists x; Assumption.
 454 Destruct 1.
 455 Qed.
 456
 457 Theorem IN_Union : (E,E',E'':Ens)
 458                 (IN E' E)->(IN E'' E')->(IN E'' (Union E)).
 459 Induction E.
 460 2: Destruct 1.
 461 Intros A f r.
 462 Intros; Simpl.
 463 Elim (IN_EXType (sup A f) E' H).
 464 Intros x e.
 465 Cut (EQ (pi2 (sup A f) x) E').
 466 2: Auto with zfc v62.
 467 Intros e1.
 468 Cut (IN E'' (pi2 (sup A f) x)).
 469 Intros i1.
 470 Elim (IN_EXType ? ? i1).
 471 Intros x0 e2.
 472 Simpl in x0.
 473 Exists  (dep_i A [x:A](pi1 (f x)) x x0).
 474 Simpl.
 475 Exact e2.
 476 Apply IN_sound_right with E'; Assumption.
 477 Qed.
 478
 479 (* CSC: This is different from Benjamin *)
 480 Theorem IN_INC_Union :
 481       (A:Type)(f:A->Ens)(E:Ens)(IN (sup A f) E)->(INC (sup A f) (Union E)).
 482 Induction E.
 483 Intros A f r H; Hnf; Hnf in H; Intros; Elim H; Intros x e.
 484 Cut (IN E0 (f0 x)).
 485 Intro in_E0_f0x; Apply IN_Union with (f0 x).
 486 Hnf; Split with x; Auto with zfc.
 487
 488 Auto with zfc.
 489 Apply IN_sound_right with (sup A f); Trivial.
 490
 491 (Simpl; Destruct 2; Destruct x).
 492 Qed.
 493
 494 Theorem Union_IN : (E,E':Ens)(IN E' (Union E))->
 495                                 (EXType ? [E1:Ens](IN E1 E)/\(IN E' E1)).
 496 Induction E.
 497 2: (Simpl; Destruct 2; Destruct x).
 498 Unfold Union ; Simpl; Intros A f r.
 499 Induction 1.
 500 Induction x.
 501 (Intros a b; Simpl).
 502 Intros.
 503 Exists  (f a).
 504 Split.
 505 (Exists  a; Auto with zfc v62).
 506
 507 (Apply IN_sound_left with (pi2 (f a) b); Auto with zfc v62).
 508 Simpl.
 509 (Generalize b ; Elim (f a); Simpl).
 510 Intros.
 511 (Exists  b0; Auto with zfc v62).
 512
 513 Destruct 2.
 514 Qed.
 515
 516 (* extentionality of union  *)
 517
 518 Theorem Union_sound
 519      : (E,E':Ens)(EQ E E')->(EQ (Union E) (Union E')).
 520 Unfold Union.
 521 Induction E ; [Intros A f r | Intros A a] ; Induction E' ;
 522  [Intros A' f' r' | Intros A' a' | Intros A' f' r' | Intros A' a'].
 523
 524 Simpl; Induction 1; Intros e1 e2; Split.
 525 Intros x; Elim x; Intros a aa; Elim (e1 a); Intros a' ea.
 526 Elim (EQ_EXType (f a)(f' a') ea aa); Intros aa' eaa.
 527 Exists (dep_i A' [x:A'](pi1 (f' x)) a' aa'); Simpl; Auto with zfc v62.
 528 Intros c'; Elim c'; Intros a' aa'; Elim (e2 a'); Intros a ea.
 529 Cut (EQ (f' a')(f a)).
 530 2 : Auto with zfc v62.
 531 Intros ea'; Elim (EQ_EXType (f' a')(f a) ea' aa'); Intros aa eaa.
 532 Exists (dep_i A [x:A](pi1 (f x)) a aa); Auto with zfc v62.
 533
 534 Contradiction.
 535 Contradiction.
 536 Destruct 1; Apply EQ_refl.
 537 Qed.
 538
 539 (* The union construction is monotone w.r.t. inclusion   *)
 540
 541 Theorem Union_mon : (E,E':Ens)(INC E E')->(INC (Union E)(Union E')).
 542 Induction E ; [Intros A f r | Intros A a] ; Induction E';
 543  [Intros A' f' r' | Contradiction | Contradiction | Intros A' a'].
 544 2: Auto with zfc.
 545 Intro; Cut (E:Ens)(IN E (sup A f))->(IN E (sup A' f')).
 546 2: Auto.
 547 Intro XXX; Cut ((E:Ens)(IN E (Union (sup A f)))->(IN E (Union (sup A' f'))))
 548     ->(INC (Union (sup A f)) (Union (sup A' f'))).
 549 2: Auto.
 550 Intros X; Apply X; Intros E0 Y; (Elim (Union_IN (sup A f) E0); Auto with zfc).
 551 Destruct 1; Intros; Cut (IN x (sup A' f')).
 552 2: Auto.
 553 Intro; (Apply IN_Union with x; Auto).
 554 Qed.
 555
 556 (******************************************************************************)
 557 (*                                 INTERSECTION                               *)
 558 (******************************************************************************)
 559
 560 Definition Inter : (E:Ens)Ens :=
 561 [E:Ens]
 562  Cases E of
 563    (sup A f) =>
 564       (sup ?
 565            [c:(depprod A
 566                [a:A](depprod ? [b:(pi1 (f a))](x:A)(IN (pi2 (f a) b)(f x)))
 567               )
 568            ]
 569            Cases c of
 570               (dep_i a (dep_i b p)) => (pi2 (f a) b)
 571            end
 572       )
 573  | (atom A a) => Vide
 574  end.
 575
 576 Theorem IN_Inter_all : (E,E':Ens)
 577                         (IN E' (Inter E))->
 578                                 (E'':Ens)(IN E'' E)->(IN E' E'').
 579 Induction E; [Intros A f r | Contradiction]; Intros E'.
 580 Induction 1; Intros c; Elim c; Intros a ca; Elim ca; Intros aa paa.
 581 Intros e E'' e''.
 582 Elim e''; Intros a1 ea1.
 583 Apply IN_sound_right with (f a1); Auto with zfc v62.
 584 Apply IN_sound_left with (pi2 (f a) aa); Auto with zfc v62.
 585 Qed.
 586
 587 Theorem all_IN_Inter : (E,E',E'':Ens)
 588                          (IN E'' E)->
 589                             ((E'':Ens)(IN E'' E)->(IN E' E''))->
 590                                 (IN E' (Inter E)).
 591 (Induction E; [Intros A f r | Contradiction]).
 592 Intros E' E'' i H.
 593 Elim (IN_EXType (sup A f) E'' i).
 594 (Intros a e; Simpl in a).
 595 Simpl in e.
 596 (Cut (IN E' E''); Auto with zfc v62).
 597 Intros i'.
 598 (Cut (IN E' (f a)); Auto with zfc v62).
 599 Intros i0.
 600 Elim (IN_EXType (f a) E' i0).
 601 Intros b e'.
 602 Simpl.
 603 Cut (x:A)(IN (pi2 (f a) b) (f x)).
 604 Intros.
 605 Exists  (dep_i A
 606           [a:A]
 607            (depprod (pi1 (f a))
 608              [b:(pi1 (f a))](x:A)(IN (pi2 (f a) b) (f x)))
 609           a
 610           (dep_i (pi1 (f a))
 611             [b:(pi1 (f a))](x:A)(IN (pi2 (f a) b) (f x)) b H0)).
 612 Simpl.
 613 Auto with zfc v62.
 614 Auto with zfc v62.
 615 Intros.
 616 Apply IN_sound_left with E'.
 617 Auto with zfc v62.
 618 Apply H.
 619 Auto with zfc v62.
 620 Simpl.
 621 (Exists  x; Auto with zfc v62).
 622 (Apply IN_sound_right with E''; Auto with zfc v62).
 623 Qed.
 624
 625 (******************************************************************************)
 626 (*                                  POWERSET                                  *)
 627 (******************************************************************************)
 628
 629 Definition Power : Ens -> Ens :=
 630 [E:Ens]
 631  Cases E of
 632   (sup A f) =>
 633    (sup ?
 634         [P:A->Prop]
 635             (sup ?
 636                  [c:(depprod A [a:A](P a))]
 637                     Cases c of
 638                       (dep_i a p) => (f a)
 639                     end
 640             )
 641    )
 642  | (atom A a) => (Sing (atom A a)) (* ??? or Vide? *)
 643  end.
 644
 645 Theorem IN_Power_INC : (E,E':Ens)(IN E' (Power E))->(INC E' E).
 646 Induction E.
 647 Intros A f r; Unfold INC ; Simpl.
 648 Intros E'; Induction 1; Intros P.
 649 Elim E'.
 650 Simpl.
 651 Intros A' f' r'.
 652 Induction 1; Intros HA HB.
 653 Intros E''; Induction 1; Intros a' e.
 654 Elim (HA a').
 655 Induction x; Intros a p.
 656 Intros; Exists  a.
 657 Apply EQ_tran with (f' a'); Auto with zfc v62.
 658 Contradiction.
 659 Auto with zfc.
 660 Qed.
 661
 662 (* CSC: This is different from Benjamin *)
 663 Theorem INC_IN_Power : (E,E':Ens)(INC E' E)->(IN E' (Power E)).
 664 Induction E.
 665 2: Induction E'.
 666 2: Contradiction.
 667 2: (Destruct 1; Unfold Power; Auto with zfc).
 668 Intros A f r; Unfold INC; Simpl; Induction E'.
 669 2: Contradiction.
 670 Intros A' f' r' i.
 671 Exists  [a:A](IN (f a) (sup A' f')).
 672 Simpl.
 673 Split.
 674 Intros.
 675 Elim (i (f' x)).
 676 Intros a e.
 677 (Cut (EQ (f a) (f' x)); Auto with zfc v62).
 678 Intros e1.
 679 Exists  (dep_i A [a:A](EXType A' [y:A'](EQ (f a) (f' y))) a
 680           (EXTypei A' [y:A'](EQ (f a) (f' y)) x e1)).
 681 Auto with zfc v62.
 682 Simpl.
 683 (Exists  x; Auto with zfc v62).
 684 Induction y; Induction 1; Intros.
 685 (Exists  x0; Auto with zfc v62).
 686 Qed.
 687
 688 Theorem Power_mon : (E,E':Ens)(INC E E')->(INC (Power E)(Power E')).
 689 Induction E; [Intros A f r | Intros A a]; Induction E';
 690  [Intros A' f' r' | Contradiction | Contradiction | Destruct 1; Auto with zfc].
 691 Intro.
 692 Hnf in H.
 693 Cut ((E:Ens)(IN E (Power (sup A f)))->(IN E (Power (sup A' f'))))
 694     ->(INC (Power (sup A f)) (Power (sup A' f'))).
 695 2: Auto.
 696 Intros.
 697 Apply H0.
 698 Intros.
 699 Cut (INC E0 (sup A f)).
 700 2: (Apply IN_Power_INC; Auto).
 701 Intro.
 702 Cut (INC E0 (sup A' f')).
 703 Intro.
 704 Apply INC_IN_Power.
 705 Assumption.
 706
 707 Generalize H2.
 708 Elim E0.
 709 Unfold INC.
 710 Auto with zfc.
 711
 712 Auto with zfc.
 713 Qed.
 714
 715 Theorem Power_sound : (E,E':Ens)(EQ E E')->(EQ (Power E)(Power E')).
 716 Induction E; [Intros A f r | Intros A a]; Induction E';
 717  [Intros A' f' r' | Contradiction | Contradiction | Destruct 1; Auto with zfc].
 718 Intro.
 719 Apply INC_EQ.
 720 Cut ((E:Ens)(IN E (Power (sup A f)))->(IN E (Power (sup A' f'))))
 721     ->(INC (Power (sup A f)) (Power (sup A' f'))).
 722 2: Auto.
 723 Intros; Apply H0; Clear H0; Intros; Cut (INC E0 (sup A f)).
 724 2: (Apply IN_Power_INC; Auto with zfc).
 725 Clear H0; Intro; Apply INC_IN_Power.
 726 (Apply INC_sound_right with (sup A f); Auto).
 727
 728 (* Using simmetry *)
 729 Cut ((E:Ens)(IN E (Power (sup A' f')))->(IN E (Power (sup A f))))
 730     ->(INC (Power (sup A' f')) (Power (sup A f))).
 731 2: Auto.
 732 Intros; Apply H0; Clear H0; Intros; Cut (INC E0 (sup A' f')).
 733 2: (Apply IN_Power_INC; Auto with zfc).
 734 Clear H0; Intro; Apply INC_IN_Power.
 735 (Apply INC_sound_right with (sup A' f'); Auto with zfc).
 736 Qed.
 737
 738 (******************************************************************************)
 739 (*                              ORDERED COUPLES                               *)
 740 (******************************************************************************)
 741
 742 (* small lemmas *)
 743
 744 Theorem not_EQ_Sing_Vide : (E:Ens)(EQ (Sing E) Vide)->F.
 745 Intros E e; Cut False.
 746 Induction 1.
 747 Cut (IN E Vide).
 748 Simpl; Induction 1; Intros xx; Elim xx; Induction 1.
 749 Apply IN_sound_right with (Sing E); Auto with zfc v62.
 750 Qed.
 751
 752 Theorem not_EQ_Vide_Sing : (E:Ens)(EQ Vide (Sing E))->F.
 753 Intros E e; Cut False.
 754 Induction 1.
 755 Cut (IN E Vide).
 756 Simpl; Induction 1; Intros xx; Elim xx; Induction 1.
 757 Apply IN_sound_right with (Sing E); Auto with zfc v62.
 758 Qed.
 759
 760 (* This definition of the ordered pair is slightly different from *)
 761 (* the usual one, since we want it to work in an intuisionistic   *)
 762 (* setting. Works the same, neitherless. The soundness proofs are *)
 763 (* unpleasant.                                                    *)
 764
 765 Definition Couple := [E,E': Ens](Paire (Sing E) (Paire Vide (Sing E'))).
 766
 767 Theorem Couple_inj_left : (A,A',B,B':Ens)
 768                 (EQ (Couple A A')(Couple B B'))->(EQ A B).
 769 (Unfold Couple; Simpl); Induction 1; (Intros HA HB; Elim (HA true)).
 770 (Intros x; Elim x; Simpl; Induction 1; Intros H3 H4; Elim (H3 void);
 771  Simpl; Destruct x0).
 772 Trivial.
 773
 774 Elim (H4 false); Destruct x1; Intros; Cut (EQ (Sing B') Vide).
 775 Simpl; Induction 1; Intros yy; Elim (yy void); Destruct x2.
 776
 777 Apply EQ_tran with A.
 778 Auto with zfc.
 779
 780 Assumption.
 781
 782 Intros; Cut (EQ (Sing B') Vide).
 783 Simpl; Induction 1; Intros yy; Elim (yy void); Destruct x1.
 784
 785 Apply EQ_tran with A.
 786 Auto with zfc.
 787
 788 Elim (H4 true); Destruct x1; Trivial.
 789 Qed.
 790
 791 Theorem Couple_inj_right :  (A,A',B,B':Ens)
 792                 (EQ (Couple A A')(Couple B B'))->(EQ A' B').
 793 Unfold Couple; Simpl.
 794 Induction 1; Intros H1 H2.
 795 Elim (H1 false).
 796 Intros bb1; Elim bb1.
 797 Intros HF.
 798 Change (EQ (Paire Vide (Sing A'))(Sing B)) in HF.
 799 Cut F.
 800 Induction 1.
 801 Apply (not_EQ_Vide_Sing A').
 802 Apply EQ_tran with B.
 803 Apply IN_Sing_EQ; Apply IN_sound_right with (Paire Vide (Sing A'));
 804  Auto with zfc v62.
 805 Apply EQ_sym; Apply IN_Sing_EQ;
 806         Apply IN_sound_right with (Paire Vide (Sing A')); Auto with zfc v62.
 807 Change (EQ (Paire Vide (Sing A'))(Paire Vide (Sing B')))->(EQ A' B').
 808 Intros HP; Cut (EQ (Sing A') (Sing B')).
 809 Intros; Auto with zfc v62.
 810 Cut (IN (Sing A')(Paire Vide (Sing B'))).
 811 Intros HI; Elim (Paire_IN Vide (Sing B')(Sing A') HI).
 812 Intros; Cut F.
 813 Induction 1.
 814 Apply not_EQ_Sing_Vide with A'; Assumption.
 815 Trivial with zfc v62.
 816 Apply IN_sound_right with (Paire Vide (Sing A')); Auto with zfc v62.
 817 Qed.
 818
 819 (******************************************************************************)
 820 (*                                   POWERSET                                 *)
 821 (******************************************************************************)
 822
 823 (* Here we cheat. It is easier to define the cartesian product using    *)
 824 (* the type theoretical product, i.e. we here use non set-theoretical   *)
 825 (* constructions. We could however use the usual definitions.           *)
 826
 827 Definition Prod : Ens -> Ens -> Ens :=
 828 [E,E':Ens]
 829  Cases E E' of
 830    (sup A f) (sup A' f') =>
 831      (sup ?
 832           [c:(prod_t A A')]
 833                Cases c of
 834                  (pair_t a a') => (Couple (f a) (f' a'))
 835                end
 836      )
 837  | _ _ => Vide
 838  end.
 839
 840 Hints Resolve Paire_sound_left Paire_sound_right : zfc.
 841
 842 Theorem Couple_sound_left :
 843         (A,A',B:Ens)(EQ A A')->(EQ (Couple A B)(Couple A' B)).
 844  Unfold Couple;Intros; Auto with zfc v62.
 845 Save.
 846
 847 Theorem Couple_sound_right:
 848         (A,B,B':Ens)(EQ B B')->(EQ (Couple A B)(Couple A B')).
 849  Unfold Couple;Intros; Auto with zfc v62.
 850 Save.
 851
 852 Theorem Couple_IN_Prod : (E1,E2,E1',E2':Ens)
 853                 (IN E1' E1)->(IN E2' E2)->
 854                         (IN (Couple E1' E2')(Prod E1 E2)).
 855 Induction E1; [Intros A1 f1 r1 | Contradiction].
 856 Induction E2; [Intros A2 f2 r2 | Contradiction].
 857 Intros E1' E2' i1 i2.
 858 Elim (IN_EXType (sup A1 f1) E1').
 859 (Intros x e1; Simpl in x).
 860 Elim (IN_EXType (sup A2 f2) E2').
 861 (Intros x0 e2; Simpl in x).
 862 Apply IN_sound_left with (Couple (pi2 (sup A1 f1) x) (pi2 (sup A2 f2) x0)).
 863 Apply EQ_tran with (Couple (pi2 (sup A1 f1) x) E2').
 864 Apply Couple_sound_right.
 865 Auto with zfc v62.
 866
 867 (Apply Couple_sound_left; Auto with zfc v62).
 868
 869 Simpl.
 870 Exists  (pair_t ? ? x x0).
 871 Simpl.
 872 Split.
 873
 874 Induction x1.
 875 Exists true; Auto with zfc.
 876 Exists false; Auto with zfc.
 877
 878 Induction y.
 879 Exists true; Auto with zfc.
 880 Exists false; Auto with zfc.
 881 Assumption.
 882 Assumption.
 883 Qed.
 884
 885 Theorem Couple_Prod_IN :  (E1,E2,E1',E2':Ens)
 886                 (IN (Couple E1' E2')(Prod E1 E2))->
 887                         (IN E1' E1)/\(IN E2' E2).
 888 Induction E1; [Intros A1 f1 r1 | Destruct 1; Destruct x].
 889 Induction E2; [Intros A2 f2 r2 | Destruct 1; Destruct x].
 890 Intros E1' E2' i.
 891 Elim (IN_EXType (Prod (sup A1 f1) (sup A2 f2)) (Couple E1' E2') i).
 892 Destruct x; Intros a1 a2 e.
 893 Change (EQ (Couple E1' E2') (Couple (f1 a1) (f2 a2))) in e.
 894 Cut (EQ E1' (f1 a1)).
 895 Cut (EQ E2' (f2 a2)).
 896 Intros e1 e2.
 897 Split.
 898 Apply IN_sound_left with (f1 a1); Auto with zfc v62; Simpl; Exists a1;
 899  Auto with zfc v62.
 900 Apply IN_sound_left with (f2 a2); Auto with zfc v62; Simpl; Exists  a2;
 901  Auto with zfc v62.
 902 Apply Couple_inj_right with A:=E1' B:=(f1 a1); Auto with zfc v62.
 903 Apply Couple_inj_left with E2' (f2 a2); Auto with zfc v62.
 904 Qed.
 905
 906 Theorem IN_Prod_EXType : (E,E',E'':Ens)(IN E'' (Prod E E'))->
 907         (EXType ? [A:Ens](EXType ? [B:Ens](EQ (Couple A B) E''))).
 908 Induction E ; [Intros A  f  r  | Destruct 1; Destruct x].
 909 Induction E'; [Intros A' f' r' | Destruct 1; Destruct x].
 910 Intros; Elim (IN_EXType (Prod (sup A f) (sup A' f')) E'').
 911 Induction x.
 912 Intros; Exists  (f y); Exists  (f' y0); Auto with zfc v62.
 913 Auto with zfc v62.
 914 Qed.
 915
 916 (******************************************************************************)
 917 (*                                  ORDINALS                                  *)
 918 (******************************************************************************)
 919
 920 Definition Succ := [E:Ens](Union (Paire E (Sing E))).
 921
 922 Inductive Ord : Ens -> Prop :=
 923   Oo : (Ord Vide)
 924 | So : (E:Ens)(Ord E)->(Ord (Succ E))
 925 | Lo : (E:Ens)((e:Ens)(IN e E)->(Ord e))->(Ord (Union E))
 926 | Eo : (E,E':Ens)(Ord E)->(EQ E E')->(Ord E').
 927
 928 Hints Resolve Oo So Lo : zfc.
 929
 930 Definition Nat : nat ->Ens.
 931 Induction 1; Intros.
 932 Exact Vide.
 933 Exact (Succ X).
 934 Save.
 935
 936 Transparent Nat.
 937
 938 Theorem Nat_Ord : (n:nat)(Ord (Nat n)).
 939 Induction n; Simpl; Auto with zfc v62.
 940 Save.
 941
 942 Definition Omega : Ens :=
 943   (sup nat Nat).
 944
 945 Theorem IN_Succ :  (E:Ens)(IN E (Succ E)).
 946 Intros E; Unfold Succ; Apply IN_Union with (Sing E); Auto with zfc v62.
 947 Qed.
 948
 949 (* CSC: This is different from Werner *)
 950 Theorem INC_Succ : (A:Type)(f:A->Ens)(INC (sup A f) (Succ (sup A f))).
 951 Intros; Cut ((E:Ens)(IN E (sup A f))->(IN E (Succ (sup A f))))
 952     ->(INC (sup A f) (Succ (sup A f))).
 953 Intros; Apply H; Unfold Succ; Intros.
 954 Apply IN_Union with (sup A f); Auto with zfc.
 955
 956 Intros; Exact H.
 957 Qed.
 958
 959 Hints Resolve IN_Succ INC_Succ : zfc.
 960
 961 Theorem IN_Succ_or : (E,E':Ens)(IN E' (Succ E))->(EQ E E')\/(IN E' E).
 962 Intros E E' i.
 963 Unfold Succ  in i.
 964 Elim (Union_IN (Paire E (Sing E)) E' i).
 965 Intros E1; Induction 1; Intros i1 i2.
 966 Elim (Paire_IN E (Sing E) E1 i1).
 967 Intros; Right; Apply IN_sound_right with E1; Auto with zfc v62.
 968 Intros; Left; Cut (IN E' (Sing E)).
 969 Auto with zfc v62.
 970 Apply IN_sound_right with E1; Auto with zfc v62.
 971 Qed.
 972
 973 Theorem E_not_IN_E : (E:Ens)(IN E E)->F.
 974 Induction E.
 975 Intros A f r i.
 976 Cut False.
 977 Induction 1.
 978 Elim (IN_EXType (sup A f) (sup A f) i); Intros a e.
 979
 980 Simpl in a.
 981 Change (EQ (sup A f) (f a)) in e.
 982 Elim (r a).
 983 Apply IN_sound_right with (sup A f); Auto with zfc v62.
 984 Exists a; Auto with zfc v62.
 985 Intros; Cut False; Contradiction.
 986 Qed.
 987
 988 Theorem Nat_IN_Omega : (n:nat)(IN (Nat n) Omega).
 989 Intros; Simpl; Exists n; Auto with zfc v62.
 990 Qed.
 991 Hints Resolve Nat_IN_Omega : zfc.
 992
 993 Theorem IN_Omega_EXType : (E:Ens)(IN E Omega)->(EXType ? [n:nat](EQ (Nat n) E)).
 994 (Simpl; Induction 1).
 995 Intros n e.
 996 (Exists  n; Auto with zfc v62).
 997 Qed.
 998
 999 Theorem IN_Nat_EXType : (n:nat)(E:Ens)(IN E (Nat n))->(EXType ? [p:nat](EQ E (Nat p))).
1000 Induction n.
1001 Simpl.
1002 Induction 1.
1003 Induction x.
1004
1005 Intros.
1006 Change (IN E (Succ (Nat n0))) in H0.
1007 Elim (IN_Succ_or (Nat n0) E H0).
1008 (Intros; Exists  n0).
1009 Auto with zfc v62.
1010
1011 Intros.
1012 (Elim (H E); Auto with zfc v62).
1013 Qed.
1014
1015 Theorem Omega_EQ_Union : (EQ Omega (Union Omega)).
1016 Apply INC_EQ.
1017 Cut ((E:Ens)(IN E Omega)->(IN E (Union Omega)))
1018     ->(INC Omega (Union Omega)).
1019 Intros; Apply H.
1020 Clear H.
1021 Intros.
1022 Elim (IN_Omega_EXType E H).
1023 Intros n e.
1024 Apply IN_Union with (Nat (S n)).
1025 Auto with zfc v62.
1026
1027 Apply IN_sound_left with (Nat n).
1028 Auto with zfc v62.
1029
1030 (Change (IN (Nat n) (Succ (Nat n))); Auto with zfc v62).
1031
1032 Intros.
1033 Exact H.
1034
1035 Cut ((E:Ens)(IN E (Union Omega))->(IN E Omega))
1036     ->(INC (Union Omega) Omega).
1037 Intros; Apply H; Clear H.
1038 Intros.
1039 Elim (Union_IN Omega E H).
1040 Intros e h.
1041 Elim h.
1042 Intros i1 i2.
1043 Elim (IN_Omega_EXType e i1).
1044 Intros n e1.
1045 Cut (IN E (Nat n)).
1046 Intros.
1047 (Elim (IN_Nat_EXType n E H0); Intros).
1048 (Apply IN_sound_left with (Nat x); Auto with zfc v62).
1049
1050 (Apply IN_sound_right with e; Auto with zfc v62).
1051
1052 Intros.
1053 Exact H.
1054 Qed.
1055
1056 Theorem Omega_Ord : (Ord Omega).
1057 Apply Eo with (Union Omega).
1058 Apply Lo.
1059 Intros.
1060 Elim (IN_Omega_EXType e H).
1061 Intros n ee.
1062 Apply Eo with (Nat n); Auto with zfc v62.
1063 Elim n.
1064 Auto with zfc v62.
1065 Auto with zfc v62.
1066 Intros.
1067 Change (Ord (Succ (Nat n0))); Auto with zfc v62.
1068 Apply EQ_sym; Auto with zfc v62.
1069 Apply Omega_EQ_Union.
1070 Qed.
1071
1072 Definition Alpha : Ens->Ens.
1073 Induction 1.
1074 Intros A f r.
1075 Apply Union.
1076 Apply (sup A).
1077 Intros a.
1078 Exact (Power (r a)).
1079 Intros A a; Exact (atom A a). (* ??? or Vide? *)
1080 Save.
1081
1082 Transparent Alpha.
1083
1084 (******************************************************************************)
1085 (*                           AXIOM OF CHOICE                                  *)
1086 (******************************************************************************)
1087
1088 (* A Type-theoretical axiom of choice gives us the collection axiom  *)
1089
1090 Definition collection :=
1091  (P:Ens->Ens->Prop)
1092   ((x,x',y:Ens)(EQ x x')->(P x y)->(P x' y))->
1093    ((E:Ens)(EXType ? (P E)))->
1094      (E:Ens)(EXType ? [A:Ens](x:Ens)(IN x E)->
1095       (EXType ? [y:Ens](IN y A)/\(P x y))).
1096
1097
1098 Definition choice :=
1099  (A,B:Type)(P:A->B->Prop)
1100    ((a:A)(EXType ? [b:B](P a b)))->
1101        (EXType ? [f:A->B]((a:A)(P a (f a)))).
1102
1103 Theorem Choice_Collection : choice -> collection.
1104 Intro; Unfold collection; Intros P comp G E;
1105  Cut (EXType ? [f:(Ens->Ens)](B:Ens)(P B (f B))).
1106 Induction 1; Intros f Pf; Elim E.
1107 Intros A g hr; Split with (sup A [a:A](f (g a))).
1108 Simpl; Intros X i; Elim i; Intros a ea; Split with (f (g a)).
1109 Split.
1110 Exists a; Auto with zfc.
1111
1112 Apply comp with (g a); Auto with zfc.
1113
1114 Auto with zfc.
1115
1116 Intros; Split with Vide; Contradiction.
1117
1118 Unfold choice in H; Apply H; Intros; Elim (G a); Intros b hb; Exists b;
1119  Assumption.
1120 Qed.
1121
1122 (* If we also assume the excluded middle, we can derive         *)
1123 (* the usual replacement schemata.                              *)
1124
1125 Definition functional :=
1126         [P:Ens->Ens->Prop](x,y,y':Ens)
1127                 (P x y)->(P x y')->(EQ y y').
1128 Definition replacement :=
1129    (P:Ens->Ens->Prop)
1130         (functional P)->
1131         ((x,y,y':Ens)(EQ y y')->(P x y)->(P x y'))->
1132         ((x,x',y:Ens)(EQ x x')->(P x y)->(P x' y))->
1133        (X:Ens)(EXType ? [Y:Ens](y:Ens)
1134                             (((IN y Y)->(EXType ? [x:Ens](IN x X)/\(P x y)))
1135                             /\((EXType ? [x:Ens](IN x X)/\(P x y))->(IN y Y)))).
1136
1137 Theorem classical_Collection_Replacement :
1138  ((S:Prop)S\/(S->False))->
1139         collection ->
1140                 replacement.
1141 Unfold replacement; Intros EM Collection P fp comp_r comp_l X.
1142 Cut (EXType ? [Y:Ens](y:Ens)((EXType ? [x:Ens](IN x X)/\(P x y))->(IN y Y))).
1143 Induction 1; Intros Y HY.
1144 Exists (Comp Y [y:Ens](EXType ? [x:Ens](IN x X)/\(P x y))).
1145 Intros y; Split.
1146 Intros HC.
1147 Apply (IN_Comp_P Y y [y0:Ens](EXType Ens [x:Ens](IN x X)/\(P x y0))); Auto with zfc v62.
1148 Intros w1 w2; Induction 1; Intros x; Induction 1; Intros Ix Px e.
1149 Exists x; Split; Auto with zfc v62.
1150 Apply comp_r with w1; Auto with zfc v62.
1151 Intros He.
1152 Apply IN_P_Comp.
1153
1154 Intros w1 w2; Induction 1; Intros x; Induction 1; Intros Ix Px e.
1155 Exists x; Split; Auto with zfc v62.
1156 Apply comp_r with w1; Auto with zfc v62.
1157 Apply HY; Auto with zfc v62.
1158 Auto with zfc v62.
1159
1160 Elim (Collection [x,y:Ens]((P x y)\/(((y':Ens)(P x y')->False)/\(EQ y Vide))))
1161         with X.
1162 Intros Y HY.
1163 Elim (EM (EXType ? [x:Ens](IN x X)/\(P x Vide))).
1164 Intros Hvide; Elim Hvide; Intros xv Hxv; Exists Y.
1165 Intros y; Induction 1; Intros x; Induction 1; Intros Hx1 Hx2.
1166 Elim (HY x Hx1).
1167 Intros y'; Induction 1; Intros Hy'1 Hy'2.
1168 Elim Hy'2.
1169 Intros Hy'3; Apply IN_sound_left with y'; Auto with zfc v62.
1170 Apply fp with x; Auto with zfc v62.
1171 Induction 1; Intros Hy'3 Hy'4.
1172 Elim (Hy'3 y Hx2).
1173 Intros HP; Exists (Comp Y [y:Ens]((EQ y Vide)->False)).
1174 Intros y; Induction 1; Intros x; Induction 1; Intros Hx1 Hx2.
1175 Apply IN_P_Comp.
1176 Intros w1 w2 Hw1 Hw Hw2; Apply Hw1; Apply EQ_tran with w2; Auto with zfc v62.
1177 Elim (HY x).
1178 Intros y'; Induction 1; Intros Hy'1 Hy'2.
1179 Elim Hy'2; Intros Hy'3.
1180 Apply IN_sound_left with y'; Auto with zfc v62.
1181 Apply fp with x; Auto with zfc v62.
1182 Elim Hy'3; Intros Hy'4 Hy'5.
1183 Elim (Hy'4 y); Auto with zfc v62.
1184 Assumption.
1185 Intros e; Apply HP; Exists x; Split; Auto with zfc v62;
1186         Apply comp_r with y; Auto with zfc v62; Apply fp; Auto with zfc v62.
1187 Intros x x' y e Hx; Elim Hx; Intros Hx1.
1188 Left; Apply comp_l with x; Auto with zfc v62.
1189 Right; Elim Hx1; Intros Hx2 Hx3; Split.
1190 2 : Assumption.
1191 Intros y' Hy'; Apply (Hx2 y'); Apply comp_l with x'; Auto with zfc v62.
1192 Intros x; Elim (EM (EXType ? [y:Ens](P x y))); Intros Hx.
1193 Elim Hx; Intros x0 Hx0; Exists x0; Left; Assumption.
1194 Exists Vide; Right; Split; Auto with zfc v62.
1195 Intros y Hy; Elim Hx; Exists y; Auto with zfc v62.
1196 Qed.
1197
1198 (******************************************************************************)
1199 (*                  SMALL SETS AND THE BIG SET OF SMALL SETS                  *)
1200 (******************************************************************************)
1201
1202 (* Some definitions replicated on another type level *)
1203
1204 Inductive EXType' [P:Type; Q:P->Prop]: Prop :=
1205  EXTypei' : (x:P)(Q x)->(EXType' P Q).
1206
1207 Inductive prod_t' [A,B:Type] : Type :=
1208  pair_t' : A->B->(prod_t' A B).
1209
1210 Inductive depprod'' [A:Type; P : A->Type] : Type :=
1211  dep_i'' : (x:A)(P x)->(depprod'' A P).
1212
1213 (* The small sets  *)
1214 Inductive Ens' : Type :=
1215    sup' : (A:Type)(A->Ens')->Ens'
1216  | atom' : (A:Type)A->Ens'.
1217
1218 (* Equality on small sets *)
1219 Definition EQ' : Ens' -> Ens' -> Prop.
1220 Induction 1.
1221 Intros A f eq1.
1222 Induction 1.
1223 Intros B g eq2.
1224 Apply and.
1225 Exact (x:A)
1226         (EXType' ? [y:B](eq1 x (g y))).
1227 Exact (y:B)
1228         (EXType' ? [x:A](eq1 x (g y))).
1229
1230 Intros A' a'.
1231 Exact False.
1232
1233 Intros A a.
1234 Induction 1.
1235 Intros A' f eq1.
1236 Exact False.
1237
1238 Intros.
1239 (*Exact (X == X0).*)
1240 Exact (eq_depT Type [A:Type]A A a A0 y).
1241 Save.
1242
1243 Transparent EQ'.
1244
1245 (* small sets can be injected into big sets *)
1246 Definition inj : Ens'->Ens.
1247 Induction 1; [Intros A f fr ; Exact (sup A fr) | Intros A a ; Exact (atom A a)].
1248 Qed.
1249
1250 Transparent inj.
1251
1252 Theorem inj_sound : (E1,E2:Ens')(EQ' E1 E2)->(EQ (inj E1)(inj E2)).
1253 Induction E1; [Intros A1 f1 r1 | Intros A a] ; Induction E2;
1254  [Intros A2 f2 r2 | Contradiction | Contradiction | Intros A' a'].
1255 (Induction 1; Intros HR1 HR2; Split).
1256 (Intros a1; Elim (HR1 a1); Intros a2 Ha2; Exists  a2; Auto with zfc v62).
1257 (Intros a2; Elim (HR2 a2); Intros a1 Ha1; Exists  a1; Auto with zfc v62).
1258
1259 Auto with zfc.
1260 Qed.
1261
1262 Definition Sing' : Ens' -> Ens' :=
1263  [E:Ens'] (sup' Un [x:Un]Cases x of void => E end).
1264
1265 Definition Power' : Ens' -> Ens' :=
1266 [E:Ens']
1267  Cases E of
1268   (sup' A f) =>
1269    (sup' ?
1270         [P:A->Prop]
1271             (sup' ?
1272                  [c:(depprod'' A [a:A](P a))]
1273                     Cases c of
1274                       (dep_i'' a p) => (f a)
1275                     end
1276             )
1277    )
1278  | (atom' A a) => (Sing' (atom' A a)) (* ??? or Vide? *)
1279  end.
1280
1281 Theorem Power_sound_inj : (E:Ens')(EQ (inj (Power' E))(Power (inj E))).
1282 Induction E; [Intros A f HR | Intros A a].
1283 Simpl; Split.
1284 Intros P; Exists P; Split.
1285 Intros c; Elim c; Intros a p.
1286 Exists (dep_i A [a0:A](P a0) a p); Simpl; Auto with zfc v62.
1287 Intros c; Elim c; Intros a p.
1288 Exists (dep_i'' A [a0:A](P a0) a p); Simpl; Auto with zfc v62.
1289 Intros P; Exists P; Split.
1290 Intros c; Elim c; Intros a p.
1291 Exists (dep_i A [a0:A](P a0) a p); Simpl; Auto with zfc v62.
1292 Intros c; Elim c; Intros a p.
1293 Exists (dep_i'' A [a0:A](P a0) a p); Simpl; Auto with zfc v62.
1294
1295 Simpl; Split.
1296 Destruct x; Exists void; Auto with zfc.
1297 Destruct y; Exists void; Auto with zfc.
1298 Qed.
1299
1300 (* The set of small sets *)
1301 Definition Big := (sup Ens' inj).
1302
1303 Theorem Big_is_big : (E:Ens')(IN (inj E) Big).
1304 Intros E; Unfold Big; Simpl; Exists E; Auto with zfc.
1305 Qed.
1306
1307 Theorem IN_Big_small : (E:Ens)(IN E Big)->(EXType' ? [E':Ens'](EQ E (inj E'))).
1308 Unfold Big; Simpl; Induction 1; Intros E' HE'; Exists E'; Assumption.
1309 Qed.
1310
1311 Theorem IN_small_small : (E:Ens)(E':Ens')(IN E (inj E'))->
1312                 (EXType' ? [E1:Ens'](EQ E (inj E1))).
1313 Induction E'; [Intros A' f' HR' | Contradiction]; Simpl;
1314         Induction 1; Intros a' e'; Exists  (f' a'); Assumption.
1315 Qed.
1316
1317 Theorem Big_closed_for_power : (E:Ens)(IN E Big)->(IN (Power E) Big).
1318 Unfold Big; Simpl; Intros E; Induction 1; Intros E' HE'; Exists (Power' E').
1319 Apply EQ_tran with (Power (inj E')).
1320 Apply Power_sound; Assumption.
1321 Apply EQ_sym; Apply Power_sound_inj.
1322 Qed.
1323
1324 (******************************************************************************)
1325 (*                            NO SET OF ALL SETS                              *)
1326 (******************************************************************************)
1327
1328 (* Just for fun : a proof that there is no set of all sets, using *)
1329 (* Russell's paradox construction                                 *)
1330 (* There, of course, are other proofs (foundation, etc)           *)
1331
1332 Theorem Russell : (E:Ens)((E':Ens)(IN E' E))->False.
1333 Intros U HU.
1334 Cut ([x:Ens](IN x x)->False (Comp U [x:Ens](IN x x)->False)).
1335 Intros HR.
1336 Apply HR.
1337 (Apply IN_P_Comp; Auto with zfc v62).
1338 (Intros w1 w2 HF e i; Apply HF; Apply IN_sound_left with w2; Auto with zfc v62;
1339  Apply IN_sound_right with w2; Auto with zfc v62).
1340 Intros H.
1341 Cut (IN (Comp U [x:Ens](IN x x)->False) (Comp U [x:Ens](IN x x)->False)).
1342 Change ([x:Ens](IN x x)->False (Comp U [x:Ens](IN x x)->False)).
1343 Cut (w1,w2:Ens)((IN w1 w1)->False)->(EQ w1 w2)->(IN w2 w2)->False.
1344 Intros ww.
1345 Exact (IN_Comp_P U (Comp U [x:Ens](IN x x)->False)
1346         [x:Ens](IN x x)->False ww H).
1347 (Intros w1 w2 HF e i; Apply HF; Apply IN_sound_left with w2; Auto with zfc v62;
1348  Apply IN_sound_right with w2; Auto with zfc v62).
1349 Assumption.
1350 Qed.
1351
1352 (******************************************************************************)
1353 (*                     SOME AXIOMS AND STRANGE THINGS ;-(                     *)
1354 (*                                                                            *)
1355 (*  The need for axioms is due to the usage of dependent equality, or to my   *)
1356 (*  ignorance about it ;-)                                                    *)
1357 (*                                                                            *)
1358 (******************************************************************************)
1359
1360 Axiom a_de_pi2 :
1361  (T:Type)(n,m:T)(existT Type [A:Type]A T n)==(existT Type [A:Type]A T m)->n==m.
1362
1363 (* The main consequence of the previous axiom *)
1364 Theorem a_pi2 : (T:Type)(n,m:T)(atom T n)==(atom T m)->n==m.
1365 Intros; Inversion H; Apply a_de_pi2; Assumption.
1366 Qed.
1367
1368 (* This theorem is really strange: I can prove this in general, but I can't  *)
1369 (* prove any of it's instance: for example I can't prove                     *)
1370 (* ~(nat==bool)->~(atom nat O)==(atom bool true) due to an internal error of *)
1371 (* Coq                                                                       *)
1372 Theorem a_npi1 : (T1,T2:Type)(t1:T1)(t2:T2)~T1==T2->~(atom T1 t1)==(atom T2 t2).
1373 Unfold not; Intros; Apply H; Inversion H0; Reflexivity.
1374 Qed.
1375
1376 (******************************************************************************)
1377 (*                  MAPPING A TYPE TO THE SET OF IT'S ELEMENTS                *)
1378 (******************************************************************************)
1379
1380 (* (Ens_of_t T t) is thought as the coercion from an element (t:T) to a set *)
1381 Definition Ens_of_t : (T:Type)T->Ens :=
1382  [T:Type][t:T](atom T t).
1383
1384 (* (Ens_of_T T) is thought as the set of the elements of type T ... *)
1385 Definition Ens_of_T : Type -> Ens :=
1386  [T:Type] (sup T [t:T](Ens_of_t T t)).
1387
1388 (* ... and (Prop_on_Ens_of_Prop T P) is thought as the proposition on Ens *)
1389 (* that is true only for (atom T t) where (t:T) and (P t) is true.        *)
1390 Inductive Prop_on_Ens_of_Prop [T:Type; P:T->Prop] : Ens->Prop :=
1391   cons : (t:T)(P t)->(Prop_on_Ens_of_Prop T P (atom T t)).
1392
1393 Theorem Prop_on_Ens_of_Prop_atom_Prop :
1394    (T:Type; P:(T->Prop); t:T)(Prop_on_Ens_of_Prop T P (atom T t))->(P t).
1395 Intros; Inversion H; Replace t with t0.
1396 Assumption.
1397
1398 Apply a_de_pi2; Assumption.
1399 Qed.
1400
1401 Theorem Prop_on_Ens_of_Prop_t :
1402   (T:Type; P:(T->Prop); E:Ens)
1403         (Prop_on_Ens_of_Prop T P E)
1404         ->(EXType T [t:T]E==(atom T t)/\(P t)).
1405 Intros.
1406 Inversion H.
1407 Split with t.
1408 Auto.
1409 Qed.
1410
1411 Lemma EQ_atom: (T:Type)(t:T)(E:Ens)(EQ (atom T t) E)->(atom T t)==E.
1412 Destruct E.
1413 Contradiction.
1414
1415 Intros.
1416 Inversion H.
1417 Reflexivity.
1418 Qed.
1419
1420
1421 Theorem Prop_on_Ens_of_Prop_sound :
1422    (E1,E2:Ens)(T:Type)(P:T->Prop)
1423     (EQ E1 E2)
1424     -> (Prop_on_Ens_of_Prop T P E1)
1425     -> (Prop_on_Ens_of_Prop T P E2).
1426 Intros.
1427 Cut (EXType ? [t:T]E1==(atom T t)/\(P t)).
1428 Destruct 1; Destruct 1.
1429 Intros.
1430 Rewrite H3 in H.
1431 Cut (atom T x)==E2.
1432 Intros.
1433 Rewrite <- H5.
1434 Constructor 1.
1435 Assumption.
1436
1437 Apply EQ_atom.
1438 Assumption.
1439
1440 Apply Prop_on_Ens_of_Prop_t.
1441 Assumption.
1442 Qed.
1443
1444
1445 (******************************************************************************)
1446 (*                             EXAMPLES OF USAGE                              *)
1447 (******************************************************************************)
1448
1449 (* We could define an implicit coercion from nat to Ens using Ens_of_t *)
1450 Coercion Ens_of_nat := [n:nat](Ens_of_t nat n).
1451
1452 (* CNat is the set of the natural numbers of Coq ... *)
1453 Definition CNat : Ens :=
1454  (Ens_of_T nat).
1455
1456 Mutual Inductive
1457  is_even : nat->Prop :=
1458     is_even_O : (is_even O)
1459   | is_even_S : (n:nat)(is_odd n)->(is_even (S n))
1460 with
1461  is_odd : nat->Prop :=
1462     id_ood_S : (n:nat)(is_even n)->(is_odd (S n)).
1463
1464 Lemma not_even_odd: (n:nat)(is_even n)->(is_odd n)->False.
1465 Induction n.
1466 Intros; Inversion H0.
1467
1468 Intros; Apply H; [Inversion H1 | Inversion H0]; Assumption.
1469 Qed.
1470
1471 Definition Cis_even : Ens -> Prop :=
1472   (Prop_on_Ens_of_Prop nat is_even).
1473
1474 Definition Cis_odd : Ens -> Prop :=
1475   (Prop_on_Ens_of_Prop nat is_odd).
1476
1477 (* ... and CEven and COdd are the sets of even/odd natural numbers of Coq *)
1478
1479 Definition CEven := (Comp CNat Cis_even).
1480
1481 Definition COdd  := (Comp CNat Cis_odd).
1482
1483 (* And now an easy fact: the intersection of CEven with COdd is empty *)
1484 Fact COdd_Inter_CEven_EQ_Vide: (EQ (Inter (Paire CEven COdd)) Vide).
1485 Apply INC_EQ.
1486 Cut (E:Ens)(IN E (Inter (Paire CEven COdd)))->(IN E Vide).
1487 Auto.
1488
1489 Intros.
1490 Cut False.
1491 Contradiction.
1492
1493 Cut (IN E CEven)/\(IN E COdd).
1494 Destruct 1.
1495 Intros.
1496 Unfold CEven in H1.
1497 Cut (Cis_even E).
1498 Unfold COdd in H2.
1499 Cut (Cis_odd E).
1500 Intros.
1501 Inversion H3.
1502 Inversion H4.
1503 Rewrite <- H6 in H8.
1504 Cut t0==t.
1505 Intro.
1506 Rewrite H9 in H7.
1507 Apply not_even_odd with t; Assumption.
1508
1509 Apply a_pi2; Assumption.
1510
1511 Apply IN_Comp_P with CNat.
1512 Intros.
1513 Unfold Cis_odd.
1514 Apply Prop_on_Ens_of_Prop_sound with w1; Assumption.
1515
1516 Assumption.
1517
1518 Apply IN_Comp_P with CNat.
1519 Intros.
1520 Unfold Cis_even.
1521 Apply Prop_on_Ens_of_Prop_sound with w1; Assumption.
1522
1523 Assumption.
1524
1525 Split.
1526 Apply IN_Inter_all with (Paire CEven COdd).
1527 Assumption.
1528
1529 Auto with zfc.
1530
1531 Apply IN_Inter_all with (Paire CEven COdd).
1532 Assumption.
1533
1534 Auto with zfc.
1535
1536 Simpl.
1537 Destruct 1.
1538 Destruct x.
1539 Qed.
1540
1541 (* Another easy fact: O is not in COdd *)
1542 Fact O_not_IN_COdd : ~(IN O COdd).
1543 Unfold not; Intro.
1544 Cut (Cis_odd O).
1545 Intro.
1546 Inversion H0.
1547 Simpl in H1.
1548 Cut t==O.
1549 Intro.
1550 Rewrite H3 in H2.
1551 Inversion H2.
1552
1553 Apply a_de_pi2.
1554 Assumption.
1555
1556 Unfold COdd in H.
1557 Apply IN_Comp_P with CNat.
1558 Intros.
1559 Unfold Cis_odd.
1560 Apply Prop_on_Ens_of_Prop_sound with w1.
1561 Assumption.
1562
1563 Exact H0.
1564
1565 Assumption.
1566 Qed.