Ltac : optional arguments tactic

Question

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.

Subtropics

Answer 1

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.

Quadratic

What is constr(x)? x in Vernacular? – Terrell

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. – Quadratic

Do you mean this? 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.) – Terrell

No, I meant this section. – Quadratic

@HuStmpHrrr Fixed, thanks. But the docs are being ported to Sphinx now, so not for long I guess. – Quadratic