liao zhang (Jun 14 2020 at 08:33): liao zhang (Jun 14 2020 at 08:33):Hi, sorry to trouble you. To prove a theorem, a Coq user needs to write command one by one.
Like “simpl.” “Intro;simpl;auto.”, all of them are one command written by a Coq user.
Is there a word to describe the single command written by the user?
I found I could not use “tactic” to describe such command, as a tactic can also refer to “intro” in “Intro;simpl;auto.”.
Also, Vernacular commands seem not suitable. Could anyone give me some help?
Kenji Maillard (Jun 14 2020 at 08:36):I would refer to these as "tactic scripts" (but never as commands, I would keep that latter term for the Vernacular in Coq).
Karl Palmskog (Jun 14 2020 at 08:37):Coq input works at the level of "sentences". Each sentence ends with a period. For example, the following are all sentences:
Theorem truth : True.
simpl.
intro;simpl;auto.
It's also fine to refer to a sentence as a "Vernacular command", since the top-level language of Coq is called "the Vernacular". Sentences in Ltac (or other tactic languages) might be described as "tactic commands" or "tactic sentences".
liao zhang (Jun 14 2020 at 08:40):Thanks very much! Now, I understand!
Karl Palmskog (Jun 14 2020 at 08:44):Kenji Maillard said:
I would refer to these as "tactic scripts" (but never as commands, I would keep that latter term for the Vernacular in Coq).
How is something emphatically not a command if it affects the proof state? I think it's fine to refer to a collection of tactic sentences as a "proof script"/"tactic script", but why would "tactic command" not be accurate?
Karl Palmskog (Jun 14 2020 at 08:46):even if you look at Coq's implementation, Ltac is written as an extension to the Vernacular, and the Vernacular is consistently described as a "command language".
Kenji Maillard (Jun 14 2020 at 08:50):It might be my own misunderstanding of Coq's system but I had the impression that the Vernacular refer to the (toplevel) commands manipulating Coq's environment (like definitions, theorems, typeclass instances, inductives...) by opposition to the various languages employed inside a proof/definition (Gallina, Ltac{1,2}, Mtac, ...) that act over the proof state
Karl Palmskog (Jun 14 2020 at 08:55):sure, you do have the basic built-in Vernacular commands, like Definition, Theorem, etc. But as per above, Ltac/Ltac2/MTac hook into (extends) the Vernacular AST at the OCaml level. Each Ltac sentence effectively has an AST that starts like this:
((VernacExpr()(VernacExtend(VernacSolve 0)((GenArg raw(OptArg(ExtraArg ltac_selector))...
Last updated: Apr 19 2024 at 17:02 UTC