Restore "Proof Using Clear Unused"

dev/ci/user-overlays/22107-SkySkimmer-keep-using.sh

@@ -0,0 +1 @@
+overlay vsrocq https://github.com/SkySkimmer/vsrocq keep-using 22107

doc/changelog/08-vernac-commands-and-options/22107-keep-using-Added.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  :flag:`Proof Using Clear Unused` which automatically clears variables not allowed by a :cmd:`Proof using` annotation at the beginning of an interactive proof
+  (`#22107 <https://github.com/rocq-prover/rocq/pull/22107>`_,
+  by Gaëtan Gilbert).

doc/sphinx/proofs/writing-proofs/proof-mode.rst

@@ -387,48 +387,49 @@ When the proof is completed, you can exit proof mode with commands such as
 
 .. _example-print-using:
 
-   .. example :: Declaring section variables
+.. example:: Declaring section variables
 
-      When a :ref:`section <section-mechanism>` is closed with :cmd:`End`, section
-      variables declared with :cmd:`Proof using` are added to the theorem as
-      additional variables.  You can see the effect on the theorem's statement
-      with commands such as :cmd:`Check`, :cmd:`Print` and :cmd:`About` after the
-      section is closed.  The :cmd:`Print` and :cmd:`About` commands also show the
-      section variables associated with a theorem before the section is closed.
+   When a :ref:`section <section-mechanism>` is closed with :cmd:`End`, section
+   variables declared with :cmd:`Proof using` are added to the theorem as
+   additional variables.  You can see the effect on the theorem's statement
+   with commands such as :cmd:`Check`, :cmd:`Print` and :cmd:`About` after the
+   section is closed.  The :cmd:`Print` and :cmd:`About` commands also show the
+   section variables associated with a theorem before the section is closed.
 
-      Adding the unnecessary section variable `radixNotZero` changes how `foo'` can be
-      applied.
+   Adding the unnecessary section variable `radixNotZero` changes how `foo'` can be
+   applied.
 
-      .. rocqtop:: in
+   .. rocqtop:: in
 
-         Section bar.
-           Variable radix : nat.
-           Hypothesis radixNotZero : 0 < radix.
+      Section bar.
+        Variable radix : nat.
+        Hypothesis radixNotZero : 0 < radix.
 
-           Lemma foo : 0 = 0.
-           Proof. reflexivity. Qed.
+        Lemma foo : 0 = 0.
+        Proof. reflexivity. Qed.
 
-           Lemma foo' : 0 = 0.
-           Proof using radixNotZero. reflexivity. Qed.  (* radixNotZero is not needed *)
+        Lemma foo' : 0 = 0.
+        Proof using radixNotZero. reflexivity. Qed.  (* radixNotZero is not needed *)
 
-      .. rocqtop:: all
+   .. rocqtop:: all
 
-           Print foo'.   (* Doesn't show radixNotZero yet *)
-         End bar.
-         Print foo.      (* Doesn't change after the End *)
-         Print foo'.     (* "End" added type radix (used by radixNotZero) and radixNotZero *)
-         Goal 0 = 0.
-         Proof.
+        Print foo'.   (* Doesn't show radixNotZero yet *)
+      End bar.
 
-      .. rocqtop:: in
+      Print foo.      (* Doesn't change after the End *)
+      Print foo'.     (* "End" added type radix (used by radixNotZero) and radixNotZero *)
+      Goal 0 = 0.
+      Proof.
 
-         Fail apply foo'.  (* Fails because of the extra variable *)
+   .. rocqtop:: in
 
-      .. rocqtop:: all
+      Fail apply foo'.  (* Fails because of the extra variable *)
 
-         apply (foo' 5).   (* Can be used if the extra variable is provided explicitly *)
+   .. rocqtop:: all
 
-      .. rocqtop:: abort none
+      apply (foo' 5).   (* Can be used if the extra variable is provided explicitly *)
+
+   .. rocqtop:: abort none
 
 Proof using options
 ```````````````````
@@ -447,6 +448,17 @@ The following options modify the behavior of ``Proof using``.
    invalid value will generate an error on a subsequent :cmd:`Proof`
    or :cmd:`Qed` command.
 
+.. flag:: Proof Using Clear Unused
+
+   When this :term:`flag` is on, :cmd:`Proof using` automatically
+   clears variables which are not allowed by the `using` expression.
+
+.. note::
+
+   When used variables are specified through :opt:`Default Proof
+   Using` or :attr:`using`, :flag:`Proof Using Clear Unused` only
+   takes effect at the :cmd:`Proof` command. If that command is left
+   implicit, no clearing occurs even when the flag is on.
 
 .. flag:: Suggest Proof Using
 

kernel/environ.ml

@@ -224,6 +224,10 @@ let var_status_ctxt ?(check=true) id ctxt =
 
 let var_status ?check id env = var_status_ctxt ?check id env.env_named_context
 
+let section_variables_ctxt ctxt = ctxt.env_named_secvars
+
+let section_variables env = section_variables_ctxt env.env_named_context
+
 let match_named_context_val c = match c.env_named_ctx with
 | [] -> None
 | decl :: ctx ->

kernel/environ.mli

@@ -109,6 +109,9 @@ val var_status_eq : var_status -> var_status -> bool
 val var_status_ctxt : ?check:bool -> Id.t -> named_context_val -> var_status
 val var_status : ?check:bool -> Id.t -> env -> var_status
 
+val section_variables_ctxt : named_context_val -> Id.Set.t
+val section_variables : env -> Id.Set.t
+
 val named_context_of_val : named_context_val -> Constr.named_context
 val val_of_named_context : (var_status * Constr.named_declaration) list -> named_context_val
 val empty_named_context_val : named_context_val

proofs/proof.ml

@@ -30,6 +30,7 @@
 *)
 
 open Util
+open Names
 
 module FocusKind = Dyn.Make()
 
@@ -112,7 +113,7 @@ type t =
   (** History of the focusings, provides information on how to unfocus
      the proof and the extra information stored while focusing.  The
      list is empty when the proof is fully unfocused. *)
-  ; name : Names.Id.t
+  ; name : Id.t
   (** the name of the theorem whose proof is being constructed *)
   ; poly : PolyFlags.t
   (** Universe polymorphism *)
@@ -362,7 +363,7 @@ type data =
   (** Entry for the proofview *)
   ; stack : (Evar.t list * Evar.t list) list
   (** A representation of the focus stack *)
-  ; name : Names.Id.t
+  ; name : Id.t
   (** The name of the theorem whose proof is being constructed *)
   ; poly : PolyFlags.t
   (** Universe polymorphism *)
@@ -470,3 +471,28 @@ let get_proof_context p =
 let purge_side_effects p =
   let proofview, eff = Proofview.Unsafe.purge_side_effects p.proofview in
   { p with proofview }, eff
+
+exception ProofUsingClearDependency of
+    Environ.env * Evd.evar_map * Id.t * Evarutil.clear_dependency_error * GlobRef.t option
+
+let set_used_variables env ~kept (p:t) =
+  let to_clear = Id.Set.diff Environ.(ids_of_named_context_val @@ named_context_val env) kept in
+  if Id.Set.is_empty to_clear then p
+  else
+    let entry = Proofview.initial_goals p.entry in
+    let err = Evarutil.OccurHypInSimpleClause None in
+    let tac =
+      Proofview.tclBIND Proofview.tclEVARMAP @@ fun sigma ->
+      let sigma =
+        List.fold_left (fun sigma (_, body, _) ->
+            try
+              Evarutil.check_and_clear_in_constr env sigma err to_clear body
+            with Evarutil.ClearDependencyError (id, err, gr) ->
+              raise (ProofUsingClearDependency (env, sigma, id, err, gr)))
+          sigma
+          entry
+      in
+      Proofview.Unsafe.tclEVARSADVANCE sigma
+    in
+    let p, _, () = run_tactic env tac p in
+    p

proofs/proof.mli

@@ -209,3 +209,13 @@ val get_goal_context_gen : t -> int -> Evd.evar_map * Environ.env
 val get_proof_context : t -> Evd.evar_map * Environ.env
 
 val purge_side_effects : t -> t * Evd.side_effects
+
+(** [set_used_variables env kept p] clears variables not in [kept]
+    from the proof terms, with an error if this is impossible
+    (eg "#[refine]" with the refine term using a forbidden
+    variable). *)
+val set_used_variables : Environ.env -> kept:Names.Id.Set.t -> t -> t
+
+(** Exposed for printing *)
+exception ProofUsingClearDependency of
+    Environ.env * Evd.evar_map * Names.Id.t * Evarutil.clear_dependency_error * Names.GlobRef.t option

tactics/tacticErrors.ml

@@ -76,6 +76,15 @@ let clear_dependency_msg env sigma id err inglobal =
       str "Cannot remove " ++ ppid id ++ str " as it would leave the existential " ++
       Printer.pr_existential_key env sigma ev ++ str" without candidates."
 
+let proof_using_clear_dependency_msg env sigma id err inglobal =
+  let msg =
+    match err with
+    | Evarutil.OccurHypInSimpleClause None ->
+      Id.print id ++ str " is used" ++ clear_in_global_msg inglobal ++ str " in the proof."
+    | _ -> clear_dependency_msg env sigma (Some id) err inglobal
+  in
+  str "Invalid \"Proof using\":" ++ spc() ++ msg
+
 let replacing_dependency_msg env sigma id err inglobal =
   let pp = clear_in_global_msg inglobal in
   match err with
@@ -118,6 +127,8 @@ exception Unhandled
 let tactic_interp_error_handler = function
   | IntroAlreadyDeclared id ->
       Id.print id ++ str " is already declared."
+  | Proof.ProofUsingClearDependency (env, sigma, id, err, inglobal) ->
+    proof_using_clear_dependency_msg env sigma id err inglobal
   | ClearDependency (env,sigma,id,err,inglobal) ->
       clear_dependency_msg env sigma id err inglobal
   | ReplacingDependency (env,sigma,id,err,inglobal) ->

test-suite/bugs/bug_12608.v

@@ -1,3 +1,4 @@
+Set Proof Using Clear Unused.
 Require Import Derive.
 Derive A in (A = 1) as B.
 Proof using Type.
@@ -10,13 +11,21 @@ Section S.
   Derive (A':nat) in nat as B'.
   Proof using .
     Unshelve.
-    all:exact n.
-    Fail Qed.
+    Fail all:exact n.
   Abort.
 
   Derive (A':nat) in nat as B'.
   Proof using n.
     Unshelve.
     all:exact n.
   Qed.
+
+  Variable A : Type.
+
+  Derive X : A -> A in (X = X) as H.
+  Proof using Type*.
+    reflexivity.
+    Unshelve.
+    exact (fun x => x).
+  Qed.
 End S.

test-suite/bugs/bug_22107_1.v

@@ -0,0 +1,9 @@
+Goal nat -> nat.
+Proof.
+  intros x .
+  epose (_:>bool).
+  (* questionable behaviour: unshelves a bool goal *)
+  unshelve eapply plus in x.
+  exact true.
+  all: exact 0.
+Qed.

test-suite/output/ProofUsingClear.out

@@ -0,0 +1,18 @@
+File "./output/ProofUsingClear.v", line 11, characters 15-16:
+The command has indeed failed with message:
+The reference y was not found in the current environment.
+File "./output/ProofUsingClear.v", line 16, characters 2-19:
+The command has indeed failed with message:
+Invalid "Proof using": x is used in the proof.
+File "./output/ProofUsingClear.v", line 18, characters 15-16:
+The command has indeed failed with message:
+The variable y was not found in the current environment.
+1 goal
+
+  x, y : nat
+  z := x + x : nat
+  ============================
+  bar = bar
+File "./output/ProofUsingClear.v", line 29, characters 2-13:
+The command has indeed failed with message:
+Invalid "Proof using": x is used implicitly in bar in the proof.

test-suite/output/ProofUsingClear.v

@@ -0,0 +1,32 @@
+Set Proof Using Clear Unused.
+
+Section S.
+
+  Variable x y : nat.
+
+  Let z := x + x.
+
+  Lemma foo : x + x = x + x.
+  Proof using .
+    Fail Check y.
+    exact (eq_refl z).
+  Defined.
+
+  #[refine] Definition bar := x + _.
+  Fail Proof using.
+  Proof using x.
+    Fail exact y.
+    exact z.
+  Defined.
+
+  Lemma baz : bar = bar.
+  Proof using y. (* x implicit through the type of the lemma *)
+    Show.
+    reflexivity.
+  Defined.
+
+  #[refine,using="y"] Definition baz' := bar + _.
+  Fail Proof.
+  Abort.
+
+End S.