问题标签 [ltac]

在尝试创建循环可变长度参数列表的 Ltac 定义时，我在 Coq 8.4pl2 上遇到了以下意外行为。谁能给我解释一下？

从属归纳似乎对我来说在Ltac和非中的工作方式不同。

以下工作正常：

dependent induction在这里有点矫枉过正，因为destruct工作得很好。此外，如果用于帮助，则无需destruct在证明脚本中命名要编辑的内容：Ltac

但是，当被替换时同样Ltac失败：destructdependent induction

Set Ltac Debug没有给出额外的有用信息，除了dependent induction事实上，在x和上都尝试过y。

奇怪的是，如果我dependent induction在另一个Ltac没有匹配项的情况下将其包装起来，并将其应用于与我实际想要执行归纳的项相同的项，一切都会顺利进行：

这里发生了什么，为什么dependent induction看起来如此依赖上下文？

我想在某些假设存在而另一个假设不存在的情况下应用规则。如何检查这种情况？

例如：

这样，为了这个目标：

more_detail.将引入第二个假设 DET：

并且连续调用more_detail.将失败。

但是more_detail.，应始终确保两者Y和Z都存在，即如果只有其中一个存在，它应该为另一个运行规则：

和：

我正在尝试为假设编写一条规则，在match构造的帮助下制定：

我怎样才能匹配这样的假设？以下直接方法失败：

在 coq 中，该destruct策略有一个变体，它接受“连接析取引入模式”，允许用户为引入的变量分配名称，即使在解包复杂的归纳类型时也是如此。

coq 中的 Ltac 语言允许用户编写自定义策略。我想编写（实际上，保持）一种策略，在将控制权交给destruct.

我希望我的自定义策略允许（或要求，以更容易者为准）用户提供我的策略可以提供的介绍模式destruct。

什么 Ltac 语法实现了这一点？

我有以下 Ltac（来自这里），它曾经在 Coq 8.4pl6 上工作，但它不适用于 Coq 8.5 beta 3：

我收到一条错误消息说

我对Ltac了解不够。谁能帮助解释如何解决这个问题？

我正在做一些关于在 Coq 中形式化简单类型 lambda 演算的练习，并希望使用 Ltac 自动化我的证明。在证明进度定理时：

我想出了这段 Ltac 代码：

==>表示评估的单个步骤（通过小步语义）。每个匹配案例的意图是：

1. 当我们有一个假设说构造函数中的第一项步骤时，匹配任何二元构造函数。
2. 当我们有一个假设说构造函数步骤中的第二项和构造函数中的第一项已经是一个值时，匹配任何二元构造函数
3. 当我们有一个假设说构造函数中的术语是步骤时，匹配任何一元构造函数。

然而，看看这段代码的行为，它看起来第三种情况也匹配二进制构造函数。如何将其限制为仅实际匹配一元构造函数？

作为我一般问题的最小示例，假设我们有以下内容：

我想实施一种blah在目标的所有假设中自动展开的策略。

我试过这个：

但只有一个假设出现了blah。

例如，我想要一种策略，它会遍历给定 HintDb 中的所有解析提示，并且对于每个解析提示h，它会执行一个pose h.. 这可能吗？如果是这样，怎么做？

Ltac 用于自动证明和修改证明环境、输出字符串和定义复杂的符号。它也可以用于 Coq 环境的“智能”修改吗？以下是两次失败的尝试：

另外，如果这不是 Ltac 的工作，也许还有另一种方法？