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 of
B are arguments? For
intros n m, could I say all of
m are arguments?
I’d say not: each builtin tactic has its own (pretty arbitrary) grammar.
e.g. in “eauto using foo”, “using” is certainly not an argument.
I’d also like to know if there is a way to call those things.
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.
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
Apparently, the manual uses "arguments" or "parameters" informally in this case, but doesn't seem to define it.
So, unlike I said, I guess
m are informally arguments
intros n m. But in that case,
m are in particular introduction patterns, and that concept _is_ defined.
Thanks very much! After taking your suggestions into consideration, to make my work more precise, I would like to define the argument only as
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
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
and maybe Ltac2 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):
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: Jan 29 2023 at 06:02 UTC