liao zhang (Jul 04 2020 at 14:07): liao zhang (Jul 04 2020 at 14:07):Hi, I am confused about what are arguments in Coq. I have read the documentation, but I have not found a formal definition of arguments thus having some confusion. For example, unfold A, B, could I say all ofA, B, A, and B are arguments? For intros n m, could I say all of n m, n, and m are arguments?
Paolo Giarrusso (Jul 04 2020 at 15:32):I’d say not: each builtin tactic has its own (pretty arbitrary) grammar.
Paolo Giarrusso (Jul 04 2020 at 15:33):e.g. in “eauto using foo”, “using” is certainly not an argument.
Paolo Giarrusso (Jul 04 2020 at 15:33):I’d also like to know if there is a way to call those things.
Paolo Giarrusso (Jul 04 2020 at 15:35):Conversely, if you define “Ltac mytactic x y z :=“, and call “mytactic a b c”, then a, b and c are clearly (Ltac-level) arguments of mytactic, which I think is an ltac-level function.
liao zhang (Jul 05 2020 at 02:24):Could I ask one more question to clarify my understanding? The documentation defines the syntax intros ident+, therefore according to the definition, the argument for intros n m can only be n m. A Single n is not the arguments of intros n m
Paolo Giarrusso (Jul 05 2020 at 10:33):Apparently, the manual uses "arguments" or "parameters" informally in this case, but doesn't seem to define it.
So, unlike I said, I guess n and m are informally arguments intros n m. But in that case, n and m are in particular introduction patterns, and that concept _is_ defined.
liao zhang (Jul 05 2020 at 10:51):Thanks very much! After taking your suggestions into consideration, to make my work more precise, I would like to define the argument only as qualid or ident which not points to Coq's kernel object or some tactics like auto. But treat A, B in unfold A, B as a list of arguments and n m in intros n m as a sequence of arguments
Paolo Giarrusso (Jul 05 2020 at 11:08):to make my work more precise
Hm, is your goal _using_ tactics or _describing_ tactics? And how accurate must the description be — a Coq introduction can be looser than a paper?
For an accurate description, you'd have to deal at least with Tactic Notation and Ltac commands:
https://coq.github.io/doc/v8.12/refman/user-extensions/syntax-extensions.html#coq:cmd.tactic-notation
https://coq.github.io/doc/v8.12/refman/proof-engine/ltac.html#defining-ltac-symbols
and maybe Ltac2 declarations:
https://coq.github.io/doc/v8.12/refman/proof-engine/ltac2.html#type-declarations
But that doesn't cover all; builtin tactics and Coq plugins can extend the syntax arbitrarily. Which is why the manual only defines things like "sentence" "command" and "tactic", but doesn't define the structure of a tactic further (not in general, at least):
https://coq.github.io/doc/v8.12/refman/language/core/basic.html
liao zhang (Jul 05 2020 at 11:57):Thanks! I need to describe tactics precisely in a paper. I should deal with Tactic Notation and Ltac. Maybe I will not consider user-extension.
Last updated: Oct 13 2024 at 01:02 UTC