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 + test-suite/output/rewrite-2172.out | 2 - test-suite/output/rewrite-2172.v | 21 -- test-suite/output/rewrite_2172.out | 2 + test-suite/output/rewrite_2172.v | 21 ++ test-suite/success/Cases-bug1834.v | 13 -- test-suite/success/Cases-bug3758.v | 17 -- test-suite/success/Cases_bug1834.v | 12 ++ test-suite/success/Cases_bug3758.v | 17 ++ test-suite/success/all-check.v | 3 - test-suite/success/all_check.v | 3 + test-suite/success/attribute-syntax.v | 33 --- test-suite/success/attribute_syntax.v | 33 +++ test-suite/success/dtauto-let-deps.v | 24 --- test-suite/success/dtauto_let_deps.v | 24 +++ test-suite/success/universes-coercion.v | 22 -- test-suite/success/universes_coercion.v | 22 ++ 28 files changed, 690 insertions(+), 691 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 delete mode 100644 test-suite/output/rewrite-2172.out delete mode 100644 test-suite/output/rewrite-2172.v create mode 100644 test-suite/output/rewrite_2172.out create mode 100644 test-suite/output/rewrite_2172.v delete mode 100644 test-suite/success/Cases-bug1834.v delete mode 100644 test-suite/success/Cases-bug3758.v create mode 100644 test-suite/success/Cases_bug1834.v create mode 100644 test-suite/success/Cases_bug3758.v delete mode 100644 test-suite/success/all-check.v create mode 100644 test-suite/success/all_check.v delete mode 100644 test-suite/success/attribute-syntax.v create mode 100644 test-suite/success/attribute_syntax.v delete mode 100644 test-suite/success/dtauto-let-deps.v create mode 100644 test-suite/success/dtauto_let_deps.v delete mode 100644 test-suite/success/universes-coercion.v create mode 100644 test-suite/success/universes_coercion.v (limited to 'test-suite') 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. diff --git a/test-suite/output/rewrite-2172.out b/test-suite/output/rewrite-2172.out deleted file mode 100644 index 27b0dc1b7b..0000000000 --- a/test-suite/output/rewrite-2172.out +++ /dev/null @@ -1,2 +0,0 @@ -The command has indeed failed with message: -Unable to find an instance for the variable E. diff --git a/test-suite/output/rewrite-2172.v b/test-suite/output/rewrite-2172.v deleted file mode 100644 index 212b1c1259..0000000000 --- a/test-suite/output/rewrite-2172.v +++ /dev/null @@ -1,21 +0,0 @@ -(* This checks an error message as reported in bug #2172 *) - -Axiom axiom : forall (E F : nat), E = F. -Lemma test : forall (E F : nat), E = F. -Proof. - intros. -(* This used to raise the following non understandable error message: - - Error: Unable to find an instance for the variable x - - The reason this error was that rewrite generated the proof - - "eq_ind ?A ?x ?P ? ?y (axiom ?E ?F)" - - and the equation ?x=?E was solved in the way ?E:=?x leaving ?x - unresolved. A stupid hack for solve this consisted in ordering - meta=meta equations the other way round (with most recent evars - instantiated first - since they are assumed to come first from the - user in rewrite/induction/destruct calls). -*) - Fail rewrite <- axiom. diff --git a/test-suite/output/rewrite_2172.out b/test-suite/output/rewrite_2172.out new file mode 100644 index 0000000000..27b0dc1b7b --- /dev/null +++ b/test-suite/output/rewrite_2172.out @@ -0,0 +1,2 @@ +The command has indeed failed with message: +Unable to find an instance for the variable E. diff --git a/test-suite/output/rewrite_2172.v b/test-suite/output/rewrite_2172.v new file mode 100644 index 0000000000..212b1c1259 --- /dev/null +++ b/test-suite/output/rewrite_2172.v @@ -0,0 +1,21 @@ +(* This checks an error message as reported in bug #2172 *) + +Axiom axiom : forall (E F : nat), E = F. +Lemma test : forall (E F : nat), E = F. +Proof. + intros. +(* This used to raise the following non understandable error message: + + Error: Unable to find an instance for the variable x + + The reason this error was that rewrite generated the proof + + "eq_ind ?A ?x ?P ? ?y (axiom ?E ?F)" + + and the equation ?x=?E was solved in the way ?E:=?x leaving ?x + unresolved. A stupid hack for solve this consisted in ordering + meta=meta equations the other way round (with most recent evars + instantiated first - since they are assumed to come first from the + user in rewrite/induction/destruct calls). +*) + Fail rewrite <- axiom. diff --git a/test-suite/success/Cases-bug1834.v b/test-suite/success/Cases-bug1834.v deleted file mode 100644 index cf102486a6..0000000000 --- a/test-suite/success/Cases-bug1834.v +++ /dev/null @@ -1,13 +0,0 @@ -(* Bug in the computation of generalization *) - -(* The following bug, elaborated by Bruno Barras, is solved from r11083 *) - -Parameter P : unit -> Prop. -Definition T := sig P. -Parameter Q : T -> Prop. -Definition U := sig Q. -Parameter a : U. -Check (match a with exist _ (exist _ tt e2) e3 => e3=e3 end). - -(* There is still a form submitted by Pierre Corbineau (#1834) which fails *) - diff --git a/test-suite/success/Cases-bug3758.v b/test-suite/success/Cases-bug3758.v deleted file mode 100644 index e48f452326..0000000000 --- a/test-suite/success/Cases-bug3758.v +++ /dev/null @@ -1,17 +0,0 @@ -(* There used to be an evar leak in the to_nat example *) - -Require Import Coq.Lists.List. -Import ListNotations. - -Fixpoint Idx {A:Type} (l:list A) : Type := - match l with - | [] => False - | _::l => True + Idx l - end. - -Fixpoint to_nat {A:Type} (l:list A) (i:Idx l) : nat := - match l,i with - | [] , i => match i with end - | _::_, inl _ => 0 - | _::l, inr i => S (to_nat l i) - end. diff --git a/test-suite/success/Cases_bug1834.v b/test-suite/success/Cases_bug1834.v new file mode 100644 index 0000000000..65372c2da4 --- /dev/null +++ b/test-suite/success/Cases_bug1834.v @@ -0,0 +1,12 @@ +(* Bug in the computation of generalization *) + +(* The following bug, elaborated by Bruno Barras, is solved from r11083 *) + +Parameter P : unit -> Prop. +Definition T := sig P. +Parameter Q : T -> Prop. +Definition U := sig Q. +Parameter a : U. +Check (match a with exist _ (exist _ tt e2) e3 => e3=e3 end). + +(* There is still a form submitted by Pierre Corbineau (#1834) which fails *) diff --git a/test-suite/success/Cases_bug3758.v b/test-suite/success/Cases_bug3758.v new file mode 100644 index 0000000000..e48f452326 --- /dev/null +++ b/test-suite/success/Cases_bug3758.v @@ -0,0 +1,17 @@ +(* There used to be an evar leak in the to_nat example *) + +Require Import Coq.Lists.List. +Import ListNotations. + +Fixpoint Idx {A:Type} (l:list A) : Type := + match l with + | [] => False + | _::l => True + Idx l + end. + +Fixpoint to_nat {A:Type} (l:list A) (i:Idx l) : nat := + match l,i with + | [] , i => match i with end + | _::_, inl _ => 0 + | _::l, inr i => S (to_nat l i) + end. diff --git a/test-suite/success/all-check.v b/test-suite/success/all-check.v deleted file mode 100644 index 391bc540e4..0000000000 --- a/test-suite/success/all-check.v +++ /dev/null @@ -1,3 +0,0 @@ -Goal True. -Fail all:Check _. -Abort. diff --git a/test-suite/success/all_check.v b/test-suite/success/all_check.v new file mode 100644 index 0000000000..391bc540e4 --- /dev/null +++ b/test-suite/success/all_check.v @@ -0,0 +1,3 @@ +Goal True. +Fail all:Check _. +Abort. diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v deleted file mode 100644 index 241d4eb200..0000000000 --- a/test-suite/success/attribute-syntax.v +++ /dev/null @@ -1,33 +0,0 @@ -From Coq Require Program.Wf. - -Section Scope. - -#[local] Coercion nat_of_bool (b: bool) : nat := - if b then 0 else 1. - -Check (refl_equal : true = 0 :> nat). - -End Scope. - -Fail Check 0 = true :> nat. - -#[polymorphic] -Definition ι T (x: T) := x. - -Check ι _ ι. - -#[program] -Fixpoint f (n: nat) {wf lt n} : nat := _. - -#[deprecated(since="8.9.0")] -Ltac foo := foo. - -Module M. - #[local] #[polymorphic] Definition zed := Type. - - #[local, polymorphic] Definition kats := Type. -End M. -Check M.zed@{_}. -Fail Check zed. -Check M.kats@{_}. -Fail Check kats. diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v new file mode 100644 index 0000000000..241d4eb200 --- /dev/null +++ b/test-suite/success/attribute_syntax.v @@ -0,0 +1,33 @@ +From Coq Require Program.Wf. + +Section Scope. + +#[local] Coercion nat_of_bool (b: bool) : nat := + if b then 0 else 1. + +Check (refl_equal : true = 0 :> nat). + +End Scope. + +Fail Check 0 = true :> nat. + +#[polymorphic] +Definition ι T (x: T) := x. + +Check ι _ ι. + +#[program] +Fixpoint f (n: nat) {wf lt n} : nat := _. + +#[deprecated(since="8.9.0")] +Ltac foo := foo. + +Module M. + #[local] #[polymorphic] Definition zed := Type. + + #[local, polymorphic] Definition kats := Type. +End M. +Check M.zed@{_}. +Fail Check zed. +Check M.kats@{_}. +Fail Check kats. diff --git a/test-suite/success/dtauto-let-deps.v b/test-suite/success/dtauto-let-deps.v deleted file mode 100644 index 094b2f8b3c..0000000000 --- a/test-suite/success/dtauto-let-deps.v +++ /dev/null @@ -1,24 +0,0 @@ -(* -This test is sensitive to changes in which let-ins are expanded when checking -for dependencies in constructors. -If the (x := X) is not reduced, Foo1 won't be recognized as a conjunction, -and if the (y := X) is reduced, Foo2 will be recognized as a conjunction. - -This tests the behavior of engine/termops.ml : prod_applist_assum, -which is currently specified to reduce exactly the parameters. - -If dtauto is changed to reduce lets in constructors before checking dependency, -this test will need to be changed. -*) - -Context (P Q : Type). -Inductive Foo1 (X : Type) (x := X) := foo1 : let y := X in P -> Q -> Foo1 x. -Inductive Foo2 (X : Type) (x := X) := foo2 : let y := X in P -> Q -> Foo2 y. - -Goal P -> Q -> Foo1 nat. -solve [dtauto]. -Qed. - -Goal P -> Q -> Foo2 nat. -Fail solve [dtauto]. -Abort. diff --git a/test-suite/success/dtauto_let_deps.v b/test-suite/success/dtauto_let_deps.v new file mode 100644 index 0000000000..094b2f8b3c --- /dev/null +++ b/test-suite/success/dtauto_let_deps.v @@ -0,0 +1,24 @@ +(* +This test is sensitive to changes in which let-ins are expanded when checking +for dependencies in constructors. +If the (x := X) is not reduced, Foo1 won't be recognized as a conjunction, +and if the (y := X) is reduced, Foo2 will be recognized as a conjunction. + +This tests the behavior of engine/termops.ml : prod_applist_assum, +which is currently specified to reduce exactly the parameters. + +If dtauto is changed to reduce lets in constructors before checking dependency, +this test will need to be changed. +*) + +Context (P Q : Type). +Inductive Foo1 (X : Type) (x := X) := foo1 : let y := X in P -> Q -> Foo1 x. +Inductive Foo2 (X : Type) (x := X) := foo2 : let y := X in P -> Q -> Foo2 y. + +Goal P -> Q -> Foo1 nat. +solve [dtauto]. +Qed. + +Goal P -> Q -> Foo2 nat. +Fail solve [dtauto]. +Abort. diff --git a/test-suite/success/universes-coercion.v b/test-suite/success/universes-coercion.v deleted file mode 100644 index d750434027..0000000000 --- a/test-suite/success/universes-coercion.v +++ /dev/null @@ -1,22 +0,0 @@ -(* This example used to emphasize the absence of LEGO-style universe - polymorphism; Matthieu's improvements of typing on 2011/3/11 now - makes (apparently) that Amokrane's automatic eta-expansion in the - coercion mechanism works; this makes its illustration as a "weakness" - of universe polymorphism obsolete (example submitted by Randy Pollack). - - Note that this example is not an evidence that the current - non-kernel eta-expansion behavior is the most expected one. -*) - -Parameter K : forall T : Type, T -> T. -Check (K (forall T : Type, T -> T) K). - -(* - note that the inferred term is - "(K (forall T (* u1 *) : Type, T -> T) (fun T:Type (* u1 *) => K T))" - which is not eta-equivalent to - "(K (forall T : Type, T -> T) K" - because the eta-expansion of the latter - "(K (forall T : Type, T -> T) (fun T:Type (* u2 *) => K T)" - assuming K of type "forall T (* u2 *) : Type, T -> T" -*) diff --git a/test-suite/success/universes_coercion.v b/test-suite/success/universes_coercion.v new file mode 100644 index 0000000000..272d3ec74a --- /dev/null +++ b/test-suite/success/universes_coercion.v @@ -0,0 +1,22 @@ +(* This example used to emphasize the absence of LEGO-style universe + polymorphism; Matthieu's improvements of typing on 2011/3/11 now + makes (apparently) that Amokrane's automatic eta-expansion in the + coercion mechanism works; this makes its illustration as a "weakness" + of universe polymorphism obsolete (example submitted by Randy Pollack). + + Note that this example is not an evidence that the current + non-kernel eta-expansion behavior is the most expected one. +*) + +Parameter K : forall T : Type, T -> T. +Check (K (forall T : Type, T -> T) K). + +(* + note that the inferred term is + "(K (forall T (* u1 *) : Type, T -> T) (fun T:Type (* u1 *) => K T))" + which is not eta-equivalent to + "(K (forall T : Type, T -> T) K" + because the eta-expansion of the latter + "(K (forall T : Type, T -> T) (fun T:Type (* u2 *) => K T)" + assuming K of type "forall T (* u2 *) : Type, T -> T" +*) -- cgit v1.2.3