diff --git a/dev/ci/user-overlays/21865-SkySkimmer-warn-missing-proof.sh b/dev/ci/user-overlays/21865-SkySkimmer-warn-missing-proof.sh new file mode 100644 index 000000000000..97f52f04a86a --- /dev/null +++ b/dev/ci/user-overlays/21865-SkySkimmer-warn-missing-proof.sh @@ -0,0 +1,14 @@ +overlay bedrock2 https://github.com/SkySkimmer/bedrock2 warn-missing-proof 21865 +# Make PRs against https://github.com/mit-plv/bedrock2 base branch master + +overlay color https://github.com/SkySkimmer/color warn-missing-proof 21865 + +overlay corn https://github.com/SkySkimmer/corn warn-missing-proof 21865 + +overlay ext_lib https://github.com/SkySkimmer/coq-ext-lib warn-missing-proof 21865 + +overlay fcsl_pcm https://github.com/SkySkimmer/fcsl-pcm warn-missing-proof 21865 + +overlay menhirlib https://gitlab.inria.fr/ggilbert/menhir badproof 21865 + +overlay coquelicot https://gitlab.inria.fr/ggilbert/coquelicot badproof 21865 diff --git a/doc/changelog/08-vernac-commands-and-options/21865-warn-missing-proof-Added.rst b/doc/changelog/08-vernac-commands-and-options/21865-warn-missing-proof-Added.rst new file mode 100644 index 000000000000..39bf234415e0 --- /dev/null +++ b/doc/changelog/08-vernac-commands-and-options/21865-warn-missing-proof-Added.rst @@ -0,0 +1,4 @@ +- **Added:** + warning when an interactive proof is not started by :cmd:`Proof`, and error when :cmd:`Proof` is used multiple times or is used after a tactic has been used + (`#21865 `_, + by Gaëtan Gilbert). diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 0c6366c5dd7d..d89d5866ecaa 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -1235,12 +1235,14 @@ subterm selection choices. Set Printing Parentheses. Local Open Scope bool_scope. Goal forall a b c : bool, a && b && c = true. + Proof. rewrite_strat innermost andbC. .. rocqtop:: none Abort. Goal forall a b c : bool, a && b && c = true. + Proof. Using :n:`outermost` instead gives this result: diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 5a1ce2821722..f7462cc08c57 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -166,10 +166,12 @@ Concrete usage Goal forall a b c:Z, (a + b + c) ^ 2 = a * a + b ^ 2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c. + Proof. intros; ring. Abort. Goal forall a b:Z, 2 * a * b = 30 -> (a + b) ^ 2 = a ^ 2 + b ^ 2 + 30. + Proof. intros a b H; ring [H]. Abort. @@ -572,10 +574,12 @@ Dealing with fields Open Scope R_scope. Goal forall x, x <> 0 -> (1 - 1 / x) * x - x + 1 = 0. + Proof. intros; field; auto. Abort. Goal forall x y, y <> 0 -> y = x -> x / y = 1. + Proof. intros x y H H1; field [H1]; auto. Abort. @@ -589,6 +593,7 @@ Dealing with fields (x * y > 0)%R -> (x * (1 / x + x / (x + y)))%R = ((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R. + Proof. intros; field. @@ -723,6 +728,7 @@ for Coq’s type checker. Let us see why: Open Scope Z_scope. Goal forall x y z : Z, x + 3 + y + y * z = x + 3 + y + z * y. + Proof. intros; rewrite (Zmult_comm y z); reflexivity. Save foo. Print foo. diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 220935e33cad..6f176364be36 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -75,6 +75,7 @@ remaining fields, e.g.: .. rocqtop:: all Next Obligation. + Proof. destruct x ; destruct y ; (discriminate || reflexivity). Defined. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 0d14c1259ee1..671955f64fa5 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -838,6 +838,7 @@ witness these temporary variables. .. rocqtop:: in Goal True. + Proof. Set Printing Universes. .. rocqtop:: all abort diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst index e1b5ed9a2630..d7a038027d50 100644 --- a/doc/sphinx/language/core/conversion.rst +++ b/doc/sphinx/language/core/conversion.rst @@ -233,6 +233,7 @@ Examples Print Nat.add. Goal 1 + 1 = 2. + Proof. cbv delta. cbv fix. cbv beta. @@ -243,6 +244,7 @@ Examples .. rocqtop:: all abort Goal 1 + 1 = 2. + Proof. cbv. .. _proof-irrelevance: diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 393e5dc3b8a5..665e630eee9d 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -560,6 +560,7 @@ constructions. .. rocqtop:: all Goal forall n:nat, plus n 0 = plus 0 n. + Proof. intros; simpl. (* plus 0 n not reducible *) .. rocqtop:: none @@ -569,6 +570,7 @@ constructions. .. rocqtop:: all Goal forall n:nat, n + 0 = 0 + n. + Proof. intros; simpl. (* n + 0 not reducible *) .. rocqtop:: none diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 6af63eb29f3a..4f494559530f 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -405,6 +405,7 @@ Examples .. rocqtop:: all Definition y : bool. + Proof. exact true. .. rocqtop:: in @@ -452,6 +453,7 @@ module can be accessed using the dot notation: Definition T := nat. Definition x := 0. Definition y : bool. + Proof. exact true. Defined. End M. diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index 2c8978ba0370..b9c85f715f76 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -282,6 +282,7 @@ Constructing records .. rocqtop:: in Theorem one_two_irred : forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1. + Proof. Admitted. (* Record form: top and bottom can be inferred from other fields *) diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index c70a1a2d0e8b..b7da1c151fc3 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -425,6 +425,7 @@ structure. .. rocqtop:: all Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y. + Proof. now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. @@ -465,14 +466,14 @@ following proofs are omitted for brevity. .. rocqtop:: all Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m. - + Proof. Admitted. Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat. Lemma pair_LEQ_compat (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) : n <= m /\ m <= n <-> n == m. - + Proof. Admitted. Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2). @@ -498,13 +499,13 @@ subsection we show how to make them more compact. (pair_LEQmx l1 l2)). Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m. - + Proof. now apply (lele_eq n m). Qed. Example test_algebraic2 (n m : nat * nat) : n <= m -> m <= n -> n == m. - + Proof. now apply (lele_eq n m). Qed. End Add_instance_attempt. diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst index 85efe17b0915..a99cf3a0947b 100644 --- a/doc/sphinx/language/extensions/evars.rst +++ b/doc/sphinx/language/extensions/evars.rst @@ -113,6 +113,7 @@ it will create new existential variable(s) when :tacn:`apply` would fail. .. rocqtop:: none reset Goal forall i j : nat, i = j. + Proof. intros. .. rocqtop:: all @@ -178,6 +179,7 @@ automatically as a side effect of other tactics. Set Printing Goal Names. Goal forall p n m : nat, n = p -> p = m -> n = m. + Proof. .. rocqtop:: all @@ -197,6 +199,7 @@ automatically as a side effect of other tactics. Set Printing Goal Names. Goal forall p n m : nat, n = p -> p = m -> n = m. + Proof. intros x y z H1 H2. eapply eq_trans. (* creates ?y : nat as a shelved goal *) diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 311c4304bfdb..f88e0ad5775f 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -300,6 +300,7 @@ as a :token:`tactic_arg`. Local symbols are also substituted into tactics: .. rocqtop:: reset none Goal True. + Proof. .. rocqtop:: all @@ -475,6 +476,7 @@ Selectors can also be used nested within a tactic expression with the .. rocqtop:: reset in Goal 1=0 /\ 2=0 /\ 3=0. + Proof. .. rocqtop:: all @@ -496,6 +498,7 @@ separately. They succeed only if there is a success for each goal. For example .. rocqtop:: reset none fail Goal True /\ False. + Proof. .. rocqtop:: out @@ -702,6 +705,7 @@ We can branch with backtracking with the following structure: .. rocqtop:: reset none Goal True. + Proof. .. rocqtop:: all @@ -788,6 +792,7 @@ In some cases backtracking may be too expensive. .. rocqtop:: reset none Goal True. + Proof. The :tacn:`fail` doesn't trigger the second :tacn:`idtac`: @@ -812,6 +817,7 @@ In some cases backtracking may be too expensive. Tactic Notation "myfirst" "[" tactic_list_sep(tacl,"|") "]" := first tacl. Goal True. + Proof. myfirst [ auto | apply I ]. Solving @@ -899,6 +905,7 @@ Rocq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*: .. rocqtop:: reset none Goal True. + Proof. .. rocqtop:: all fail @@ -1210,6 +1217,7 @@ Pattern matching on terms: match .. rocqtop:: reset none Goal True. + Proof. .. rocqtop:: all @@ -1258,6 +1266,7 @@ Pattern matching on terms: match .. rocqtop:: in reset Goal True. + Proof. .. rocqtop:: all @@ -1279,6 +1288,7 @@ Pattern matching on terms: match | _ => idtac end. Goal True. + Proof. .. rocqtop:: all @@ -1390,6 +1400,7 @@ Examples: .. rocqtop:: reset all Goal forall A B : Prop, A -> B -> (A->B). + Proof. intros. match goal with | H : _ |- _ => idtac "apply " H; apply H @@ -1404,6 +1415,7 @@ Examples: .. rocqtop:: reset all Goal forall A B : Prop, A -> B -> (A->B). + Proof. intros. match reverse goal with | H : _ |- _ => idtac "apply " H; apply H @@ -1421,6 +1433,7 @@ Examples: .. rocqtop:: reset all Goal forall A B : Prop, A -> B -> (A->B). + Proof. intros A B H. match goal with | H1 : _, H2 : _ |- _ => idtac "match " H1 H2; fail @@ -1458,6 +1471,7 @@ produce subgoals but generates a term to be used in tactic expressions: .. rocqtop:: reset all Goal True /\ True. + Proof. match goal with | |- context G [True] => let x := context G [False] in idtac x end. @@ -1492,6 +1506,7 @@ expression returns an identifier: .. rocqtop:: reset none Goal True -> True. + Proof. .. rocqtop:: out @@ -1567,6 +1582,7 @@ Counting goals: numgoals Ltac pr_numgoals := let n := numgoals in idtac "There are" n "goals". Goal True /\ True /\ True. + Proof. split;[|split]. .. rocqtop:: all abort @@ -1601,6 +1617,7 @@ Testing boolean expressions: guard .. rocqtop:: in Goal True /\ True /\ True. + Proof. split;[|split]. .. rocqtop:: all @@ -1710,6 +1727,7 @@ succeeds, and results in an error otherwise. .. rocqtop:: reset in Goal True. + Proof. is_fix (fix f (n : nat) := match n with S n => f n | O => O end). .. tacn:: is_cofix @one_term @@ -1727,6 +1745,7 @@ succeeds, and results in an error otherwise. CoInductive Stream (A : Type) : Type := Cons : A -> Stream A -> Stream A. Goal True. + Proof. let c := constr:(cofix f : Stream unit := Cons _ tt f) in is_cofix c. @@ -1763,6 +1782,7 @@ succeeds, and results in an error otherwise. Record Box {T : Type} := box { unbox : T }. Arguments box {_} _. Goal True. + Proof. is_proj (unbox (box 0)). Timing @@ -1849,6 +1869,7 @@ different :token:`string` parameters to :tacn:`restart_timer` and ret. Goal True. + Proof. let v := time_constr ltac:(fun _ => let x := time_constr1 ltac:(fun _ => constr:(10 * 10)) in @@ -2088,6 +2109,7 @@ Proving that a list is a permutation of a second list .. rocqtop:: out Goal perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). + Proof. .. rocqtop:: all abort @@ -2098,6 +2120,7 @@ Proving that a list is a permutation of a second list Goal perm nat (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). + Proof. .. rocqtop:: all abort @@ -2378,6 +2401,7 @@ Tracing execution Ltac t x := exists x; reflexivity. Goal exists n, n=0. + Proof. .. rocqtop:: all diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index e5a5dae3406e..3a92b0e948fd 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -206,6 +206,7 @@ For example, `Message.print` defined in `Message.v` is used to print messages: .. rocqtop:: none Goal True. + Proof. .. rocqtop:: all abort @@ -976,6 +977,7 @@ one from Ltac1, except that it requires the goal to be focused. .. rocqtop:: none Goal True. + Proof. In :tacn:`lazy_match!`, if :token:`ltac2_expr` fails, the :tacn:`lazy_match!` fails; it doesn't look for further matches. In :tacn:`match!`, if :token:`ltac2_expr` fails @@ -1161,6 +1163,7 @@ Match over goals .. rocqtop:: all abort Goal forall A B : Prop, A -> B -> (A->B). + Proof. intros. match! goal with | [ h : _ |- _ ] => let h := Control.hyp h in print (of_constr h); apply $h @@ -1177,6 +1180,7 @@ Match over goals .. rocqtop:: all abort Goal forall A B : Prop, A -> B -> (A->B). + Proof. intros. match! reverse goal with | [ h : _ |- _ ] => let h := Control.hyp h in print (of_constr h); apply $h @@ -1196,6 +1200,7 @@ Match over goals .. rocqtop:: all abort Goal forall A B : Prop, A -> B -> (A->B). + Proof. intros A B H. match! goal with | [ h1 : _, h2 : _ |- _ ] => @@ -1316,6 +1321,7 @@ Notations .. rocqtop:: none Goal True. + Proof. .. rocqtop:: all @@ -2028,6 +2034,7 @@ It has the same typing rules as `ltac2:()` except the expression must have type f x. Goal True. + Proof. let z := constr:(0) in let v := add1 z in idtac v. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index a94a6d1cdd2d..6aed1c8a1f33 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -459,6 +459,7 @@ For example, the tactic :tacn:`pose (ssreflect)` supports parameters: .. rocqtop:: all Lemma test : True. + Proof. pose f x y := x + y. The |SSR| :tacn:`pose (ssreflect)` tactic also supports (co)fixpoints, by providing @@ -575,6 +576,7 @@ where: .. rocqtop:: all Lemma test x : f x + f x = f x. + Proof. set t := f _. .. rocqtop:: all restart @@ -622,6 +624,7 @@ conditions. .. rocqtop:: all Lemma test (x y z : nat) : x + y = z. + Proof. set t := _ x. + In the special case where :token:`term` is of the form @@ -643,6 +646,7 @@ conditions. .. rocqtop:: all Lemma test : (let f x y z := x + y + z in f 1) 2 3 = 6. + Proof. set t := (let g y z := S y + z in g) 2. The notation ``unkeyed`` defined in ``ssreflect.v`` is a shorthand for @@ -664,6 +668,7 @@ Moreover: .. rocqtop:: all Lemma test x y z : x + y = z. + Proof. set t := _ + _. + The type of the subterm matched should fit the type (possibly casted @@ -684,6 +689,7 @@ Moreover: .. rocqtop:: all Lemma test : forall x : nat, x + 1 = 0. + Proof. Fail set t := _ + 1. + Typeclass inference should fill in any residual hole, but matching @@ -718,6 +724,7 @@ An *occurrence switch* can be: .. rocqtop:: all Lemma test : f 2 + f 8 = f 2 + f 2. + Proof. set x := {+1 3}(f 2). Notice that some occurrences of a given term may be @@ -740,6 +747,7 @@ An *occurrence switch* can be: Notation "a < b":= (le (S a) b). Lemma test x y : x < y -> S x < S y. + Proof. set t := S x. + A list of natural numbers ``{n1 … nm}``. @@ -761,6 +769,7 @@ An *occurrence switch* can be: .. rocqtop:: all Lemma test : f 2 + f 8 = f 2 + f 2. + Proof. set x := {-2}(f 2). @@ -791,6 +800,7 @@ selection. .. rocqtop:: all Lemma test x y z : x + y = x + y + z. + Proof. set a := {2}(_ + _). Hence, in the following goal, the same tactic fails since there is @@ -808,6 +818,7 @@ only one occurrence of the selected term. .. rocqtop:: all Lemma test x y z : (x + y) + (z + z) = z + z. + Proof. Fail set a := {2}(_ + _). @@ -836,6 +847,7 @@ context of a goal thanks to the ``in`` tactical. .. rocqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. + Proof. set z := 3 in Hx. .. tacv:: set @ident := @term in {+ @ident} * @@ -852,6 +864,7 @@ context of a goal thanks to the ``in`` tactical. .. rocqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. + Proof. set z := 3 in Hx * . Indeed, remember that 4 is just a notation for (S 3). @@ -971,6 +984,7 @@ constants to the goal. .. rocqtop:: all Lemma subnK : forall m n, n <= m -> m - n + n = m. + Proof. might start with @@ -1032,6 +1046,7 @@ The ``:`` tactical is used to operate on an element in the context. .. rocqtop:: all Lemma subnK : forall m n, n <= m -> m - n + n = m. + Proof. move=> m n le_n_m. elim: n m le_n_m => [|n IHn] m => [_ | lt_n_m]. @@ -1121,6 +1136,7 @@ The move tactic. From Corelib Require Import ssreflect_rw. Goal not False. + Proof. move. More precisely, the :tacn:`move ` tactic inspects the goal and does nothing @@ -1197,6 +1213,7 @@ The elim tactic .. rocqtop:: all Lemma test m : forall n : nat, m <= n. + Proof. elim. @@ -1238,6 +1255,7 @@ existential metavariables of sort :g:`Prop`. .. rocqtop:: all Lemma test : forall y, 1 < y -> y < 2 -> exists x : { n | n < 3 }, 0 < proj1_sig x. + Proof. move=> y y_gt1 y_lt2; apply: (ex_intro _ (exist _ y _)). by apply: lt_trans y_lt2 _. by move=> y_lt3; apply: lt_trans y_gt1. @@ -1419,6 +1437,7 @@ context to interpret wildcards; in particular, it can accommodate the .. rocqtop:: all Lemma test (Hfg : forall x, f x = g x) a b : f a = g b. + Proof. apply: trans_equal (Hfg _) _. This tactic is equivalent (see Section @@ -1711,6 +1730,7 @@ Clears are deferred until the end of the intro pattern. From Corelib Require Import ssrbool. Lemma test x y : Nat.leb 0 x = true -> (Nat.leb 0 x) && (Nat.leb y 2) = true. + Proof. move=> {x} ->. If the cleared names are reused in the same intro pattern, a renaming @@ -1825,6 +1845,7 @@ deal with the possible parameters of the constants introduced. .. rocqtop:: all Lemma test (a b :nat) : a <> b. + Proof. case E : a => [|n]. If the user does not provide a branching :token:`i_item` as first @@ -1844,6 +1865,7 @@ under fresh |SSR| names. .. rocqtop:: all Lemma test (a b :nat) : a <> b. + Proof. case E : a => H. Show 2. @@ -1929,6 +1951,7 @@ be substituted. | LastAdd s x : last_spec (add_last x s). Theorem lastP : forall l : list A, last_spec l. + Proof. Admitted. We are now ready to use ``lastP`` in conjunction with ``case``. @@ -1936,6 +1959,7 @@ be substituted. .. rocqtop:: all Lemma test l : (length l) * 2 = length (l ++ l). + Proof. case: (lastP l). Applied to the same goal, the tactic ``case: l / (lastP l)`` @@ -1965,6 +1989,7 @@ be substituted. .. rocqtop:: all Lemma test l : (length l) * 2 = length (l ++ l). + Proof. case E: {1 3}l / (lastP l) => [|s x]. Show 2. @@ -2218,6 +2243,7 @@ to the others. | C4 n of n = 4 : test n. Lemma example n (t : test n) : True. + Proof. case: t; last 2 [move=> k| move=> l]; idtac. @@ -2333,6 +2359,7 @@ between standard Ltac ``in`` and the |SSR| tactical in. Ltac mytac H := rw H. Lemma test x y (H1 : x = y) (H2 : y = 3) : x + y = 6. + Proof. do [mytac H2] in H1 *. the last tactic rewrites the hypothesis ``H2 : y = 3`` both in @@ -2406,6 +2433,7 @@ the holes are abstracted in term. .. rocqtop:: all Lemma test : True. + Proof. have: _ * 0 = 0. The invocation of ``have`` is equivalent to: @@ -2417,6 +2445,7 @@ the holes are abstracted in term. Unset Strict Implicit. Unset Printing Implicit Defensive. Lemma test : True. + Proof. .. rocqtop:: all @@ -2435,6 +2464,7 @@ tactic: Unset Strict Implicit. Unset Printing Implicit Defensive. Lemma test : True. + Proof. .. rocqtop:: all @@ -2491,6 +2521,7 @@ the further use of the intermediate step. For instance, .. rocqtop:: all Lemma test a : 3 * a - 1 = a. + Proof. have -> : forall x, x * a = a. Note how the second goal was rewritten using the stated equality. @@ -2519,6 +2550,7 @@ destruction of existential assumptions like in the tactic: .. rocqtop:: all Lemma test : True. + Proof. have [x Px]: exists x : nat, x > 0; last first. An alternative use of the ``have`` tactic is to provide the explicit proof @@ -2546,6 +2578,7 @@ term for the intermediate lemma, using tactics of the form: .. rocqtop:: all Lemma test : True. + Proof. have H := forall x, (x, x) = (x, x). adds to the context ``H : Type -> Prop.`` This is a schematic example, but @@ -2571,6 +2604,7 @@ The following example requires the mathcomp and mczify libraries. From mathcomp Require Import ssrfun ssrbool ssrnat zify. Lemma test : True. + Proof. have H x (y : nat) : 2 * x + y = x + x + y by lia. A proof term provided after ``:=`` can mention these bound variables @@ -2624,6 +2658,7 @@ context entry name. Arguments Sub {_} _ _. Lemma test n m (H : m + 1 < n) : True. + Proof. have @i : 'I_n by apply: (Sub m); lia. Note that the subterm produced by :tacn:`lia` is in general huge and @@ -2636,6 +2671,7 @@ For this purpose the ``[: name]`` intro pattern and the tactic .. rocqtop:: all abort extra-mathcomp Lemma test n m (H : m + 1 < n) : True. + Proof. have [:pm] @i : 'I_n by apply: (Sub m); abstract: pm; lia. The type of ``pm`` can be cleaned up by its annotation ``(*1*)`` by just @@ -2649,6 +2685,7 @@ with`` have`` and an explicit term, they must be used as follows: .. rocqtop:: all abort extra-mathcomp Lemma test n m (H : m + 1 < n) : True. + Proof. have [:pm] @i : 'I_n := Sub m pm. by lia. @@ -2668,6 +2705,7 @@ makes use of it). .. rocqtop:: all abort extra-mathcomp Lemma test n m (H : m + 1 < n) : True. + Proof. have [:pm] @i k : 'I_(n+k) by apply: (Sub m); abstract: pm k; lia. Last, notice that the use of intro patterns for abstract constants is @@ -2688,6 +2726,7 @@ typeclass inference. Axiom t : ty. Goal True. + Proof. .. rocqtop:: all @@ -2767,6 +2806,7 @@ The ``have`` modifier can follow the ``suff`` tactic. .. rocqtop:: all abort Lemma test : G. + Proof. suff have H : P. Note that, in contrast with ``have suff``, the name H has been introduced @@ -2842,6 +2882,7 @@ The following example requires the mathcomp library. Lemma quo_rem_unicity d q1 q2 r1 r2 : q1*d + r1 = q2*d + r2 -> r1 < d -> r2 < d -> (q1, r1) = (q2, r2). + Proof. wlog: q1 q2 r1 r2 / q1 <= q2. by case: (leqP q1 q2); last symmetry; eauto. @@ -2876,6 +2917,7 @@ pattern will be used to process its instance. .. rocqtop:: all Lemma simple n (ngt0 : 0 < n ) : P n. + Proof. gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0); last first. @@ -2922,6 +2964,7 @@ illustrated in the following example. Variable x : nat. Definition addx z := z + x. Lemma test : x <= addx x. + Proof. wlog H : (y := x) (@twoy := addx x) / twoy = 2 * y. To avoid unfolding the term captured by the pattern ``add x``, one can use @@ -2939,6 +2982,7 @@ illustrated in the following example. Variable x : nat. Definition addx z := z + x. Lemma test : x <= addx x. + Proof. .. rocqtop:: all @@ -3073,6 +3117,7 @@ A :token:`r_item` can be one of the following. Definition double x := x + x. Definition ddouble x := double (double x). Lemma test x : ddouble x = 4 * x. + Proof. rw [ddouble _]/double. .. warning:: @@ -3084,6 +3129,7 @@ A :token:`r_item` can be one of the following. Definition f := fun x y => x + y. Lemma test x y : x + y = f y x. + Proof. .. rocqtop:: all fail @@ -3194,10 +3240,12 @@ proof of basic results on natural numbers arithmetic. Axiom addSnnS : forall m n, S m + n = m + S n. Lemma addnCA m n p : m + (n + p) = n + (m + p). + Proof. by elim: m p => [ | m Hrec] p; rw ?addSnnS -?addnS. Qed. Lemma addnC n m : m + n = n + m. + Proof. by rw -{1}[n]addn0 addnCA addn0. Qed. @@ -3226,6 +3274,7 @@ side of the equality the user wants to rewrite. .. rocqtop:: all Lemma test (H : forall t u, t + u = u + t) x y : x + y = y + x. + Proof. rw [y + _]H. Note that if this first pattern matching is not compatible with the @@ -3246,6 +3295,7 @@ the equality. .. rocqtop:: all Lemma test (H : forall t u, t + u * 0 = t) x y : x + y * 4 + 2 * 0 = x + 2 * 0. + Proof. Fail rw [x + _]H. Indeed, the left-hand side of ``H`` does not match @@ -3269,6 +3319,7 @@ Occurrence switches and redex switches .. rocqtop:: all Lemma test x y : x + y + 0 = x + y + y + 0 + 0 + (x + y + 0). + Proof. rw {2}[_ + y + 0](_: forall z, z + 0 = z). The second subgoal is generated by the use of an anonymous lemma in @@ -3298,6 +3349,7 @@ repetition. .. rocqtop:: all Lemma test x y (z : nat) : x + 1 = x + y + 1. + Proof. rw 2!(_ : _ + 1 = z). This last tactic generates *three* subgoals because @@ -3334,6 +3386,7 @@ rewrite operations prescribed by the rules on the current goal. Hypothesis eqac : a = c. Lemma test : a = a. + Proof. rw (eqab, eqac). Indeed, rule ``eqab`` is the first to apply among the ones @@ -3364,6 +3417,7 @@ literal matches have priority. Definition multi2 := (eqab, eqd0). Lemma test : d = b. + Proof. rw multi2. Indeed, rule ``eqd0`` applies without unfolding the @@ -3382,6 +3436,7 @@ repeated anew. Definition multi3 := (eq_adda_b, eq_adda_c, eqb0). Lemma test : 1 + a = 12 + a. + Proof. rw 2!multi3. It uses ``eq_adda_b`` then ``eqb0`` on the left-hand @@ -3464,6 +3519,7 @@ Anyway this tactic is *not* equivalent to .. rocqtop:: all Lemma test y z : y * 0 + y * (z * 0) = 0. + Proof. rw (_ : _ * 0 = 0). while the other tactic results in @@ -3518,6 +3574,7 @@ cases. Axiom H : forall x, g x = 0. Lemma test : f 3 + f 3 = f 6. + Proof. (* we call the standard rewrite tactic here *) rewrite H. @@ -3583,6 +3640,7 @@ corresponding new goals will be generated. Axiom insubT : forall n x Px, insub n x = Some (Sub x Px). Lemma test (x : 'I_2) y : Some x = insub 2 y. + Proof. rw insubT. Since the argument corresponding to ``Px`` is not supplied by the user, the @@ -3595,6 +3653,7 @@ corresponding new goals will be generated. .. rocqtop:: all abort Lemma test (x : 'I_2) y (H : y < 2) : Some x = insub 2 y. + Proof. rw insubT. @@ -3638,6 +3697,7 @@ complete terms, as shown by the simple example below. .. rocqtop:: all Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. + Proof. In this context, one cannot directly use ``eq_map``: @@ -3661,6 +3721,7 @@ complete terms, as shown by the simple example below. .. rocqtop:: all abort Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. + Proof. under eq_map => m do rw subnn. @@ -3698,6 +3759,7 @@ Let us redo the running example in interactive mode. .. rocqtop:: all abort Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. + Proof. under eq_map => m. rw subnn. over. @@ -3874,6 +3936,7 @@ Notes: Lemma test_big_nested (m n : nat) : \sum_(0 <= a < m | prime a) \sum_(0 <= j < n | odd (j * 1)) (a + j) = \sum_(0 <= i < m | prime i) \sum_(0 <= j < n | odd j) (j + i). + Proof. under eq_bigr => i prime_i do under eq_big => [ j | j odd_j ] do [ rw (muln1 j) | rw (addnC i j) ]. @@ -3934,6 +3997,7 @@ selective rewriting, blocking on the fly the reduction in the term ``t``. if l is cons x l then p x || (has p l) else false. Lemma test p x y l (H : p x = true) : has p ( x :: y :: l) = true. + Proof. rw {2}[cons]lock /= -lock. It is sometimes desirable to globally prevent a definition from being @@ -3955,6 +4019,7 @@ definition. Definition lid := locked (fun x : nat => x). Lemma test : lid 3 = 3. + Proof. rw /=. unlock lid. @@ -4065,10 +4130,12 @@ which the function is supplied: .. rocqtop:: all Lemma test (x y z : nat) (H : x = y) : x = z. + Proof. congr (_ = _) : H. Abort. Lemma test (x y z : nat) : x = y -> x = z. + Proof. congr (_ = _). The optional :token:`natural` forces the number of arguments for which the @@ -4096,6 +4163,7 @@ which the function is supplied: Definition g (n m : nat) := plus. Lemma test x y : f 0 x y = g 1 1 x y. + Proof. congr plus. This script shows that the ``congr`` tactic matches ``plus`` @@ -4114,6 +4182,7 @@ which the function is supplied: .. rocqtop:: all Lemma test n m (Hnm : m <= n) : S m + (S n - S m) = S n. + Proof. congr S; rw -/plus. The tactic ``rw -/plus`` folds back the expansion of ``plus``, @@ -4134,6 +4203,7 @@ which the function is supplied: .. rocqtop:: all Lemma test x y : x + (y * (y + x - x)) = x * 1 + (y + 0) * y. + Proof. congr ( _ + (_ * _)). .. _contextual_patterns_ssr: @@ -4313,6 +4383,7 @@ parentheses are required around more complex patterns. .. rocqtop:: all Lemma test a b : a + b + 1 = b + (a + 1). + Proof. set t := (X in _ = X). rw {}/t. set t := (a + _ in X in _ = X). @@ -4358,6 +4429,7 @@ Contextual patterns in rewrite Axiom addnC : forall m n, m + n = n + m. Lemma test x y z f : (x.+1 + y) + f (x.+1 + y) (z + (x + y).+1) = 0. + Proof. rw [in f _ _]addSn. Note: the simplification rule ``addSn`` is applied only under the ``f`` @@ -4535,6 +4607,7 @@ generation (see Section :ref:`generation_of_equations_ssr`). .. rocqtop:: all Lemma test (x : d) (l : list d): l = l. + Proof. elim/last_ind_list E : l=> [| u v]; last first. @@ -4594,6 +4667,7 @@ Here is an example of a regular, but nontrivial, eliminator. | 0 => True | S _ => False end -> P _x m) -> forall n : nat, P n (plus m n). + Proof. Admitted. .. rocqtop:: all @@ -4606,6 +4680,7 @@ Here is an example of a regular, but nontrivial, eliminator. About plus_ind. Lemma test x y z : plus (plus x y) z = plus x (plus y z). + Proof. The following tactics are all valid and perform the same elimination on this goal. @@ -4637,6 +4712,7 @@ Here is an example of a regular, but nontrivial, eliminator. end -> P _x m) -> forall n : nat, P n (plus m n). Lemma test x y z : plus (plus x y) z = plus x (plus y z). + Proof. .. rocqtop:: all @@ -4669,6 +4745,7 @@ Here is an example of a regular, but nontrivial, eliminator. end -> P _x m) -> forall n : nat, P n (plus m n). Lemma test x y z : plus (plus x y) z = plus x (plus y z). + Proof. .. rocqtop:: all @@ -4762,6 +4839,7 @@ disjunction. Hypothesis P2Q : forall a b, P (a || b) -> Q a. Lemma test a : P (a || a) -> True. + Proof. move=> HPa; move: {HPa}(P2Q HPa) => HQa. which transforms the hypothesis ``HPa : P a``, which has been introduced @@ -4781,6 +4859,7 @@ disjunction. Hypothesis P2Q : forall a b, P (a || b) -> Q a. Lemma test a : P (a || a) -> True. + Proof. .. rocqtop:: all @@ -4818,6 +4897,7 @@ equation-name generation mechanism (see Section :ref:`generation_of_equations_ss Hypothesis Q2P : forall a b, Q (a || b) -> P a \/ P b. Lemma test a b : Q (a || b) -> True. + Proof. case/Q2P=> [HPa | HPb]. This view tactic performs: @@ -4851,6 +4931,7 @@ relevant for the current goal. Hypothesis PQequiv : forall a b, P (a || b) <-> Q a. Lemma test a b : P (a || b) -> True. + Proof. move/PQequiv=> HQab. has the same behavior as the first example above. @@ -4891,6 +4972,7 @@ assumption to some given arguments. .. rocqtop:: all Lemma test z : (forall x y, x + y = z -> z = x) -> z = 0. + Proof. move/(_ 0 z). @@ -4925,6 +5007,7 @@ bookkeeping steps. Hypothesis PQequiv : forall a b, P (a || b) <-> Q a. Lemma test a : P ((~~ a) || a). + Proof. apply/PQequiv. thus in this case, the tactic ``apply/PQequiv`` is equivalent to @@ -4996,6 +5079,7 @@ analysis From Corelib Require Import ssrbool. Lemma test b : b || ~~ b = true. + Proof. by case: b. Once ``b`` is replaced by ``true`` in the first goal and by ``false`` in the @@ -5087,16 +5171,13 @@ Let us compare the respective behaviors of ``andE`` and ``andP``. .. rocqtop:: all Lemma test (b1 b2 : bool) : if (b1 && b2) then b1 else ~~(b1||b2). + Proof. .. rocqtop:: all case: (@andE b1 b2). - .. rocqtop:: none - - Restart. - - .. rocqtop:: all + .. rocqtop:: all restart case: (@andP b1 b2). @@ -5128,6 +5209,7 @@ The view mechanism is compatible with reflect predicates. From Corelib Require Import ssrbool. Lemma test (a b : bool) (Ha : a) (Hb : b) : a /\ b. + Proof. apply/andP. Conversely @@ -5135,6 +5217,7 @@ The view mechanism is compatible with reflect predicates. .. rocqtop:: all Lemma test (a b : bool) : a /\ b -> a. + Proof. move/andP. The same tactics can also be used to perform the converse operation, @@ -5251,6 +5334,7 @@ but they also allow complex transformation, involving negations. .. rocqtop:: all Lemma test (a b : bool) (Ha : a) (Hb : b) : ~~ (a && b). + Proof. apply/andP. In fact, this last script does not @@ -5281,6 +5365,7 @@ actually uses its propositional interpretation. From Corelib Require Import ssrbool. Lemma test (a b : bool) (pab : b && a) : b. + Proof. have /andP [pa ->] : (a && b) by rw andbC. Interpreting goals @@ -5345,6 +5430,7 @@ In this context, the identity view can be used when no view has to be applied: From Corelib Require Import ssrbool. Lemma test (b1 b2 b3 : bool) : ~~ (b1 || b2) = b3. + Proof. apply/idP/idP. The same goal can be decomposed in several ways, and the user may @@ -5362,6 +5448,7 @@ In this context, the identity view can be used when no view has to be applied: From Corelib Require Import ssrbool. Lemma test (b1 b2 b3 : bool) : ~~ (b1 || b2) = b3. + Proof. apply/norP/idP. @@ -5444,6 +5531,7 @@ pass a given hypothesis to a lemma. Variable Q2R : Q -> R. Lemma test (p : P) : True. + Proof. move/P2Q/Q2R in p. If the list of views is of length two, ``Hint Views`` for interpreting diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 964c854a5639..5a94cfcb7ce6 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -285,6 +285,7 @@ Examples: .. rocqtop:: reset none Goal forall (A: Prop) (B: Prop), (A /\ B) -> True. + Proof. .. rocqtop:: out @@ -301,6 +302,7 @@ Examples: .. rocqtop:: reset none Goal forall (A: Prop) (B: Prop), (A \/ B) -> True. + Proof. .. rocqtop:: out @@ -317,6 +319,7 @@ Examples: .. rocqtop:: reset none Goal forall (x:nat) (y:nat) (z:nat), (x = y) -> (y = z) -> (x = z). + Proof. .. rocqtop:: out @@ -338,6 +341,7 @@ Examples: .. rocqtop:: reset none Goal forall (n m:nat), (S n) = (S m) -> (S O)=(S (S O)) -> False. + Proof. .. rocqtop:: out @@ -362,6 +366,7 @@ Examples: .. rocqtop:: out Goal A /\ (exists x:nat, B x /\ C) -> True. + Proof. .. rocqtop:: all @@ -374,6 +379,7 @@ Examples: .. rocqtop:: reset out Goal forall (A: Prop) (B: Prop), A -> B. + Proof. .. rocqtop:: all @@ -386,6 +392,7 @@ Examples: .. rocqtop:: reset out Goal forall (A: Prop) (B: Prop), A -> B. + Proof. .. rocqtop:: all @@ -396,6 +403,7 @@ Examples: .. rocqtop:: reset out Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. + Proof. .. rocqtop:: all @@ -417,7 +425,8 @@ Examples: .. rocqtop:: out Example ThreeIntroPatternsCombined : - S (length ys) = 1 -> xs ++ ys = xs. + S (length ys) = 1 -> xs ++ ys = xs. + Proof. .. rocqtop:: all @@ -624,6 +633,7 @@ Applying theorems | Ok : bool -> Option. Definition get : forall x:Option, x <> Fail -> bool. + Proof. refine (fun x:Option => match x return x <> Fail -> bool with @@ -787,6 +797,7 @@ Applying theorems .. rocqtop:: reset none Goal forall A B C: Prop, (A -> B -> C) -> C. + Proof. .. rocqtop:: out @@ -802,6 +813,7 @@ Applying theorems .. rocqtop:: reset none Goal forall A B C: Prop, (A -> B -> C) -> (B -> C). + Proof. .. rocqtop:: out @@ -817,6 +829,7 @@ Applying theorems .. rocqtop:: reset none Goal forall A B C: Prop, B -> (A -> B -> C) -> True. + Proof. .. rocqtop:: out @@ -840,6 +853,7 @@ Applying theorems Axiom le_trans : forall n m p, n <= m -> m <= p -> n <= p. Goal forall (x y : nat), x <= y -> x * x <= y * y. + Proof. .. rocqtop:: out @@ -870,6 +884,7 @@ Applying theorems Axiom le_trans : forall n m p, n <= m -> m <= p -> n <= p. Goal forall (x y : nat), x * x <= y * y -> x <= y. + Proof. .. rocqtop:: out @@ -896,6 +911,7 @@ Applying theorems .. rocqtop:: reset none Goal forall (A B: Prop) (H1: A <-> B) (H: A), A. + Proof. .. rocqtop:: out @@ -917,6 +933,7 @@ Applying theorems .. rocqtop:: reset none Goal forall x y, x + y = y + x. + Proof. .. rocqtop:: out @@ -973,6 +990,7 @@ Applying theorems Definition id (x : nat) := x. Parameter H : forall x y, id x = y. Goal O = O. + Proof. Fail simple apply H. Because it reasons modulo a limited amount of conversion, :tacn:`simple apply` fails @@ -1009,6 +1027,7 @@ Applying theorems .. rocqtop:: in Goal R n p. + Proof. The direct application of ``Rtrans`` with ``apply`` fails because no value for ``y`` in ``Rtrans`` is found by ``apply``: @@ -1135,6 +1154,7 @@ Managing the local context .. rocqtop:: reset out Goal forall m n, m < n -> (let x := 0 in True). + Proof. .. rocqtop:: all @@ -1148,6 +1168,7 @@ Managing the local context .. rocqtop:: reset out Goal forall m n, m < n -> (let x := 0 in True). + Proof. .. rocqtop:: all @@ -1182,6 +1203,7 @@ Managing the local context .. rocqtop:: reset out Goal forall x y : nat, x = y -> y = x. + Proof. .. rocqtop:: all @@ -1192,6 +1214,7 @@ Managing the local context .. rocqtop:: reset out Goal forall x y : nat, x = y -> y = x. + Proof. .. rocqtop:: all @@ -1309,6 +1332,7 @@ Managing the local context .. rocqtop:: reset none Goal forall x :nat, x = 0 -> forall y z:nat, y=y-> 0=x. + Proof. .. rocqtop:: out @@ -1373,6 +1397,7 @@ Managing the local context .. rocqtop:: reset none Goal forall n, n = 0. + Proof. .. rocqtop:: out @@ -1576,6 +1601,7 @@ Controlling the proof flow .. rocqtop:: reset none Goal (forall n m: nat, n + m = m + n) -> True. + Proof. .. rocqtop:: out @@ -1770,14 +1796,17 @@ Controlling the proof flow Inductive F :=. (* Another empty inductive type *) Goal F -> False. + Proof. contradiction. Qed. Goal forall (A : Prop), A -> ~A -> False. + Proof. contradiction. Qed. Goal forall (A : Type) (x : A), ~(x = x) -> False. + Proof. contradiction. Qed. @@ -1790,6 +1819,7 @@ Controlling the proof flow .. rocqtop:: in Goal forall (A : Prop), 0 < 0 -> A. + Proof. .. rocqtop:: all @@ -1852,6 +1882,7 @@ Performance-oriented tactic variants .. rocqtop:: all abort Goal False. + Proof. exact_no_check I. Fail Qed. @@ -1866,6 +1897,7 @@ Performance-oriented tactic variants .. rocqtop:: all abort Goal False. + Proof. vm_cast_no_check I. Fail Qed. @@ -1880,5 +1912,6 @@ Performance-oriented tactic variants .. rocqtop:: all abort Goal False. + Proof. native_cast_no_check I. Fail Qed. diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index 4d57b51e0432..b6ab4645b41d 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -118,6 +118,7 @@ Tactics Hint Resolve eq_refl : db. Goal forall n, n=1 -> exists x y : nat, x = y /\ x = 0. + Proof. intros. do 2 eexists; subst. (* Fix 2: replace with "do 2 (eexists; subst)." *) @@ -171,6 +172,7 @@ Tactics Hint Resolve ex_intro : core. Goal forall P:nat -> Prop, P 0 -> exists n, P n. + Proof. eauto. `ex_intro` is declared as a hint so the proof succeeds. @@ -273,9 +275,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. rocqtop:: all Lemma ResAck0 : Ack 3 2 = 29. - - .. rocqtop:: all - + Proof. autorewrite with base0 using try reflexivity. .. example:: MacCarthy function @@ -304,6 +304,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. rocqtop:: in extra-stdlib Lemma Resg0 : g 1 110 = 100. + Proof. .. rocqtop:: out extra-stdlib @@ -656,7 +657,8 @@ Creating Hints .. rocqtop:: in reset Definition one := 1. - Theorem thm : one = 1. reflexivity. Qed. + Theorem thm : one = 1. + Proof. reflexivity. Qed. Create HintDb db1. Hint Opaque one : db1. @@ -664,6 +666,7 @@ Creating Hints Create HintDb db2. Goal 1 = 1. + Proof. (* "one" is not unfolded because it's opaque in db1, where bar is *) Fail typeclasses eauto with db1 db2 nocore. (* fails with tc eauto *) Succeed eauto with db1 db2 nocore. (* ignores the distinction *) @@ -684,7 +687,7 @@ Creating Hints Definition one := 1. Opaque one. (* not relevant to hint selection *) - Theorem bar: 1=1. reflexivity. Qed. + Theorem bar: 1=1. Proof. reflexivity. Qed. Create HintDb db. (* constants, etc. transparent by default *) Hint Opaque one : db. (* except for "one" *) @@ -692,6 +695,7 @@ Creating Hints Set Typeclasses Debug Verbosity 1. Goal one = 1. + Proof. Fail typeclasses eauto with db nocore. (* fail: no match for (one = 1) *) Hint Transparent one : db. @@ -718,6 +722,7 @@ Creating Hints Hint Resolve I : db. Print HintDb db. (* For XXX -> indicates XXX is the head constant *) Goal Tru. + Proof. .. rocqtop:: all @@ -787,6 +792,7 @@ Creating Hints Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. Goal forall a b:list (nat * nat), {a = b} + {a <> b}. + Proof. info_auto with eqdec. .. cmd:: Hint Cut [ @hints_regexp ] {? : {+ @ident } } diff --git a/doc/sphinx/proofs/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst index 21087b97443e..bf7973440ad0 100644 --- a/doc/sphinx/proofs/automatic-tactics/logic.rst +++ b/doc/sphinx/proofs/automatic-tactics/logic.rst @@ -20,6 +20,7 @@ Solvers for logic and equality .. rocqtop:: reset all Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x. + Proof. intros. tauto. @@ -32,6 +33,7 @@ Solvers for logic and equality .. rocqtop:: reset all Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x. + Proof. tauto. .. note:: @@ -198,12 +200,18 @@ Solvers for logic and equality .. rocqtop:: reset all - Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a. + Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b : + a = (f a) -> (g b (f a)) = (f (f a)) -> (g a b) = (f (g b a)) -> + (g a b) = a. + Proof. intros. congruence. Qed. - Theorem inj (A:Type) (f:A -> A * A) (a c d: A) : f = pair a -> Some (f c) = Some (f d) -> c=d. + Theorem inj (A:Type) (f:A -> A * A) (a c d: A) : + f = pair a -> Some (f c) = Some (f d) -> + c = d. + Proof. intros. congruence. Qed. diff --git a/doc/sphinx/proofs/writing-proofs/equality.rst b/doc/sphinx/proofs/writing-proofs/equality.rst index a91d26c81fe1..5d9e94b20ff4 100644 --- a/doc/sphinx/proofs/writing-proofs/equality.rst +++ b/doc/sphinx/proofs/writing-proofs/equality.rst @@ -202,6 +202,7 @@ Rewriting with Leibniz and setoid equality .. rocqtop:: out Lemma example x y : x + y = y + x. + Proof. .. rocqtop:: all fail @@ -467,6 +468,7 @@ which reduction engine to use. See :ref:`type-cast`.) For example: .. rocqtop:: all Goal 3 + 4 = 7. + Proof. Show Proof. Show Existentials. cbv. @@ -782,6 +784,7 @@ which reduction engine to use. See :ref:`type-cast`.) For example: .. rocqtop:: all Goal ~0=0. + Proof. unfold not. This :tacn:`fold` doesn't undo the preceeding :tacn:`unfold` (it makes no change): @@ -813,6 +816,7 @@ which reduction engine to use. See :ref:`type-cast`.) For example: .. rocqtop:: all abort Goal forall x xs, fold_right and True (x::xs). + Proof. red. fold (fold_right and True). @@ -1130,6 +1134,7 @@ unfolding. Rocq has multiple notions of opaque: Opaque id. Goal id 10 = 10. + Proof. Fail unfold id. with_strategy transparent [id] unfold id. @@ -1174,6 +1179,7 @@ unfolding. Rocq has multiple notions of opaque: .. rocqtop:: all abort Goal True. + Proof. Time assert (id (fact 8) = fact 8) by reflexivity. Time assert (id (fact 9) = fact 9) by reflexivity. @@ -1187,6 +1193,7 @@ unfolding. Rocq has multiple notions of opaque: .. rocqtop:: all Goal True. + Proof. Fail Timeout 1 assert (id (fact 100) = fact 100) by reflexivity. Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] reflexivity. @@ -1204,6 +1211,7 @@ unfolding. Rocq has multiple notions of opaque: .. rocqtop:: all Goal True. + Proof. Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] abstract reflexivity. exact I. Time Defined. diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst index c80b808c019b..646dbaa66bc2 100644 --- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst +++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst @@ -69,6 +69,7 @@ local context: .. rocqtop:: out Goal forall n m: nat, n > m -> P 1 /\ P 2. + Proof. After applying the :tacn:`intros` :term:`tactic`, we see hypotheses above the line. The names of variables (`n` and `m`) and hypotheses (`H`) appear before a colon, followed by @@ -270,13 +271,26 @@ When the proof is completed, you can exit proof mode with commands such as .. cmd:: Proof - Is a no-op which is useful to delimit the sequence of tactic commands - which start a proof, after a :cmd:`Theorem` command. It is a good practice to + Outside sections it is a no-op which is useful to delimit the sequence of tactic commands + which start a proof, e.g. after a :cmd:`Theorem` command. It is a good practice to use :cmd:`Proof` as an opening parenthesis, closed in the script with a - closing :cmd:`Qed`. + closing :cmd:`Qed` or :cmd:`Defined`. + + In sections this command is necessary to make :opt:`Default Proof Using` work. + + Some IDEs may also need the presence of this command to enable + asynchronous execution for an interactive proof. .. seealso:: :cmd:`Proof with` + .. warn:: This interactive proof is not started by the "Proof" command + :name: missing-proof-command + + Some features (for instance :opt:`Default Proof Using`) may not + work properly when interactive proofs are not delimited by + :cmd:`Proof` (or :cmd:`Proof using`). This warning helps find + such interactive proofs. + .. cmd:: Proof using @section_var_expr {? with @generic_tactic } .. insertprodn section_var_expr starred_ident_ref @@ -364,6 +378,7 @@ When the proof is completed, you can exit proof mode with commands such as #[using="Hn"] Lemma example : 0 < n. + Proof. .. rocqtop:: in @@ -403,6 +418,7 @@ When the proof is completed, you can exit proof mode with commands such as Print foo. (* Doesn't change after the End *) Print foo'. (* "End" added type radix (used by radixNotZero) and radixNotZero *) Goal 0 = 0. + Proof. .. rocqtop:: in @@ -638,6 +654,7 @@ Curly braces .. rocqtop:: all reset Goal exists n : nat, n = n. + Proof. eexists ?[x]. reflexivity. [x]: exact 0. @@ -780,6 +797,7 @@ but a name can be given by using :n:`refine ?[@ident]`, or generated using the Set Generate Goal Names. Goal forall n, n + 0 = n. + Proof. .. rocqtop:: all @@ -808,6 +826,7 @@ but a name can be given by using :n:`refine ?[@ident]`, or generated using the .. rocqtop:: in Goal forall n : nat, even n \/ odd n. + Proof. .. rocqtop:: all abort @@ -825,6 +844,7 @@ but a name can be given by using :n:`refine ?[@ident]`, or generated using the Set Generate Goal Names. Goal forall n m : nat, n + m = m + n. + Proof. intros. induction m; simpl. [O]: { induction n. @@ -891,6 +911,7 @@ tactic that unshelves goals by name. .. rocqtop:: all abort Goal exists n, n=0. + Proof. refine (ex_intro _ _ _). all: shelve_unifiable. reflexivity. @@ -936,6 +957,7 @@ Reordering goals .. rocqtop:: in abort Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. + Proof. repeat split. (* P 1, P 2, P 3, P 4, P 5 *) all: cycle 2. (* P 3, P 4, P 5, P 1, P 2 *) all: cycle -3. (* P 5, P 1, P 2, P 3, P 4 *) @@ -954,6 +976,7 @@ Reordering goals .. rocqtop:: in abort Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. + Proof. repeat split. (* P 1, P 2, P 3, P 4, P 5 *) all: swap 1 3. (* P 3, P 2, P 1, P 4, P 5 *) all: swap 1 -1. (* P 5, P 2, P 1, P 4, P 3 *) @@ -969,6 +992,7 @@ Reordering goals .. rocqtop:: in abort Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. + Proof. repeat split. (* P 1, P 2, P 3, P 4, P 5 *) all: revgoals. (* P 5, P 4, P 3, P 2, P 1 *) @@ -1064,6 +1088,7 @@ Requesting information .. rocqtop:: all abort Goal exists n, n = 0. + Proof. eexists ?[n]. Show n. diff --git a/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst b/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst index e03dfd42f305..7b3aecba9085 100644 --- a/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst +++ b/doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst @@ -87,7 +87,8 @@ The tactics presented here specialize :tacn:`apply` and .. rocqtop:: reset all Print or. (* or, represented by \/, has two constructors, or_introl and or_intror *) - Goal forall P1 P2 : Prop, P1 -> P1 \/ P2. + Goal forall P1 P2 : Prop, P1 -> P1 \/ P2. + Proof. constructor 1. (* equivalent to "left" *) apply H. (* success *) @@ -95,7 +96,8 @@ The tactics presented here specialize :tacn:`apply` and .. rocqtop:: reset none - Goal forall P1 P2 : Prop, P1 -> P1 \/ P2. + Goal forall P1 P2 : Prop, P1 -> P1 \/ P2. + Proof. .. rocqtop:: all @@ -105,7 +107,8 @@ The tactics presented here specialize :tacn:`apply` and .. rocqtop:: reset none - Goal forall P1 P2 : Prop, P1 -> P1 \/ P2. + Goal forall P1 P2 : Prop, P1 -> P1 \/ P2. + Proof. .. rocqtop:: all @@ -210,6 +213,7 @@ analysis on inductive or coinductive objects (see :ref:`variants`). .. rocqtop:: reset none Goal forall m n: nat, n = n -> m + n = n + m. + Proof. .. rocqtop:: out @@ -232,6 +236,7 @@ analysis on inductive or coinductive objects (see :ref:`variants`). .. rocqtop:: reset none Goal forall m n: nat, n = n -> m + n = n + m. + Proof. .. rocqtop:: out @@ -249,6 +254,7 @@ analysis on inductive or coinductive objects (see :ref:`variants`). .. rocqtop:: reset none Goal forall A B: Prop, A /\ B -> True. + Proof. .. rocqtop:: out @@ -269,6 +275,7 @@ analysis on inductive or coinductive objects (see :ref:`variants`). .. rocqtop:: all Goal (A -> B \/ C) -> D. + Proof. intros until 1. destruct H. Show 2. @@ -328,6 +335,7 @@ analysis on inductive or coinductive objects (see :ref:`variants`). .. rocqtop:: reset all Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C. + Proof. intros A B C H; decompose [and or] H. all: assumption. Qed. @@ -418,6 +426,7 @@ Induction Axiom P : N -> Prop. Goal forall n:nat, P n. + Proof. intros. Fail induction n using strong. change N in n. @@ -433,6 +442,7 @@ Induction .. rocqtop:: reset all Lemma induction_test : forall n:nat, n = n -> n <= n. + Proof. intros n H. induction n. exact (le_n 0). @@ -444,6 +454,7 @@ Induction .. rocqtop:: reset all Lemma induction_test2 : forall n m:nat, n = m -> n <= m. + Proof. intros n m H. induction n in m, H |- *. Show 2. @@ -512,6 +523,7 @@ Induction .. rocqtop:: reset all Lemma lt_1_r : forall n:nat, n < 1 -> n = 0. + Proof. intros n H ; induction H. Here we did not get any information on the indexes to help fulfill @@ -524,6 +536,7 @@ Induction Require Import Stdlib.Program.Equality. Lemma lt_1_r : forall n:nat, n < 1 -> n = 0. + Proof. intros n H ; dependent induction H. The subgoal is cleaned up as the tactic tries to automatically @@ -669,6 +682,7 @@ This section describes some special purpose tactics to work with .. rocqtop:: reset in Goal 1 <> 2. + Proof. discriminate. Qed. @@ -684,6 +698,7 @@ This section describes some special purpose tactics to work with .. rocqtop:: in Goal 1 <> 2. + Proof. .. rocqtop:: all @@ -701,6 +716,7 @@ This section describes some special purpose tactics to work with .. rocqtop:: reset in Goal forall n:nat, n <> S n. + Proof. intro n. induction n. @@ -776,6 +792,7 @@ This section describes some special purpose tactics to work with | cons : nat -> list -> list. Parameter P : list -> Prop. Goal forall l n, P nil -> cons n l = cons 0 nil -> P l. + Proof. .. rocqtop:: all @@ -932,6 +949,7 @@ This section describes some special purpose tactics to work with .. rocqtop:: in Goal forall l:list nat, contains0 (1 :: l) -> contains0 l. + Proof. .. rocqtop:: all @@ -1008,6 +1026,7 @@ This section describes some special purpose tactics to work with Variable P : nat -> nat -> Prop. Variable Q : forall n m:nat, Le n m -> Prop. Goal forall n m, Le (S n) m -> P n m. + Proof. .. rocqtop:: out @@ -1047,6 +1066,7 @@ This section describes some special purpose tactics to work with Abort. Goal forall n m (H:Le (S n) m), Q (S n) m H. + Proof. .. rocqtop:: out @@ -1130,6 +1150,7 @@ Helper tactics Goal forall (P Q : Prop) (Hp : {P} + {~P}) (Hq : {Q} + {~Q}), P -> ~Q -> (if Hp then true else false) = (if Hq then false else true). + Proof. .. rocqtop:: all extra-stdlib @@ -1624,6 +1645,7 @@ Generation of inversion principles with ``Derive`` ``Inversion`` .. rocqtop:: none Goal forall (n m : nat) (H : Le (S n) m), P n m. + Proof. intros. .. rocqtop:: all @@ -1733,6 +1755,7 @@ redo what we've done manually with dependent destruction: .. rocqtop:: in extra-stdlib Lemma ex : forall n m:nat, Le (S n) m -> P n m. + Proof. .. rocqtop:: in extra-stdlib diff --git a/doc/tools/rocqrst/rocqdomain.py b/doc/tools/rocqrst/rocqdomain.py index b167182f99b2..65051ffcce90 100644 --- a/doc/tools/rocqrst/rocqdomain.py +++ b/doc/tools/rocqrst/rocqdomain.py @@ -873,6 +873,7 @@ def add_rocq_output_1(self, repl, node): if options['restart']: repl.sendone('Restart.') + repl.sendone('Proof.') if options['reset']: repl.sendone('Reset Initial.') repl.send_initial_options() diff --git a/test-suite/ide/reopen1.fake b/test-suite/ide/reopen1.fake index b0618c770ad7..4ba3cc25b6e8 100644 --- a/test-suite/ide/reopen1.fake +++ b/test-suite/ide/reopen1.fake @@ -14,7 +14,7 @@ EDIT_AT here ADD here2 { Proof. } ADD here3 { Qed. } WAIT -EDIT_AT here2 +EDIT_AT here # Fixing the proof ADD { Proof. } ADD { trivial. } diff --git a/test-suite/output-coqtop/BracketLoc.out b/test-suite/output-coqtop/BracketLoc.out index 89345bc2e5b6..5919ad77dff5 100644 --- a/test-suite/output-coqtop/BracketLoc.out +++ b/test-suite/output-coqtop/BracketLoc.out @@ -4,9 +4,10 @@ Rocq < 1 goal ============================ True -Toplevel input, characters 11-12: -> Goal True. } -> ^ +Unnamed_thm < +Toplevel input, characters 7-8: +> Proof. } +> ^ Error: The proof is not focused Unnamed_thm < Toplevel input, characters 2-3: diff --git a/test-suite/output-coqtop/BracketLoc.v b/test-suite/output-coqtop/BracketLoc.v index 9a5c142649b8..648f9fadf474 100644 --- a/test-suite/output-coqtop/BracketLoc.v +++ b/test-suite/output-coqtop/BracketLoc.v @@ -1,4 +1,5 @@ -Goal True. } +Goal True. +Proof. } } } exact 0. diff --git a/test-suite/output-coqtop/bug_16462.out b/test-suite/output-coqtop/bug_16462.out index 57ed0d4eb48b..c8f837bfa0be 100644 --- a/test-suite/output-coqtop/bug_16462.out +++ b/test-suite/output-coqtop/bug_16462.out @@ -11,6 +11,7 @@ Rocq < 1 goal ============================ True +Unnamed_thm < Unnamed_thm < Unnamed_thm_subproof Unnamed_thm_subproof Toplevel input, characters 2-7: diff --git a/test-suite/output-coqtop/bug_16462.v b/test-suite/output-coqtop/bug_16462.v index 2f1ba4054f90..c97ff6709695 100644 --- a/test-suite/output-coqtop/bug_16462.v +++ b/test-suite/output-coqtop/bug_16462.v @@ -9,4 +9,5 @@ Ltac baz x := let H := fresh in f F () () ]. Set Ltac Backtrace. Goal True. +Proof. baz I. diff --git a/test-suite/output-coqtop/diffs_in_show_cmd.out b/test-suite/output-coqtop/diffs_in_show_cmd.out index a1d6a61b567b..e43da8b9f417 100644 --- a/test-suite/output-coqtop/diffs_in_show_cmd.out +++ b/test-suite/output-coqtop/diffs_in_show_cmd.out @@ -4,6 +4,7 @@ Rocq < Rocq < 1 goal ============================ forall n m : nat, n = m +Unnamed_thm < Unnamed_thm < 1 goal (?foo) ============================ diff --git a/test-suite/output-coqtop/diffs_in_show_cmd.v b/test-suite/output-coqtop/diffs_in_show_cmd.v index 7847caa32e07..bf629ecad2f6 100644 --- a/test-suite/output-coqtop/diffs_in_show_cmd.v +++ b/test-suite/output-coqtop/diffs_in_show_cmd.v @@ -1,5 +1,6 @@ (* -*- coq-prog-args: ("-color" "on"); -*- *) Goal forall n m:nat, n = m. +Proof. refine ?[foo]. intros. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 44d996320118..01f06468bd8f 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -36,7 +36,7 @@ Arguments myrefl {C}%_type_scope x _ (where some original arguments have been renamed) myrefl uses section variable A. Expands to: Constructor Arguments_renaming.Test1.myrefl -Declared in library Arguments_renaming, line 25, characters 40-46 +Declared in library Arguments_renaming, line 26, characters 40-46 myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := match n with @@ -56,7 +56,7 @@ The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Arguments_renaming.Test1.myplus -Declared in library Arguments_renaming, line 31, characters 9-15 +Declared in library Arguments_renaming, line 32, characters 9-15 @myplus : forall Z : Type, Z -> nat -> nat -> nat Inductive myEq (A B : Type) (x : A) : A -> Prop := @@ -71,7 +71,7 @@ myrefl is template universe polymorphic Arguments myrefl A%_type_scope {C}%_type_scope x _ (where some original arguments have been renamed) Expands to: Constructor Arguments_renaming.myrefl -Declared in library Arguments_renaming, line 25, characters 40-46 +Declared in library Arguments_renaming, line 26, characters 40-46 myrefl : forall (A C : Type) (x : A), C -> myEq A C x x myplus = @@ -93,29 +93,29 @@ The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Arguments_renaming.myplus -Declared in library Arguments_renaming, line 31, characters 9-15 +Declared in library Arguments_renaming, line 32, characters 9-15 @myplus : forall Z : Type, Z -> nat -> nat -> nat -File "./output/Arguments_renaming.v", line 49, characters 0-36: +File "./output/Arguments_renaming.v", line 50, characters 0-36: The command has indeed failed with message: Argument lists should agree on the names they provide. -File "./output/Arguments_renaming.v", line 50, characters 0-41: +File "./output/Arguments_renaming.v", line 51, characters 0-41: The command has indeed failed with message: Sequences of implicit arguments must be of different lengths. -File "./output/Arguments_renaming.v", line 51, characters 0-37: +File "./output/Arguments_renaming.v", line 52, characters 0-37: The command has indeed failed with message: Argument number 3 is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ]. -File "./output/Arguments_renaming.v", line 52, characters 0-37: +File "./output/Arguments_renaming.v", line 53, characters 0-37: The command has indeed failed with message: Argument z is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ]. -File "./output/Arguments_renaming.v", line 53, characters 0-28: +File "./output/Arguments_renaming.v", line 54, characters 0-28: The command has indeed failed with message: Extra arguments: y. -File "./output/Arguments_renaming.v", line 54, characters 0-26: +File "./output/Arguments_renaming.v", line 55, characters 0-26: The command has indeed failed with message: Flag "rename" expected to rename A into R. -File "./output/Arguments_renaming.v", line 58, characters 2-36: +File "./output/Arguments_renaming.v", line 59, characters 2-36: The command has indeed failed with message: Arguments of section variables such as allTrue may not be renamed. diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 0be5b9d1578f..ddd020f82158 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -10,6 +10,7 @@ Print eq_refl. About eq_refl. Goal 3 = 3. +Proof. Succeed apply @eq_refl with (B := nat). Succeed apply @eq_refl with (y := 3). diff --git a/test-suite/output/CantApplyBadType.out b/test-suite/output/CantApplyBadType.out index ca34e43809b8..803e22e36eda 100644 --- a/test-suite/output/CantApplyBadType.out +++ b/test-suite/output/CantApplyBadType.out @@ -11,7 +11,7 @@ cannot be applied to the term "Type" : "Type" This term has type "Type@{u+1}" which should be a subtype of "Type@{u1}". -File "./output/CantApplyBadType.v", line 27, characters 2-108: +File "./output/CantApplyBadType.v", line 28, characters 2-108: The command has indeed failed with message: Illegal application: The term "idu1" of type "Type -> Type" diff --git a/test-suite/output/CantApplyBadType.v b/test-suite/output/CantApplyBadType.v index 97151e5ed2ee..2206050e5c89 100644 --- a/test-suite/output/CantApplyBadType.v +++ b/test-suite/output/CantApplyBadType.v @@ -24,6 +24,7 @@ This term has type "Type@{u+1}" which should be coercible to (* typing.ml error *) Goal True. +Proof. Fail let c := constr:(ltac:(refine (idu1 _); exact_no_check Type@{u})) in let _ := type of c in idtac. diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 226918e1e256..5d1a3dfb321c 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -175,7 +175,7 @@ fun x : K => match x with | _ => 2 end : K -> nat -File "./output/Cases.v", line 224, characters 38-86: +File "./output/Cases.v", line 229, characters 38-86: The command has indeed failed with message: Pattern "S _, _" is redundant in this clause. stray = @@ -192,21 +192,21 @@ end : Tree -> Tree Arguments stray N -File "./output/Cases.v", line 253, characters 4-5: +File "./output/Cases.v", line 258, characters 4-5: Warning: Unused variable B might be a misspelled constructor. Use _ or _B to silence this warning. [unused-pattern-matching-variable,default] -File "./output/Cases.v", line 266, characters 33-40: +File "./output/Cases.v", line 271, characters 33-40: The command has indeed failed with message: Application of arguments to a recursive notation not supported in patterns. -File "./output/Cases.v", line 267, characters 33-43: +File "./output/Cases.v", line 272, characters 33-43: The command has indeed failed with message: The constructor cons (in type list) is expected to be applied to 2 arguments while it is actually applied to 3 arguments. -File "./output/Cases.v", line 268, characters 33-39: +File "./output/Cases.v", line 273, characters 33-39: The command has indeed failed with message: The constructor cons (in type list) is expected to be applied to 2 arguments while it is actually applied to 1 argument. -File "./output/Cases.v", line 271, characters 33-45: +File "./output/Cases.v", line 276, characters 33-45: The command has indeed failed with message: The constructor D' (in type J') is expected to be applied to 4 arguments (or 6 arguments when including variables for local definitions) while it is @@ -220,23 +220,23 @@ fun x : J' bool (true, true) => match x with | D' _ _ _ n p _ => n + p end : J' bool (true, true) -> nat -File "./output/Cases.v", line 277, characters 33-40: +File "./output/Cases.v", line 282, characters 33-40: The command has indeed failed with message: Application of arguments to a recursive notation not supported in patterns. -File "./output/Cases.v", line 278, characters 33-43: +File "./output/Cases.v", line 283, characters 33-43: The command has indeed failed with message: The constructor cons (in type list) is expected to be applied to 2 arguments while it is actually applied to 3 arguments. -File "./output/Cases.v", line 279, characters 33-39: +File "./output/Cases.v", line 284, characters 33-39: The command has indeed failed with message: The constructor cons (in type list) is expected to be applied to 2 arguments while it is actually applied to 1 argument. -File "./output/Cases.v", line 281, characters 33-39: +File "./output/Cases.v", line 286, characters 33-39: The command has indeed failed with message: The constructor D' (in type J') is expected to be applied to 3 arguments (or 4 arguments when including variables for local definitions) while it is actually applied to 2 arguments. -File "./output/Cases.v", line 282, characters 33-45: +File "./output/Cases.v", line 287, characters 33-45: The command has indeed failed with message: The constructor D' (in type J') is expected to be applied to 3 arguments (or 4 arguments when including variables for local definitions) while it is @@ -251,16 +251,16 @@ match x with | @D' _ _ _ _ n _ p _ => (n, p) end : J' bool (true, true) -> nat * nat -File "./output/Cases.v", line 313, characters 3-4: +File "./output/Cases.v", line 318, characters 3-4: Warning: Unused variable x might be a misspelled constructor. Use _ or _x to silence this warning. [unused-pattern-matching-variable,default] -File "./output/Cases.v", line 314, characters 6-7: +File "./output/Cases.v", line 319, characters 6-7: Warning: Unused variable y might be a misspelled constructor. Use _ or _y to silence this warning. [unused-pattern-matching-variable,default] -File "./output/Cases.v", line 314, characters 3-4: +File "./output/Cases.v", line 319, characters 3-4: Warning: Unused variable x might be a misspelled constructor. Use _ or _x to silence this warning. [unused-pattern-matching-variable,default] -File "./output/Cases.v", line 325, characters 4-12: +File "./output/Cases.v", line 330, characters 4-12: The command has indeed failed with message: Once notations are expanded, the resulting constructor true (in type bool) is expected to be applied to no arguments while it is actually applied to diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 8cca5ef8909f..98ee85518031 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -128,6 +128,7 @@ Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p. (* Test use of idents bound to ltac names in a "match" *) Lemma lem1 : forall k, k=k :>nat * nat. +Proof. let x := fresh "aa" in let y := fresh "bb" in let z := fresh "cc" in @@ -137,6 +138,7 @@ Qed. Print lem1. Lemma lem2 : forall k, k=k :> bool. +Proof. let x := fresh "aa" in let y := fresh "bb" in let z := fresh "cc" in @@ -146,6 +148,7 @@ Qed. Print lem2. Lemma lem3 : forall k, k=k :>nat * nat. +Proof. let x := fresh "aa" in let y := fresh "bb" in let z := fresh "cc" in @@ -155,6 +158,7 @@ Qed. Print lem3. Lemma lem4 x : x+0=0. +Proof. match goal with |- ?y = _ => pose (match y with 0 => 0 | S n => 0 end) end. match goal with |- ?y = _ => pose (match y as y with 0 => 0 | S n => 0 end) end. match goal with |- ?y = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end. @@ -167,6 +171,7 @@ Show. Abort. Lemma lem5 (p:nat) : eq_refl p = eq_refl p. +Proof. let y := fresh "n" in (* Checking that y is hidden *) let z := fresh "e" in (* Checking that z is hidden *) match goal with diff --git a/test-suite/output/DebugRelevances.v b/test-suite/output/DebugRelevances.v index 0d853a3cfd69..1e22f5f55fbd 100644 --- a/test-suite/output/DebugRelevances.v +++ b/test-suite/output/DebugRelevances.v @@ -22,6 +22,7 @@ Print boz. Inductive sFalse : SProp := . Goal True. +Proof. Unset Printing Notations. (* arrow notation has no binder so relevance isn't printed *) pose (f:=fun A (a:A) => A). Show. diff --git a/test-suite/output/Deprecation.out b/test-suite/output/Deprecation.out index 2063c7e82973..7a985117f16d 100644 --- a/test-suite/output/Deprecation.out +++ b/test-suite/output/Deprecation.out @@ -2,26 +2,26 @@ File "./output/Deprecation.v", line 4, characters 33-48: The command has indeed failed with message: This command does not support this attribute: why. [unsupported-attributes,parsing,default] -File "./output/Deprecation.v", line 7, characters 0-3: +File "./output/Deprecation.v", line 8, characters 0-3: Warning: Tactic foo is deprecated since X.Y. Use idtac instead. [deprecated-tactic-since-X.Y,deprecated-since-X.Y,deprecated-tactic,deprecated,default] -File "./output/Deprecation.v", line 19, characters 5-8: +File "./output/Deprecation.v", line 22, characters 5-8: The command has indeed failed with message: Tactic foo is deprecated since X.Y. Use idtac instead. [deprecated-tactic-since-X.Y,deprecated-since-X.Y,deprecated-tactic,deprecated,default] -File "./output/Deprecation.v", line 26, characters 0-3: +File "./output/Deprecation.v", line 30, characters 0-3: Warning: Tactic bar is deprecated since library X.Y. Use baz instead. [deprecated-tactic-since-library-X.Y,deprecated-since-library-X.Y,deprecated-tactic,deprecated,default] -File "./output/Deprecation.v", line 31, characters 6-9: +File "./output/Deprecation.v", line 35, characters 6-9: Warning: hello [warn-reference,user-warn,default] bar : nat -File "./output/Deprecation.v", line 36, characters 6-13: +File "./output/Deprecation.v", line 40, characters 6-13: Warning: use less +s [warn-notation-fragile-too-many-plus,too-many-plus,fragile,warn-notation,user-warn,default] 1 ++ 2 : nat -File "./output/Deprecation.v", line 37, characters 6-12: +File "./output/Deprecation.v", line 41, characters 6-12: Warning: use less +s 2 [warn-notation-too-many-plus,too-many-plus,warn-notation,user-warn,default] 1 ++ 2 diff --git a/test-suite/output/Deprecation.v b/test-suite/output/Deprecation.v index 7b273f00556a..a78bbbcd0ee0 100644 --- a/test-suite/output/Deprecation.v +++ b/test-suite/output/Deprecation.v @@ -4,18 +4,21 @@ Fail #[deprecated(since="today", why="I said so")] Definition foo := 1. Goal True. +Proof. foo. Abort. Set Warnings "-deprecated-since-X.Y". Goal True. +Proof. foo. Abort. Set Warnings "+deprecated-since-X.Y". Goal True. +Proof. Fail foo. Abort. @@ -23,6 +26,7 @@ Abort. Ltac bar := idtac. Goal True. +Proof. bar. Abort. diff --git a/test-suite/output/ErrorLocation_12152.out b/test-suite/output/ErrorLocation_12152.out index 9cddd411564d..dd663c5a7348 100644 --- a/test-suite/output/ErrorLocation_12152.out +++ b/test-suite/output/ErrorLocation_12152.out @@ -1,6 +1,6 @@ -File "./output/ErrorLocation_12152.v", line 3, characters 5-12: +File "./output/ErrorLocation_12152.v", line 4, characters 5-12: The command has indeed failed with message: No product even after head-reduction. -File "./output/ErrorLocation_12152.v", line 4, characters 5-13: +File "./output/ErrorLocation_12152.v", line 5, characters 5-13: The command has indeed failed with message: No product even after head-reduction. diff --git a/test-suite/output/ErrorLocation_12152.v b/test-suite/output/ErrorLocation_12152.v index e65c6820b34d..99063da38f03 100644 --- a/test-suite/output/ErrorLocation_12152.v +++ b/test-suite/output/ErrorLocation_12152.v @@ -1,5 +1,6 @@ (* Reported in #12152 *) Goal True. +Proof. Fail intro H; auto. Fail intros H; auto. Abort. diff --git a/test-suite/output/ErrorLocation_12255.out b/test-suite/output/ErrorLocation_12255.out index 078147255011..a225c6c07fa8 100644 --- a/test-suite/output/ErrorLocation_12255.out +++ b/test-suite/output/ErrorLocation_12255.out @@ -1,4 +1,4 @@ -File "./output/ErrorLocation_12255.v", line 4, characters 5-21: +File "./output/ErrorLocation_12255.v", line 5, characters 5-21: The command has indeed failed with message: Ltac variable x is bound to i > 0 of type constr which cannot be coerced to an evaluable reference. diff --git a/test-suite/output/ErrorLocation_12255.v b/test-suite/output/ErrorLocation_12255.v index 865bce34b262..a60eac165b1c 100644 --- a/test-suite/output/ErrorLocation_12255.v +++ b/test-suite/output/ErrorLocation_12255.v @@ -1,5 +1,6 @@ Ltac can_unfold x := let b := eval cbv delta [x] in x in idtac. Definition i := O. Goal False. +Proof. Fail can_unfold (i>0). Abort. diff --git a/test-suite/output/ErrorLocation_12774.out b/test-suite/output/ErrorLocation_12774.out index 651c776e7c2e..28c8f579ffd7 100644 --- a/test-suite/output/ErrorLocation_12774.out +++ b/test-suite/output/ErrorLocation_12774.out @@ -1,9 +1,9 @@ -File "./output/ErrorLocation_12774.v", line 5, characters 18-19: +File "./output/ErrorLocation_12774.v", line 6, characters 18-19: The command has indeed failed with message: The term "0" has type "nat" while it is expected to have type "Type". -File "./output/ErrorLocation_12774.v", line 6, characters 14-15: +File "./output/ErrorLocation_12774.v", line 7, characters 14-15: The command has indeed failed with message: The term "0" has type "nat" while it is expected to have type "Type". -File "./output/ErrorLocation_12774.v", line 7, characters 5-6: +File "./output/ErrorLocation_12774.v", line 8, characters 5-6: The command has indeed failed with message: No product even after head-reduction. diff --git a/test-suite/output/ErrorLocation_12774.v b/test-suite/output/ErrorLocation_12774.v index d5039f767651..411220b0c4de 100644 --- a/test-suite/output/ErrorLocation_12774.v +++ b/test-suite/output/ErrorLocation_12774.v @@ -2,6 +2,7 @@ Ltac f := simpl. Ltac g := auto; intro. Goal Type. +Proof. Fail simpl; exact 0. Fail f; exact 0. Fail g. diff --git a/test-suite/output/ErrorLocation_13241.out b/test-suite/output/ErrorLocation_13241.out index 2c697a88d9b9..ca366e44869f 100644 --- a/test-suite/output/ErrorLocation_13241.out +++ b/test-suite/output/ErrorLocation_13241.out @@ -1,6 +1,6 @@ -File "./output/ErrorLocation_13241.v", line 5, characters 5-6: +File "./output/ErrorLocation_13241.v", line 6, characters 5-6: The command has indeed failed with message: No product even after head-reduction. -File "./output/ErrorLocation_13241.v", line 13, characters 5-6: +File "./output/ErrorLocation_13241.v", line 15, characters 5-6: The command has indeed failed with message: No product even after head-reduction. diff --git a/test-suite/output/ErrorLocation_13241.v b/test-suite/output/ErrorLocation_13241.v index 05120a5d46d5..1fb40cc97f97 100644 --- a/test-suite/output/ErrorLocation_13241.v +++ b/test-suite/output/ErrorLocation_13241.v @@ -2,6 +2,7 @@ Module Direct. Ltac a := intro. Ltac b := a. Goal True. +Proof. Fail b. Abort. End Direct. @@ -10,6 +11,7 @@ Module Thunked. Ltac a _ := intro. Ltac b := a (). Goal True. +Proof. Fail b. Abort. End Thunked. diff --git a/test-suite/output/ErrorLocation_ltac.out b/test-suite/output/ErrorLocation_ltac.out index be2519b8c434..7db15421dda0 100644 --- a/test-suite/output/ErrorLocation_ltac.out +++ b/test-suite/output/ErrorLocation_ltac.out @@ -1,12 +1,12 @@ -File "./output/ErrorLocation_ltac.v", line 5, characters 12-16: +File "./output/ErrorLocation_ltac.v", line 6, characters 12-16: The command has indeed failed with message: Tactic failure: Cannot solve this goal. -File "./output/ErrorLocation_ltac.v", line 6, characters 12-13: +File "./output/ErrorLocation_ltac.v", line 7, characters 12-13: The command has indeed failed with message: Tactic failure. -File "./output/ErrorLocation_ltac.v", line 7, characters 12-15: +File "./output/ErrorLocation_ltac.v", line 8, characters 12-15: The command has indeed failed with message: Not a negated primitive equality. -File "./output/ErrorLocation_ltac.v", line 8, characters 27-28: +File "./output/ErrorLocation_ltac.v", line 9, characters 27-28: The command has indeed failed with message: Tactic failure. diff --git a/test-suite/output/ErrorLocation_ltac.v b/test-suite/output/ErrorLocation_ltac.v index 6de9d9047d99..07c887fc4f18 100644 --- a/test-suite/output/ErrorLocation_ltac.v +++ b/test-suite/output/ErrorLocation_ltac.v @@ -2,6 +2,7 @@ Ltac f := fail. Ltac inj := injection. Goal False. +Proof. Fail idtac; easy. Fail idtac; f. Fail idtac; inj. diff --git a/test-suite/output/ErrorLocation_tac_in_term.out b/test-suite/output/ErrorLocation_tac_in_term.out index 5424ea92fa10..96d01a0f75c4 100644 --- a/test-suite/output/ErrorLocation_tac_in_term.out +++ b/test-suite/output/ErrorLocation_tac_in_term.out @@ -13,9 +13,9 @@ The command has indeed failed with message: Illegal application (Non-functional construction): The expression "I" of type "True" cannot be applied to the term "I" : "True" -File "./output/ErrorLocation_tac_in_term.v", line 17, characters 26-30: +File "./output/ErrorLocation_tac_in_term.v", line 18, characters 26-30: The command has indeed failed with message: The term "true" has type "bool" while it is expected to have type "nat". -File "./output/ErrorLocation_tac_in_term.v", line 18, characters 17-25: +File "./output/ErrorLocation_tac_in_term.v", line 19, characters 17-25: The command has indeed failed with message: The term "true" has type "bool" while it is expected to have type "nat". diff --git a/test-suite/output/ErrorLocation_tac_in_term.v b/test-suite/output/ErrorLocation_tac_in_term.v index bd78bfb611e6..c33d1cefeaff 100644 --- a/test-suite/output/ErrorLocation_tac_in_term.v +++ b/test-suite/output/ErrorLocation_tac_in_term.v @@ -14,6 +14,7 @@ Fail Check baz (I I). Ltac f x y := apply (x y). Goal True. +Proof. Fail apply ltac:(apply (S true)). Fail apply ltac:(f S true). Abort. diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index e336d7230e74..e126c2e1db72 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -1,39 +1,39 @@ File "./output/Errors.v", line 12, characters 0-11: The command has indeed failed with message: The field t is missing in Errors.M. -File "./output/Errors.v", line 19, characters 18-19: +File "./output/Errors.v", line 20, characters 18-19: The command has indeed failed with message: Unable to unify "nat" with "True". -File "./output/Errors.v", line 20, characters 12-15: +File "./output/Errors.v", line 21, characters 12-15: The command has indeed failed with message: Unable to unify "nat" with "True". In nested Ltac calls to "f" and "apply x", last call failed. -File "./output/Errors.v", line 29, characters 21-30: +File "./output/Errors.v", line 31, characters 21-30: The command has indeed failed with message: Instance is not well-typed in the environment of ?x. Ltac call to "instantiate ( (ident) := (lglob) )" failed. -File "./output/Errors.v", line 34, characters 19-20: +File "./output/Errors.v", line 36, characters 19-20: The command has indeed failed with message: Cannot infer ?T in the partial instance "?T -> nat" found for the type of f. -File "./output/Errors.v", line 35, characters 22-24: +File "./output/Errors.v", line 37, characters 22-24: The command has indeed failed with message: Cannot infer ?T in the partial instance "?T -> nat" found for the implicit parameter A of id whose type is "Type". -File "./output/Errors.v", line 36, characters 17-18: +File "./output/Errors.v", line 38, characters 17-18: The command has indeed failed with message: Cannot infer ?T in the partial instance "forall x : nat, ?T" found for the type of f in environment: x : nat -File "./output/Errors.v", line 44, characters 5-23: +File "./output/Errors.v", line 47, characters 5-23: The command has indeed failed with message: The first term has type "nat" while the second term has incompatible type "bool". -File "./output/Errors.v", line 49, characters 7-24: +File "./output/Errors.v", line 53, characters 7-24: The command has indeed failed with message: Replacement would lead to an ill-typed term: Illegal application: The term "@eq" of type "forall A : Type, A -> A -> Prop" diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v index 4ee12a18ac39..d94d5ddaa0ca 100644 --- a/test-suite/output/Errors.v +++ b/test-suite/output/Errors.v @@ -16,6 +16,7 @@ Fail End M. Ltac f x := apply x. Goal True. +Proof. Fail simpl; apply 0. Fail simpl; f 0. Abort. @@ -23,6 +24,7 @@ Abort. (* Test instantiate error messages *) Goal forall T1 (P1 : T1 -> Type), sigT P1 -> sigT P1. +Proof. intros T1 P1 H1. eexists ?[x]. destruct H1 as [x1 H1]. @@ -41,10 +43,12 @@ End M. Module Change. Goal 0 = 0. +Proof. Fail change 0 with true. Abort. Goal nat = nat. +Proof. pose (nat : Type) as n. Fail change nat with n. (* Error: Replacement would lead to an ill-typed term. *) Abort. diff --git a/test-suite/output/Existentials.v b/test-suite/output/Existentials.v index 924f1f559264..b118b1d2c359 100644 --- a/test-suite/output/Existentials.v +++ b/test-suite/output/Existentials.v @@ -6,6 +6,7 @@ Variable p:nat. Let q := S p. Goal forall n m:nat, n = m. +Proof. intros. eapply eq_trans. clearbody q. diff --git a/test-suite/output/InvalidDisjunctiveIntro.out b/test-suite/output/InvalidDisjunctiveIntro.out index 361aac6f2365..d80cffe08cfa 100644 --- a/test-suite/output/InvalidDisjunctiveIntro.out +++ b/test-suite/output/InvalidDisjunctiveIntro.out @@ -1,23 +1,23 @@ -File "./output/InvalidDisjunctiveIntro.v", line 2, characters 31-32: +File "./output/InvalidDisjunctiveIntro.v", line 3, characters 31-32: The command has indeed failed with message: Cannot coerce to a disjunctive/conjunctive pattern. -File "./output/InvalidDisjunctiveIntro.v", line 4, characters 2-32: +File "./output/InvalidDisjunctiveIntro.v", line 5, characters 2-32: The command has indeed failed with message: Disjunctive/conjunctive introduction pattern expected. -File "./output/InvalidDisjunctiveIntro.v", line 6, characters 48-49: +File "./output/InvalidDisjunctiveIntro.v", line 7, characters 48-49: The command has indeed failed with message: Cannot coerce to a disjunctive/conjunctive pattern. -File "./output/InvalidDisjunctiveIntro.v", line 8, characters 49-50: +File "./output/InvalidDisjunctiveIntro.v", line 9, characters 49-50: The command has indeed failed with message: Cannot coerce to a disjunctive/conjunctive pattern. -File "./output/InvalidDisjunctiveIntro.v", line 10, characters 32-33: +File "./output/InvalidDisjunctiveIntro.v", line 11, characters 32-33: The command has indeed failed with message: Ltac variable H is bound to idtac of type tactic which cannot be coerced to an introduction pattern. -File "./output/InvalidDisjunctiveIntro.v", line 13, characters 2-52: +File "./output/InvalidDisjunctiveIntro.v", line 14, characters 2-52: The command has indeed failed with message: Disjunctive/conjunctive introduction pattern expected. -File "./output/InvalidDisjunctiveIntro.v", line 15, characters 50-52: +File "./output/InvalidDisjunctiveIntro.v", line 16, characters 50-52: The command has indeed failed with message: Ltac variable H' is bound to idtac of type tactic which cannot be coerced to an introduction pattern. diff --git a/test-suite/output/InvalidDisjunctiveIntro.v b/test-suite/output/InvalidDisjunctiveIntro.v index 4febdf034490..b5c31b559e5e 100644 --- a/test-suite/output/InvalidDisjunctiveIntro.v +++ b/test-suite/output/InvalidDisjunctiveIntro.v @@ -1,4 +1,5 @@ Theorem test (A:Prop) : A \/ A -> A. +Proof. Fail intros H; destruct H as H. (* Cannot coerce to a disjunctive/conjunctive pattern. *) Fail intro H; destruct H as H. diff --git a/test-suite/output/Match_subterm.v b/test-suite/output/Match_subterm.v index bf862c946d5b..7a0e9d90328a 100644 --- a/test-suite/output/Match_subterm.v +++ b/test-suite/output/Match_subterm.v @@ -1,4 +1,5 @@ Goal 0 = 1. +Proof. match goal with | |- context [?v] => idtac v ; fail diff --git a/test-suite/output/MissingProof.out b/test-suite/output/MissingProof.out new file mode 100644 index 000000000000..7989a41d20f3 --- /dev/null +++ b/test-suite/output/MissingProof.out @@ -0,0 +1,30 @@ +File "./output/MissingProof.v", line 2, characters 2-8: +Warning: This interactive proof is not started by the "Proof" command. +[missing-proof-command,fragile,default] +Quickfix: +Replace File "./output/MissingProof.v", line 2, characters 2-2 with Proof. + +File "./output/MissingProof.v", line 7, characters 2-3: +Warning: This interactive proof is not started by the "Proof" command. +[missing-proof-command,fragile,default] +Quickfix: +Replace File "./output/MissingProof.v", line 7, characters 2-2 with Proof. + +File "./output/MissingProof.v", line 11, characters 0-9: +Warning: This interactive proof is not started by the "Proof" command. +[missing-proof-command,fragile,default] +Quickfix: +Replace File "./output/MissingProof.v", line 11, characters 0-0 with Proof. + +File "./output/MissingProof.v", line 20, characters 2-13: +The command has indeed failed with message: +Multiple "Proof" commands not supported. +File "./output/MissingProof.v", line 24, characters 2-8: +Warning: This interactive proof is not started by the "Proof" command. +[missing-proof-command,fragile,default] +Quickfix: +Replace File "./output/MissingProof.v", line 24, characters 2-2 with Proof. + +File "./output/MissingProof.v", line 25, characters 2-13: +The command has indeed failed with message: +"Proof" must be the first command in an interactive proof. diff --git a/test-suite/output/MissingProof.v b/test-suite/output/MissingProof.v new file mode 100644 index 000000000000..16573025ddc8 --- /dev/null +++ b/test-suite/output/MissingProof.v @@ -0,0 +1,26 @@ +Goal True. + idtac. + idtac. (* second command doesn't repeat the warning *) +Abort. + +Goal True. + { +Abort. + +Goal True. +Admitted. + +(* abort doesn't warn (NB it would be very annoying to make it warn + because the stm sends the proof data from the proof opening command to Abort) *) +Goal True. +Abort. + +Goal True. +Proof. + Fail Proof. +Abort. + +Goal True. + idtac. + Fail Proof. +Abort. diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out index ecb93f428ece..0c5b7b113abb 100644 --- a/test-suite/output/Naming.out +++ b/test-suite/output/Naming.out @@ -63,18 +63,18 @@ H : a = 0 -> forall a : nat, a = 0 ============================ a = 0 -File "./output/Naming.v", line 101, characters 47-48: +File "./output/Naming.v", line 104, characters 47-48: Warning: Ignoring implicit binder declaration in unexpected position. [unexpected-implicit-declaration,syntax,default] -File "./output/Naming.v", line 105, characters 36-37: +File "./output/Naming.v", line 108, characters 36-37: Warning: Ignoring implicit binder declaration in unexpected position. [unexpected-implicit-declaration,syntax,default] -File "./output/Naming.v", line 106, characters 34-35: +File "./output/Naming.v", line 109, characters 34-35: Warning: Ignoring implicit binder declaration in unexpected position. [unexpected-implicit-declaration,syntax,default] -File "./output/Naming.v", line 112, characters 22-23: +File "./output/Naming.v", line 115, characters 22-23: Warning: Ignoring implicit binder declaration in unexpected position. [unexpected-implicit-declaration,syntax,default] -File "./output/Naming.v", line 112, characters 30-31: +File "./output/Naming.v", line 115, characters 30-31: Warning: Ignoring implicit binder declaration in unexpected position. [unexpected-implicit-declaration,syntax,default] diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v index 4c35296d7c1f..ea03673d3bb5 100644 --- a/test-suite/output/Naming.v +++ b/test-suite/output/Naming.v @@ -7,6 +7,7 @@ Section A. Variable x3:nat. Goal forall x x1 x2 x3:nat, (forall x x3:nat, x+x1 = x2+x3) -> x+x1 = x2+x3. +Proof. Show. intros. Show. @@ -39,6 +40,7 @@ Abort. Goal forall x x1 x2 x3:nat, (forall x x3:nat, x+x1 = x2+x3 -> foo (S x + x1)) -> x+x1 = x2+x3 -> foo (S x). +Proof. Show. unfold foo. Show. @@ -84,6 +86,7 @@ Abort. (* Check naming in hypotheses *) Goal forall a, (a = 0 -> forall a, a = 0) -> a = 0. +Proof. intros. Show. apply H with (a:=a). (* test compliance with printing *) diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index aa8a989b7526..e59623a8e3d7 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -84,7 +84,7 @@ Arguments bar {x} Module Corelib.Init.Peano Notation sym_eq := eq_sym Expands to: Notation Corelib.Init.Logic.sym_eq -Declared in library Corelib.Init.Logic, line 764, characters 0-45 +Declared in library Corelib.Init.Logic, line 767, characters 0-45 eq_sym : forall [A : Type] [x y : A], x = y -> y = x @@ -140,7 +140,7 @@ fst is a projection of prod Arguments fst (A B)%_type_scope p fst is transparent Expands to: Constant PrintInfos.AboutProj.fst -Declared in library PrintInfos, line 57, characters 21-24 +Declared in library PrintInfos, line 59, characters 21-24 fst : forall A B : Type, prod A B -> A fst is not universe polymorphic @@ -148,4 +148,4 @@ fst is a primitive projection of prod Arguments fst (A B)%_type_scope p fst is transparent Expands to: Constant PrintInfos.AboutPrimProj.fst -Declared in library PrintInfos, line 63, characters 21-24 +Declared in library PrintInfos, line 65, characters 21-24 diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v index b32628ee28bf..e2ea98e45b0f 100644 --- a/test-suite/output/PrintInfos.v +++ b/test-suite/output/PrintInfos.v @@ -36,12 +36,14 @@ Print eq_refl. Definition newdef := fun x:nat => x. Goal forall n:nat, n <> newdef n -> newdef n <> n -> False. +Proof. intros n h h'. About n. (* search hypothesis *) About h. (* search hypothesis *) Abort. Goal forall n:nat, let g := newdef in n <> newdef n -> newdef n <> n -> False. +Proof. intros n g h h'. About g. (* search hypothesis *) About h. (* search hypothesis *) diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 1e5d2617bee9..b88bb362732e 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -326,13 +326,13 @@ h: n <> newdef n h: n <> newdef n h: n <> newdef n h': newdef n <> n -File "./output/Search.v", line 23, characters 2-23: +File "./output/Search.v", line 24, characters 2-23: The command has indeed failed with message: [Focus] No such goal. -File "./output/Search.v", line 24, characters 2-25: +File "./output/Search.v", line 25, characters 2-25: The command has indeed failed with message: Query commands only support the single numbered goal selector. -File "./output/Search.v", line 25, characters 2-25: +File "./output/Search.v", line 26, characters 2-25: The command has indeed failed with message: Query commands only support the single numbered goal selector. h: P n diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index 0cfec9581f0e..7e405244df40 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -10,6 +10,7 @@ Search (@eq _ _ _) true -false "prop" -"intro". (* andb_prop *) Definition newdef := fun x:nat => x. Goal forall n:nat, n <> newdef n -> newdef n <> n -> False. +Proof. cut False. intros _ n h h'. Search n. (* search hypothesis *) @@ -26,6 +27,7 @@ Goal forall n:nat, n <> newdef n -> newdef n <> n -> False. Abort. Goal forall n (P:nat -> Prop), P n -> ~P n -> False. +Proof. intros n P h h'. Search P. (* search hypothesis also for patterns *) Search (P _). (* search hypothesis also for patterns *) diff --git a/test-suite/output/SearchPattern.v b/test-suite/output/SearchPattern.v index de9f48873a03..866ed34c5d2b 100644 --- a/test-suite/output/SearchPattern.v +++ b/test-suite/output/SearchPattern.v @@ -21,12 +21,14 @@ SearchPattern (Exc _). Definition newdef := fun x:nat => x. Goal forall n:nat, n <> newdef n -> False. +Proof. intros n h. SearchPattern ( _ <> newdef _). (* search hypothesis *) SearchPattern ( n <> newdef _). (* search hypothesis *) Abort. Goal forall n (P:nat -> Prop), P n -> ~P n -> False. +Proof. intros n P h h'. SearchPattern (P _). (* search hypothesis also for patterns *) Search (~P n). (* search hypothesis also for patterns *) diff --git a/test-suite/output/SearchRewrite.v b/test-suite/output/SearchRewrite.v index 53d043c6816d..eed5801faf20 100644 --- a/test-suite/output/SearchRewrite.v +++ b/test-suite/output/SearchRewrite.v @@ -6,6 +6,7 @@ SearchRewrite (0+_). (* right *) Definition newdef := fun x:nat => x. Goal forall n:nat, n = newdef n -> False. +Proof. intros n h. SearchRewrite (newdef _). SearchRewrite n. (* use hypothesis for patterns *) diff --git a/test-suite/output/Search_bug17963.v b/test-suite/output/Search_bug17963.v index 3ab78ef37ea7..42cfaa697aff 100644 --- a/test-suite/output/Search_bug17963.v +++ b/test-suite/output/Search_bug17963.v @@ -1,4 +1,5 @@ Goal exists y, Some y = Some y :> option nat -> True. +Proof. eexists. intro H. Search Some eq. Abort. diff --git a/test-suite/output/Search_headconcl.v b/test-suite/output/Search_headconcl.v index 8b168dcd25a5..4b0a22e60cac 100644 --- a/test-suite/output/Search_headconcl.v +++ b/test-suite/output/Search_headconcl.v @@ -7,12 +7,14 @@ Search headconcl: (@eq nat). (* complex pattern *) Definition newdef := fun x:nat => x = x. Goal forall n:nat, newdef n -> False. +Proof. intros n h. Search headconcl: newdef. (* search hypothesis *) Abort. Goal forall n (P:nat -> Prop), P n -> False. +Proof. intros n P h. Search headconcl: P. (* search hypothesis also for patterns *) Abort. diff --git a/test-suite/output/ShowUnivs.v b/test-suite/output/ShowUnivs.v index 39abd31ee731..8367ad4f68c2 100644 --- a/test-suite/output/ShowUnivs.v +++ b/test-suite/output/ShowUnivs.v @@ -4,6 +4,7 @@ Show Universes. Abort. Goal True. +Proof. pose (fun x => let y := Type in x y :y). Show Universes. Abort. diff --git a/test-suite/output/SuggestProofUsing.v b/test-suite/output/SuggestProofUsing.v index 449cf38039bf..97ddcce6afde 100644 --- a/test-suite/output/SuggestProofUsing.v +++ b/test-suite/output/SuggestProofUsing.v @@ -8,7 +8,7 @@ Lemma nosec : nat. Proof. exact 0. Qed. Lemma nosec_exactproof : bool. Proof false. Program Definition nosec_program : nat := _. -Next Obligation. exact 1. Qed. +Next Obligation. Proof. exact 1. Qed. Lemma nosec_abstract : nat. Proof. abstract exact 3. Defined. @@ -43,7 +43,7 @@ Section Sec. (* No suggest, is this OK? There's nowhere to put it anyway. *) Program Definition program : nat := _. - Next Obligation. exact 1. Qed. + Next Obligation. Proof. exact 1. Qed. (* Must not suggest *) Lemma sec_abstract : nat. diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 25f68dc74c74..833f131cd088 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -9,10 +9,10 @@ File "./output/Tactics.v", line 23, characters 20-26: The command has indeed failed with message: H is already used. a -File "./output/Tactics.v", line 36, characters 29-34: +File "./output/Tactics.v", line 38, characters 29-34: The command has indeed failed with message: The term "False" has type "Prop" while it is expected to have type "True". -File "./output/Tactics.v", line 42, characters 16-17: +File "./output/Tactics.v", line 45, characters 16-17: The command has indeed failed with message: This variable is used in hypothesis H. Ltac test a b c d e := apply a, b in c as [], d, e as -> diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index a038df046be1..36a1972f6915 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -27,18 +27,21 @@ Abort. (* Test that assert_succeeds only runs a tactic once *) Ltac should_not_loop := idtac + should_not_loop. Goal True. +Proof. assert_succeeds should_not_loop. assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *) Abort. (* assert_succeeds preserves the error *) Goal True. +Proof. Fail assert_succeeds exact False. Abort. Module IntroWildcard. Theorem foo : { p:nat*nat & p = (0,0) } -> True. +Proof. Fail intros ((n,_),H). Abort. diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out index 434ac396538f..289f95aff1f5 100644 --- a/test-suite/output/TypeclassDebug.out +++ b/test-suite/output/TypeclassDebug.out @@ -13,6 +13,6 @@ Debug: 1.1-1.1-1.1-1.1-1 : foo Debug: 1.1-1.1-1.1-1.1-1: looking for foo without backtracking Debug: 1.1-1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s) Debug: 1.1-1.1-1.1-1.1-1.1-1 : foo -File "./output/TypeclassDebug.v", line 13, characters 5-33: +File "./output/TypeclassDebug.v", line 14, characters 5-33: The command has indeed failed with message: Tactic failure: Proof search reached its limit. diff --git a/test-suite/output/TypeclassDebug.v b/test-suite/output/TypeclassDebug.v index 092307f4e13e..1593b1592c67 100644 --- a/test-suite/output/TypeclassDebug.v +++ b/test-suite/output/TypeclassDebug.v @@ -9,6 +9,7 @@ Create HintDb foo. #[global] Hint Resolve H : foo. Goal foo. +Proof. Typeclasses eauto := debug. Fail typeclasses eauto 5 with foo. Abort. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 29badc0be435..ad17a58ec3c0 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -276,21 +276,21 @@ Declared in library UnivBinders, line 227, characters 10-14 File "./output/UnivBinders.v", line 242, characters 2-38: The command has indeed failed with message: Universe u0 already exists. -File "./output/UnivBinders.v", line 249, characters 6-26: +File "./output/UnivBinders.v", line 250, characters 6-26: The command has indeed failed with message: Tactic failure: Not equal (due to universes). eq_rect : forall (A : Type@{eq_rect.u1}) (x : A) (P : A -> Type@{eq_rect.u0}), P x -> forall y : A, x = y -> P y -File "./output/UnivBinders.v", line 267, characters 18-19: +File "./output/UnivBinders.v", line 268, characters 18-19: Warning: Separating sorts from universes with "|" is deprecated. Use ";" instead. [deprecated-sort-poly-syntax,deprecated-since-9.1,deprecated,default] -File "./output/UnivBinders.v", line 267, characters 33-34: +File "./output/UnivBinders.v", line 268, characters 33-34: Warning: Separating sorts from universes with "|" is deprecated. Use ";" instead. [deprecated-sort-poly-syntax,deprecated-since-9.1,deprecated,default] -File "./output/UnivBinders.v", line 273, characters 16-17: +File "./output/UnivBinders.v", line 274, characters 16-17: Warning: Separating sorts from universes with "|" is deprecated. Use ";" instead. [deprecated-sort-poly-syntax,deprecated-since-9.1,deprecated,default] diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index af12fd328a65..79a8d948a78d 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -243,6 +243,7 @@ Module Collision. Definition x := Type. Goal True. + Proof. Fail let a := eval cbv in x.a in let b := eval cbv in x in diff --git a/test-suite/output/UnivNotations.v b/test-suite/output/UnivNotations.v index 6235358847fd..86d97350f72f 100644 --- a/test-suite/output/UnivNotations.v +++ b/test-suite/output/UnivNotations.v @@ -20,6 +20,7 @@ Check foo _ S. Fail Check ! S. Goal True. +Proof. (* sort unification variable matches Type (and is printed as Type in the [forall] annotation) *) (* NB don't use Check here as it collapses before printing (maybe this will change someday?) *) assert (forall A, A -> foo _ A). 2:trivial. @@ -36,6 +37,7 @@ Check ! nat. Check foo _ S. Goal True. +Proof. (* sort unif variable doesn't match Type *) assert (forall A, A -> foo _ A). 2:trivial. Show. diff --git a/test-suite/output/apply_with.out b/test-suite/output/apply_with.out index 32e3c4a4f82a..de8e0ce35f98 100644 --- a/test-suite/output/apply_with.out +++ b/test-suite/output/apply_with.out @@ -1,18 +1,18 @@ -File "./output/apply_with.v", line 3, characters 11-26: +File "./output/apply_with.v", line 4, characters 11-26: The command has indeed failed with message: No such bound variable d (possible names are: a, b and c). -File "./output/apply_with.v", line 4, characters 11-26: +File "./output/apply_with.v", line 5, characters 11-26: The command has indeed failed with message: Unable to find an instance for the variable b. -File "./output/apply_with.v", line 5, characters 24-25: +File "./output/apply_with.v", line 6, characters 24-25: The command has indeed failed with message: No such bound variable d (possible names are: a, b and c). -File "./output/apply_with.v", line 6, characters 5-31: +File "./output/apply_with.v", line 7, characters 5-31: The command has indeed failed with message: Unable to find an instance for the variables b, c. -File "./output/apply_with.v", line 14, characters 23-24: +File "./output/apply_with.v", line 16, characters 23-24: The command has indeed failed with message: No such bound variable c (possible names are: a and b). -File "./output/apply_with.v", line 15, characters 5-16: +File "./output/apply_with.v", line 17, characters 5-16: The command has indeed failed with message: Unable to find an instance for the variables a, b. diff --git a/test-suite/output/apply_with.v b/test-suite/output/apply_with.v index 827fa7a8267c..361737508ba8 100644 --- a/test-suite/output/apply_with.v +++ b/test-suite/output/apply_with.v @@ -1,5 +1,6 @@ Axiom f : forall a b c, a + b = 0 -> c = 0. Goal 0 = 0. +Proof. Fail apply f with (d := 0). Fail apply f with (a := 0). Fail rewrite <- f with (d := 0). @@ -10,6 +11,7 @@ Qed. Axiom g : forall a b, S a = S b. Goal forall n, n = 0. +Proof. intros n. Fail injection g with (c := 0). Fail injection g. diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v index 08d3cdb514a4..5c8b019983ea 100644 --- a/test-suite/output/auto.v +++ b/test-suite/output/auto.v @@ -1,6 +1,7 @@ (* testing info_*/debug auto/eauto *) Goal False \/ (True -> True). +Proof. Succeed info_auto. Succeed debug auto. Succeed info_eauto. @@ -8,5 +9,6 @@ debug eauto. Defined. Goal True. +Proof. info_trivial. Defined. diff --git a/test-suite/output/auto_order.out b/test-suite/output/auto_order.out index c38488d7d714..9a2c2a389997 100644 --- a/test-suite/output/auto_order.out +++ b/test-suite/output/auto_order.out @@ -27,6 +27,6 @@ first fifth, different hintDb fourth third -File "./output/auto_order.v", line 26, characters 5-45: +File "./output/auto_order.v", line 27, characters 5-45: The command has indeed failed with message: Tactic failure: Proof search failed. diff --git a/test-suite/output/auto_order.v b/test-suite/output/auto_order.v index 26381f2fda05..8f8c4b740344 100644 --- a/test-suite/output/auto_order.v +++ b/test-suite/output/auto_order.v @@ -19,6 +19,7 @@ Hint Extern 1 => idtac "fifth, different hintDb"; fail : plus2. Print HintDb plus. Goal False. +Proof. (* auto tries hintdbs in order, ignoring cost. the others apply cost across hintdbs *) info_auto with plus plus2 nocore. diff --git a/test-suite/output/bug5778.out b/test-suite/output/bug5778.out index b90ffd82a71f..9d6b9e7daaaf 100644 --- a/test-suite/output/bug5778.out +++ b/test-suite/output/bug5778.out @@ -1,4 +1,4 @@ -File "./output/bug5778.v", line 7, characters 7-11: +File "./output/bug5778.v", line 8, characters 7-11: The command has indeed failed with message: The term "I" has type "True" which should be Set, Prop or Type. diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v index 441e87af84bf..6bd16c94e519 100644 --- a/test-suite/output/bug5778.v +++ b/test-suite/output/bug5778.v @@ -4,5 +4,6 @@ Ltac b _ := a (). Ltac abs _ := abstract b (). Ltac c _ := abs (). Goal True. +Proof. Fail c (). Abort. diff --git a/test-suite/output/bug6404.out b/test-suite/output/bug6404.out index b57b9934e88f..33c5126a276f 100644 --- a/test-suite/output/bug6404.out +++ b/test-suite/output/bug6404.out @@ -1,4 +1,4 @@ -File "./output/bug6404.v", line 7, characters 7-11: +File "./output/bug6404.v", line 8, characters 7-11: The command has indeed failed with message: The term "I" has type "True" which should be Set, Prop or Type. diff --git a/test-suite/output/bug6404.v b/test-suite/output/bug6404.v index d9e5e20b6653..c9186f00f7b5 100644 --- a/test-suite/output/bug6404.v +++ b/test-suite/output/bug6404.v @@ -4,5 +4,6 @@ Ltac b _ := a (). Ltac abs _ := transparent_abstract b (). Ltac c _ := abs (). Goal True. +Proof. Fail c (). Abort. diff --git a/test-suite/output/bug_11608.out b/test-suite/output/bug_11608.out index 793ff768d40b..074a66154abe 100644 --- a/test-suite/output/bug_11608.out +++ b/test-suite/output/bug_11608.out @@ -1 +1,7 @@ +File "./output/bug_11608.v", line 10, characters 4-40: +Warning: This interactive proof is not started by the "Proof" command. +[missing-proof-command,fragile,default] +Quickfix: +Replace File "./output/bug_11608.v", line 10, characters 4-4 with Proof. + creating x without [Proof.] diff --git a/test-suite/output/bug_13857.out b/test-suite/output/bug_13857.out index 18abb4a0ba28..4d63a4a4fdb3 100644 --- a/test-suite/output/bug_13857.out +++ b/test-suite/output/bug_13857.out @@ -1,9 +1,9 @@ -File "./output/bug_13857.v", line 6, characters 13-16: +File "./output/bug_13857.v", line 7, characters 13-16: The command has indeed failed with message: Unable to find an instance for the variable x. -File "./output/bug_13857.v", line 7, characters 13-17: +File "./output/bug_13857.v", line 8, characters 13-17: The command has indeed failed with message: Unable to unify "foo2" with "foo". -File "./output/bug_13857.v", line 8, characters 13-17: +File "./output/bug_13857.v", line 9, characters 13-17: The command has indeed failed with message: Unable to unify "foo3" with "foo". diff --git a/test-suite/output/bug_13857.v b/test-suite/output/bug_13857.v index 9578b18c6ef7..4fdaa6e64700 100644 --- a/test-suite/output/bug_13857.v +++ b/test-suite/output/bug_13857.v @@ -3,6 +3,7 @@ Inductive foo2 := Foo2 (x : nat). Inductive foo3 := Foo3 (f : foo2). Goal foo. +Proof. Fail apply Foo. Fail apply Foo2. Fail apply Foo3. diff --git a/test-suite/output/bug_14899.v b/test-suite/output/bug_14899.v index 9355239296a8..b95fc83f7147 100644 --- a/test-suite/output/bug_14899.v +++ b/test-suite/output/bug_14899.v @@ -1,4 +1,5 @@ Definition a : { x | 0 < x }. +Proof. exists 3. eauto. Defined. diff --git a/test-suite/output/bug_15106.v b/test-suite/output/bug_15106.v index c971370850df..365aa73f7008 100644 --- a/test-suite/output/bug_15106.v +++ b/test-suite/output/bug_15106.v @@ -6,4 +6,7 @@ Axiom P : Prop. Axiom p : P. Program Definition foo := (fun (x : P) (y : True) => I) _ _. Fail Obligation 2. -Obligation 1. exact p. Qed. +Obligation 1. +Proof. + exact p. +Qed. diff --git a/test-suite/output/bug_17372.out b/test-suite/output/bug_17372.out index b96da0b6c40d..3af74abb0ba6 100644 --- a/test-suite/output/bug_17372.out +++ b/test-suite/output/bug_17372.out @@ -1,3 +1,3 @@ -File "./output/bug_17372.v", line 2, characters 13-16: +File "./output/bug_17372.v", line 3, characters 13-16: The command has indeed failed with message: The reference bar was not found in the current environment. diff --git a/test-suite/output/bug_17372.v b/test-suite/output/bug_17372.v index a82059322d02..de80642e8038 100644 --- a/test-suite/output/bug_17372.v +++ b/test-suite/output/bug_17372.v @@ -1,3 +1,4 @@ Goal Prop. +Proof. Fail refine (bar (A := nat)). Abort. diff --git a/test-suite/output/bug_17386.v b/test-suite/output/bug_17386.v index 280c3eba5339..4c6e6531a1a3 100644 --- a/test-suite/output/bug_17386.v +++ b/test-suite/output/bug_17386.v @@ -1,4 +1,5 @@ Goal True. +Proof. evar (x:nat). pose (y:=1). let _ := constr:(eq_refl : x = 1) in idtac. diff --git a/test-suite/output/bug_17594.out b/test-suite/output/bug_17594.out index 3c378791af12..fb934f1c2117 100644 --- a/test-suite/output/bug_17594.out +++ b/test-suite/output/bug_17594.out @@ -2,47 +2,47 @@ 3 2 3 -File "./output/bug_17594.v", line 12, characters 19-20: +File "./output/bug_17594.v", line 13, characters 19-20: The command has indeed failed with message: The term "0" has type "nat" while it is expected to have type "True". 1 3 2 3 -File "./output/bug_17594.v", line 17, characters 26-27: +File "./output/bug_17594.v", line 18, characters 26-27: The command has indeed failed with message: The term "0" has type "nat" while it is expected to have type "True". 1 3 2 3 -File "./output/bug_17594.v", line 23, characters 19-20: +File "./output/bug_17594.v", line 24, characters 19-20: The command has indeed failed with message: The term "0" has type "nat" while it is expected to have type "True". 1 3 2 3 -File "./output/bug_17594.v", line 28, characters 26-27: +File "./output/bug_17594.v", line 29, characters 26-27: The command has indeed failed with message: The term "0" has type "nat" while it is expected to have type "True". 1 3 -File "./output/bug_17594.v", line 31, characters 2-106: +File "./output/bug_17594.v", line 32, characters 2-106: The command has indeed failed with message: Uncaught Ltac2 exception: Match_failure 1 3 -File "./output/bug_17594.v", line 37, characters 2-113: +File "./output/bug_17594.v", line 38, characters 2-113: The command has indeed failed with message: No matching clauses for match. 1 3 -File "./output/bug_17594.v", line 42, characters 2-119: +File "./output/bug_17594.v", line 43, characters 2-119: The command has indeed failed with message: No matching clauses for match. 1 3 -File "./output/bug_17594.v", line 48, characters 2-119: +File "./output/bug_17594.v", line 49, characters 2-119: The command has indeed failed with message: No matching clauses for match. diff --git a/test-suite/output/bug_17594.v b/test-suite/output/bug_17594.v index f46e2e5fde56..2d711a58540d 100644 --- a/test-suite/output/bug_17594.v +++ b/test-suite/output/bug_17594.v @@ -4,6 +4,7 @@ From Ltac2 Require Import Message. Ltac2 msg s := print (of_string s). Goal True. +Proof. (* should be the exact error *) Fail multi_match! 'True with | True => msg "1" diff --git a/test-suite/output/bug_18368.v b/test-suite/output/bug_18368.v index 950df239d38c..de549354e34a 100644 --- a/test-suite/output/bug_18368.v +++ b/test-suite/output/bug_18368.v @@ -2,5 +2,6 @@ Tactic Notation (at level 4) "test" := idtac "A". Tactic Notation (at level 5) "test" := idtac "B". Goal True. +Proof. test. Abort. diff --git a/test-suite/output/bug_19138.v b/test-suite/output/bug_19138.v index e8ba77411071..64cce835567f 100644 --- a/test-suite/output/bug_19138.v +++ b/test-suite/output/bug_19138.v @@ -2,6 +2,7 @@ From Ltac2 Require Import Ltac2 Constr. Import Constr.Unsafe. Goal True. +Proof. let t := open_constr:(_ :> False) in match kind t with | Evar e _ => Control.new_goal e > [refine 'I|] @@ -11,6 +12,7 @@ Goal True. Abort. Goal True. +Proof. let t := unshelve open_constr:(_ :> False) in Control.extend [Control.shelve] (fun () => ()) []; match kind t with diff --git a/test-suite/output/bug_21288.out b/test-suite/output/bug_21288.out index 3d81633abf32..04dbead50214 100644 --- a/test-suite/output/bug_21288.out +++ b/test-suite/output/bug_21288.out @@ -1,5 +1,5 @@ Ltac foo := (intuition idtac) || fail "boom" Ltac bar := intuition idtac || fail "baam" -File "./output/bug_21288.v", line 12, characters 7-10: +File "./output/bug_21288.v", line 13, characters 7-10: The command has indeed failed with message: Tactic failure: baam. diff --git a/test-suite/output/bug_21288.v b/test-suite/output/bug_21288.v index b57625a37237..0f17a63a93fc 100644 --- a/test-suite/output/bug_21288.v +++ b/test-suite/output/bug_21288.v @@ -7,6 +7,7 @@ Print Ltac foo. Print Ltac bar. Goal True -> 2 = 3. +Proof. (* yet foo is not equivalent to bar ( "||" runs the second tactic if the first doesn't make progress) *) Succeed foo. Fail bar. diff --git a/test-suite/output/bug_3810.v b/test-suite/output/bug_3810.v index 906b0f37d479..78cbd558f969 100644 --- a/test-suite/output/bug_3810.v +++ b/test-suite/output/bug_3810.v @@ -1,6 +1,7 @@ Class Foo. Fixpoint test (H : Foo) (n : nat) {A : Type} {struct n} : A. +Proof. Admitted. About test. diff --git a/test-suite/output/idtac.v b/test-suite/output/idtac.v index ac60ea91759c..4ff7e65ea2b2 100644 --- a/test-suite/output/idtac.v +++ b/test-suite/output/idtac.v @@ -2,37 +2,46 @@ Tactic Notation "myidtac" string(v) := idtac v. Goal True. +Proof. myidtac "foo". Abort. Tactic Notation "myidtac2" ref(c) := idtac c. Goal True. +Proof. myidtac2 True. Abort. Tactic Notation "myidtac3" preident(s) := idtac s. Goal True. +Proof. myidtac3 foo. Abort. Tactic Notation "myidtac4" int_or_var(n) := idtac n. Goal True. +Proof. myidtac4 3. Abort. Tactic Notation "myidtac5" ident(id) := idtac id. Goal True. +Proof. myidtac5 foo. Abort. (* Checking non focussing of idtac for integers *) -Goal True/\True. split. +Goal True/\True. +Proof. +split. all:let c:=numgoals in idtac c. Abort. (* Checking printing of lists and its focussing *) Tactic Notation "myidtac6" constr_list(l) := idtac "<" l ">". -Goal True/\True. split. +Goal True/\True. +Proof. +split. all:myidtac6 True False Prop. (* An empty list is focussing because of interp_genarg of a constr *) (* even if it is not focussing on printing *) @@ -40,6 +49,8 @@ all:myidtac6. Abort. Tactic Notation "myidtac7" int_list(l) := idtac "<<" l ">>". -Goal True/\True. split. +Goal True/\True. +Proof. +split. all:myidtac7 1 2 3. Abort. diff --git a/test-suite/output/injection.out b/test-suite/output/injection.out index f0c48c95efb8..555ef6872b61 100644 --- a/test-suite/output/injection.out +++ b/test-suite/output/injection.out @@ -1,6 +1,6 @@ -File "./output/injection.v", line 4, characters 39-42: +File "./output/injection.v", line 5, characters 39-42: The command has indeed failed with message: Unexpected pattern. -File "./output/injection.v", line 5, characters 35-42: +File "./output/injection.v", line 6, characters 35-42: The command has indeed failed with message: Unexpected injection pattern. diff --git a/test-suite/output/injection.v b/test-suite/output/injection.v index bfd5a67bf549..c7015c5349a3 100644 --- a/test-suite/output/injection.v +++ b/test-suite/output/injection.v @@ -1,6 +1,7 @@ (* Test error messages *) Goal forall x, (x,0) = (0, S x) -> x = 0. +Proof. Fail intros x H; injection H as [= H'] H''. Fail intros x H; injection H as H' [= H'']. intros x H; injection H as [= H' H'']. diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index c6c2f7d97824..e60d33a1f27b 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,40 +1,40 @@ -File "./output/ltac.v", line 8, characters 13-31: +File "./output/ltac.v", line 9, characters 13-31: The command has indeed failed with message: Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := symmetry in x, y; auto with z; auto; intros; clearbody x; generalize dependent z -File "./output/ltac.v", line 38, characters 5-9: +File "./output/ltac.v", line 41, characters 5-9: The command has indeed failed with message: The term "I" has type "True" while it is expected to have type "False". In nested Ltac calls to "g1" and "refine (uconstr)", last call failed. -File "./output/ltac.v", line 39, characters 5-9: +File "./output/ltac.v", line 42, characters 5-9: The command has indeed failed with message: The term "I" has type "True" while it is expected to have type "False". In nested Ltac calls to "f1 (constr)" and "refine (uconstr)", last call failed. -File "./output/ltac.v", line 40, characters 5-9: +File "./output/ltac.v", line 43, characters 5-9: The command has indeed failed with message: The term "I" has type "True" while it is expected to have type "False". In nested Ltac calls to "g2 (constr)", "g1" and "refine (uconstr)", last call failed. -File "./output/ltac.v", line 41, characters 5-9: +File "./output/ltac.v", line 44, characters 5-9: The command has indeed failed with message: The term "I" has type "True" while it is expected to have type "False". In nested Ltac calls to "f2", "f1 (constr)" and "refine (uconstr)", last call failed. -File "./output/ltac.v", line 46, characters 5-8: +File "./output/ltac.v", line 50, characters 5-8: The command has indeed failed with message: No primitive equality found. In nested Ltac calls to "h" and "injection (destruction_arg)", last call failed. -File "./output/ltac.v", line 48, characters 5-8: +File "./output/ltac.v", line 52, characters 5-8: The command has indeed failed with message: No primitive equality found. In nested Ltac calls to "h" and "injection (destruction_arg)", last call diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index fcd5dd05f04a..2cfa2eec71a0 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -2,6 +2,7 @@ Set Ltac Backtrace. (* This used to refer to b instead of z sometimes between 8.4 and 8.5beta3 *) Goal True. +Proof. Fail let T := constr:((fun a b : nat => a+b) 1 1) in lazymatch T with | (fun x z => ?y) 1 1 @@ -11,6 +12,7 @@ Abort. (* This should not raise a warning (see #4317) *) Goal True. +Proof. assert (H:= eq_refl ((fun x => x) 1)). let HT := type of H in lazymatch goal with @@ -35,6 +37,7 @@ Tactic Notation "g2" constr(x) := g1 x. Tactic Notation "f1" constr(x) := refine x. Ltac f2 x := f1 x. Goal False. +Proof. Fail g1 I. Fail f1 I. Fail g2 I. @@ -43,6 +46,7 @@ Abort. Ltac h x := injection x. Goal True -> False. +Proof. Fail h I. intro H. Fail h H. @@ -51,12 +55,15 @@ Abort. (* Check printing of the "var" argument "Hx" *) Ltac m H := idtac H; exact H. Goal True. +Proof. let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac. Abort. (* Check consistency of interpretation scopes (#4398) *) -Goal nat*(0*0=0) -> nat*(0*0=0). intro. +Goal nat*(0*0=0) -> nat*(0*0=0). +Proof. +intro. match goal with H: ?x*?y |- _ => idtac x end. match goal with |- ?x*?y => idtac x end. match goal with H: context [?x*?y] |- _ => idtac x end. @@ -77,6 +84,7 @@ Print Ltac foo. (* Ltac renaming was not applied to "fix" and "cofix" *) Goal forall a, a = 0. +Proof. match goal with |- (forall x, x = _) => assert (forall n, (fix x n := match n with O => O | S n => x n end) n = n) end. diff --git a/test-suite/output/ltac2_bt.v b/test-suite/output/ltac2_bt.v index 67e75f85c396..dcda47ce54c8 100644 --- a/test-suite/output/ltac2_bt.v +++ b/test-suite/output/ltac2_bt.v @@ -18,5 +18,6 @@ Ltac2 g () := print_stack (). Ltac2 h () := g (). Goal True. +Proof. h (). Abort. diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out index f08e9f855f56..f13c326b1bfa 100644 --- a/test-suite/output/ltac_missing_args.out +++ b/test-suite/output/ltac_missing_args.out @@ -1,39 +1,39 @@ -File "./output/ltac_missing_args.v", line 11, characters 2-11: +File "./output/ltac_missing_args.v", line 12, characters 2-11: The command has indeed failed with message: The user-defined tactic "foo" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. Ltac call to "foo" failed. -File "./output/ltac_missing_args.v", line 12, characters 2-11: +File "./output/ltac_missing_args.v", line 13, characters 2-11: The command has indeed failed with message: The user-defined tactic "bar" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. Ltac call to "bar" failed. -File "./output/ltac_missing_args.v", line 13, characters 2-16: +File "./output/ltac_missing_args.v", line 14, characters 2-16: The command has indeed failed with message: The user-defined tactic "bar" was not fully applied: There is a missing argument for variable y and 1 more, 1 argument was provided. Ltac call to "bar" failed. -File "./output/ltac_missing_args.v", line 14, characters 2-11: +File "./output/ltac_missing_args.v", line 15, characters 2-11: The command has indeed failed with message: The user-defined tactic "baz" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. In nested Ltac calls to "baz" and "foo", last call failed. -File "./output/ltac_missing_args.v", line 15, characters 2-11: +File "./output/ltac_missing_args.v", line 16, characters 2-11: The command has indeed failed with message: The user-defined tactic "qux" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. In nested Ltac calls to "qux" and "bar", last call failed. -File "./output/ltac_missing_args.v", line 16, characters 2-36: +File "./output/ltac_missing_args.v", line 17, characters 2-36: The command has indeed failed with message: The user-defined tactic "mydo" was not fully applied: There is a missing argument for variable _, @@ -41,25 +41,25 @@ no arguments at all were provided. In nested Ltac calls to "mydo" and "tac" (bound to fun _ _ => idtac), last call failed. -File "./output/ltac_missing_args.v", line 17, characters 2-42: +File "./output/ltac_missing_args.v", line 18, characters 2-42: The command has indeed failed with message: An unnamed user-defined tactic was not fully applied: There is a missing argument for variable _, no arguments at all were provided. -File "./output/ltac_missing_args.v", line 18, characters 2-24: +File "./output/ltac_missing_args.v", line 19, characters 2-24: The command has indeed failed with message: An unnamed user-defined tactic was not fully applied: There is a missing argument for variable _, no arguments at all were provided. -File "./output/ltac_missing_args.v", line 19, characters 2-16: +File "./output/ltac_missing_args.v", line 20, characters 2-16: The command has indeed failed with message: The user-defined tactic "rec" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. In nested Ltac calls to "rec" and "rec", last call failed. -File "./output/ltac_missing_args.v", line 20, characters 2-40: +File "./output/ltac_missing_args.v", line 21, characters 2-40: The command has indeed failed with message: An unnamed user-defined tactic was not fully applied: There is a missing argument for variable x, 1 argument was provided. diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v index e30c97aac664..b111d0616fcb 100644 --- a/test-suite/output/ltac_missing_args.v +++ b/test-suite/output/ltac_missing_args.v @@ -8,6 +8,7 @@ Ltac mydo tac := tac (). Ltac rec x := rec. Goal True. +Proof. Fail foo. Fail bar. Fail bar True. diff --git a/test-suite/output/names.v b/test-suite/output/names.v index e9033bd73280..7856c5d4e13d 100644 --- a/test-suite/output/names.v +++ b/test-suite/output/names.v @@ -5,6 +5,7 @@ Parameter a : forall x, {y:nat|x=y}. Fail Definition b y : {x:nat|x=y} := a y. Goal (forall n m, n <= m -> m <= n -> n = m) -> True. +Proof. intro H; epose proof (H _ 3) as H. Show. Abort. diff --git a/test-suite/output/optimize_heap.v b/test-suite/output/optimize_heap.v index 31b451039776..15c47e9d2e58 100644 --- a/test-suite/output/optimize_heap.v +++ b/test-suite/output/optimize_heap.v @@ -1,6 +1,7 @@ (* optimize_heap should not affect the proof state *) Goal True. +Proof. idtac. Show. optimize_heap. diff --git a/test-suite/output/print_hintdb_metas.v b/test-suite/output/print_hintdb_metas.v index 36410050537c..c35bb449d11d 100644 --- a/test-suite/output/print_hintdb_metas.v +++ b/test-suite/output/print_hintdb_metas.v @@ -1,4 +1,5 @@ Theorem x : forall n m:nat, n = 1 /\ forall n : nat, n = m. +Proof. Admitted. Create HintDb foo. Hint Resolve x : foo. diff --git a/test-suite/output/rewrite_in_err.out b/test-suite/output/rewrite_in_err.out index c32d4838f84d..16ae621c7149 100644 --- a/test-suite/output/rewrite_in_err.out +++ b/test-suite/output/rewrite_in_err.out @@ -1,3 +1,3 @@ -File "./output/rewrite_in_err.v", line 6, characters 7-23: +File "./output/rewrite_in_err.v", line 7, characters 7-23: The command has indeed failed with message: Found no subterm matching "i" in H. diff --git a/test-suite/output/rewrite_in_err.v b/test-suite/output/rewrite_in_err.v index 85db8edbca32..3cc9022b8eac 100644 --- a/test-suite/output/rewrite_in_err.v +++ b/test-suite/output/rewrite_in_err.v @@ -3,6 +3,7 @@ Require Export Morphisms. Axiom T : nat -> Prop. Lemma test i j (Hle : i <= j) (H : T j) : T j. +Proof. Fail rewrite Hle in H. (* The command has indeed failed with message: Found no subterm matching "i" in the current goal. *) diff --git a/test-suite/output/set.v b/test-suite/output/set.v index 0e745354ab3a..28737aadf6a4 100644 --- a/test-suite/output/set.v +++ b/test-suite/output/set.v @@ -1,4 +1,5 @@ Goal let x:=O+O in x=x. +Proof. intro. set (y1:=O) in (type of x). Show. diff --git a/test-suite/output/sort_poly_elab.out b/test-suite/output/sort_poly_elab.out index 9d36d74f87c4..1985d1a1d71b 100644 --- a/test-suite/output/sort_poly_elab.out +++ b/test-suite/output/sort_poly_elab.out @@ -725,13 +725,13 @@ Arguments bool_to_Prop' b bool_to_Prop' is transparent Expands to: Constant sort_poly_elab.Inductives.bool_to_Prop' Declared in library sort_poly_elab, line 490, characters 21-34 -File "./output/sort_poly_elab.v", line 502, characters 58-60: +File "./output/sort_poly_elab.v", line 503, characters 58-60: The command has indeed failed with message: The term "tt" has type "unit" while it is expected to have type "?P@{b:=true@{Test ; }}" (unable to find a well-typed instantiation for "?P": cannot ensure that "Set" is a subtype of "Type@{Test ; sort_poly_elab.350}"). -File "./output/sort_poly_elab.v", line 510, characters 58-66: +File "./output/sort_poly_elab.v", line 511, characters 58-66: The command has indeed failed with message: The term "testctor" has type "testind" while it is expected to have type "?P@{b:=true@{Test ; }}" @@ -752,7 +752,7 @@ unit@{α ; u} may only be eliminated to produce values whose type is in sort qua (SProp <= Prop <= Type, and all variables <= Type) than the instantiation of α. Expands to: Inductive sort_poly_elab.Inductives.unit -Declared in library sort_poly_elab, line 518, characters 12-16 +Declared in library sort_poly_elab, line 519, characters 12-16 FooNat@{α ; } : Type@{α ; Set} (* α ; |= *) @@ -763,7 +763,7 @@ FooNat@{α ; } may only be eliminated to produce values whose type is in sort qu (SProp <= Prop <= Type, and all variables <= Type) than the instantiation of α. Expands to: Inductive sort_poly_elab.Inductives.FooNat -Declared in library sort_poly_elab, line 526, characters 12-18 +Declared in library sort_poly_elab, line 527, characters 12-18 Foo@{α α0 ; } : forall _ : FooNat@{α ; }, FooNat@{α0 ; } (* α α0 ; |= α -> α0 *) @@ -772,15 +772,15 @@ Foo is universe polymorphic Arguments Foo n Foo is transparent Expands to: Constant sort_poly_elab.Inductives.Foo -Declared in library sort_poly_elab, line 531, characters 13-16 +Declared in library sort_poly_elab, line 532, characters 13-16 Foo@{Type Prop ; } : forall _ : FooNat@{Type ; }, FooNat@{Prop ; } -File "./output/sort_poly_elab.v", line 539, characters 2-30: +File "./output/sort_poly_elab.v", line 541, characters 2-30: The command has indeed failed with message: The quality constraints are inconsistent: cannot enforce Prop -> Type because it would identify Type and Prop which is inconsistent. This is introduced by the constraints Prop -> Type -File "./output/sort_poly_elab.v", line 548, characters 2-30: +File "./output/sort_poly_elab.v", line 550, characters 2-30: The command has indeed failed with message: The record R1 could not be defined as a primitive record because it has no projections. [non-primitive-record,records,default] @@ -791,7 +791,7 @@ R2 is universe polymorphic R2 has primitive projections with eta conversion depending on sort instantiation. Arguments R2 A%_type_scope Expands to: Inductive sort_poly_elab.Records.R2 -Declared in library sort_poly_elab, line 550, characters 9-11 +Declared in library sort_poly_elab, line 552, characters 9-11 R3@{α α0 ; u} : forall _ : Type@{α ; u}, Type@{α0 ; u} (* α α0 ; u |= α0 -> α *) @@ -800,7 +800,7 @@ R3 is universe polymorphic R3 has primitive projections with eta conversion depending on sort instantiation. Arguments R3 A%_type_scope Expands to: Inductive sort_poly_elab.Records.R3 -Declared in library sort_poly_elab, line 554, characters 9-11 +Declared in library sort_poly_elab, line 556, characters 9-11 R4@{s ; } : forall _ : Type@{s ; Set}, Type@{s ; Set} (* s ; |= *) @@ -808,8 +808,8 @@ R4 is universe polymorphic R4 has primitive projections with eta conversion. Arguments R4 A%_type_scope Expands to: Inductive sort_poly_elab.Records.R4 -Declared in library sort_poly_elab, line 559, characters 9-11 -File "./output/sort_poly_elab.v", line 563, characters 2-49: +Declared in library sort_poly_elab, line 561, characters 9-11 +File "./output/sort_poly_elab.v", line 565, characters 2-49: The command has indeed failed with message: The record R5 could not be defined as a primitive record because it is squashed. [non-primitive-record,records,default] @@ -820,7 +820,7 @@ R5 is universe polymorphic R5@{α ; u} may only be eliminated to produce values whose type is SProp. Arguments R5 A%_type_scope Expands to: Inductive sort_poly_elab.Records.R5 -Declared in library sort_poly_elab, line 565, characters 11-13 +Declared in library sort_poly_elab, line 567, characters 11-13 R6@{s ; } : forall _ : Type@{s ; Set}, Set (* s ; |= *) @@ -828,7 +828,7 @@ R6 is universe polymorphic R6 has primitive projections with eta conversion. Arguments R6 A%_type_scope Expands to: Inductive sort_poly_elab.Records.R6 -Declared in library sort_poly_elab, line 570, characters 9-11 +Declared in library sort_poly_elab, line 572, characters 9-11 fun (A : SProp) (x y : R6@{SProp ; } A) => @eq_refl (Conversion.Box@{SProp Type ; sort_poly_elab.365} A) (Conversion.box@{SProp Type ; sort_poly_elab.365} A (R6f1 _ x)) @@ -841,7 +841,7 @@ fun (A : SProp) (x y : R6@{SProp ; } A) => (Conversion.box@{SProp Type ; sort_poly_elab.365} A (R6f1 _ x)) (Conversion.box@{SProp Type ; sort_poly_elab.365} A (R6f1 _ y)) (* {sort_poly_elab.365} |= *) -File "./output/sort_poly_elab.v", line 576, characters 10-17: +File "./output/sort_poly_elab.v", line 578, characters 10-17: The command has indeed failed with message: In environment A : Prop @@ -860,7 +860,7 @@ while it is expected to have type (Conversion.box@{α380 Type ; sort_poly_elab.369} A (R6f1 _ y))" (cannot unify "Conversion.box@{α380 Type ; sort_poly_elab.369} A (R6f1 _ x)" and "Conversion.box@{α380 Type ; sort_poly_elab.369} A (R6f1 _ y)"). -File "./output/sort_poly_elab.v", line 578, characters 10-17: +File "./output/sort_poly_elab.v", line 580, characters 10-17: The command has indeed failed with message: In environment A : SProp @@ -891,7 +891,7 @@ R7@{α α0 ; u} may only be eliminated to produce values whose type is in sort q than the instantiation of α0. Arguments R7 A%_type_scope Expands to: Inductive sort_poly_elab.Records.R7 -Declared in library sort_poly_elab, line 581, characters 38-40 +Declared in library sort_poly_elab, line 583, characters 38-40 R7f1@{α α0 ; u} : forall (A : Type@{α ; u}) (_ : R7@{α α0 ; u} A), A (* α α0 ; u |= α0 -> α *) @@ -901,7 +901,7 @@ R7f1 is a projection of R7 Arguments R7f1 A%_type_scope r R7f1 is transparent Expands to: Constant sort_poly_elab.Records.R7f1 -Declared in library sort_poly_elab, line 581, characters 55-59 +Declared in library sort_poly_elab, line 583, characters 55-59 R7f2@{α α0 ; u} : forall (A : Type@{α ; u}) (_ : R7@{α α0 ; u} A), nat (* α α0 ; u |= α0 -> Type *) @@ -911,7 +911,7 @@ R7f2 is a projection of R7 Arguments R7f2 A%_type_scope r R7f2 is transparent Expands to: Constant sort_poly_elab.Records.R7f2 -Declared in library sort_poly_elab, line 581, characters 65-69 +Declared in library sort_poly_elab, line 583, characters 65-69 Rsigma@{s ; u v} : forall (A : Type@{s ; u}) (_ : forall _ : A, Type@{s ; v}), Type@{s ; max(u,v)} @@ -921,7 +921,7 @@ Rsigma is universe polymorphic Rsigma has primitive projections with eta conversion. Arguments Rsigma A%_type_scope B%_function_scope Expands to: Inductive sort_poly_elab.Records.Rsigma -Declared in library sort_poly_elab, line 592, characters 9-15 +Declared in library sort_poly_elab, line 594, characters 9-15 Rsigma_srect@{α α0 ; u u0 u1} : forall (A : Type@{α ; u}) (B : forall _ : A, Type@{α ; u0}) (P : forall _ : Rsigma@{α ; u u0} A B, Type@{α0 ; u1}) @@ -934,7 +934,7 @@ Rsigma_srect is universe polymorphic Arguments Rsigma_srect A%_type_scope (B P H)%_function_scope s Rsigma_srect is transparent Expands to: Constant sort_poly_elab.Records.Rsigma_srect -Declared in library sort_poly_elab, line 597, characters 13-25 +Declared in library sort_poly_elab, line 599, characters 13-25 sexists@{α ; u} : forall (A : Type@{α ; u}) (_ : forall _ : A, Prop), Prop (* α ; u |= *) @@ -944,7 +944,7 @@ sexists@{α ; u} may only be eliminated to produce values whose type is SProp or unless instantiated such that the quality α is SProp or Prop. Arguments sexists A%_type_scope B%_function_scope Expands to: Inductive sort_poly_elab.Records.sexists -Declared in library sort_poly_elab, line 611, characters 12-19 +Declared in library sort_poly_elab, line 613, characters 12-19 sexists_ind@{Type ; sort_poly_elab.396} : forall (A : Type@{sort_poly_elab.396}) (B : forall _ : A, Prop) @@ -962,7 +962,7 @@ R8@{α α0 ; u} may only be eliminated to produce values whose type is in sort q (SProp <= Prop <= Type, and all variables <= Type) than the instantiation of α. Expands to: Inductive sort_poly_elab.Records.R8 -Declared in library sort_poly_elab, line 621, characters 9-11 +Declared in library sort_poly_elab, line 623, characters 9-11 R8f1@{α α0 ; u} : forall _ : R8@{α α0 ; u}, Type@{α0 ; u} (* α α0 ; u |= α -> Type *) @@ -972,7 +972,7 @@ R8f1 is a projection of R8 Arguments R8f1 r R8f1 is transparent Expands to: Constant sort_poly_elab.Records.R8f1 -Declared in library sort_poly_elab, line 622, characters 4-8 +Declared in library sort_poly_elab, line 624, characters 4-8 R8f2@{α α0 ; u} : forall r : R8@{α α0 ; u}, R8f1@{α α0 ; u} r (* α α0 ; u |= α -> α0 @@ -983,7 +983,7 @@ R8f2 is a projection of R8 Arguments R8f2 r R8f2 is transparent Expands to: Constant sort_poly_elab.Records.R8f2 -Declared in library sort_poly_elab, line 623, characters 4-8 +Declared in library sort_poly_elab, line 625, characters 4-8 R9@{α α0 α1 ; } : Type@{α ; Set} (* α α0 α1 ; |= *) @@ -994,7 +994,7 @@ R9@{α α0 α1 ; } may only be eliminated to produce values whose type is in sor (SProp <= Prop <= Type, and all variables <= Type) than the instantiation of α. Expands to: Inductive sort_poly_elab.Records.R9 -Declared in library sort_poly_elab, line 641, characters 9-11 +Declared in library sort_poly_elab, line 643, characters 9-11 R9f1@{α α0 α1 ; } : forall _ : R9@{α α0 α1 ; }, bool@{α0 ; } (* α α0 α1 ; |= α -> α0 *) @@ -1004,7 +1004,7 @@ R9f1 is a projection of R9 Arguments R9f1 r R9f1 is transparent Expands to: Constant sort_poly_elab.Records.R9f1 -Declared in library sort_poly_elab, line 642, characters 4-8 +Declared in library sort_poly_elab, line 644, characters 4-8 R9f2@{α α0 α1 ; } : forall _ : R9@{α α0 α1 ; }, bool@{α1 ; } (* α α0 α1 ; |= α -> α1 *) @@ -1014,7 +1014,7 @@ R9f2 is a projection of R9 Arguments R9f2 r R9f2 is transparent Expands to: Constant sort_poly_elab.Records.R9f2 -Declared in library sort_poly_elab, line 643, characters 4-8 +Declared in library sort_poly_elab, line 645, characters 4-8 R10@{α α0 α1 α2 ; u u0} : forall _ : Type@{α0 ; u}, Type@{α ; max(Set,u,u0)} (* α α0 α1 α2 ; u u0 |= *) @@ -1027,7 +1027,7 @@ R10@{α α0 α1 α2 ; u u0} may only be eliminated to produce values whose type than the instantiation of α. Arguments R10 A%_type_scope Expands to: Inductive sort_poly_elab.Records.R10 -Declared in library sort_poly_elab, line 655, characters 9-12 +Declared in library sort_poly_elab, line 657, characters 9-12 R10f1@{α α0 α1 α2 ; u u0} : forall (A : Type@{α0 ; u}) (_ : R10@{α α0 α1 α2 ; u u0} A), A (* α α0 α1 α2 ; u u0 |= α -> α0 *) @@ -1037,7 +1037,7 @@ R10f1 is a projection of R10 Arguments R10f1 A%_type_scope r R10f1 is transparent Expands to: Constant sort_poly_elab.Records.R10f1 -Declared in library sort_poly_elab, line 656, characters 4-9 +Declared in library sort_poly_elab, line 658, characters 4-9 R10f2@{α α0 α1 α2 ; u u0} : forall (A : Type@{α0 ; u}) (r : R10@{α α0 α1 α2 ; u u0} A), @eq@{α0 α1 ; u u0} A (R10f1@{α α0 α1 α2 ; u u0} A r) @@ -1050,7 +1050,7 @@ R10f2 is a projection of R10 Arguments R10f2 A%_type_scope r R10f2 is transparent Expands to: Constant sort_poly_elab.Records.R10f2 -Declared in library sort_poly_elab, line 657, characters 4-9 +Declared in library sort_poly_elab, line 659, characters 4-9 R10f3@{α α0 α1 α2 ; u u0} : forall (A : Type@{α0 ; u}) (_ : R10@{α α0 α1 α2 ; u u0} A), bool@{α2 ; } (* α α0 α1 α2 ; u u0 |= α -> α2 *) @@ -1060,7 +1060,7 @@ R10f3 is a projection of R10 Arguments R10f3 A%_type_scope r R10f3 is transparent Expands to: Constant sort_poly_elab.Records.R10f3 -Declared in library sort_poly_elab, line 658, characters 4-9 +Declared in library sort_poly_elab, line 660, characters 4-9 R11@{α α0 α1 α2 α3 α4 α5 ; u} : Type@{α ; Set} (* α α0 α1 α2 α3 α4 α5 ; u |= α0 -> α3 @@ -1073,7 +1073,7 @@ R11@{α α0 α1 α2 α3 α4 α5 ; u} may only be eliminated to produce values wh (SProp <= Prop <= Type, and all variables <= Type) than the instantiation of α. Expands to: Inductive sort_poly_elab.Records.R11 -Declared in library sort_poly_elab, line 674, characters 9-12 +Declared in library sort_poly_elab, line 676, characters 9-12 R11f1@{α α0 α1 α2 α3 α4 α5 ; u} : forall _ : R11@{α α0 α1 α2 α3 α4 α5 ; u}, bool@{α3 ; } (* α α0 α1 α2 α3 α4 α5 ; u |= α -> α3 @@ -1085,7 +1085,7 @@ R11f1 is a projection of R11 Arguments R11f1 r R11f1 is transparent Expands to: Constant sort_poly_elab.Records.R11f1 -Declared in library sort_poly_elab, line 675, characters 4-9 +Declared in library sort_poly_elab, line 677, characters 4-9 R11f2@{α α0 α1 α2 α3 α4 α5 ; u} : forall r : R11@{α α0 α1 α2 α3 α4 α5 ; u}, let r0 : R10@{α0 α1 α2 α3 ; Set u} bool@{α1 ; } := @@ -1107,7 +1107,7 @@ R11f2 is a projection of R11 Arguments R11f2 r R11f2 is transparent Expands to: Constant sort_poly_elab.Records.R11f2 -Declared in library sort_poly_elab, line 676, characters 4-9 +Declared in library sort_poly_elab, line 678, characters 4-9 R11f3@{α α0 α1 α2 α3 α4 α5 ; u} : forall _ : R11@{α α0 α1 α2 α3 α4 α5 ; u}, bool@{α5 ; } (* α α0 α1 α2 α3 α4 α5 ; u |= α -> α5 @@ -1119,7 +1119,7 @@ R11f3 is a projection of R11 Arguments R11f3 r R11f3 is transparent Expands to: Constant sort_poly_elab.Records.R11f3 -Declared in library sort_poly_elab, line 681, characters 4-9 +Declared in library sort_poly_elab, line 683, characters 4-9 R12@{α α0 ; } : Type@{α ; Set} (* α α0 ; |= α0 -> Type *) @@ -1130,7 +1130,7 @@ R12@{α α0 ; } may only be eliminated to produce values whose type is in sort q (SProp <= Prop <= Type, and all variables <= Type) than the instantiation of α. Expands to: Inductive sort_poly_elab.Records.R12 -Declared in library sort_poly_elab, line 700, characters 9-12 +Declared in library sort_poly_elab, line 702, characters 9-12 R12f1@{α α0 ; } : forall _ : R12@{α α0 ; }, bool@{α0 ; } (* α α0 ; |= α -> α0 @@ -1141,7 +1141,7 @@ R12f1 is a projection of R12 Arguments R12f1 r R12f1 is transparent Expands to: Constant sort_poly_elab.Records.R12f1 -Declared in library sort_poly_elab, line 701, characters 4-9 +Declared in library sort_poly_elab, line 703, characters 4-9 R12f2@{α α0 ; } : forall r : R12@{α α0 ; }, let f' : forall _ : nat, nat := @@ -1164,7 +1164,7 @@ R12f2 is a projection of R12 Arguments R12f2 r R12f2 is transparent Expands to: Constant sort_poly_elab.Records.R12f2 -Declared in library sort_poly_elab, line 702, characters 4-9 +Declared in library sort_poly_elab, line 704, characters 4-9 R13@{α α0 α1 α2 ; u u0} : Type@{α ; max(Set,u+1,u0+1)} (* α α0 α1 α2 ; u u0 |= α1 -> Type @@ -1178,7 +1178,7 @@ R13@{α α0 α1 α2 ; u u0} may only be eliminated to produce values whose type (SProp <= Prop <= Type, and all variables <= Type) than the instantiation of α. Expands to: Inductive sort_poly_elab.Records.R13 -Declared in library sort_poly_elab, line 717, characters 9-12 +Declared in library sort_poly_elab, line 719, characters 9-12 R13f1@{α α0 α1 α2 ; u u0} : forall _ : R13@{α α0 α1 α2 ; u u0}, Type@{α0 ; u} (* α α0 α1 α2 ; u u0 |= α -> Type @@ -1191,7 +1191,7 @@ R13f1 is a projection of R13 Arguments R13f1 r R13f1 is transparent Expands to: Constant sort_poly_elab.Records.R13f1 -Declared in library sort_poly_elab, line 718, characters 4-9 +Declared in library sort_poly_elab, line 720, characters 4-9 R13f2@{α α0 α1 α2 ; u u0} : forall _ : R13@{α α0 α1 α2 ; u u0}, Type@{α0 ; u0} (* α α0 α1 α2 ; u u0 |= α -> Type @@ -1204,7 +1204,7 @@ R13f2 is a projection of R13 Arguments R13f2 r R13f2 is transparent Expands to: Constant sort_poly_elab.Records.R13f2 -Declared in library sort_poly_elab, line 719, characters 4-9 +Declared in library sort_poly_elab, line 721, characters 4-9 R13f3@{α α0 α1 α2 ; u u0} : forall _ : R13@{α α0 α1 α2 ; u u0}, bool@{α1 ; } (* α α0 α1 α2 ; u u0 |= α -> α1 @@ -1217,7 +1217,7 @@ R13f3 is a projection of R13 Arguments R13f3 r R13f3 is transparent Expands to: Constant sort_poly_elab.Records.R13f3 -Declared in library sort_poly_elab, line 720, characters 4-9 +Declared in library sort_poly_elab, line 722, characters 4-9 R13f4@{α α0 α1 α2 ; u u0} : forall (r : R13@{α α0 α1 α2 ; u u0}) (b : bool@{α2 ; }), match b return Type@{α0 ; u} with @@ -1240,7 +1240,7 @@ R13f4 is a projection of R13 Arguments R13f4 r b R13f4 is transparent Expands to: Constant sort_poly_elab.Records.R13f4 -Declared in library sort_poly_elab, line 721, characters 4-9 +Declared in library sort_poly_elab, line 723, characters 4-9 C1@{α α0 ; u} : forall _ : Type@{α ; u}, Type@{α0 ; u} (* α α0 ; u |= *) @@ -1252,7 +1252,7 @@ C1@{α α0 ; u} may only be eliminated to produce values whose type is in sort q than the instantiation of α0. Arguments C1 A%_type_scope Expands to: Inductive sort_poly_elab.Classes.C1 -Declared in library sort_poly_elab, line 756, characters 8-10 +Declared in library sort_poly_elab, line 758, characters 8-10 C1f1@{α α0 ; u} : forall {A : Type@{α ; u}} {_ : C1@{α α0 ; u} A}, A (* α α0 ; u |= α0 -> α *) @@ -1262,41 +1262,41 @@ C1f1 is a projection of C1 Arguments C1f1 {A}%_type_scope {C1} C1f1 is transparent Expands to: Constant sort_poly_elab.Classes.C1f1 -Declared in library sort_poly_elab, line 757, characters 4-8 +Declared in library sort_poly_elab, line 759, characters 4-8 C1I1@{α α0 ; u} : C1@{α α0 ; u} unit@{α ; u} (* α α0 ; u |= *) C1I1 is universe polymorphic C1I1 is transparent Expands to: Constant sort_poly_elab.Classes.C1I1 -Declared in library sort_poly_elab, line 764, characters 11-15 +Declared in library sort_poly_elab, line 766, characters 11-15 C1ProgramI1@{α α0 ; u} : C1@{α α0 ; u} unit@{α ; u} (* α α0 ; u |= *) C1ProgramI1 is universe polymorphic C1ProgramI1 is transparent Expands to: Constant sort_poly_elab.Classes.C1ProgramI1 -Declared in library sort_poly_elab, line 767, characters 19-30 +Declared in library sort_poly_elab, line 769, characters 19-30 C1RefineI1@{α α0 ; u} : C1@{α α0 ; u} unit@{α ; u} (* α α0 ; u |= *) C1RefineI1 is universe polymorphic C1RefineI1 is transparent Expands to: Constant sort_poly_elab.Classes.C1RefineI1 -Declared in library sort_poly_elab, line 774, characters 11-21 +Declared in library sort_poly_elab, line 777, characters 11-21 C1InteractiveI1@{α α0 ; u} : C1@{α α0 ; u} unit@{α ; u} (* α α0 ; u |= *) C1InteractiveI1 is universe polymorphic C1InteractiveI1 is transparent Expands to: Constant sort_poly_elab.Classes.C1InteractiveI1 -Declared in library sort_poly_elab, line 779, characters 11-26 +Declared in library sort_poly_elab, line 783, characters 11-26 C1AxiomaticI1@{α α0 ; u} : C1@{α α0 ; u} unit@{α ; u} (* α α0 ; u |= *) C1AxiomaticI1 is universe polymorphic Expands to: Constant sort_poly_elab.Classes.C1AxiomaticI1 -Declared in library sort_poly_elab, line 783, characters 9-22 +Declared in library sort_poly_elab, line 787, characters 9-22 C1InductiveI1@{α ; u} : Type@{α ; u} (* α ; u |= *) @@ -1307,8 +1307,8 @@ C1InductiveI1@{α ; u} may only be eliminated to produce values whose type is in (SProp <= Prop <= Type, and all variables <= Type) than the instantiation of α. Expands to: Inductive sort_poly_elab.Classes.C1InductiveI1 -Declared in library sort_poly_elab, line 787, characters 12-25 -File "./output/sort_poly_elab.v", line 796, characters 0-76: +Declared in library sort_poly_elab, line 791, characters 12-25 +File "./output/sort_poly_elab.v", line 800, characters 0-76: The command has indeed failed with message: Sort metavariables must be collapsed to Type in universe monomorphic constructions. Attr@{α ; u} : Type@{α ; u} @@ -1321,4 +1321,4 @@ Attr@{α ; u} may only be eliminated to produce values whose type is in sort qua (SProp <= Prop <= Type, and all variables <= Type) than the instantiation of α. Expands to: Inductive sort_poly_elab.Attr -Declared in library sort_poly_elab, line 800, characters 10-14 +Declared in library sort_poly_elab, line 804, characters 10-14 diff --git a/test-suite/output/sort_poly_elab.v b/test-suite/output/sort_poly_elab.v index b5a87eb0b567..4cef9de86f99 100644 --- a/test-suite/output/sort_poly_elab.v +++ b/test-suite/output/sort_poly_elab.v @@ -489,6 +489,7 @@ Module Inductives. (* Using Program *) Program Definition bool_to_Prop' (b : bool) : Prop := _. Next Obligation. + Proof. intro b; destruct b. - exact True. - exact False. @@ -529,6 +530,7 @@ Module Inductives. About FooNat. Definition Foo (n : FooNat) : FooNat. + Proof. destruct n. - exact FO. - exact FO. @@ -766,12 +768,14 @@ Module Classes. Program Instance C1ProgramI1 : C1 unit. Next Obligation. + Proof. exact tt. Defined. About C1ProgramI1. #[refine] Instance C1RefineI1 : C1 unit := { C1f1 := _ }. + Proof. exact tt. Defined. About C1RefineI1. diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.out b/test-suite/output/ssr_error_multiple_intro_after_case.out index d7bc9cf79635..82f9ab706b95 100644 --- a/test-suite/output/ssr_error_multiple_intro_after_case.out +++ b/test-suite/output/ssr_error_multiple_intro_after_case.out @@ -1,3 +1,3 @@ -File "./output/ssr_error_multiple_intro_after_case.v", line 3, characters 5-16: +File "./output/ssr_error_multiple_intro_after_case.v", line 4, characters 5-16: The command has indeed failed with message: x already used diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.v b/test-suite/output/ssr_error_multiple_intro_after_case.v index b3a078fdfda7..dc2ba241c0bc 100644 --- a/test-suite/output/ssr_error_multiple_intro_after_case.v +++ b/test-suite/output/ssr_error_multiple_intro_after_case.v @@ -1,4 +1,5 @@ Require Import ssreflect. Goal forall p : nat * nat , True. +Proof. Fail case => x x. Abort. diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out index 3f967402d940..36792fd3ff07 100644 --- a/test-suite/output/ssr_explain_match.out +++ b/test-suite/output/ssr_explain_match.out @@ -50,6 +50,6 @@ instance: (addnC z (x + y)) matches: (x + y + z) instance: (addnC y x) matches: (x + y) instance: (addnC y x) matches: (x + y) END INSTANCES -File "./output/ssr_explain_match.v", line 22, characters 5-38: +File "./output/ssr_explain_match.v", line 23, characters 5-38: The command has indeed failed with message: Not supported diff --git a/test-suite/output/ssr_explain_match.v b/test-suite/output/ssr_explain_match.v index 38725eae462d..73e8c15c8e46 100644 --- a/test-suite/output/ssr_explain_match.v +++ b/test-suite/output/ssr_explain_match.v @@ -14,6 +14,7 @@ Require Import ssreflect ssrbool TestSuite.ssr_mini_mathcomp. Definition addnAC := (addnA, addnC). Lemma test x y z : x + y + z = x + y. +Proof. ssrinstancesoftpat (_ + _). ssrinstancesofruleL2R addnC. diff --git a/test-suite/output/ssr_under.v b/test-suite/output/ssr_under.v index d100488d0abb..1b4179fbef2a 100644 --- a/test-suite/output/ssr_under.v +++ b/test-suite/output/ssr_under.v @@ -10,6 +10,7 @@ Axiom eq_G : Ltac show := match goal with [|-?g] => idtac g end. Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. +Proof. under eq_G => m do [show; rw subnn]. show. Abort. diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v index b64d012c521c..b4058a75c6ac 100644 --- a/test-suite/output/subst.v +++ b/test-suite/output/subst.v @@ -7,6 +7,7 @@ Abbreviation goal := Ltac do_intros := intros * Hx Hy Hz H1 HA H2 H3 HB H4. Goal goal. +Proof. do_intros. (* From now on, the order after subst is consistently H1, HA, H2, H3, HB, H4 *) subst x. @@ -15,6 +16,7 @@ Show. Abort. Goal goal. +Proof. do_intros. subst y. (* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *) @@ -22,6 +24,7 @@ Show. Abort. Goal goal. +Proof. do_intros. subst z. (* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *) @@ -29,6 +32,7 @@ Show. Abort. Goal goal. +Proof. do_intros. subst. (* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *) diff --git a/test-suite/output/unidecls.out b/test-suite/output/unidecls.out index 0b9de40d4574..5ee18fc43a01 100644 --- a/test-suite/output/unidecls.out +++ b/test-suite/output/unidecls.out @@ -46,14 +46,14 @@ The command has indeed failed with message: Undeclared universe A.u. Type@{Arg.u} : Type@{Arg.u+1} -File "./output/unidecls.v", line 79, characters 59-60: +File "./output/unidecls.v", line 81, characters 15-16: The command has indeed failed with message: In environment A : Type@{v} The term "A" has type "Type@{v}" while it is expected to have type "Type@{Arg.u}" (universe inconsistency: Cannot enforce v <= Arg.u because Arg.u < v). -File "./output/unidecls.v", line 93, characters 17-24: +File "./output/unidecls.v", line 96, characters 17-24: The command has indeed failed with message: Undeclared universe FnApp.v. Type@{Fn.v} @@ -62,14 +62,14 @@ FnApp.foo : Type@{Fn.v} FnApp.bar : Type@{Arg.u} -File "./output/unidecls.v", line 99, characters 17-26: +File "./output/unidecls.v", line 102, characters 17-26: The command has indeed failed with message: Undeclared universe ArgImpl.u. FnApp2.foo : Type@{Fn.v} FnApp2.bar : Type@{Arg.u} -File "./output/unidecls.v", line 113, characters 17-21: +File "./output/unidecls.v", line 116, characters 17-21: The command has indeed failed with message: Undeclared universe: poly. Set < nat_rect.u0 diff --git a/test-suite/output/unidecls.v b/test-suite/output/unidecls.v index 64adb338a5e2..a6f14c270cf5 100644 --- a/test-suite/output/unidecls.v +++ b/test-suite/output/unidecls.v @@ -76,7 +76,10 @@ Module Fn(A : Arg). Definition foo : Type@{v} := nat. Definition bar : Type@{Arg.u} := nat. - Definition foo'(A : Type@{v}) : Type@{Arg.u}. Fail exact A. Abort. + Definition foo'(A : Type@{v}) : Type@{Arg.u}. + Proof. + Fail exact A. + Abort. End Fn. Module ArgImpl : Arg. diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out index a75f64ef7402..df92677f073f 100644 --- a/test-suite/output/unifconstraints.out +++ b/test-suite/output/unifconstraints.out @@ -59,7 +59,7 @@ unification constraint: True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = veeryyyyyyyyyyyyloooooooooooooonggidentifier -File "./output/unifconstraints.v", line 29, characters 56-57: +File "./output/unifconstraints.v", line 31, characters 56-57: The command has indeed failed with message: In environment P : nat -> Type @@ -68,6 +68,6 @@ h : P x Unable to unify "P x" with "?P x" (unable to find a well-typed instantiation for "?P": cannot ensure that "nat -> Type" is a subtype of "nat -> Prop"). -File "./output/unifconstraints.v", line 37, characters 5-15: +File "./output/unifconstraints.v", line 40, characters 5-15: The command has indeed failed with message: Tactic failure: congruence failed (cannot build a well-typed proof). diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v index 96af0bac85b2..047e575bab99 100644 --- a/test-suite/output/unifconstraints.v +++ b/test-suite/output/unifconstraints.v @@ -5,6 +5,7 @@ Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat. Goal True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = veeryyyyyyyyyyyyloooooooooooooonggidentifier. +Proof. refine (nat_rect _ _ _ _). Show. Admitted. @@ -13,6 +14,7 @@ Set Printing Existential Instances. Goal forall n m : nat, True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = veeryyyyyyyyyyyyloooooooooooooonggidentifier. +Proof. intros. refine (nat_rect _ _ _ _). Show. @@ -34,6 +36,7 @@ Set Universe Polymorphism. Section S. Polymorphic Universes i j. Goal Type@{i} -> (Type@{j} : Type@{i}). +Proof. Fail congruence. Abort. End S. diff --git a/test-suite/output/unification.v b/test-suite/output/unification.v index 98ee190f3137..48fb03dc7526 100644 --- a/test-suite/output/unification.v +++ b/test-suite/output/unification.v @@ -16,18 +16,21 @@ End A. (* Choice of evar names *) Goal (forall x, S (S (S x)) = x) -> exists x, S x = 0. +Proof. eexists. rewrite H. Show. Abort. Goal (forall x, S (S (S x)) = x) -> exists x, S x = 0. +Proof. eexists ?[x]. rewrite H. Show. Abort. Goal (forall x, S (S (S x)) = x) -> exists x, S x = 0. +Proof. eexists ?[y]. rewrite H. Show. @@ -37,6 +40,7 @@ Qed. (* Preserve the name if there is one *) Goal (forall x, S x = x) -> exists x, S x = 0. +Proof. eexists ?[y]. rewrite H. Show. diff --git a/theories/Corelib/Classes/RelationClasses.v b/theories/Corelib/Classes/RelationClasses.v index 27869a342746..7919b1b6d512 100644 --- a/theories/Corelib/Classes/RelationClasses.v +++ b/theories/Corelib/Classes/RelationClasses.v @@ -441,12 +441,15 @@ Program Instance predicate_equivalence_equivalence {l} : Equivalence (@predicate_equivalence l). Next Obligation. + Proof. intro l; induction l ; firstorder. Qed. Next Obligation. + Proof. intro l; induction l ; firstorder. Qed. Next Obligation. + Proof. intro l. fold pointwise_lifting. induction l as [|T l IHl]. @@ -459,9 +462,11 @@ Program Instance predicate_equivalence_equivalence {l} : Program Instance predicate_implication_preorder {l} : PreOrder (@predicate_implication l). Next Obligation. + Proof. intro l; induction l ; firstorder. Qed. Next Obligation. + Proof. intro l. induction l as [|T l IHl]. - firstorder. diff --git a/theories/Corelib/Floats/FloatAxioms.v b/theories/Corelib/Floats/FloatAxioms.v index 732244044245..e73c54edffce 100644 --- a/theories/Corelib/Floats/FloatAxioms.v +++ b/theories/Corelib/Floats/FloatAxioms.v @@ -29,11 +29,18 @@ Axiom SF2Prim_Prim2SF : forall x, SF2Prim (Prim2SF x) = x. Axiom Prim2SF_SF2Prim : forall x, valid_binary x = true -> Prim2SF (SF2Prim x) = x. Theorem Prim2SF_inj : forall x y, Prim2SF x = Prim2SF y -> x = y. +Proof. intros. rewrite <- SF2Prim_Prim2SF. symmetry. rewrite <- SF2Prim_Prim2SF. now rewrite H. Qed. Theorem SF2Prim_inj : forall x y, SF2Prim x = SF2Prim y -> valid_binary x = true -> valid_binary y = true -> x = y. - intros. rewrite <- Prim2SF_SF2Prim by assumption. symmetry. rewrite <- Prim2SF_SF2Prim by assumption. rewrite H. reflexivity. +Proof. + intros. + rewrite <- Prim2SF_SF2Prim by assumption. + symmetry. + rewrite <- Prim2SF_SF2Prim by assumption. + rewrite H. + reflexivity. Qed. Axiom opp_spec : forall x, Prim2SF (-x)%float = SFopp (Prim2SF x). diff --git a/theories/Corelib/Init/Logic.v b/theories/Corelib/Init/Logic.v index ff3f97dc9a18..b77c74682be1 100644 --- a/theories/Corelib/Init/Logic.v +++ b/theories/Corelib/Init/Logic.v @@ -464,6 +464,7 @@ Section Logic_lemmas. Definition eq_ind_r : forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y. + Proof. intros A x P H y H0. elim eq_sym with (1 := H0); assumption. Defined. @@ -472,11 +473,13 @@ Section Logic_lemmas. Definition eq_rec_r : forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y. + Proof. intros A x P H y H0; elim eq_sym with (1 := H0); assumption. Defined. Definition eq_rect_r : forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y. + Proof. intros A x P H y H0; elim eq_sym with (1 := H0); assumption. Defined. diff --git a/theories/Corelib/Init/Wf.v b/theories/Corelib/Init/Wf.v index 38ccd33200e3..83f451697807 100644 --- a/theories/Corelib/Init/Wf.v +++ b/theories/Corelib/Init/Wf.v @@ -36,7 +36,8 @@ Section Well_founded. Register Acc as core.wf.acc. Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y. - destruct 1; trivial. + Proof. + destruct 1; trivial. Defined. Global Arguments Acc_inv [x] _ [y] _, [x] _ y _. diff --git a/theories/Corelib/ssr/ssrbool.v b/theories/Corelib/ssr/ssrbool.v index a1d23ba841a8..b1a0d6914aab 100644 --- a/theories/Corelib/ssr/ssrbool.v +++ b/theories/Corelib/ssr/ssrbool.v @@ -733,7 +733,8 @@ Proof. by case; [apply: introT | apply: introF]. Qed. Lemma decPcases : if b then P else ~ P. Proof. by case Pb. Qed. -Definition decP : decidable P. by case: b decPcases; [left | right]. Defined. +Definition decP : decidable P. +Proof. by case: b decPcases; [left | right]. Defined. Lemma rwP : P <-> b. Proof. by split; [apply: introT | apply: elimT]. Qed. diff --git a/vernac/declare.ml b/vernac/declare.ml index 1bf87833a2de..e93d26436c4d 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1783,9 +1783,13 @@ module Proof = struct type nonrec closed_proof_output = closed_proof_output type proof_object = Proof_object.t +type late_init = Explicit | Implicit + type t = { endline_tactic : Gentactic.glob_generic_tactic option ; using : Id.Set.t option + ; has_late_init : late_init option + (** Explicit if Proof was used, Implicit if we started modifying the proof before Proof was used *) ; proof : Proof.t ; initial_euctx : UState.t (** The initial universe context (for the statement) *) @@ -1818,6 +1822,10 @@ let compact pf = map ~f:Proof.compact pf let set_endline_tactic tac ps = { ps with endline_tactic = Some tac } +let finish_late_init ps explicit = { ps with has_late_init = Some explicit } + +let has_late_init ps = ps.has_late_init + let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right @@ -1838,6 +1846,7 @@ let start_proof_core ~name ~pinfo ?using sigma goals = let proof = Proof.start ~name ~poly ?typing_flags sigma goals in let initial_euctx = Evd.ustate Proof.((data proof).sigma) in { proof + ; has_late_init = None ; endline_tactic = None ; using ; initial_euctx @@ -1863,6 +1872,7 @@ let start_dependent ~info ~cinfo ~name ~proof_ending goals = let initial_euctx = Evd.ustate Proof.((data proof).sigma) in let pinfo = Proof_info.make ~info ~cinfo ~proof_ending () in { proof + ; has_late_init = None ; endline_tactic = None ; using = None ; initial_euctx diff --git a/vernac/declare.mli b/vernac/declare.mli index 3f107286215c..00e998902ec6 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -268,6 +268,11 @@ module Proof : sig (** Sets the tactic to be used when a tactic line is closed with [...] *) val set_endline_tactic : Gentactic.glob_generic_tactic -> t -> t + type late_init = Explicit | Implicit + + val finish_late_init : t -> late_init -> t + val has_late_init : t -> late_init option + val definition_scope : t -> Locality.definition_scope (** Sets the section variables assumed by the proof, returns its closure diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 2e2826a7dae3..82993c2b299c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2573,12 +2573,20 @@ let vernac_proof pstate tac using = in None in + let () = match Declare.Proof.has_late_init pstate with + | None -> () + | Some Explicit -> + CErrors.user_err Pp.(str "Multiple \"Proof\" commands not supported.") + | Some Implicit -> + CErrors.user_err Pp.(str "\"Proof\" must be the first command in an interactive proof.") + in let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in let usings = if Option.is_empty using then "using:no" else "using:yes" in Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings); let pstate = Option.fold_left vernac_set_end_tac pstate tac in let set_proof_using ps using = Declare.Proof.set_proof_using ps using |> snd in let pstate = Option.fold_left set_proof_using pstate using in + let pstate = Declare.Proof.finish_late_init pstate Explicit in pstate let translate_vernac_synterp ?loc ~atts v = let open Vernactypes in match v with @@ -2687,7 +2695,7 @@ let translate_pure_vernac ?loc ~atts v = let open Vernactypes in match v with | VernacStartTheoremProof (k,l) -> vtopenproof(fun () -> with_def_attributes ~atts vernac_start_proof k l) | VernacExactProof c -> - vtcloseproof (fun ~lemma -> + vtcloseproof ~check_late_init:false (fun ~lemma -> unsupported_attributes atts; vernac_exact_proof ~lemma c) @@ -2955,7 +2963,7 @@ let translate_pure_vernac ?loc ~atts v = let open Vernactypes in match v with unsupported_attributes atts; Feedback.msg_notice @@ vernac_validate_proof ~pstate) | VernacProof (tac, using) -> - vtmodifyproof(fun ~pstate -> + vtmodifyproof ~check_late_init:false (fun ~pstate -> unsupported_attributes atts; vernac_proof pstate tac using) @@ -2965,7 +2973,7 @@ let translate_pure_vernac ?loc ~atts v = let open Vernactypes in match v with | VernacAbort -> unsupported_attributes atts; - vtcloseproof vernac_abort + vtcloseproof ~check_late_init:false vernac_abort let translate_vernac ?loc ~atts v = match v with diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 1855b8d60f3c..1756496b37dc 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -77,7 +77,7 @@ and interp_expr_core ?loc ~atts ~st c = let fv = Vernacentries.translate_vernac ?loc ~atts v in let stack = st.Vernacstate.interp.lemmas in let program = st.Vernacstate.interp.program in - let {Vernactypes.prog; proof; opaque_access=(); }, () = Vernactypes.run fv { + let {Vernactypes.prog; proof; opaque_access=(); }, () = Vernactypes.run ?loc fv { prog=program; proof=stack; opaque_access=(); diff --git a/vernac/vernactypes.ml b/vernac/vernactypes.ml index 68121bd05d49..de650bdabcf1 100644 --- a/vernac/vernactypes.ml +++ b/vernac/vernactypes.ml @@ -6,7 +6,7 @@ The additional return data ['d] is useful when combining runners. We don't need an additional input data as it can just go in the closure. *) -type ('a,'b,'x) runner = { run : 'd. 'x -> ('a -> 'b * 'd) -> 'x * 'd } +type ('a,'b,'x) runner = { run : 'd. ?loc:Loc.t -> 'x -> ('a -> 'b * 'd) -> 'x * 'd } module Prog = struct @@ -22,7 +22,7 @@ module Prog = struct | Pop : (state, unit) t let runner (type a b) (ty:(a,b) t) : (a,b,stack) runner = - { run = fun pm f -> + { run = fun ?loc pm f -> match ty with | Ignore -> let (), v = f () in pm, v | Modify -> @@ -52,23 +52,40 @@ module Proof = struct type (_,_) t = | Ignore : (unit, unit) t - | Modify : (state, state) t + | Modify : { check_late_init : bool } -> (state, state) t | Read : (state, unit) t | ReadOpt : (state option, unit) t | Reject : (unit, unit) t - | Close : (state, unit) t + | Close : { check_late_init : bool } -> (state, unit) t | Open : (unit, state) t let use = function | None -> CErrors.user_err (Pp.str "Command not supported (No proof-editing in progress).") | Some stack -> LStack.pop stack + let quickfix_missing_proof ~loc () = + (* quickfix is purely additive so the loc is 0 characters long, at the beginning of the command. *) + let loc = { loc with Loc.ep = loc.Loc.bp } in + [Quickfix.make ~loc Pp.(str "Proof." ++ fnl())] + + let warn_missing_proof = CWarnings.create ~name:"missing-proof-command" ~category:CWarnings.CoreCategories.fragile + ~quickfix:quickfix_missing_proof + Pp.(fun () -> str "This interactive proof is not started by the \"Proof\" command.") + + let check_late_init ?loc p = + if Option.has_some @@ Declare.Proof.has_late_init p then p + else begin + warn_missing_proof ?loc (); + Declare.Proof.finish_late_init p Implicit + end + let runner (type a b) (ty:(a,b) t) : (a,b,stack) runner = - { run = fun stack f -> + { run = fun ?loc stack f -> match ty with | Ignore -> let (), v = f () in stack, v - | Modify -> + | Modify o -> let p, rest = use stack in + let p = if o.check_late_init then check_late_init ?loc p else p in let p, v = f p in Some (LStack.push rest p), v | Read -> @@ -85,8 +102,9 @@ module Proof = struct in let (), v = f () in stack, v - | Close -> + | Close o -> let p, rest = use stack in + let p = if o.check_late_init then check_late_init ?loc p else p in let (), v = f p in rest, v | Open -> @@ -109,7 +127,7 @@ module OpaqueAccess = struct let access = Library.indirect_accessor[@@warning "-3"] let runner (type a) (ty:a t) : (a,unit,unit) runner = - { run = fun () f -> + { run = fun ?loc () f -> match ty with | Ignore -> let (), v = f () in (), v | Access -> let (), v = f access in (), v @@ -120,9 +138,9 @@ end (* lots of messing with tuples in there, can we do better? *) let combine_runners (type a b x c d y) (r1:(a,b,x) runner) (r2:(c,d,y) runner) : (a*c, b*d, x*y) runner - = { run = fun (x,y) f -> - match r1.run x @@ fun x -> - match r2.run y @@ fun y -> + = { run = fun ?loc (x,y) f -> + match r1.run ?loc x @@ fun x -> + match r2.run ?loc y @@ fun y -> match f (x,y) with ((b, d), o) -> (d, (b, o)) with (y, (b, o)) -> (b, (y, o)) @@ -157,10 +175,10 @@ type typed_vernac = unit typed_vernac_gen type full_state = (Prog.stack,Vernacstate.LemmaStack.t option,unit) state_gen -let run (TypedVernac { spec = { prog; proof; opaque_access }; run }) (st:full_state) : full_state * _ = +let run ?loc (TypedVernac { spec = { prog; proof; opaque_access }; run }) (st:full_state) : full_state * _ = let ( * ) = combine_runners in let runner = Prog.runner prog * Proof.runner proof * OpaqueAccess.runner opaque_access in - let st, v = runner.run (tuple st) @@ fun st -> + let st, v = runner.run ?loc (tuple st) @@ fun st -> let st, v= run @@ untuple st in tuple st, v in untuple st, v @@ -175,13 +193,15 @@ let vtdefault f = typed_vernac ignore_state let vtnoproof f = typed_vernac { ignore_state with proof = Reject } (fun (_:no_state) -> let () = f () in no_state) -let vtcloseproof f = typed_vernac { ignore_state with prog = Modify; proof = Close } +let vtcloseproof ?(check_late_init=true) f = + typed_vernac { ignore_state with prog = Modify; proof = Close { check_late_init } } (fun {prog; proof} -> let prog = f ~lemma:proof ~pm:prog in { no_state with prog }) let vtopenproof f = typed_vernac { ignore_state with proof = Open } (fun (_:no_state) -> let proof = f () in { no_state with proof }) -let vtmodifyproof f = typed_vernac { ignore_state with proof = Modify } +let vtmodifyproof ?(check_late_init=true) f = + typed_vernac { ignore_state with proof = Modify { check_late_init } } (fun {proof} -> let proof = f ~pstate:proof in { no_state with proof }) let vtreadproofopt f = typed_vernac { ignore_state with proof = ReadOpt } diff --git a/vernac/vernactypes.mli b/vernac/vernactypes.mli index b92aa90c5193..7488e8f6b847 100644 --- a/vernac/vernactypes.mli +++ b/vernac/vernactypes.mli @@ -26,11 +26,11 @@ module Proof : sig type (_,_) t = | Ignore : (unit, unit) t - | Modify : (state, state) t + | Modify : { check_late_init : bool } -> (state, state) t | Read : (state, unit) t | ReadOpt : (state option, unit) t | Reject : (unit, unit) t - | Close : (state, unit) t + | Close : { check_late_init : bool } -> (state, unit) t | Open : (unit, state) t end @@ -77,15 +77,15 @@ val typed_vernac type full_state = (Prog.stack, Vernacstate.LemmaStack.t option, unit) state_gen -val run : 'r typed_vernac_gen -> full_state -> full_state * 'r +val run : ?loc:Loc.t -> 'r typed_vernac_gen -> full_state -> full_state * 'r (** Some convenient typed_vernac constructors. Used by coqpp. *) val vtdefault : (unit -> unit) -> typed_vernac val vtnoproof : (unit -> unit) -> typed_vernac -val vtcloseproof : (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t) -> typed_vernac +val vtcloseproof : ?check_late_init:bool -> (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t) -> typed_vernac val vtopenproof : (unit -> Declare.Proof.t) -> typed_vernac -val vtmodifyproof : (pstate:Declare.Proof.t -> Declare.Proof.t) -> typed_vernac +val vtmodifyproof : ?check_late_init:bool -> (pstate:Declare.Proof.t -> Declare.Proof.t) -> typed_vernac val vtreadproofopt : (pstate:Declare.Proof.t option -> unit) -> typed_vernac val vtreadproof : (pstate:Declare.Proof.t -> unit) -> typed_vernac val vtreadprogram : (pm:Declare.OblState.t -> unit) -> typed_vernac