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`A, B`

, `A`

, and `B`

are arguments? For `intros n m`

, could I say all of `n m`

, `n`

, and `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 `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.

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

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

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