diff options
author | 2006-04-28 14:59:16 +0000 | |
---|---|---|
committer | 2006-04-28 14:59:16 +0000 | |
commit | 2c4a6b4efe55a2c6ca9ca7b185723e7909e57269 (patch) | |
tree | e1542c8adb83ff297284eefc23a2703461713d9b /test-suite/failure/universes-buraliforti.v | |
parent | 514dce2dfe717e3ed2e37dce6467b56219d451c1 (diff) | |
parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) |
Merge commit 'upstream/8.0pl3+8.1alpha' into 8.0pl3+8.1alpha
Diffstat (limited to 'test-suite/failure/universes-buraliforti.v')
-rw-r--r-- | test-suite/failure/universes-buraliforti.v | 250 |
1 files changed, 130 insertions, 120 deletions
diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v index 01d46133..d18d2119 100644 --- a/test-suite/failure/universes-buraliforti.v +++ b/test-suite/failure/universes-buraliforti.v @@ -4,38 +4,41 @@ (* Some properties about relations on objects in Type *) - Inductive ACC [A : Type; R : A->A->Prop] : A->Prop := - ACC_intro : (x:A)((y:A)(R y x)->(ACC A R y))->(ACC A R x). + Inductive ACC (A : Type) (R : A -> A -> Prop) : A -> Prop := + ACC_intro : + forall x : A, (forall y : A, R y x -> ACC A R y) -> ACC A R x. - Lemma ACC_nonreflexive: - (A:Type)(R:A->A->Prop)(x:A)(ACC A R x)->(R x x)->False. -Induction 1; Intros. -Exact (H1 x0 H2 H2). -Save. + Lemma ACC_nonreflexive : + forall (A : Type) (R : A -> A -> Prop) (x : A), + ACC A R x -> R x x -> False. +simple induction 1; intros. +exact (H1 x0 H2 H2). +Qed. - Definition WF := [A:Type][R:A->A->Prop](x:A)(ACC A R x). + Definition WF (A : Type) (R : A -> A -> Prop) := forall x : A, ACC A R x. Section Inverse_Image. - Variables A,B:Type; R:B->B->Prop; f:A->B. + Variables (A B : Type) (R : B -> B -> Prop) (f : A -> B). - Definition Rof : A->A->Prop := [x,y:A](R (f x) (f y)). + Definition Rof (x y : A) : Prop := R (f x) (f y). - Remark ACC_lemma : (y:B)(ACC B R y)->(x:A)(y==(f x))->(ACC A Rof x). - Induction 1; Intros. - Constructor; Intros. - Apply (H1 (f y0)); Trivial. - Elim H2 using eqT_ind_r; Trivial. - Save. + Remark ACC_lemma : + forall y : B, ACC B R y -> forall x : A, y = f x -> ACC A Rof x. + simple induction 1; intros. + constructor; intros. + apply (H1 (f y0)); trivial. + elim H2 using eq_ind_r; trivial. + Qed. - Lemma ACC_inverse_image : (x:A)(ACC B R (f x)) -> (ACC A Rof x). - Intros; Apply (ACC_lemma (f x)); Trivial. - Save. + Lemma ACC_inverse_image : forall x : A, ACC B R (f x) -> ACC A Rof x. + intros; apply (ACC_lemma (f x)); trivial. + Qed. - Lemma WF_inverse_image: (WF B R)->(WF A Rof). - Red; Intros; Apply ACC_inverse_image; Auto. - Save. + Lemma WF_inverse_image : WF B R -> WF A Rof. + red in |- *; intros; apply ACC_inverse_image; auto. + Qed. End Inverse_Image. @@ -44,8 +47,9 @@ End Inverse_Image. Section Burali_Forti_Paradox. - Definition morphism := [A:Type][R:A->A->Prop][B:Type][S:B->B->Prop][f:A->B] - (x,y:A)(R x y)->(S (f x) (f y)). + Definition morphism (A : Type) (R : A -> A -> Prop) + (B : Type) (S : B -> B -> Prop) (f : A -> B) := + forall x y : A, R x y -> S (f x) (f y). (* The hypothesis of the paradox: assumes there exists an universal system of notations, i.e: @@ -53,120 +57,125 @@ Section Burali_Forti_Paradox. - An injection i0 from relations on any type into A0 - The proof that i0 is injective modulo morphism *) - Variable A0 : Type. (* Type_i *) - Variable i0 : (X:Type)(X->X->Prop)->A0. (* X: Type_j *) - Hypothesis inj : (X1:Type)(R1:X1->X1->Prop)(X2:Type)(R2:X2->X2->Prop) - (i0 X1 R1)==(i0 X2 R2) - ->(EXT f:X1->X2 | (morphism X1 R1 X2 R2 f)). + Variable A0 : Type. (* Type_i *) + Variable i0 : forall X : Type, (X -> X -> Prop) -> A0. (* X: Type_j *) + Hypothesis + inj : + forall (X1 : Type) (R1 : X1 -> X1 -> Prop) (X2 : Type) + (R2 : X2 -> X2 -> Prop), + i0 X1 R1 = i0 X2 R2 -> exists f : X1 -> X2, morphism X1 R1 X2 R2 f. (* Embedding of x in y: x and y are images of 2 well founded relations R1 and R2, the ordinal of R2 being strictly greater than that of R1. *) - Record emb [x,y:A0]: Prop := { - X1: Type; - R1: X1->X1->Prop; - eqx: x==(i0 X1 R1); - X2: Type; - R2: X2->X2->Prop; - eqy: y==(i0 X2 R2); - W2: (WF X2 R2); - f: X1->X2; - fmorph: (morphism X1 R1 X2 R2 f); - maj: X2; - majf: (z:X1)(R2 (f z) maj) }. - - - Lemma emb_trans: (x,y,z:A0)(emb x y)->(emb y z)->(emb x z). -Intros. -Case H; Intros. -Case H0; Intros. -Generalize eqx0; Clear eqx0. -Elim eqy using eqT_ind_r; Intro. -Case (inj ? ? ? ? eqx0); Intros. -Exists X1 R1 X3 R3 [x:X1](f0 (x0 (f x))) maj0; Trivial. -Red; Auto. + Record emb (x y : A0) : Prop := + {X1 : Type; + R1 : X1 -> X1 -> Prop; + eqx : x = i0 X1 R1; + X2 : Type; + R2 : X2 -> X2 -> Prop; + eqy : y = i0 X2 R2; + W2 : WF X2 R2; + f : X1 -> X2; + fmorph : morphism X1 R1 X2 R2 f; + maj : X2; + majf : forall z : X1, R2 (f z) maj}. + + + Lemma emb_trans : forall x y z : A0, emb x y -> emb y z -> emb x z. +intros. +case H; intros. +case H0; intros. +generalize eqx0; clear eqx0. +elim eqy using eq_ind_r; intro. +case (inj _ _ _ _ eqx0); intros. +exists X1 R1 X3 R3 (fun x : X1 => f0 (x0 (f x))) maj0; trivial. +red in |- *; auto. Defined. - Lemma ACC_emb: (X:Type)(R:X->X->Prop)(x:X)(ACC X R x) - ->(Y:Type)(S:Y->Y->Prop)(f:Y->X)(morphism Y S X R f) - ->((y:Y)(R (f y) x)) - ->(ACC A0 emb (i0 Y S)). -Induction 1; Intros. -Constructor; Intros. -Case H4; Intros. -Elim eqx using eqT_ind_r. -Case (inj X2 R2 Y S). -Apply sym_eqT; Assumption. - -Intros. -Apply H1 with y:=(f (x1 maj)) f:=[x:X1](f (x1 (f0 x))); Try Red; Auto. + Lemma ACC_emb : + forall (X : Type) (R : X -> X -> Prop) (x : X), + ACC X R x -> + forall (Y : Type) (S : Y -> Y -> Prop) (f : Y -> X), + morphism Y S X R f -> (forall y : Y, R (f y) x) -> ACC A0 emb (i0 Y S). +simple induction 1; intros. +constructor; intros. +case H4; intros. +elim eqx using eq_ind_r. +case (inj X2 R2 Y S). +apply sym_eq; assumption. + +intros. +apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x))); + try red in |- *; auto. Defined. (* The embedding relation is well founded *) - Lemma WF_emb: (WF A0 emb). -Constructor; Intros. -Case H; Intros. -Elim eqx using eqT_ind_r. -Apply ACC_emb with X:=X2 R:=R2 x:=maj f:=f; Trivial. + Lemma WF_emb : WF A0 emb. +constructor; intros. +case H; intros. +elim eqx using eq_ind_r. +apply ACC_emb with (X := X2) (R := R2) (x := maj) (f := f); trivial. Defined. (* The following definition enforces Type_j >= Type_i *) - Definition Omega: A0 := (i0 A0 emb). + Definition Omega : A0 := i0 A0 emb. Section Subsets. - Variable a: A0. + Variable a : A0. (* We define the type of elements of A0 smaller than a w.r.t embedding. The Record is in Type, but it is possible to avoid such structure. *) - Record sub: Type := { - witness : A0; - emb_wit : (emb witness a) }. + Record sub : Type := {witness : A0; emb_wit : emb witness a}. (* F is its image through i0 *) - Definition F : A0 := (i0 sub (Rof ? ? emb witness)). + Definition F : A0 := i0 sub (Rof _ _ emb witness). (* F is embedded in Omega: - the witness projection is a morphism - a is an upper bound because emb_wit proves that witness is smaller than a. *) - Lemma F_emb_Omega: (emb F Omega). -Exists sub (Rof ? ? emb witness) A0 emb witness a; Trivial. -Exact WF_emb. + Lemma F_emb_Omega : emb F Omega. +exists sub (Rof _ _ emb witness) A0 emb witness a; trivial. +exact WF_emb. -Red; Trivial. +red in |- *; trivial. -Exact emb_wit. +exact emb_wit. Defined. End Subsets. - Definition fsub: (a,b:A0)(emb a b)->(sub a)->(sub b):= - [_,_][H][x] - (Build_sub ? (witness ? x) (emb_trans ? ? ? (emb_wit ? x) H)). + Definition fsub (a b : A0) (H : emb a b) (x : sub a) : + sub b := Build_sub _ (witness _ x) (emb_trans _ _ _ (emb_wit _ x) H). (* F is a morphism: a < b => F(a) < F(b) - the morphism from F(a) to F(b) is fsub above - the upper bound is a, which is in F(b) since a < b *) - Lemma F_morphism: (morphism A0 emb A0 emb F). -Red; Intros. -Exists (sub x) (Rof ? ? emb (witness x)) (sub y) - (Rof ? ? emb (witness y)) (fsub x y H) (Build_sub ? x H); -Trivial. -Apply WF_inverse_image. -Exact WF_emb. - -Unfold morphism Rof fsub; Simpl; Intros. -Trivial. - -Unfold Rof fsub; Simpl; Intros. -Apply emb_wit. + Lemma F_morphism : morphism A0 emb A0 emb F. +red in |- *; intros. +exists + (sub x) + (Rof _ _ emb (witness x)) + (sub y) + (Rof _ _ emb (witness y)) + (fsub x y H) + (Build_sub _ x H); trivial. +apply WF_inverse_image. +exact WF_emb. + +unfold morphism, Rof, fsub in |- *; simpl in |- *; intros. +trivial. + +unfold Rof, fsub in |- *; simpl in |- *; intros. +apply emb_wit. Defined. @@ -174,23 +183,23 @@ Defined. - F is a morphism - Omega is an upper bound of the image of F *) - Lemma Omega_refl: (emb Omega Omega). -Exists A0 emb A0 emb F Omega; Trivial. -Exact WF_emb. + Lemma Omega_refl : emb Omega Omega. +exists A0 emb A0 emb F Omega; trivial. +exact WF_emb. -Exact F_morphism. +exact F_morphism. -Exact F_emb_Omega. +exact F_emb_Omega. Defined. (* The paradox is that Omega cannot be embedded in itself, since the embedding relation is well founded. *) - Theorem Burali_Forti: False. -Apply ACC_nonreflexive with A0 emb Omega. -Apply WF_emb. + Theorem Burali_Forti : False. +apply ACC_nonreflexive with A0 emb Omega. +apply WF_emb. -Exact Omega_refl. +exact Omega_refl. Defined. @@ -200,21 +209,23 @@ End Burali_Forti_Paradox. (* The following type seems to satisfy the hypothesis of the paradox. But it does not! *) - Record A0: Type := (* Type_i' *) - i0 { X0: Type; R0: X0->X0->Prop }. (* X0: Type_j' *) + Record A0 : Type := (* Type_i' *) + i0 {X0 : Type; R0 : X0 -> X0 -> Prop}. (* X0: Type_j' *) (* Note: this proof uses a large elimination of A0. *) - Lemma inj : (X1:Type)(R1:X1->X1->Prop)(X2:Type)(R2:X2->X2->Prop) - (i0 X1 R1)==(i0 X2 R2) - ->(EXT f:X1->X2 | (morphism X1 R1 X2 R2 f)). -Intros. -Change Cases (i0 X1 R1) (i0 X2 R2) of - (i0 x1 r1) (i0 x2 r2) => (EXT f | (morphism x1 r1 x2 r2 f)) - end. -Case H; Simpl. -Exists [x:X1]x. -Red; Trivial. + Lemma inj : + forall (X1 : Type) (R1 : X1 -> X1 -> Prop) (X2 : Type) + (R2 : X2 -> X2 -> Prop), + i0 X1 R1 = i0 X2 R2 -> exists f : X1 -> X2, morphism X1 R1 X2 R2 f. +intros. +change + match i0 X1 R1, i0 X2 R2 with + | i0 x1 r1, i0 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f + end in |- *. +case H; simpl in |- *. +exists (fun x : X1 => x). +red in |- *; trivial. Defined. (* The following command raises 'Error: Universe Inconsistency'. @@ -223,5 +234,4 @@ Defined. with the constraint j >= i in the paradox. *) - Definition Paradox: False := (Burali_Forti A0 i0 inj). - + Definition Paradox : False := Burali_Forti A0 i0 inj. |