diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/failure/universes-buraliforti-redef.v | 246 |
1 files changed, 246 insertions, 0 deletions
diff --git a/test-suite/failure/universes-buraliforti-redef.v b/test-suite/failure/universes-buraliforti-redef.v new file mode 100644 index 000000000..049f97f22 --- /dev/null +++ b/test-suite/failure/universes-buraliforti-redef.v @@ -0,0 +1,246 @@ +(* A variant of Burali-Forti that used to pass in V8.1beta, because of + a bug in the instantiation of sort-polymorphic inductive types *) + +(* The following type seems to satisfy the hypothesis of the paradox below *) +(* It should infer constraints forbidding the paradox to go through, but via *) +(* a redefinition that did not propagate constraints correctly in V8.1beta *) +(* it was exploitable to derive an inconsistency *) + +(* We keep the file as a non regression test of the bug *) + + Record A1 (B:Type) (g:B->Type) : Type := (* Type_i' *) + i1 {X0 : B; R0 : g X0 -> g X0 -> Prop}. (* X0: Type_j' *) + + Definition A2 := A1. (* here was the bug *) + + Definition A0 := (A2 Type (fun x => x)). + Definition i0 := (i1 Type (fun x => x)). + +(* The rest is as in universes-buraliforti.v *) + + +(* Some properties about relations on objects in Type *) + + 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 : + 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) := forall x : A, ACC A R x. + + +Section Inverse_Image. + + Variables (A B : Type) (R : B -> B -> Prop) (f : A -> B). + + Definition Rof (x y : A) : Prop := R (f x) (f y). + + 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 : 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 in |- *; intros; apply ACC_inverse_image; auto. + Qed. + +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) := + 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: + - 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 : 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 : 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 X1 R1 eqx X2 R2 eqy; intros. +case H0; intros X3 R3 eqx0 X4 R4 eqy0; intros. +generalize eqx0; clear eqx0. +elim eqy using eq_ind_r; intro. +case (inj _ _ _ _ eqx0); intros. +exists X1 R1 X4 R4 (fun x : X1 => f0 (x0 (f x))) maj0; trivial. +red in |- *; auto. +Defined. + + + 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 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. + + +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 in |- *; trivial. + +exact emb_wit. +Defined. + +End Subsets. + + + 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 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. + + + (* 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. + + + (* Note: this proof uses a large elimination of A0. *) + 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 + | i1 x1 r1, i1 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'. + 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. |