Stream: Coq users

Topic: Arguments in tactic


view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Jul 04 2020 at 15:32):

I’d say not: each builtin tactic has its own (pretty arbitrary) grammar.

view this post on Zulip Paolo Giarrusso (Jul 04 2020 at 15:33):

e.g. in “eauto using foo”, “using” is certainly not an argument.

view this post on Zulip Paolo Giarrusso (Jul 04 2020 at 15:33):

I’d also like to know if there is a way to call those things.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Jan 29 2023 at 06:02 UTC