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

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 menhir https://gitlab.inria.fr/ggilbert/menhir badproof 21865
+
+overlay coquelicot https://gitlab.inria.fr/ggilbert/coquelicot badproof 21865

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/type-classes.rst

@@ -75,6 +75,7 @@ remaining fields, e.g.:
 .. rocqtop:: all
 
    Next Obligation.
+   Proof.
      destruct x ; destruct y ; (discriminate || reflexivity).
    Defined.
 

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