Ltac: необязательные аргументы тактики

Question

Я хочу сделать тактику Ltac в coq, которая будет принимать 1 или 3 аргумента. Я читал о ltac_No_arg в LibTactics модуль, но если я правильно понял, мне пришлось бы использовать мою тактику с помощью:

Coq < mytactic arg_1 ltac_no_arg ltac_no_arg.

что не очень удобно.

Есть ли способ получить такой результат?:

Coq < mytactic arg_1.

Coq < mytactic arg_1 arg_2 arg_3.

Answer 1

Мы можем использовать Tactic Notation механизм, чтобы попытаться решить вашу проблему, потому что он может обрабатывать различные аргументы.

Давайте использовать повторно ltac_No_arg и определить фиктивную тактику mytactic в целях демонстрации

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.

Теперь давайте определим вышеупомянутые обозначения тактики:

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.

тесты:

Goal True.
  mytactic_notation 1.
  mytactic_notation 1 2 3.
Abort.