diff options
Diffstat (limited to 'test-suite/failure/universes-buraliforti.v')
| -rw-r--r-- | test-suite/failure/universes-buraliforti.v | 227 |
1 files changed, 227 insertions, 0 deletions
diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v new file mode 100644 index 00000000..01d46133 --- /dev/null +++ b/test-suite/failure/universes-buraliforti.v @@ -0,0 +1,227 @@ +(* Check that Burali-Forti paradox does not go through *) + +(* Source: contrib/Rocq/PARADOX/{Logics,BuraliForti},v *) + +(* 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). + + 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. + + Definition WF := [A:Type][R:A->A->Prop](x:A)(ACC A R x). + + +Section Inverse_Image. + + Variables A,B:Type; R:B->B->Prop; f:A->B. + + Definition Rof : A->A->Prop := [x,y:A](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. + + Lemma ACC_inverse_image : (x:A)(ACC B R (f x)) -> (ACC A Rof x). + Intros; Apply (ACC_lemma (f x)); Trivial. + Save. + + Lemma WF_inverse_image: (WF B R)->(WF A Rof). + Red; Intros; Apply ACC_inverse_image; Auto. + Save. + +End Inverse_Image. + + +(* Remark: the paradox is written in Type, but also works in Prop or Set. *) + +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)). + + (* The hypothesis of the paradox: + assumes there exists an universal system of notations, i.e: + - A type A0 + - 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)). + + (* 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. +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. +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. +Defined. + + + (* The following definition enforces Type_j >= Type_i *) + Definition Omega: A0 := (i0 A0 emb). + + +Section Subsets. + + 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) }. + + (* F is its image through i0 *) + 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. + +Red; Trivial. + +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)). + + (* 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. +Defined. + + + (* Omega is embedded in itself: + - 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. + +Exact F_morphism. + +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. + +Exact Omega_refl. + +Defined. + +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' *) + + + (* 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. +Defined. + +(* The following command raises 'Error: Universe Inconsistency'. + To allow large elimination of A0, i0 must not be a large constructor. + Hence, the constraint Type_j' < Type_i' is added, which is incompatible + with the constraint j >= i in the paradox. +*) + + Definition Paradox: False := (Burali_Forti A0 i0 inj). + |