6

I want to make a Ltac tactic in coq which would take either 1 or 3 arguments. I have read about ltac_No_arg in the LibTactics module but if I understood it correctly I would have to invoke my tactic with :

Coq < mytactic arg_1 ltac_no_arg ltac_no_arg.

which is not very convenient.

Is there any way to get a result like this ? :

Coq < mytactic arg_1.

Coq < mytactic arg_1 arg_2 arg_3.
L. Soret
  • 169
  • 10

1 Answers1

8

We can use the Tactic Notation mechanism to try to solve your issue because it can handle variadic arguments.

Let's reuse ltac_No_arg and define a dummy tactic mytactic for the purposes of demonstration

Inductive ltac_No_arg : Set :=
  | ltac_no_arg : ltac_No_arg.

Ltac mytactic x y z :=
  match type of y with
  | ltac_No_arg => idtac "x =" x  (* a bunch of cases omitted *)
  | _ => idtac "x =" x "; y =" y "; z =" z
  end.

Now let's define the aforementioned tactic notations:

Tactic Notation "mytactic_notation" constr(x) :=
  mytactic x ltac_no_arg ltac_no_arg.
Tactic Notation "mytactic_notation" constr(x) constr(y) constr(z) :=
  mytactic x y z.

Tests:

Goal True.
  mytactic_notation 1.
  mytactic_notation 1 2 3.
Abort.
Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
  • What is `constr(x)`? `x` in Vernacular? – jaam Oct 03 '17 at 22:39
  • It specifies the type of an argument for `Tactic Notation`. Here, `constr(x)` means we parse and interpret `x` as a term, not an identifier, integer and so on. – Anton Trunov Oct 04 '17 at 06:53
  • Do you mean [this](https://coq.inria.fr/refman/Reference-Manual003.html#term)? The definition is as broad as it gets (e.g. types and sorts are proper subclasses of terms, `qualid` is a term, defined as identifier, etc.) – jaam Oct 04 '17 at 20:17
  • 1
    No, I meant [this section](https://coq.inria.fr/distrib/current/refman/Reference-Manual014.html#sec578). – Anton Trunov Oct 04 '17 at 20:19
  • @HuStmpHrrr Fixed, thanks. But the docs are being ported to Sphinx now, so not for long I guess. – Anton Trunov Mar 15 '18 at 20:20