From 826cc836b812dc45470ee21f09742e9bb9359827 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 14 May 2024 15:53:44 +0200 Subject: [PATCH 1/2] Move core bracket handling code to proof.ml from vernacentries --- proofs/proof.ml | 20 ++++++++++++++++++++ proofs/proof.mli | 10 ++++++++++ vernac/vernacentries.ml | 25 +++++++++---------------- 3 files changed, 39 insertions(+), 16 deletions(-) diff --git a/proofs/proof.ml b/proofs/proof.ml index 3304bbffcdc1..1e26e41e579e 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -262,6 +262,26 @@ 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 Names.Id.t + +let start_subproof gln p = + match gln with + | SubproofNth n -> focus subproof_cond () n p + | SubproofId id -> focus_id subproof_cond () id p + +let end_subproof p = + unfocus subproof_kind p () + (*** Proof Creation/Termination ***) (* [end_of_stack] is unfocused by return to close every loose focus. *) diff --git a/proofs/proof.mli b/proofs/proof.mli index c96b378c7698..37447127b502 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -143,6 +143,16 @@ 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 Names.Id.t + +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]. *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f2a305d9d288..cd4c36262213 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2487,26 +2487,19 @@ 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 + | None -> SubproofNth 1 + | Some (Goal_select.SelectList [NthSelector n]) -> SubproofNth n + | Some (Goal_select.SelectList [IdSelector id]) -> SubproofId id + | _ -> 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 -> From 1109e0cbcc9214ffd8eda103c6bc0031cdaf7aac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 14 May 2024 17:02:46 +0200 Subject: [PATCH 2/2] `abstract:{` tactic block --- .../19023-SkySkimmer-abstract-subproof.sh | 1 + .../04-tactics/19023-abstract-subproof.rst | 4 + .../proofs/writing-proofs/proof-mode.rst | 9 ++- doc/tools/docgram/common.edit_mlg | 8 +- doc/tools/docgram/fullGrammar | 1 + doc/tools/docgram/orderedGrammar | 2 +- proofs/proof.ml | 77 +++++++++++++++++-- proofs/proof.mli | 5 +- tactics/abstract.ml | 3 + test-suite/success/abstract_subproof.v | 33 ++++++++ vernac/g_vernac.mlg | 3 +- vernac/ppvernac.ml | 6 +- vernac/vernacentries.ml | 9 ++- vernac/vernacexpr.mli | 6 +- 14 files changed, 148 insertions(+), 19 deletions(-) create mode 100644 dev/ci/user-overlays/19023-SkySkimmer-abstract-subproof.sh create mode 100644 doc/changelog/04-tactics/19023-abstract-subproof.rst create mode 100644 test-suite/success/abstract_subproof.v diff --git a/dev/ci/user-overlays/19023-SkySkimmer-abstract-subproof.sh b/dev/ci/user-overlays/19023-SkySkimmer-abstract-subproof.sh new file mode 100644 index 000000000000..66ab4375aa7e --- /dev/null +++ b/dev/ci/user-overlays/19023-SkySkimmer-abstract-subproof.sh @@ -0,0 +1 @@ +overlay coq_lsp https://github.com/SkySkimmer/coq-lsp abstract-subproof 19023 diff --git a/doc/changelog/04-tactics/19023-abstract-subproof.rst b/doc/changelog/04-tactics/19023-abstract-subproof.rst new file mode 100644 index 000000000000..d0a822ae537c --- /dev/null +++ b/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 `_, + by Gaëtan Gilbert). diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst index 138bbd0ee983..4f623091070d 100644 --- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst +++ b/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. diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 87f047dc569f..5049fa476687 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/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 ] diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 0ef386fab6fc..2c71eadd3f78 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -892,6 +892,7 @@ noedit_mode: [ subprf: [ | BULLET | "}" +| "abstract" ":" "{" ] subprf_with_selector: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index ac4d92becc59..0416965c3628 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/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 diff --git a/proofs/proof.ml b/proofs/proof.ml index 1e26e41e579e..4af16447ddfd 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -272,15 +272,80 @@ let subproof_cond = done_cond subproof_kind type subproof_select = | SubproofNth of int - | SubproofId of Names.Id.t + | SubproofId of Libnames.qualid + | SubproofAbstract let start_subproof gln p = match gln with - | SubproofNth n -> focus subproof_cond () n p - | SubproofId id -> focus_id subproof_cond () id p - -let end_subproof p = - unfocus subproof_kind p () + | 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 ***) diff --git a/proofs/proof.mli b/proofs/proof.mli index 37447127b502..8fa24b07723b 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -147,7 +147,8 @@ val unfocus_all : t -> t type subproof_select = | SubproofNth of int - | SubproofId of Names.Id.t + | SubproofId of Libnames.qualid + | SubproofAbstract val start_subproof : subproof_select -> t -> t @@ -229,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 diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 417c60dd35ad..69d2ee53d096 100644 --- a/tactics/abstract.ml +++ b/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) diff --git a/test-suite/success/abstract_subproof.v b/test-suite/success/abstract_subproof.v new file mode 100644 index 000000000000..be1ba8c0c66b --- /dev/null +++ b/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. diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index a4e6a9080b01..d78119172cd5 100644 --- a/vernac/g_vernac.mlg +++ b/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 } ] ] diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 70d723e65527..76ef157ed53f 100644 --- a/vernac/ppvernac.ml +++ b/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 "}") diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index cd4c36262213..9a84a8765142 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2491,10 +2491,11 @@ let vernac_subproof gln ~pstate = let gln = let open Proof in match gln with - | None -> SubproofNth 1 - | Some (Goal_select.SelectList [NthSelector n]) -> SubproofNth n - | Some (Goal_select.SelectList [IdSelector id]) -> SubproofId id - | _ -> user_err (str "Brackets do not support multi-goal selectors.") + | 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 diff --git a/vernac/vernacexpr.mli b/vernac/vernacexpr.mli index fe8a16a63143..684baee722d8 100644 --- a/vernac/vernacexpr.mli +++ b/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