abstract:{ tactic block

dev/ci/user-overlays/19023-SkySkimmer-abstract-subproof.sh

@@ -0,0 +1 @@
+overlay coq_lsp https://github.com/SkySkimmer/coq-lsp abstract-subproof 19023

doc/changelog/04-tactics/19023-abstract-subproof.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  :tacn:`abstract` support for proof blocks, e.g. `abstract:{ tac1. tac2. }`
+  (`#19023 <https://github.com/coq/coq/pull/19023>`_,
+  by Gaëtan Gilbert).

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

@@ -612,7 +612,7 @@ subgoals are also focused.  The two focusing constructs are
 Curly braces
 ~~~~~~~~~~~~
 
-.. tacn:: {? {| @natural | [ @qualid ] } : } %{
+.. tacn:: {? {| @natural | [ @qualid ] | abstract } : } %{
           %}
    :name: {; }
 
@@ -672,6 +672,13 @@ Curly braces
          [x]: exact 0.
          Qed.
 
+   :n:`abstract: %{`
+      Focuses on the first goal. The subproof is saved as an auxiliary
+      lemma, like with tactic :tacn:`abstract`. In other words, when
+      the subproof is a single tactic `tac`, `abstract:{ tac. }` is
+      equivalent to `{ abstract tac. }`, but `abstract:{` also allows
+      multi-command subproofs.
+
    .. exn:: This proof is focused, but cannot be unfocused this way.
 
       You are trying to use ``}`` but the current subproof has not been fully solved.

doc/tools/docgram/common.edit_mlg

@@ -1761,12 +1761,16 @@ tactic_mode: [
 | MOVETO simple_tactic subprf
 | REPLACE OPT toplevel_selector "{"
 (* semantically restricted *)
-| WITH OPT ( [ natural | "[" fullyqualid "]" ] ":" ) "{"
-| MOVETO simple_tactic OPT ( [ natural | "[" fullyqualid "]" ] ":" ) "{"
+| WITH OPT ( [ natural | "[" fullyqualid "]" | "abstract" ] ":" ) "{"
+| MOVETO simple_tactic OPT ( [ natural | "[" fullyqualid "]" | "abstract" ] ":" ) "{"
 | DELETE command
 | DELETENT
 ]
 
+subprf: [
+| DELETE "abstract" ":" "{"
+]
+
 SPLICE: [
 | subprf
 ]

doc/tools/docgram/fullGrammar

@@ -892,6 +892,7 @@ noedit_mode: [
 subprf: [
 | BULLET
 | "}"
+| "abstract" ":" "{"
 ]
 
 subprf_with_selector: [

doc/tools/docgram/orderedGrammar

@@ -1440,9 +1440,9 @@ simple_tactic: [
 | "replace" OPT [ "->" | "<-" ] one_term "with" one_term OPT occurrences OPT ( "by" ltac_expr3 )
 | "typeclasses" "eauto" OPT [ "bfs" | "dfs" | "best_effort" ] OPT nat_or_var OPT ( "with" LIST1 ident )
 | "setoid_replace" one_term "with" one_term OPT ( "using" "relation" one_term ) OPT ( "in" ident ) OPT ( "at" LIST1 int_or_var ) OPT ( "by" ltac_expr3 )
-| OPT ( [ natural | "[" qualid "]" ] ":" ) "{"
 | [ LIST1 "-" | LIST1 "+" | LIST1 "*" ]
 | "}"
+| OPT ( [ natural | "[" qualid "]" | "abstract" ] ":" ) "{"
 | "try" ltac_expr3
 | "do" nat_or_var ltac_expr3
 | "timeout" nat_or_var ltac_expr3

proofs/proof.ml

@@ -262,6 +262,91 @@ let rec maximal_unfocus k p =
     with FullyUnfocused | CannotUnfocusThisWay -> p
   else p
 
+(** Brackets "{" and "}" *)
+
+(* "{" focuses on the first goal, "n: {" focuses on the n-th goal
+    "}" unfocuses, provided that the proof of the goal has been completed.
+*)
+let subproof_kind = new_focus_kind "subproof"
+let subproof_cond = done_cond subproof_kind
+
+type subproof_select =
+  | SubproofNth of int
+  | SubproofId of Libnames.qualid
+  | SubproofAbstract
+
+let start_subproof gln p =
+  match gln with
+  | SubproofNth n -> focus subproof_cond None n p
+  | SubproofId id -> focus_id subproof_cond None id p
+  | SubproofAbstract ->
+    let (focused_goals, _) = Proofview.proofview p.proofview in
+    match focused_goals with
+    | [] -> raise (NoSuchGoals (1,1))
+    | g :: _ ->
+      let tac =
+        let open Proofview in
+        let open Proofview.Notations in
+        tclFOCUS 1 1 begin
+          (* some way to say "don't worry about this evar" would be nice,
+             currently when it's the last goal in the proof
+             it says "some existentials remain" between the solving tactic and the "}" *)
+          Proofview.Unsafe.tclSETGOALS [] >>= fun () ->
+          tclEVARMAP >>= fun sigma ->
+          let evi = Evd.find_undefined sigma g in
+          let sigma, g' =
+            Evd.new_pure_evar
+              ~relevance:(Evd.evar_relevance evi)
+              (Evd.evar_filtered_hyps evi)
+              sigma
+              (Evd.evar_concl evi)
+          in
+          Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+          Proofview.Unsafe.tclSETGOALS [Proofview.with_empty_state g'] >>= fun () ->
+          tclUNIT g'
+        end
+      in
+      let g', pr, _, _, _ = Proofview.apply ~name:p.name ~poly:p.poly (Global.env()) tac p.proofview in
+      let p = { p with proofview = pr } in
+      focus subproof_cond (Some (g,g')) 1 p
+
+let abstract_v, abstract_hook = Hook.make ()
+let abstract_v : (unit Proofview.tactic -> unit Proofview.tactic) Hook.value = abstract_v
+
+let end_subproof p0 =
+  let p = unfocus subproof_kind p0 () in
+  let data = try get_at_focus subproof_kind p0
+    with NoSuchFocus ->
+      (* unfocus should have failed *)
+      assert false
+  in
+  match data with
+  | None -> p
+  | Some (g,g') ->
+    let tac =
+      let open Proofview in
+      let open Proofview.Notations in
+      Proofview.Unsafe.tclNEWGOALS ~before:true [Proofview.with_empty_state g] >>= fun () ->
+      tclFOCUS 1 1 begin
+        Hook.get abstract_v begin
+          (* [gl] is a clone of [g] generated by abstract internals *)
+          Goal.enter_one ~__LOC__ @@ fun gl ->
+          let sigma = Goal.sigma gl in
+          let evi = match Evd.find_defined sigma g' with
+            | Some evi -> evi
+            | None -> CErrors.user_err Pp.(str "Cannot unfocus abstract block: proof not complete.")
+          in
+          let c = EConstr.mkEvar (g', Evd.evar_identity_subst evi) in
+          let sigma = Evd.define (Goal.goal gl) c sigma in
+          Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+          Proofview.Unsafe.tclSETGOALS []
+        end
+      end
+    in
+    let (), pr, _, _, _ = Proofview.apply ~name:p.name ~poly:p.poly (Global.env()) tac p.proofview in
+    let p = { p with proofview = pr } in
+    p
+
 (*** Proof Creation/Termination ***)
 
 (* [end_of_stack] is unfocused by return to close every loose focus. *)

proofs/proof.mli

@@ -143,6 +143,17 @@ val unfocused : t -> bool
 (** Unfocus everything (fail if no allowed). *)
 val unfocus_all : t -> t
 
+(** Brackets "{" and "}" *)
+
+type subproof_select =
+  | SubproofNth of int
+  | SubproofId of Libnames.qualid
+  | SubproofAbstract
+
+val start_subproof : subproof_select -> t -> t
+
+val end_subproof : t -> t
+
 (* [get_at_focus k] gets the information stored at the closest focus point
     of kind [k].
     Raises [NoSuchFocus] if there is no focus point of kind [k]. *)
@@ -219,3 +230,5 @@ 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
+
+val abstract_hook : (unit Proofview.tactic -> unit Proofview.tactic) Hook.t

tactics/abstract.ml

@@ -93,3 +93,6 @@ let { Goptions.get = get_inline_abstract_subproof } =
     ~key:["Inline"; "Abstract"; "Subproof"]
     ~value:false
     ()
+
+let () = Hook.set Proof.abstract_hook
+    (fun tac -> tclABSTRACT None tac)

test-suite/success/abstract_subproof.v

@@ -0,0 +1,33 @@
+
+Axiom foo : nat -> bool -> nat.
+
+Lemma bar : nat.
+Proof.
+  apply foo.
+  abstract:{
+    exact 0.
+  }
+  exact true.
+Defined.
+
+Fail Check eq_refl : bar = foo 0 true.
+
+Check eq_refl : bar = foo _ true.
+
+Check bar_subproof : nat.
+
+Lemma baz : nat.
+Proof.
+  abstract:{
+    shelve.
+    Fail }
+    Unshelve.
+    exact 0.
+  }
+Qed.
+
+Lemma bii : forall x, x = 0 + x.
+Proof.
+  intros x.
+  abstract:{ reflexivity. }
+Qed.

vernac/g_vernac.mlg

@@ -170,10 +170,11 @@ GRAMMAR EXTEND Gram
   subprf:
   [ [ s = BULLET -> { VernacBullet (make_bullet s) }
     | "}" -> { VernacEndSubproof }
+    | IDENT "abstract"; ":"; "{" -> { VernacSubproof AbstractSubproof }
     ] ]
   ;
   subprf_with_selector:
-  [ [ "{" -> { fun g -> VernacSubproof g }
+  [ [ "{" -> { fun g -> VernacSubproof (GoalSubproof g) }
     (* query_command needs to be here to factor with VernacSubproof *)
     | c = query_command -> { c }
     ] ]

vernac/ppvernac.ml

@@ -1341,10 +1341,12 @@ let pr_synpure_vernac_expr v =
         | Star n -> str (String.make n '*')
         | Plus n -> str (String.make n '+')
       end)
-  | VernacSubproof None ->
+  | VernacSubproof (GoalSubproof None) ->
     return (str "{")
-  | VernacSubproof (Some i) ->
+  | VernacSubproof (GoalSubproof (Some i)) ->
     return (Goal_select.pr_goal_selector i ++ str ":" ++ spc () ++ str "{")
+  | VernacSubproof AbstractSubproof ->
+    return (str "abstract:" ++ spc() ++ str "{")
   | VernacEndSubproof ->
     return (str "}")
 

vernac/vernacentries.ml

@@ -2487,26 +2487,20 @@ let vernac_unfocused ~pstate =
   else
     user_err Pp.(str "The proof is not fully unfocused.")
 
-(* "{" focuses on the first goal, "n: {" focuses on the n-th goal
-    "}" unfocuses, provided that the proof of the goal has been completed.
-*)
-let subproof_kind = Proof.new_focus_kind "subproof"
-let subproof_cond = Proof.done_cond subproof_kind
-
 let vernac_subproof gln ~pstate =
-  Declare.Proof.map ~f:(fun p ->
+  let gln =
+    let open Proof in
     match gln with
-    | None -> Proof.focus subproof_cond () 1 p
-    | Some (Goal_select.SelectList [NthSelector n]) -> Proof.focus subproof_cond () n p
-    | Some (Goal_select.SelectList [IdSelector id]) -> Proof.focus_id subproof_cond () id p
-    | _ -> user_err
-             (str "Brackets do not support multi-goal selectors."))
-    pstate
+    | GoalSubproof None -> SubproofNth 1
+    | GoalSubproof (Some (Goal_select.SelectList [NthSelector n])) -> SubproofNth n
+    | GoalSubproof (Some (Goal_select.SelectList [IdSelector id])) -> SubproofId id
+    | AbstractSubproof -> SubproofAbstract
+    | GoalSubproof _ -> user_err (str "Brackets do not support multi-goal selectors.")
+  in
+  Declare.Proof.map ~f:(fun p -> Proof.start_subproof gln p) pstate
 
 let vernac_end_subproof ~pstate =
-  Declare.Proof.map ~f:(fun p ->
-      Proof.unfocus subproof_kind p ())
-    pstate
+  Declare.Proof.map ~f:Proof.end_subproof pstate
 
 let vernac_bullet (bullet : Proof_bullet.t) ~pstate =
   Declare.Proof.map ~f:(fun p ->

vernac/vernacexpr.mli

@@ -265,6 +265,10 @@ type scheme = {
   sch_sort : UnivGen.QualityOrSet.t ;
 }
 
+type subproof_kind =
+  | AbstractSubproof
+  | GoalSubproof of Goal_select.t option
+
 type section_subset_expr =
   | SsEmpty
   | SsType
@@ -505,7 +509,7 @@ type nonrec synpure_vernac_expr =
   | VernacUnfocus
   | VernacUnfocused
   | VernacBullet of Proof_bullet.t
-  | VernacSubproof of Goal_select.t option
+  | VernacSubproof of subproof_kind
   | VernacEndSubproof
   | VernacShow of showable
   | VernacCheckGuard