Skip to content

Adding "Body", synonymous of "Proof", for interactively-defined definitions #18709

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
herbelin wants to merge 1 commit into from
Closed

Adding "Body", synonymous of "Proof", for interactively-defined definitions #18709

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions doc/tools/docgram/common.edit_mlg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1328,9 +1328,9 @@ command: [
| REPLACE "Preterm" "of" identref
| WITH "Preterm" OPT ( "of" identref )
| DELETE "Preterm"
| REPLACE "Proof" "using" section_var_expr "with" Pltac.tactic
| WITH "Proof" "using" section_subset_expr OPT [ "with" ltac_expr5 ]
| DELETE "Proof" "using" section_var_expr
| REPLACE proof_kw "using" section_var_expr "with" Pltac.tactic
| WITH proof_kw "using" section_subset_expr OPT [ "with" ltac_expr5 ]
| DELETE proof_kw "using" section_var_expr

(* hide the fact that table names are limited to 2 IDENTs *)
| REPLACE "Remove" IDENT IDENT LIST1 table_value
Expand All @@ -1348,7 +1348,7 @@ command: [
| REPLACE "Show" "Ltac" "Profile" "CutOff" integer
| WITH "Show" "Ltac" "Profile" OPT [ "CutOff" integer | string ]
| DELETE "Show" "Ltac" "Profile" string
| DELETE "Show" "Proof" (* combined with Show Proof Diffs in vernac_toplevel *)
| DELETE "Show" proof_kw (* combined with Show Proof Diffs in vernac_toplevel *)
| REPLACE "Solve" "All" "Obligations" "with" tactic
| WITH "Solve" "All" "Obligations" OPT ( "with" tactic )
| DELETE "Solve" "All" "Obligations"
Expand Down Expand Up @@ -1555,8 +1555,8 @@ vernac_toplevel: [
| WITH "BackTo" natural
| REPLACE "Show" "Goal" natural "at" natural "."
| WITH "Show" "Goal" natural "at" natural
| REPLACE "Show" "Proof" "Diffs" OPT "removed" "."
| WITH "Show" "Proof" OPT ( "Diffs" OPT "removed" )
| REPLACE "Show" proof_kw "Diffs" OPT "removed" "."
| WITH "Show" proof_kw OPT ( "Diffs" OPT "removed" )
| DELETE vernac_control
]

Expand Down
21 changes: 13 additions & 8 deletions doc/tools/docgram/fullGrammar
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -482,7 +482,7 @@ vernac_toplevel: [
| "Quit" "."
| "BackTo" natural "."
| test_show_goal "Show" "Goal" natural "at" natural "."
| "Show" "Proof" "Diffs" OPT "removed" "."
| "Show" proof_kw "Diffs" OPT "removed" "."
| Pvernac.Vernac_.main_entry
]

Expand All @@ -491,12 +491,17 @@ opt_hintbases: [
| ":" LIST1 IDENT
]

proof_kw: [
| "Proof"
| "Body"
]

command: [
| "Goal" lconstr
| "Proof"
| "Proof" "using" G_vernac.section_subset_expr
| proof_kw
| proof_kw "using" G_vernac.section_subset_expr
| "Proof" "Mode" string
| "Proof" lconstr
| proof_kw lconstr
| "Abort"
| "Abort" "All"
| "Admitted"
Expand All @@ -514,16 +519,16 @@ command: [
| "Unfocused"
| "Show"
| "Show" natural
| "Show" proof_kw
| "Show" ident
| "Show" "Existentials"
| "Show" "Universes"
| "Show" "Conjectures"
| "Show" "Proof"
| "Show" "Intro"
| "Show" "Intros"
| "Show" "Match" reference
| "Guarded"
| "Validate" "Proof"
| "Validate" proof_kw
| "Create" "HintDb" IDENT; [ "discriminated" | ]
| "Remove" "Hints" LIST1 global opt_hintbases
| "Hint" hint opt_hintbases
Expand Down Expand Up @@ -610,8 +615,8 @@ command: [
| "Typeclasses" "Transparent" LIST1 reference
| "Typeclasses" "Opaque" LIST1 reference
| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT natural
| "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ]
| "Proof" "using" G_vernac.section_subset_expr "with" Pltac.tactic
| proof_kw "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ]
| proof_kw "using" G_vernac.section_subset_expr "with" Pltac.tactic
| "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic
| "Print" "Ltac" reference
| "Locate" "Ltac" reference
Expand Down
17 changes: 11 additions & 6 deletions doc/tools/docgram/orderedGrammar
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -707,6 +707,11 @@ strategy_level: [
| "transparent"
]

proof_kw: [
| "Proof"
| "Body"
]

strategy_level_or_var: [
| strategy_level
| ident
Expand All @@ -723,6 +728,7 @@ simple_reserv: [

command: [
| "Goal" type
| proof_kw
| "Pwd"
| "Cd" OPT string
| "Load" OPT "Verbose" [ string | ident ]
Expand Down Expand Up @@ -808,9 +814,8 @@ command: [
| "Extract" "Inlined" "Constant" qualid "=>" [ ident | string ] (* extraction plugin *)
| "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string (* extraction plugin *)
| "Show" "Extraction" (* extraction plugin *)
| "Proof"
| "Proof" "Mode" string
| "Proof" term
| proof_kw term
| "Abort" OPT "All"
| "Admitted"
| "Qed"
Expand All @@ -825,12 +830,11 @@ command: [
| "Show" "Existentials"
| "Show" "Universes"
| "Show" "Conjectures"
| "Show" "Proof" OPT ( "Diffs" OPT "removed" )
| "Show" "Intro"
| "Show" "Intros"
| "Show" "Match" qualid
| "Guarded"
| "Validate" "Proof"
| "Validate" proof_kw
| "Create" "HintDb" ident OPT "discriminated"
| "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident )
| "Comments" LIST0 [ one_term | string | natural ]
Expand Down Expand Up @@ -872,8 +876,8 @@ command: [
| "Typeclasses" "Transparent" LIST1 qualid
| "Typeclasses" "Opaque" LIST1 qualid
| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural
| "Proof" "with" ltac_expr OPT [ "using" section_var_expr ]
| "Proof" "using" section_var_expr OPT [ "with" ltac_expr ]
| proof_kw "with" ltac_expr OPT [ "using" section_var_expr ]
| proof_kw "using" section_var_expr OPT [ "with" ltac_expr ]
| "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr
| "Print" "Rewrite" "HintDb" ident
| "Print" "Ltac" qualid
Expand Down Expand Up @@ -1001,6 +1005,7 @@ command: [
| "Quit"
| "BackTo" natural
| "Show" "Goal" natural "at" natural
| "Show" proof_kw OPT ( "Diffs" OPT "removed" )
]

section_var_expr: [
Expand Down
5 changes: 3 additions & 2 deletions plugins/ltac/g_ltac.mlg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ open Pcoq.Prim
open Pcoq.Constr
open Pvernac.Vernac_
open Pltac
open G_proofs

let fail_default_value = Locus.ArgArg 0

Expand Down Expand Up @@ -288,10 +289,10 @@ GRAMMAR EXTEND Gram
| g = OPT toplevel_selector; "{" -> { Vernacexpr.VernacSynPure (Vernacexpr.VernacSubproof g) } ] ]
;
command: TOP
[ [ IDENT "Proof"; "with"; ta = Pltac.tactic;
[ [ proof_kw; "with"; ta = Pltac.tactic;
l = OPT [ IDENT "using"; l = G_vernac.section_subset_expr -> { l } ] ->
{ Vernacexpr.VernacSynPure (Vernacexpr.VernacProof (Some (in_tac ta), l)) }
| IDENT "Proof"; IDENT "using"; l = G_vernac.section_subset_expr;
| proof_kw; IDENT "using"; l = G_vernac.section_subset_expr;
"with"; ta = Pltac.tactic ->
{ Vernacexpr.VernacSynPure (Vernacexpr.VernacProof (Some (in_tac ta),Some l)) } ] ]
;
Expand Down
3 changes: 2 additions & 1 deletion toplevel/g_toplevel.mlg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ DECLARE GLOBAL PLUGIN
open Pcoq
open Pcoq.Prim
open Vernacexpr
open G_proofs

(* Vernaculars specific to the toplevel *)
type vernac_toplevel =
Expand Down Expand Up @@ -46,7 +47,7 @@ GRAMMAR EXTEND Gram
(* show a goal for the specified proof state *)
| test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." ->
{ Some (VernacShowGoal {gid; sid}) }
| IDENT "Show"; IDENT "Proof"; IDENT "Diffs"; removed = OPT [ IDENT "removed" -> { () } ]; "." ->
| IDENT "Show"; proof_kw; IDENT "Diffs"; removed = OPT [ IDENT "removed" -> { () } ]; "." ->
{ Some (VernacShowProofDiffs
(if removed = None then Proof_diffs.DiffOn else Proof_diffs.DiffRemoved)) }
| cmd = Pvernac.Vernac_.main_entry ->
Expand Down
19 changes: 12 additions & 7 deletions vernac/g_proofs.mlg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,8 @@ let thm_token = G_vernac.thm_token

let hint = Entry.make "hint"

let proof_kw = Entry.make "proof_kw"

let warn_deprecated_focus =
CWarnings.create ~name:"deprecated-focus" ~category:Deprecation.Version.v8_8
Pp.(function
Expand All @@ -48,20 +50,23 @@ let warn_deprecated_unfocus =

(* Proof commands *)
GRAMMAR EXTEND Gram
GLOBAL: hint command;
GLOBAL: hint command proof_kw;

opt_hintbases:
[ [ -> { [] }
| ":"; l = LIST1 [id = IDENT -> { id } ] -> { l } ] ]
;
proof_kw:
[ [ IDENT "Proof" -> { Opaque } | IDENT "Body" -> { Transparent } ] ]
;
command: TOP
[ [ IDENT "Goal"; c = lconstr ->
{ VernacSynPure (VernacDefinition (Decls.(NoDischarge, Definition), ((CAst.make ~loc Names.Anonymous), None), ProveBody ([], c))) }
| IDENT "Proof" -> { VernacSynPure (VernacProof (None,None)) }
| IDENT "Proof"; IDENT "using"; l = G_vernac.section_subset_expr ->
| proof_kw -> { VernacSynPure (VernacProof (None,None)) }
| proof_kw; IDENT "using"; l = G_vernac.section_subset_expr ->
{ VernacSynPure (VernacProof (None,Some l)) }
| IDENT "Proof" ; IDENT "Mode" ; mn = string -> { VernacSynterp (VernacProofMode mn) }
| IDENT "Proof"; c = lconstr -> { VernacSynPure (VernacExactProof c) }
| IDENT "Proof"; IDENT "Mode" ; mn = string -> { VernacSynterp (VernacProofMode mn) }
| kw = proof_kw; c = lconstr -> { VernacSynPure (VernacExactProof (kw, c)) }
| IDENT "Abort" -> { VernacSynPure VernacAbort }
| IDENT "Abort"; IDENT "All" -> { VernacSynPure VernacAbortAll }
| IDENT "Admitted" -> { VernacSynPure (VernacEndProof Admitted) }
Expand All @@ -87,16 +92,16 @@ GRAMMAR EXTEND Gram
| IDENT "Unfocused" -> { VernacSynPure VernacUnfocused }
| IDENT "Show" -> { VernacSynPure (VernacShow (ShowGoal OpenSubgoals)) }
| IDENT "Show"; n = natural -> { VernacSynPure (VernacShow (ShowGoal (NthGoal n))) }
| IDENT "Show"; proof_kw -> { VernacSynPure (VernacShow ShowProof) }
| IDENT "Show"; id = ident -> { VernacSynPure (VernacShow (ShowGoal (GoalId id))) }
| IDENT "Show"; IDENT "Existentials" -> { VernacSynPure (VernacShow ShowExistentials) }
| IDENT "Show"; IDENT "Universes" -> { VernacSynPure (VernacShow ShowUniverses) }
| IDENT "Show"; IDENT "Conjectures" -> { VernacSynPure (VernacShow ShowProofNames) }
| IDENT "Show"; IDENT "Proof" -> { VernacSynPure (VernacShow ShowProof) }
| IDENT "Show"; IDENT "Intro" -> { VernacSynPure (VernacShow (ShowIntros false)) }
| 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 }
| IDENT "Validate"; proof_kw -> { VernacSynPure VernacValidateProof }
(* Hints for Auto and EAuto *)
| IDENT "Create"; IDENT "HintDb" ;
id = IDENT ; b = [ IDENT "discriminated" -> { true } | -> { false } ] ->
Expand Down
2 changes: 2 additions & 0 deletions vernac/g_proofs.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,3 +11,5 @@
val thm_token : Decls.theorem_kind Pcoq.Entry.t

val hint : Vernacexpr.hints_expr Pcoq.Entry.t

val proof_kw : Vernacexpr.opacity_flag Pcoq.Entry.t
5 changes: 3 additions & 2 deletions vernac/ppvernac.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -859,8 +859,9 @@ let pr_synpure_vernac_expr v =
| Opaque -> keyword "Qed")
| Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
)
| VernacExactProof c ->
return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
| VernacExactProof (opac, c) ->
let proof_kw = match opac with Transparent -> "Body" | Opaque -> "Proof" in
return (hov 2 (keyword proof_kw ++ pr_lconstrarg c))
| VernacAssumption ((discharge,kind),t,l) ->
let n = List.length (List.flatten (List.map fst (List.map snd l))) in
let pr_params (c, (xl, t)) =
Expand Down
8 changes: 4 additions & 4 deletions vernac/vernacentries.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -732,11 +732,11 @@ let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function

let vernac_abort ~lemma:_ ~pm = pm

let vernac_exact_proof ~lemma ~pm c =
let vernac_exact_proof ~lemma ~pm opaque c =
(* spiwack: for simplicity I do not enforce that "Proof proof_term" is
called only at the beginning of a proof. *)
let lemma, status = Declare.Proof.by (Tactics.exact_proof c) lemma in
let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque:Opaque ~idopt:None in
let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque ~idopt:None in
if not status then Feedback.feedback Feedback.AddedAxiom;
pm

Expand Down Expand Up @@ -2344,10 +2344,10 @@ let translate_pure_vernac ?loc ~atts v = let open Vernactypes in match v with

| VernacStartTheoremProof (k,l) ->
vtopenproof(fun () -> with_def_attributes ~atts vernac_start_proof k l)
| VernacExactProof c ->
| VernacExactProof (opaque,c) ->
vtcloseproof (fun ~lemma ->
unsupported_attributes atts;
vernac_exact_proof ~lemma c)
vernac_exact_proof ~lemma opaque c)

| VernacAssumption ((discharge,kind),nl,l) ->
vtdefault(fun () -> with_def_attributes ~atts vernac_assumption discharge kind l nl)
Expand Down
2 changes: 1 addition & 1 deletion vernac/vernacexpr.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -405,7 +405,7 @@ type nonrec synpure_vernac_expr =
| VernacDefinition of (discharge * Decls.definition_object_kind) * name_decl * definition_expr
| VernacStartTheoremProof of Decls.theorem_kind * proof_expr list
| VernacEndProof of proof_end
| VernacExactProof of constr_expr
| VernacExactProof of opacity_flag * constr_expr
| VernacAssumption of (discharge * Decls.assumption_object_kind) *
Declaremods.inline * (ident_decl list * constr_expr) with_coercion list
| VernacSymbol of (ident_decl list * constr_expr) with_coercion list
Expand Down