Ltac ：可选参数策略

Question

我想在 coq 中制定一个 Ltac 策略，它需要 1 个或 3 个参数。我已经在 LibTactics 模块中阅读了有关 ltac_No_arg 的内容，但如果我理解正确，我将不得不调用我的策略：

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.

Ltac ：可选参数策略

Ltac : optional arguments tactic

coq

variadic

ltac