From 1b06197525c2a3a5be8c6b20eef3227fa5ef3dc8 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Wed, 3 Oct 2018 07:21:53 +0000 Subject: test-suite: rename a few files --- test-suite/failure/guard-cofix.v | 43 ---- test-suite/failure/guard_cofix.v | 43 ++++ test-suite/failure/prop-set-proof-irrelevance.v | 12 -- test-suite/failure/prop_set_proof_irrelevance.v | 12 ++ test-suite/failure/universes-buraliforti-redef.v | 246 ----------------------- test-suite/failure/universes-buraliforti.v | 237 ---------------------- test-suite/failure/universes-sections1.v | 8 - test-suite/failure/universes-sections2.v | 10 - test-suite/failure/universes_buraliforti.v | 237 ++++++++++++++++++++++ test-suite/failure/universes_buraliforti_redef.v | 246 +++++++++++++++++++++++ test-suite/failure/universes_sections1.v | 8 + test-suite/failure/universes_sections2.v | 10 + 12 files changed, 556 insertions(+), 556 deletions(-) delete mode 100644 test-suite/failure/guard-cofix.v create mode 100644 test-suite/failure/guard_cofix.v delete mode 100644 test-suite/failure/prop-set-proof-irrelevance.v create mode 100644 test-suite/failure/prop_set_proof_irrelevance.v delete mode 100644 test-suite/failure/universes-buraliforti-redef.v delete mode 100644 test-suite/failure/universes-buraliforti.v delete mode 100644 test-suite/failure/universes-sections1.v delete mode 100644 test-suite/failure/universes-sections2.v create mode 100644 test-suite/failure/universes_buraliforti.v create mode 100644 test-suite/failure/universes_buraliforti_redef.v create mode 100644 test-suite/failure/universes_sections1.v create mode 100644 test-suite/failure/universes_sections2.v (limited to 'test-suite/failure') diff --git a/test-suite/failure/guard-cofix.v b/test-suite/failure/guard-cofix.v deleted file mode 100644 index 3ae8770546..0000000000 --- a/test-suite/failure/guard-cofix.v +++ /dev/null @@ -1,43 +0,0 @@ -(* This script shows, in two different ways, the inconsistency of the -propositional extensionality axiom with the guard condition for cofixpoints. It -is the dual of the problem on fixpoints (cf subterm.v, subterm2.v, -subterm3.v). Posted on Coq-club by Maxime Dénès (02/26/2014). *) - -(* First example *) - -CoInductive CoFalse : Prop := CF : CoFalse -> False -> CoFalse. - -CoInductive Pandora : Prop := C : CoFalse -> Pandora. - -Axiom prop_ext : forall P Q : Prop, (P<->Q) -> P = Q. - -Lemma foo : Pandora = CoFalse. -apply prop_ext. -constructor. -intro x; destruct x; assumption. -exact C. -Qed. - -Fail CoFixpoint loop : CoFalse := -match foo in (_ = T) return T with eq_refl => C loop end. - -Fail Definition ff : False := match loop with CF _ t => t end. - -(* Second example *) - -Inductive omega : Prop := Omega : omega -> omega. - -Lemma H : omega = CoFalse. -Proof. -apply prop_ext; constructor. - induction 1; assumption. -destruct 1; destruct H0. -Qed. - -Fail CoFixpoint loop' : CoFalse := - match H in _ = T return T with - eq_refl => - Omega match eq_sym H in _ = T return T with eq_refl => loop' end - end. - -Fail Definition ff' : False := match loop' with CF _ t => t end. diff --git a/test-suite/failure/guard_cofix.v b/test-suite/failure/guard_cofix.v new file mode 100644 index 0000000000..3ae8770546 --- /dev/null +++ b/test-suite/failure/guard_cofix.v @@ -0,0 +1,43 @@ +(* This script shows, in two different ways, the inconsistency of the +propositional extensionality axiom with the guard condition for cofixpoints. It +is the dual of the problem on fixpoints (cf subterm.v, subterm2.v, +subterm3.v). Posted on Coq-club by Maxime Dénès (02/26/2014). *) + +(* First example *) + +CoInductive CoFalse : Prop := CF : CoFalse -> False -> CoFalse. + +CoInductive Pandora : Prop := C : CoFalse -> Pandora. + +Axiom prop_ext : forall P Q : Prop, (P<->Q) -> P = Q. + +Lemma foo : Pandora = CoFalse. +apply prop_ext. +constructor. +intro x; destruct x; assumption. +exact C. +Qed. + +Fail CoFixpoint loop : CoFalse := +match foo in (_ = T) return T with eq_refl => C loop end. + +Fail Definition ff : False := match loop with CF _ t => t end. + +(* Second example *) + +Inductive omega : Prop := Omega : omega -> omega. + +Lemma H : omega = CoFalse. +Proof. +apply prop_ext; constructor. + induction 1; assumption. +destruct 1; destruct H0. +Qed. + +Fail CoFixpoint loop' : CoFalse := + match H in _ = T return T with + eq_refl => + Omega match eq_sym H in _ = T return T with eq_refl => loop' end + end. + +Fail Definition ff' : False := match loop' with CF _ t => t end. diff --git a/test-suite/failure/prop-set-proof-irrelevance.v b/test-suite/failure/prop-set-proof-irrelevance.v deleted file mode 100644 index fee33432b0..0000000000 --- a/test-suite/failure/prop-set-proof-irrelevance.v +++ /dev/null @@ -1,12 +0,0 @@ -Require Import ProofIrrelevance. - -Lemma proof_irrelevance_set : forall (P : Set) (p1 p2 : P), p1 = p2. - Fail exact proof_irrelevance. -(*Qed. - -Lemma paradox : False. - assert (H : 0 <> 1) by discriminate. - apply H. - Fail apply proof_irrelevance. (* inlined version is rejected *) - apply proof_irrelevance_set. -Qed.*) diff --git a/test-suite/failure/prop_set_proof_irrelevance.v b/test-suite/failure/prop_set_proof_irrelevance.v new file mode 100644 index 0000000000..fee33432b0 --- /dev/null +++ b/test-suite/failure/prop_set_proof_irrelevance.v @@ -0,0 +1,12 @@ +Require Import ProofIrrelevance. + +Lemma proof_irrelevance_set : forall (P : Set) (p1 p2 : P), p1 = p2. + Fail exact proof_irrelevance. +(*Qed. + +Lemma paradox : False. + assert (H : 0 <> 1) by discriminate. + apply H. + Fail apply proof_irrelevance. (* inlined version is rejected *) + apply proof_irrelevance_set. +Qed.*) diff --git a/test-suite/failure/universes-buraliforti-redef.v b/test-suite/failure/universes-buraliforti-redef.v deleted file mode 100644 index e016815880..0000000000 --- a/test-suite/failure/universes-buraliforti-redef.v +++ /dev/null @@ -1,246 +0,0 @@ -(* 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; 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; 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; 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; 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; 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. - - - (* 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. -case H; simpl. -exists (fun x : X1 => x). -red; trivial. -Defined. - -(* The following command should raise '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. -*) - - Fail Definition Paradox : False := Burali_Forti A0 i0 inj. diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v deleted file mode 100644 index dba1a794fa..0000000000 --- a/test-suite/failure/universes-buraliforti.v +++ /dev/null @@ -1,237 +0,0 @@ -(* 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 : - 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; 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. -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; 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; 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; 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; 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 : - 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. -case H; simpl. -exists (fun 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. -*) - - Fail Definition Paradox : False := Burali_Forti A0 i0 inj. diff --git a/test-suite/failure/universes-sections1.v b/test-suite/failure/universes-sections1.v deleted file mode 100644 index 3f8e444623..0000000000 --- a/test-suite/failure/universes-sections1.v +++ /dev/null @@ -1,8 +0,0 @@ -(* Check that constraints on definitions are preserved by discharging *) - -Section A. - Definition Type2 := Type. - Definition Type1 : Type2 := Type. -End A. - -Fail Definition Inconsistency : Type1 := Type2. diff --git a/test-suite/failure/universes-sections2.v b/test-suite/failure/universes-sections2.v deleted file mode 100644 index 34b2a11ded..0000000000 --- a/test-suite/failure/universes-sections2.v +++ /dev/null @@ -1,10 +0,0 @@ -(* Check that constraints on locals are preserved by discharging *) - -Definition Type2 := Type. - -Section A. - Let Type1 : Type2 := Type. - Definition Type1' := Type1. -End A. - -Fail Definition Inconsistency : Type1' := Type2. diff --git a/test-suite/failure/universes_buraliforti.v b/test-suite/failure/universes_buraliforti.v new file mode 100644 index 0000000000..dba1a794fa --- /dev/null +++ b/test-suite/failure/universes_buraliforti.v @@ -0,0 +1,237 @@ +(* 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 : + 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; 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. +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; 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; 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; 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; 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 : + 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. +case H; simpl. +exists (fun 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. +*) + + Fail Definition Paradox : False := Burali_Forti A0 i0 inj. diff --git a/test-suite/failure/universes_buraliforti_redef.v b/test-suite/failure/universes_buraliforti_redef.v new file mode 100644 index 0000000000..e016815880 --- /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; 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; 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; 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; 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; 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. + + + (* 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. +case H; simpl. +exists (fun x : X1 => x). +red; trivial. +Defined. + +(* The following command should raise '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. +*) + + Fail Definition Paradox : False := Burali_Forti A0 i0 inj. diff --git a/test-suite/failure/universes_sections1.v b/test-suite/failure/universes_sections1.v new file mode 100644 index 0000000000..3f8e444623 --- /dev/null +++ b/test-suite/failure/universes_sections1.v @@ -0,0 +1,8 @@ +(* Check that constraints on definitions are preserved by discharging *) + +Section A. + Definition Type2 := Type. + Definition Type1 : Type2 := Type. +End A. + +Fail Definition Inconsistency : Type1 := Type2. diff --git a/test-suite/failure/universes_sections2.v b/test-suite/failure/universes_sections2.v new file mode 100644 index 0000000000..34b2a11ded --- /dev/null +++ b/test-suite/failure/universes_sections2.v @@ -0,0 +1,10 @@ +(* Check that constraints on locals are preserved by discharging *) + +Definition Type2 := Type. + +Section A. + Let Type1 : Type2 := Type. + Definition Type1' := Type1. +End A. + +Fail Definition Inconsistency : Type1' := Type2. -- cgit v1.2.3 From 1e4ac27962aaab5132c9294156ac2a0da9652a43 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 2 Oct 2018 14:06:10 +0000 Subject: test-suite: cleaning --- test-suite/failure/ClearBody.v | 1 + test-suite/failure/Reordering.v | 1 + test-suite/failure/Sections.v | 2 ++ test-suite/failure/Tauto.v | 1 + test-suite/failure/autorewritein.v | 4 +--- test-suite/failure/clashes.v | 1 + test-suite/failure/coqbugs0266.v | 2 ++ test-suite/failure/evarclear1.v | 2 +- test-suite/failure/evarclear2.v | 1 + test-suite/failure/fixpoint2.v | 1 + test-suite/failure/ltac1.v | 1 + test-suite/failure/ltac2.v | 1 + test-suite/failure/ltac4.v | 2 +- test-suite/failure/pattern.v | 1 + test-suite/failure/prop_set_proof_irrelevance.v | 1 + test-suite/failure/rewrite_in_goal.v | 1 + test-suite/failure/rewrite_in_hyp.v | 1 + test-suite/failure/rewrite_in_hyp2.v | 1 + test-suite/failure/subtyping.v | 7 +++++++ 19 files changed, 27 insertions(+), 5 deletions(-) (limited to 'test-suite/failure') diff --git a/test-suite/failure/ClearBody.v b/test-suite/failure/ClearBody.v index e321e59f58..e865f121e8 100644 --- a/test-suite/failure/ClearBody.v +++ b/test-suite/failure/ClearBody.v @@ -6,3 +6,4 @@ set (n := 0) in *. set (I := refl_equal 0) in *. change (n = 0) in (type of I). Fail clearbody n. +Abort. diff --git a/test-suite/failure/Reordering.v b/test-suite/failure/Reordering.v index e79b20737b..75cf372b43 100644 --- a/test-suite/failure/Reordering.v +++ b/test-suite/failure/Reordering.v @@ -3,3 +3,4 @@ Goal forall (A:Set) (x:A) (A':=A), True. intros. Fail change ((fun (_:A') => Set) x) in (type of A). +Abort. diff --git a/test-suite/failure/Sections.v b/test-suite/failure/Sections.v index 928e214f47..815fadd8a5 100644 --- a/test-suite/failure/Sections.v +++ b/test-suite/failure/Sections.v @@ -2,3 +2,5 @@ Module A. Section B. Fail End A. (*End A.*) +End B. +End A. diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v index 81d5b6358e..c10cb0b869 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -20,3 +20,4 @@ Goal (forall A : Prop, A \/ ~ A) -> forall x y : nat, x = y \/ x <> y. Proof. Fail tauto. +Abort. diff --git a/test-suite/failure/autorewritein.v b/test-suite/failure/autorewritein.v index 191e035b3a..b734d85933 100644 --- a/test-suite/failure/autorewritein.v +++ b/test-suite/failure/autorewritein.v @@ -10,6 +10,4 @@ Lemma ResAck2 : forall H:(Ack 2 2 = 7 -> False), H=H -> False. Proof. intros. Fail autorewrite with base0 in * using try (apply H1;reflexivity). - - - +Abort. diff --git a/test-suite/failure/clashes.v b/test-suite/failure/clashes.v index 1a59ec66d1..1abec329c4 100644 --- a/test-suite/failure/clashes.v +++ b/test-suite/failure/clashes.v @@ -7,3 +7,4 @@ Section S. Variable n : nat. Fail Inductive P : Set := n : P. +End S. diff --git a/test-suite/failure/coqbugs0266.v b/test-suite/failure/coqbugs0266.v index cc3f307a20..79ea5ede47 100644 --- a/test-suite/failure/coqbugs0266.v +++ b/test-suite/failure/coqbugs0266.v @@ -5,3 +5,5 @@ Let a := 0. Definition b := a. Goal b = b. Fail clear a. +Abort. +End S. diff --git a/test-suite/failure/evarclear1.v b/test-suite/failure/evarclear1.v index 60adadef40..82697bf41e 100644 --- a/test-suite/failure/evarclear1.v +++ b/test-suite/failure/evarclear1.v @@ -7,4 +7,4 @@ unfold z. clear y z. (* should fail because the evar should no longer be allowed to depend on z *) Fail instantiate (1:=z). - +Abort. diff --git a/test-suite/failure/evarclear2.v b/test-suite/failure/evarclear2.v index 0f7768112b..45eeef6aa7 100644 --- a/test-suite/failure/evarclear2.v +++ b/test-suite/failure/evarclear2.v @@ -7,3 +7,4 @@ rename y into z. unfold z at 1 2. (* should fail because the evar type depends on z *) Fail clear z. +Abort. diff --git a/test-suite/failure/fixpoint2.v b/test-suite/failure/fixpoint2.v index 7f11a99b16..2d2d6a02cd 100644 --- a/test-suite/failure/fixpoint2.v +++ b/test-suite/failure/fixpoint2.v @@ -4,3 +4,4 @@ Goal nat->nat. fix f 1. intro n; apply f; assumption. Fail Guarded. +Abort. diff --git a/test-suite/failure/ltac1.v b/test-suite/failure/ltac1.v index eef16525d6..1cd119f3eb 100644 --- a/test-suite/failure/ltac1.v +++ b/test-suite/failure/ltac1.v @@ -5,3 +5,4 @@ Ltac X := match goal with Goal True -> True -> True. intros. Fail X. +Abort. diff --git a/test-suite/failure/ltac2.v b/test-suite/failure/ltac2.v index d66fb6808d..8a9157df84 100644 --- a/test-suite/failure/ltac2.v +++ b/test-suite/failure/ltac2.v @@ -4,3 +4,4 @@ Goal True -> True. Fail E ltac:(match goal with | |- _ => intro H end). +Abort. diff --git a/test-suite/failure/ltac4.v b/test-suite/failure/ltac4.v index 5b0396d164..58b791eb38 100644 --- a/test-suite/failure/ltac4.v +++ b/test-suite/failure/ltac4.v @@ -3,4 +3,4 @@ Goal forall n : nat, n = n. induction n. Fail try REflexivity. - +Abort. diff --git a/test-suite/failure/pattern.v b/test-suite/failure/pattern.v index 216eb254c1..480f579502 100644 --- a/test-suite/failure/pattern.v +++ b/test-suite/failure/pattern.v @@ -7,3 +7,4 @@ Variable P : forall m : nat, m = n -> Prop. Goal forall p : n = n, P n p. intro. Fail pattern n, p. +Abort. diff --git a/test-suite/failure/prop_set_proof_irrelevance.v b/test-suite/failure/prop_set_proof_irrelevance.v index fee33432b0..ed6d4300e0 100644 --- a/test-suite/failure/prop_set_proof_irrelevance.v +++ b/test-suite/failure/prop_set_proof_irrelevance.v @@ -10,3 +10,4 @@ Lemma paradox : False. Fail apply proof_irrelevance. (* inlined version is rejected *) apply proof_irrelevance_set. Qed.*) +Abort. diff --git a/test-suite/failure/rewrite_in_goal.v b/test-suite/failure/rewrite_in_goal.v index dedfdf01eb..e7823f1cb1 100644 --- a/test-suite/failure/rewrite_in_goal.v +++ b/test-suite/failure/rewrite_in_goal.v @@ -1,3 +1,4 @@ Goal forall T1 T2 (H:T1=T2) (f:T1->Prop) (x:T1) , f x -> Type. intros until x. Fail rewrite H in x. +Abort. diff --git a/test-suite/failure/rewrite_in_hyp.v b/test-suite/failure/rewrite_in_hyp.v index 1eef0fa033..f1b2203acc 100644 --- a/test-suite/failure/rewrite_in_hyp.v +++ b/test-suite/failure/rewrite_in_hyp.v @@ -1,3 +1,4 @@ Goal forall (T1 T2 : Type) (f:T1 -> Prop) (x:T1) (H:T1=T2), f x -> 0=1. intros T1 T2 f x H fx. Fail rewrite H in x. +Abort. diff --git a/test-suite/failure/rewrite_in_hyp2.v b/test-suite/failure/rewrite_in_hyp2.v index 112a856e32..60994fe1ed 100644 --- a/test-suite/failure/rewrite_in_hyp2.v +++ b/test-suite/failure/rewrite_in_hyp2.v @@ -6,3 +6,4 @@ Goal forall b, S b = O -> (fun a => 0 = (S a)) b -> True. intros b H H0. Fail rewrite H in H0. +Abort. diff --git a/test-suite/failure/subtyping.v b/test-suite/failure/subtyping.v index e48c668916..6996f4232a 100644 --- a/test-suite/failure/subtyping.v +++ b/test-suite/failure/subtyping.v @@ -19,3 +19,10 @@ Module TT : T. | L1 : (A -> Prop) -> L. Fail End TT. + + Reset L. + Inductive L : Prop := + | L0 + | L1 : (A -> Prop) -> L. + +End TT. -- cgit v1.2.3