diff options
Diffstat (limited to 'test-suite')
37 files changed, 582 insertions, 66 deletions
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex e0324b0232..b3bcb5b056 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache diff --git a/test-suite/bugs/closed/bug_10757.v b/test-suite/bugs/closed/bug_10757.v new file mode 100644 index 0000000000..a531f6e563 --- /dev/null +++ b/test-suite/bugs/closed/bug_10757.v @@ -0,0 +1,38 @@ +Require Import Program Extraction ExtrOcamlBasic. +Print sig. +Section FIXPOINT. + +Variable A: Type. + +Variable eq: A -> A -> Prop. +Variable beq: A -> A -> bool. +Hypothesis beq_eq: forall x y, beq x y = true -> eq x y. +Hypothesis beq_neq: forall x y, beq x y = false -> ~eq x y. + +Variable le: A -> A -> Prop. +Hypothesis le_trans: forall x y z, le x y -> le y z -> le x z. + +Definition gt (x y: A) := le y x /\ ~eq y x. +Hypothesis gt_wf: well_founded gt. + +Variable F: A -> A. +Hypothesis F_mon: forall x y, le x y -> le (F x) (F y). + +Program Fixpoint iterate + (x: A) (PRE: le x (F x)) (SMALL: forall z, le (F z) z -> le x z) + {wf gt x} + : {y : A | eq y (F y) /\ forall z, le (F z) z -> le y z } := + let x' := F x in + match beq x x' with + | true => x + | false => iterate x' _ _ + end. +Next Obligation. + split. +- auto. +- apply beq_neq. auto. +Qed. + +End FIXPOINT. + +Recursive Extraction iterate. diff --git a/test-suite/bugs/closed/bug_3481.v b/test-suite/bugs/closed/bug_3481.v index 41e1a8e959..f54810d359 100644 --- a/test-suite/bugs/closed/bug_3481.v +++ b/test-suite/bugs/closed/bug_3481.v @@ -1,7 +1,6 @@ Set Implicit Arguments. -Require Import Logic. Module NonPrim. Local Set Nonrecursive Elimination Schemes. Record prodwithlet (A B : Type) : Type := diff --git a/test-suite/bugs/closed/bug_4498.v b/test-suite/bugs/closed/bug_4498.v index 9b3210860c..ba63b707af 100644 --- a/test-suite/bugs/closed/bug_4498.v +++ b/test-suite/bugs/closed/bug_4498.v @@ -1,6 +1,7 @@ Require Export Coq.Unicode.Utf8. Require Export Coq.Classes.Morphisms. Require Export Coq.Relations.Relation_Definitions. +Require Export Coq.Setoids.Setoid. Set Universe Polymorphism. @@ -17,8 +18,6 @@ Class Category := { Proper (@equiv B C ==> @equiv A B ==> @equiv A C) (@compose A B C); }. -Require Export Coq.Setoids.Setoid. - Add Parametric Morphism `{Category} {A B C} : (@compose _ A B C) with signature equiv ==> equiv ==> equiv as compose_mor. Proof. apply comp_respects. Qed. diff --git a/test-suite/bugs/closed/bug_9294.v b/test-suite/bugs/closed/bug_9294.v new file mode 100644 index 0000000000..a079d672d3 --- /dev/null +++ b/test-suite/bugs/closed/bug_9294.v @@ -0,0 +1,29 @@ +Set Printing Universes. + +Inductive Foo@{i} (A:Type@{i}) : Type := foo : (Set:Type@{i}) -> Foo A. +Arguments foo {_} _. +Print Universes Subgraph (Foo.i). +Definition bar : Foo True -> Set := fun '(foo x) => x. + +Definition foo_bar (n : Foo True) : foo (bar n) = n. +Proof. destruct n;reflexivity. Qed. + +Definition bar_foo (n : Set) : bar (foo n) = n. +Proof. reflexivity. Qed. + +Require Import Hurkens. + +Inductive box (A : Set) : Prop := Box : A -> box A. + +Definition Paradox : False. +Proof. +Fail unshelve refine ( + NoRetractFromSmallPropositionToProp.paradox + (Foo True) + (fun A => foo A) + (fun A => box (bar A)) + _ + _ + False +). +Abort. diff --git a/test-suite/coqchk/inductive_functor_template.v b/test-suite/coqchk/inductive_functor_template.v index bc5cd0fb68..4b6916af55 100644 --- a/test-suite/coqchk/inductive_functor_template.v +++ b/test-suite/coqchk/inductive_functor_template.v @@ -2,7 +2,7 @@ Module Type E. Parameter T : Type. End E. Module F (X:E). - #[universes(template)] Inductive foo := box : X.T -> foo. + Inductive foo := box : X.T -> foo. End F. Module ME. Definition T := nat. End ME. diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v new file mode 100644 index 0000000000..75b2a56169 --- /dev/null +++ b/test-suite/failure/Template.v @@ -0,0 +1,32 @@ +(* +Module TestUnsetTemplateCheck. + Unset Template Check. + + Section Foo. + + Context (A : Type). + + Definition cstr := nat : ltac:(let ty := type of A in exact ty). + + Inductive myind := + | cons : A -> myind. + End Foo. + + (* Can only succeed if no template check is performed *) + Check myind True : Prop. + + Print Assumptions myind. + (* + Axioms: + myind is template polymorphic on all its universe parameters. + *) + About myind. +(* +myind : Type@{Top.60} -> Type@{Top.60} + +myind is assumed template universe polymorphic on Top.60 +Argument scope is [type_scope] +Expands to: Inductive Top.TestUnsetTemplateCheck.myind +*) +End TestUnsetTemplateCheck. +*) diff --git a/test-suite/micromega/non_lin_ci.v b/test-suite/micromega/non_lin_ci.v index ec39209230..2a66cc9a5a 100644 --- a/test-suite/micromega/non_lin_ci.v +++ b/test-suite/micromega/non_lin_ci.v @@ -43,18 +43,18 @@ Proof. Qed. Goal - forall (__x1 __x2 __x3 __x4 __x5 __x6 __x7 __x8 __x9 __x10 __x11 __x12 __x13 - __x14 __x15 __x16 : Z) - (H6 : __x8 < __x10 ^ 2 * __x15 ^ 2 + 2 * __x10 * __x15 * __x14 + __x14 ^ 2) - (H7 : 0 <= __x8) - (H12 : 0 <= __x14) - (H0 : __x8 = __x15 * __x11 + __x9) - (H14 : __x10 ^ 2 * __x15 + __x10 * __x14 < __x16) - (H17 : __x16 <= 0) - (H15 : 0 <= __x9) - (H18 : __x9 < __x15) - (H16 : 0 <= __x12) - (H19 : __x12 < (__x10 * __x15 + __x14) * __x10) + forall (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 + x14 x15 x16 : Z) + (H6 : x8 < x10 ^ 2 * x15 ^ 2 + 2 * x10 * x15 * x14 + x14 ^ 2) + (H7 : 0 <= x8) + (H12 : 0 <= x14) + (H0 : x8 = x15 * x11 + x9) + (H14 : x10 ^ 2 * x15 + x10 * x14 < x16) + (H17 : x16 <= 0) + (H15 : 0 <= x9) + (H18 : x9 < x15) + (H16 : 0 <= x12) + (H19 : x12 < (x10 * x15 + x14) * x10) , False. Proof. intros. diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v index 52dc9ed2e0..354c608e23 100644 --- a/test-suite/micromega/rexample.v +++ b/test-suite/micromega/rexample.v @@ -24,6 +24,16 @@ Proof. lra. Qed. +Goal + forall (a c : R) + (Had : a <> a), + a > c. +Proof. + intros. + lra. +Qed. + + (* Other (simple) examples *) Lemma binomial : forall x y, ((x+y)^2 = x^2 + 2 *x*y + y^2). @@ -32,7 +42,6 @@ Proof. lra. Qed. - Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m. Proof. intros ; lra. diff --git a/test-suite/micromega/rsyntax.v b/test-suite/micromega/rsyntax.v index f02d93f911..a0afe99181 100644 --- a/test-suite/micromega/rsyntax.v +++ b/test-suite/micromega/rsyntax.v @@ -60,7 +60,6 @@ Proof. lia. (* exponent is a constant expr *) Qed. - Goal (1 / IZR (Z.pow_pos 10 25) = 1 / 10 ^ 25)%R. Proof. lra. diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v index 55691f553c..3d99af95ec 100644 --- a/test-suite/micromega/zomicron.v +++ b/test-suite/micromega/zomicron.v @@ -1,5 +1,63 @@ Require Import ZArith. Require Import Lia. + +Section S. + Variables H1 H2 H3 H4 : True. + + Lemma bug_9848 : True. + Proof using. + lia. + Qed. +End S. + +Lemma concl_in_Type : forall (k : nat) + (H : (k < 0)%nat) (F : k < 0 -> Type), + F H. +Proof. + intros. + lia. +Qed. + +Lemma bug_10707 : forall + (T : Type) + (t : nat -> Type) + (k : nat) + (default : T) + (arr : t 0 -> T) + (H : (k < 0)%nat) of_nat_lt, + match k with + | 0 | _ => default + end = arr (of_nat_lt H). +Proof. + intros. + lia. +Qed. + +Axiom decompose_nat : nat -> nat -> nat. +Axiom inleft : forall {P}, {m : nat & P m} -> nat. +Axiom foo : nat. + +Lemma bug_7886 : forall (x x0 : nat) + (e : 0 = x0 + S x) + (H : decompose_nat x 0 = inleft (existT (fun m : nat => 0 = m + S x) x0 e)) + (x1 : nat) + (e0 : 0 = x1 + S (S x)) + (H1 : decompose_nat (S x) 0 = inleft (existT (fun m : nat => 0 = m + S (S x)) x1 e0)), + False. +Proof. + intros. + lia. +Qed. + + +Lemma bug_8898 : forall (p : 0 < 0) (H: p = p), False. +Proof. + intros p H. + lia. +Qed. + + + Open Scope Z_scope. Lemma two_x_eq_1 : forall x, 2 * x = 1 -> False. @@ -34,12 +92,12 @@ Proof. Qed. Lemma compact_proof : forall z, - (z < 0) -> - (z >= 0) -> - (0 >= z \/ 0 < z) -> False. + (z < 0) -> + (z >= 0) -> + (0 >= z \/ 0 < z) -> False. Proof. - intros. - lia. + intros. + lia. Qed. Lemma dummy_ex : exists (x:Z), x = x. @@ -74,9 +132,17 @@ Proof. lia. Qed. + +Lemma fresh1 : forall (__p1 __p2 __p3 __p5:Prop) (x y z:Z), (x = 0 /\ y = 0) /\ z = 0 -> x = 0. +Proof. + intros. + lia. +Qed. + + Class Foo {x : Z} := { T : Type ; dec : T -> Z }. Goal forall bound {F : @Foo bound} (x y : T), 0 <= dec x < bound -> 0 <= dec y -< bound -> dec x + dec y >= bound -> dec x + dec y < 2 * bound. + < bound -> dec x + dec y >= bound -> dec x + dec y < 2 * bound. Proof. intros. lia. @@ -98,7 +164,19 @@ Section S. lia. Qed. - End S. +End S. + +Section S. + Variable x y: Z. + Variable H1 : 1 > 0 -> x = 1. + Variable H2 : x = y. + + Goal x = y. + Proof using H2. + lia. + Qed. + +End S. (* Bug 5073 *) Lemma opp_eq_0_iff a : -a = 0 <-> a = 0. @@ -122,8 +200,50 @@ Goal forall (H5 : - b < r) (H6 : r <= 0) (H2 : 0 <= b), - b = 0 -> False. + b = 0 -> False. Proof. intros b q r. lia. Qed. + + +Section S. + (* From bedrock2, used to be slow *) + Variables (x3 q r q2 r3 : Z) + (H : 2 ^ 2 <> 0 -> r3 + 3 = 2 ^ 2 * q + r) + (H0 : 0 < 2 ^ 2 -> 0 <= r < 2 ^ 2) + (H1 : 2 ^ 2 < 0 -> 2 ^ 2 < r <= 0) + (H2 : 2 ^ 2 = 0 -> q = 0) + (H3 : 2 ^ 2 = 0 -> r = 0) + (q0 r0 : Z) + (H4 : 4 <> 0 -> 0 = 4 * q0 + r0) + (H5 : 0 < 4 -> 0 <= r0 < 4) + (H6 : 4 < 0 -> 4 < r0 <= 0) + (H7 : 4 = 0 -> q0 = 0) + (H8 : 4 = 0 -> r0 = 0) + (q1 r1 : Z) + (H9 : 4 <> 0 -> q + q + (q + q) = 4 * q1 + r1) + (H10 : 0 < 4 -> 0 <= r1 < 4) + (H11 : 4 < 0 -> 4 < r1 <= 0) + (H12 : 4 = 0 -> q1 = 0) + (H13 : 4 = 0 -> r1 = 0) + (r2 : Z) + (H14 : 2 ^ 16 <> 0 -> x3 = 2 ^ 16 * q2 + r2) + (H15 : 0 < 2 ^ 16 -> 0 <= r2 < 2 ^ 16) + (H16 : 2 ^ 16 < 0 -> 2 ^ 16 < r2 <= 0) + (H17 : 2 ^ 16 = 0 -> q2 = 0) + (H18 : 2 ^ 16 = 0 -> r2 = 0) + (q3 : Z) + (H19 : 16383 + 1 <> 0 -> q2 = (16383 + 1) * q3 + r3) + (H20 : 0 < 16383 + 1 -> 0 <= r3 < 16383 + 1) + (H21 : 16383 + 1 < 0 -> 16383 + 1 < r3 <= 0) + (H22 : 16383 + 1 = 0 -> q3 = 0) + (H23 : 16383 + 1 = 0 -> r3 = 0). + + Goal r0 = r1. + Proof using H10 H9 H5 H4. + intros. + lia. + Qed. + +End S. diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 4e949dcb04..a040b69b44 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -84,7 +84,6 @@ Print f. (* Was enhancement request #5142 (error message reported on the most general return clause heuristic) *) -#[universes(template)] Inductive gadt : Type -> Type := | gadtNat : nat -> gadt nat | gadtTy : forall T, T -> gadt T. diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v index 6976f35a88..0e84bf3966 100644 --- a/test-suite/output/Coercions.v +++ b/test-suite/output/Coercions.v @@ -1,7 +1,7 @@ (* Submitted by Randy Pollack *) -#[universes(template)] Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. -#[universes(template)] Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. +Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. +Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. Section testSection. Variables (S : Set) (P : pred S) (R : rel S) (x : S). diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v index f9398fdca9..1ecd9771eb 100644 --- a/test-suite/output/Extraction_matchs_2413.v +++ b/test-suite/output/Extraction_matchs_2413.v @@ -101,7 +101,7 @@ Section decoder_result. Variable inst : Type. - #[universes(template)] Inductive decoder_result : Type := + Inductive decoder_result : Type := | DecUndefined : decoder_result | DecUnpredictable : decoder_result | DecInst : inst -> decoder_result diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 9b25c2dbd3..61ae4edbd1 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -44,7 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). omega. Qed. -#[universes(template)] CoInductive Inf := S { projS : Inf }. +CoInductive Inf := S { projS : Inf }. Definition expand_Inf (x : Inf) := S (projS x). CoFixpoint inf := S inf. Eval compute in inf. diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v index c0ef9b392d..668be1fdbc 100644 --- a/test-suite/output/MExtraction.v +++ b/test-suite/output/MExtraction.v @@ -1,14 +1,65 @@ -Require Import micromega.MExtraction. -Require Import RingMicromega. -Require Import QArith. -Require Import VarMap. +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(* *) +(* Micromega: A reflexive tactic using the Positivstellensatz *) +(* *) +(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* *) +(************************************************************************) + +(* Used to generate micromega.ml *) + +Require Extraction. Require Import ZMicromega. Require Import QMicromega. Require Import RMicromega. +Require Import VarMap. +Require Import RingMicromega. +Require Import NArith. +Require Import QArith. + +Extract Inductive prod => "( * )" [ "(,)" ]. +Extract Inductive list => list [ "[]" "(::)" ]. +Extract Inductive bool => bool [ true false ]. +Extract Inductive sumbool => bool [ true false ]. +Extract Inductive option => option [ Some None ]. +Extract Inductive sumor => option [ Some None ]. +(** Then, in a ternary alternative { }+{ }+{ }, + - leftmost choice (Inleft Left) is (Some true), + - middle choice (Inleft Right) is (Some false), + - rightmost choice (Inright) is (None) *) + + +(** To preserve its laziness, andb is normally expanded. + Let's rather use the ocaml && *) +Extract Inlined Constant andb => "(&&)". + +Import Reals.Rdefinitions. + +Extract Constant R => "int". +Extract Constant R0 => "0". +Extract Constant R1 => "1". +Extract Constant Rplus => "( + )". +Extract Constant Rmult => "( * )". +Extract Constant Ropp => "fun x -> - x". +Extract Constant Rinv => "fun x -> 1 / x". +(** In order to avoid annoying build dependencies the actual + extraction is only performed as a test in the test suite. *) Recursive Extraction -Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula - ZMicromega.cnfZ ZMicromega.Zeval_const ZMicromega.bound_problem_fr QMicromega.cnfQ + Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula + Tauto.abst_form + ZMicromega.cnfZ ZMicromega.bound_problem_fr ZMicromega.Zeval_const QMicromega.cnfQ List.map simpl_cone (*map_cone indexes*) denorm Qpower vm_add normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. +(* Local Variables: *) +(* coding: utf-8 *) +(* End: *) diff --git a/test-suite/output/NoAxiomFromR.out b/test-suite/output/NoAxiomFromR.out new file mode 100644 index 0000000000..7d7c521343 --- /dev/null +++ b/test-suite/output/NoAxiomFromR.out @@ -0,0 +1 @@ +Closed under the global context diff --git a/test-suite/output/NoAxiomFromR.v b/test-suite/output/NoAxiomFromR.v new file mode 100644 index 0000000000..9cf6879699 --- /dev/null +++ b/test-suite/output/NoAxiomFromR.v @@ -0,0 +1,10 @@ +Require Import Psatz. + +Inductive TT : Set := +| C : nat -> TT. + +Lemma lem4 : forall (n m : nat), +S m <= m -> C (S m) <> C n -> False. +Proof. firstorder. Qed. + +Print Assumptions lem4. diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 29614c032a..aeebc0f98b 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -123,7 +123,7 @@ Check fun n => foo4 n (fun x y z => (fun _ => y=0) z). (**********************************************************************) (* Test printing of #4932 *) -#[universes(template)] Inductive ftele : Type := +Inductive ftele : Type := | fb {T:Type} : T -> ftele | fr {T} : (T -> ftele) -> ftele. diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index 0c1b08f5a3..d671053c07 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -53,7 +53,7 @@ Module Suboptimal. (** This test shows an example which exposes the [let] introduced by the pattern notation in binders. *) -#[universes(template)] Inductive Fin (n:nat) := Z : Fin n. +Inductive Fin (n:nat) := Z : Fin n. Definition F '(n,p) : Type := (Fin n * Fin p)%type. Definition both_z '(n,p) : F (n,p) := (Z _,Z _). Print both_z. diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index ab4172711e..e788977fb7 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,6 +1,6 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} -existT is template universe polymorphic +existT is template universe polymorphic on sigT.u0 sigT.u1 Argument A is implicit Argument scopes are [type_scope function_scope _ _] Expands to: Constructor Coq.Init.Specif.existT diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v index 35f36e87d7..14d63d39c4 100644 --- a/test-suite/output/Projections.v +++ b/test-suite/output/Projections.v @@ -6,7 +6,7 @@ Class HostFunction := host_func : Type. Section store. Context `{HostFunction}. - #[universes(template)] Record store := { store_funcs : host_func }. + Record store := { store_funcs : host_func }. End store. Check (fun (S:@store nat) => S.(store_funcs)). diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index 4fe7b051f8..d9a649fadc 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -20,12 +20,12 @@ Check {| field := 5 |}. Check build_r 5. Check build_c 5. -#[universes(template)] Record N := C { T : Type; _ : True }. +Record N := C { T : Type; _ : True }. Check fun x:N => let 'C _ p := x in p. Check fun x:N => let 'C T _ := x in T. Check fun x:N => let 'C T p := x in (T,p). -#[universes(template)] Record M := D { U : Type; a := 0; q : True }. +Record M := D { U : Type; a := 0; q : True }. Check fun x:M => let 'D T _ p := x in p. Check fun x:M => let 'D T _ p := x in T. Check fun x:M => let 'D T p := x in (T,p). diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v index 99183f2064..9cf6ad35b8 100644 --- a/test-suite/output/ShowMatch.v +++ b/test-suite/output/ShowMatch.v @@ -3,12 +3,12 @@ *) Module A. - #[universes(template)] Inductive foo := f. + Inductive foo := f. Show Match foo. (* no need to disambiguate *) End A. Module B. - #[universes(template)] Inductive foo := f. + Inductive foo := f. (* local foo shadows A.foo, so constructor "f" needs disambiguation *) Show Match A.foo. End B. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 222a808768..a89fd64999 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -68,9 +68,9 @@ mono The command has indeed failed with message: Universe u already exists. bobmorane = -let tt := Type@{UnivBinders.32} in -let ff := Type@{UnivBinders.34} in tt -> ff - : Type@{max(UnivBinders.31,UnivBinders.33)} +let tt := Type@{UnivBinders.33} in +let ff := Type@{UnivBinders.35} in tt -> ff + : Type@{max(UnivBinders.32,UnivBinders.34)} The command has indeed failed with message: Universe u already bound. foo@{E M N} = @@ -143,16 +143,16 @@ Applied.infunct@{u v} = inmod@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) -axfoo@{i UnivBinders.56 UnivBinders.57} : -Type@{UnivBinders.56} -> Type@{i} -(* i UnivBinders.56 UnivBinders.57 |= *) +axfoo@{i UnivBinders.57 UnivBinders.58} : +Type@{UnivBinders.57} -> Type@{i} +(* i UnivBinders.57 UnivBinders.58 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo -axbar@{i UnivBinders.56 UnivBinders.57} : -Type@{UnivBinders.57} -> Type@{i} -(* i UnivBinders.56 UnivBinders.57 |= *) +axbar@{i UnivBinders.57 UnivBinders.58} : +Type@{UnivBinders.58} -> Type@{i} +(* i UnivBinders.57 UnivBinders.58 |= *) axbar is universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v index 0eb5db1733..7465442cab 100644 --- a/test-suite/output/Warnings.v +++ b/test-suite/output/Warnings.v @@ -1,5 +1,5 @@ (* Term in warning was not printed in the right environment at some time *) -#[universes(template)] Record A := { B:Type; b:B->B }. +Record A := { B:Type; b:B->B }. Definition a B := {| B:=B; b:=fun x => x |}. Canonical Structure a. diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out index 2761b87b02..5e81b43504 100644 --- a/test-suite/output/auto.out +++ b/test-suite/output/auto.out @@ -2,18 +2,18 @@ simple apply or_intror (in core). intro. assumption. -Debug: (* debug auto: *) -Debug: * assumption. (*fail*) -Debug: * intro. (*fail*) -Debug: * simple apply or_intror (in core). (*success*) -Debug: ** assumption. (*fail*) -Debug: ** intro. (*success*) -Debug: ** assumption. (*success*) +(* debug auto: *) +* assumption. (*fail*) +* intro. (*fail*) +* simple apply or_intror (in core). (*success*) +** assumption. (*fail*) +** intro. (*success*) +** assumption. (*success*) (* info eauto: *) simple apply or_intror. intro. exact H. -Debug: (* debug eauto: *) +(* debug eauto: *) Debug: 1 depth=5 Debug: 1.1 depth=4 simple apply or_intror Debug: 1.1.1 depth=4 intro diff --git a/test-suite/output/bug7191.out b/test-suite/output/bug7191.out new file mode 100644 index 0000000000..005455e30c --- /dev/null +++ b/test-suite/output/bug7191.out @@ -0,0 +1,9 @@ + +type unit0 = +| Tt + +(** val f : unit0 -> unit0 **) + +let f _ = + assert false (* absurd case *) + diff --git a/test-suite/output/bug7191.v b/test-suite/output/bug7191.v new file mode 100644 index 0000000000..1aa4625b6c --- /dev/null +++ b/test-suite/output/bug7191.v @@ -0,0 +1,3 @@ +Require Extraction. +Definition f (x : False) : unit -> unit := match x with end. +Recursive Extraction f. diff --git a/test-suite/output/bug7348.out b/test-suite/output/bug7348.out new file mode 100644 index 0000000000..325ee95ae2 --- /dev/null +++ b/test-suite/output/bug7348.out @@ -0,0 +1,45 @@ +Extracted code successfully compiled + +type __ = Obj.t + +type unit0 = +| Tt + +type bool = +| True +| False + +module Case1 = + struct + type coq_rec = { f : bool } + + (** val f : bool -> coq_rec -> bool **) + + let f _ r = + r.f + + (** val silly : bool -> coq_rec -> __ **) + + let silly x b = + match x with + | True -> Obj.magic b.f + | False -> Obj.magic Tt + end + +module Case2 = + struct + type coq_rec = { f : (bool -> bool) } + + (** val f : bool -> coq_rec -> bool -> bool **) + + let f _ r = + r.f + + (** val silly : bool -> coq_rec -> __ **) + + let silly x b = + match x with + | True -> Obj.magic b.f False + | False -> Obj.magic Tt + end + diff --git a/test-suite/output/bug7348.v b/test-suite/output/bug7348.v new file mode 100644 index 0000000000..782b27ce96 --- /dev/null +++ b/test-suite/output/bug7348.v @@ -0,0 +1,25 @@ +Require Extraction. + +Extraction Language OCaml. +Set Extraction KeepSingleton. + +Module Case1. + +Record rec (x : bool) := { f : bool }. + +Definition silly x (b : rec x) := + if x return (if x then bool else unit) then f x b else tt. + +End Case1. + +Module Case2. + +Record rec (x : bool) := { f : bool -> bool }. + +Definition silly x (b : rec x) := + if x return (if x then bool else unit) then f x b false else tt. + +End Case2. + +Extraction TestCompile Case1.silly Case2.silly. +Recursive Extraction Case1.silly Case2.silly. diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index 209fedc343..57a4739e9f 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -21,6 +21,6 @@ Print P. (* Note: exact numbers of evars are not important... *) -#[universes(template)] Inductive T (n:nat) : Type := A : T n. +Inductive T (n:nat) : Type := A : T n. Check fun n (y:=A n:T n) => _ _ : T n. Check fun n => _ _ : T n. diff --git a/test-suite/ssr/bang_rewrite.v b/test-suite/ssr/bang_rewrite.v new file mode 100644 index 0000000000..30e6d57a7a --- /dev/null +++ b/test-suite/ssr/bang_rewrite.v @@ -0,0 +1,13 @@ +Set Universe Polymorphism. + +Require Import ssreflect. + +Axiom mult@{i} : nat -> nat -> nat. +Notation "m * n" := (mult m n). + +Axiom multA : forall a b c, (a * b) * c = a * (b * c). + +(* Previously the following gave a universe error: *) + +Lemma multAA a b c d : ((a * b) * c) * d = a * (b * (c * d)). +Proof. by rewrite !multA. Qed. diff --git a/test-suite/ssr/congr.v b/test-suite/ssr/congr.v index 026f7538e8..f85791b00b 100644 --- a/test-suite/ssr/congr.v +++ b/test-suite/ssr/congr.v @@ -32,3 +32,11 @@ Coercion f : nat >-> Equality.sort. Lemma test4 : forall a b : nat, b = a -> @eq S (b + b) (a + a). Proof. move=> a b Eba; congr (_ + _); exact: Eba. Qed. + +Open Scope type_scope. + +Lemma test5 : forall (P Q Q' : Type) (h : Q = Q'), P * Q = P * Q'. +Proof. move=>*; by congr (_ * _). Qed. + +Lemma test6 : forall (P Q Q' : Type) (h : Q = Q'), P * Q -> P * Q'. +Proof. move=> P Q Q' h; by congr (_ * _). Qed. diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v index 62ecece792..2eac9660b4 100644 --- a/test-suite/success/Nia.v +++ b/test-suite/success/Nia.v @@ -4,7 +4,8 @@ Open Scope Z_scope. (** Add [Z.to_euclidean_division_equations] to the end of [zify], just for this file. *) -Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.to_euclidean_division_equations. +Require Zify. +Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations. Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed. Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed. diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v index e38affd7fa..381fbabe72 100644 --- a/test-suite/success/Nsatz.v +++ b/test-suite/success/Nsatz.v @@ -58,8 +58,8 @@ Section Geometry. https://docs.google.com/fileview?id=0ByhB3nPmbnjTYzFiZmIyNGMtYTkwNC00NWFiLWJiNzEtODM4NmVkYTc2NTVk&hl=fr *) -Require Import List. Require Import Reals. +Require Import List. Record point:Type:={ X:R; diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v index cfc25c3346..656362b8fc 100644 --- a/test-suite/success/Template.v +++ b/test-suite/success/Template.v @@ -46,3 +46,129 @@ Module No. Definition j_lebox (A:Type@{j}) := Box A. Fail Definition box_lti A := Box A : Type@{i}. End No. + +Module DefaultProp. + Inductive identity (A : Type) (a : A) : A -> Type := id_refl : identity A a a. + + (* By default template polymorphism does not interact with inductives + which naturally fall in Prop *) + Check (identity nat 0 0 : Prop). +End DefaultProp. + +Module ExplicitTemplate. + #[universes(template)] + Inductive identity@{i} (A : Type@{i}) (a : A) : A -> Type@{i} := id_refl : identity A a a. + + (* Weird interaction of template polymorphism and inductive types + which naturally fall in Prop: this one is template polymorphic but not on i: + it just lives in any universe *) + Check (identity Type nat nat : Prop). +End ExplicitTemplate. + +Polymorphic Definition f@{i} : Type@{i} := nat. +Polymorphic Definition baz@{i} : Type@{i} -> Type@{i} := fun x => x. + +Section Foo. + Universe u. + Context (A : Type@{u}). + + Inductive Bar := + | bar : A -> Bar. + + Set Universe Minimization ToSet. + Inductive Baz := + | cbaz : A -> baz Baz -> Baz. + + Inductive Baz' := + | cbaz' : A -> baz@{Set} nat -> Baz'. + + (* 2 constructors, at least in Set *) + Inductive Bazset@{v} := + | cbaz1 : A -> baz@{v} Bazset -> Bazset + | cbaz2 : Bazset. + + Eval compute in ltac:(let T := type of A in exact T). + + Inductive Foo : Type := + | foo : A -> f -> Foo. + +End Foo. + +Set Printing Universes. +(* Cannot fall back to Prop or Set anymore as baz is no longer template-polymorphic *) +Fail Check Bar True : Prop. +Fail Check Bar nat : Set. +About Baz. + +Check cbaz True I. + +(** Neither can it be Set *) +Fail Check Baz nat : Set. + +(** No longer possible for Baz' which contains a type in Set *) +Fail Check Baz' True : Prop. +Fail Check Baz' nat : Set. + +Fail Check Bazset True : Prop. +Fail Check Bazset True : Set. + +(** We can force the universe instantiated in [baz Bazset] to be [u], so Bazset lives in max(Set, u). *) +Constraint u = Bazset.v. +(** As u is global it is already > Set, so: *) +Definition bazsetex@{i | i < u} : Type@{u} := Bazset Type@{i}. + +(* Bazset is closed for universes u = u0, cannot be instantiated with Prop *) +Definition bazseetpar (X : Type@{u}) : Type@{u} := Bazset X. + +(** Would otherwise break singleton elimination and extraction. *) +Fail Check Foo True : Prop. +Fail Check Foo True : Set. + +Definition foo_proj {A} (f : Foo A) : nat := + match f with foo _ _ n => n end. + +Definition ex : Foo True := foo _ I 0. +Check foo_proj ex. + +(** See failure/Template.v for a test of the unsafe Unset Template Check usage *) + +Module AutoTemplateTest. +Set Warnings "+auto-template". +Section Foo. + Universe u'. + Context (A : Type@{u'}). + + (* Not failing as Bar cannot be made template polymorphic at all *) + Inductive Bar := + | bar : A -> Bar. +End Foo. +End AutoTemplateTest. + +Module TestTemplateAttribute. + Section Foo. + Universe u. + Context (A : Type@{u}). + + (* Failing as Bar cannot be made template polymorphic at all *) + Fail #[universes(template)] Inductive Bar := + | bar : A -> Bar. + + End Foo. +End TestTemplateAttribute. + +Module SharingWithoutSection. +Inductive Foo A (S:= fun _ => Set : ltac:(let ty := type of A in exact ty)) + := foo : S A -> Foo A. +Fail Check Foo True : Prop. +End SharingWithoutSection. + +Module OkNotCovered. +(* Here it happens that box is safe but we don't see it *) +Section S. +Universe u. +Variable A : Type@{u}. +Inductive box (A:Type@{u}) := Box : A -> box A. +Definition B := Set : Type@{u}. +End S. +Fail Check box True : Prop. +End OkNotCovered. |