Ltac : optional arguments tactic

问题:

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.

回答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.