Validate Proof command: runs typing.ml on the current proof

doc/changelog/08-vernac-commands-and-options/17467-validate-proof.rst

@@ -0,0 +1,5 @@
+- **Added:**
+  :cmd:`Validate Proof` runs the type checker on the current proof,
+  complementary with :cmd:`Guarded` which runs the guard checker.
+  (`#17467 <https://github.com/coq/coq/pull/17467>`_,
+  by Gaëtan Gilbert).

doc/sphinx/language/core/variants.rst

@@ -39,6 +39,11 @@ Private (matching) inductive types
    quotient types / higher-order inductive types in projects such as
    the `HoTT library <https://github.com/HoTT/HoTT>`_.
 
+   Reducing definitions from the inductive's module can expose
+   :g:`match` constructs to unification, which may result in invalid proof terms.
+   Errors from such terms are delayed until proof completion (i.e. on the :cmd:`Qed`). Use
+   :cmd:`Validate Proof` to identify which tactic produced the problematic term.
+
 .. example::
 
    .. coqtop:: all

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

@@ -1023,6 +1023,13 @@ Requesting information
    fixpoint and cofixpoint is violated at some time of the construction
    of the proof without having to wait the completion of the proof.
 
+.. cmd:: Validate Proof
+
+   Checks that the current partial proof is well-typed.
+   It is useful for finding tactic bugs since without it, such errors will only be detected at :cmd:`Qed` time.
+
+   It does not check the guard condition.  Use :cmd:`Guarded` for that.
+
 .. _showing_diffs:
 
 Showing differences between proof steps

doc/tools/docgram/fullGrammar

@@ -520,6 +520,7 @@ command: [
 | "Show" "Intros"
 | "Show" "Match" reference
 | "Guarded"
+| "Validate" "Proof"
 | "Create" "HintDb" IDENT; [ "discriminated" | ]
 | "Remove" "Hints" LIST1 global opt_hintbases
 | "Hint" hint opt_hintbases

doc/tools/docgram/orderedGrammar

@@ -818,6 +818,7 @@ command: [
 | "Show" "Intros"
 | "Show" "Match" qualid
 | "Guarded"
+| "Validate" "Proof"
 | "Create" "HintDb" ident OPT "discriminated"
 | "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident )
 | "Comments" LIST0 [ one_term | string | natural ]

test-suite/success/ValidateProof.v

@@ -0,0 +1,22 @@
+
+Module M.
+  Private Inductive foo := .
+
+  Definition to_nat (f:foo) : nat := match f with end.
+End M.
+
+Lemma bar : False.
+Proof.
+  exact_no_check I.
+  Fail Validate Proof.
+Abort.
+
+Lemma bar f : M.to_nat f = 0.
+Proof.
+  Validate Proof.
+
+  cbv.
+
+  Fail Validate Proof.
+
+Abort.

vernac/g_proofs.mlg

@@ -95,6 +95,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Show"; IDENT "Intros" -> { VernacSynPure (VernacShow (ShowIntros true)) }
       | IDENT "Show"; IDENT "Match"; id = reference -> { VernacSynPure (VernacShow (ShowMatch id)) }
       | IDENT "Guarded" -> { VernacSynPure VernacCheckGuard }
+      | IDENT "Validate"; IDENT "Proof" -> { VernacSynPure VernacValidateProof }
       (* Hints for Auto and EAuto *)
       | IDENT "Create"; IDENT "HintDb" ;
           id = IDENT ; b = [ IDENT "discriminated" -> { true } | -> { false } ] ->

vernac/ppvernac.ml

@@ -724,6 +724,8 @@ let pr_synpure_vernac_expr v =
   | VernacCheckGuard ->
     return (keyword "Guarded")
 
+  | VernacValidateProof -> return (keyword "Validate Proof")
+
   (* Resetting *)
   | VernacResetName id ->
     return (keyword "Reset" ++ spc() ++ pr_lident id)

vernac/vernac_classifier.ml

@@ -100,7 +100,7 @@ let classify_vernac e =
     | VernacProof _
     | VernacFocus _ | VernacUnfocus
     | VernacSubproof _
-    | VernacCheckGuard
+    | VernacCheckGuard | VernacValidateProof
     | VernacUnfocused
     | VernacBullet _ ->
         VtProofStep { proof_block_detection = Some "bullet" }

vernac/vernacentries.ml

@@ -2151,16 +2151,50 @@ let vernac_show ~pstate =
 let vernac_check_guard ~pstate =
   let pts = Declare.Proof.get pstate in
   let pfterm = List.hd (Proof.partial_proof pts) in
-  let message =
-    try
-      let { Proof.entry; Proof.sigma } = Proof.data pts in
-      let hyps, _, _ = List.hd (Proofview.initial_goals entry) in
-      let env = Environ.reset_with_named_context hyps (Global.env ()) in
-      Inductiveops.control_only_guard env sigma pfterm;
-      (str "The condition holds up to here")
-    with UserError s ->
-      (str ("Condition violated: ") ++ s ++ str ".")
-  in message
+  let { Proof.entry; Proof.sigma } = Proof.data pts in
+  let hyps, _, _ = List.hd (Proofview.initial_goals entry) in
+  let env = Environ.reset_with_named_context hyps (Global.env ()) in
+  Inductiveops.control_only_guard env sigma pfterm;
+  str "The condition holds up to here."
+
+let vernac_validate_proof ~pstate =
+  let pts = Declare.Proof.get pstate in
+  let { Proof.entry; Proof.sigma } = Proof.data pts in
+  let hyps, pfterm, pftyp = List.hd (Proofview.initial_goals entry) in
+  (* XXX can the initial hyps contain something broken? For now assume they're correct.
+     NB: in the "Lemma foo args : bla." case the args are part of the
+     term and intro'd after the proof is opened. Only the section
+     variables are in the hyps. *)
+  let env = Environ.reset_with_named_context hyps (Global.env ()) in
+  let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
+  let sigma' = Typing.check env sigma pfterm pftyp in
+  let evar_issues =
+    (* Use Evar.Map.merge as a kind of for_all2 *)
+    Evar.Map.merge (fun e orig now -> match orig, now with
+        | None, None -> assert false
+        | Some _, Some _ -> None (* assume same *)
+        | Some evi, None ->
+          let EvarInfo evi' = Evd.find sigma' e in
+          let body = match Evd.evar_body evi' with
+            | Evar_empty -> assert false
+            | Evar_defined body -> body
+          in
+          Some
+            Pp.(str "Evar " ++ Printer.pr_evar sigma (e, evi)
+                ++ spc() ++ str "was inferred by unification to be" ++ spc()
+                ++ pr_econstr_env (Evd.evar_env env evi') sigma' body)
+        | None, Some _ -> (* ignore new evar *)
+          assert (not (Evd.is_defined sigma e));
+          None
+      )
+      (Evd.undefined_map sigma)
+      (Evd.undefined_map sigma')
+  in
+  (* TODO check ustate *)
+
+  if Evar.Map.is_empty evar_issues then
+    str "No issues found."
+  else prlist_with_sep fnl snd (Evar.Map.bindings evar_issues)
 
 let translate_vernac_synterp ?loc ~atts v = let open Vernacextend in match v with
   | EVernacNotation { local; decl } ->
@@ -2482,6 +2516,10 @@ let translate_pure_vernac ?loc ~atts v = let open Vernacextend in match v with
     vtreadproof(fun ~pstate ->
         unsupported_attributes atts;
         Feedback.msg_notice @@ vernac_check_guard ~pstate)
+  | VernacValidateProof ->
+    vtreadproof(fun ~pstate ->
+        unsupported_attributes atts;
+        Feedback.msg_notice @@ vernac_validate_proof ~pstate)
   | VernacProof (tac, using) ->
     vtmodifyproof(fun ~pstate ->
     unsupported_attributes atts;

vernac/vernacexpr.mli

@@ -486,6 +486,7 @@ type nonrec synpure_vernac_expr =
   | VernacEndSubproof
   | VernacShow of showable
   | VernacCheckGuard
+  | VernacValidateProof
   | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
 
   | VernacAddOption of Goptions.option_name * Goptions.table_value list