Warning for missing "Proof" command and error on duplicate or late "Proof"

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 <https://github.com/rocq-prover/rocq/pull/21865>`_,
+  by Gaëtan Gilbert).

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:
 

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.

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

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:

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

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.

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 *)

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.

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 *)
 

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