LTAC:可选参数策略

问题描述

我想在Coq中制定一个Ltac策略，该策略可以使用1个或3个参数.我已经在 LibTactics 模块中阅读了有关ltac_No_arg的信息，但如果我理解正确，我必须使用:

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.

这不是很方便.

有什么办法可以得到这样的结果吗? :

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

Coq < mytactic arg_1.

Coq < mytactic arg_1 arg_2 arg_3.

推荐答案

我们可以使用 Tactic Notation 机制来尝试解决您的问题，因为它可以处理可变参数.

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

为了演示，让我们重用ltac_No_arg并定义一个虚拟策略mytactic

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.

测试:

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

这篇关于LTAC:可选参数策略的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！