问题标签 [ltac]

所以，我有一个看起来像这样的证明：

它解决了我的所有目标，但是当我这样做时Qed，我收到以下错误：

Cannot guess decreasing argument of fix.

所以在生成的证明项的某个地方，存在没有充分根据的递归。问题是，我不知道在哪里。

有没有办法调试这种错误，或者查看策略脚本生成的（可能是非停止的）证明项？

我想写一个带有可选变量名的策略。原来的战术是这样的：

我想让用户有机会选择他想要的名称并使用它：save a例如。

我使用此解决方案编写了一个变体：

然而，这个证明失败了save h：

错误信息：

我想我必须确保它h是新鲜的，但我不确定如何做到这一点。

我正在考虑编写策略，该策略将着眼于多个目标并据此做出决定。但是，当我使用match goal with并凝视一个目标时，我该怎么说“请找到另一个看起来像这样的目标”？

或者更确切地说，一个更普遍的问题是，我如何在 Ltac 中的目标之间切换？

我目前正在研究证明，我发现自己一遍又一遍地编写这样的代码：

也就是说，我有一些相互归纳的类型，并且我同时推导出所有这些类型的相等性。

我想做的是有某种宏，我可以写

它将机械地生成上述命令，以便我可以将其用于各种互感类型。

我对 LTac 不是很了解，但我不确定它是否适用于这里，因为我不仅要自动生成证明术语，还要自动定义白话中的值。（不过我可能完全错了）。

我想知道的是，有没有办法定义一个可以自动化的“白话宏”？或者这是可以用 LTac 完成的事情吗？或者是在 OCaml 中编写 Coq 插件的唯一方法？

我有一个证明脚本，我正在探索多个案例，目前速度很慢，因为我有许多解决目标的策略，并且我正在尝试每个案例中的每一个。

我知道在某些情况下我需要应用某些策略，但我不确定如何做到这一点。

这是我现在拥有的：

这给出了错误Incorrect number of goals (expected 26 tactics, was given 2)。

对于归纳产生的每种情况，我都试图thing1在第一个目标destruct和thing2第二个目标中做。destruct

问题是，induction生成 13 个子目标，每个子目标被分成 2 个destruct。本地选择器[> thing1 | thing2 ]试图匹配所有子目标，而不仅仅是特定破坏产生的子目标。

我如何对策略进行排序，以便destruct在归纳生成的每个案例上thing1运行，然后在第一个破坏生成的目标上thing2运行，然后在第二个生成的目标上运行，对于每个归纳案例。

我处于以下形式的目标的情况：

哪里y : T2和f : T1 -> T2。诀窍是我已经定义了它们的构造函数T1并T2以这样的方式对应，所以对于人类来说，很容易看出什么值x将使相等成立。

但是，我有大量案例，并且希望我的脚本健壮，所以我想自动找到这样一个x.

我如何使用证明搜索来找到这样的值x？

现在我有这样的东西（借用 CPDT 的粉碎策略）：

即我为 创建了一个evar x，将其搁置，使用构造函数求解，用evas填充构造函数生成的所有子目标，然后使用证明搜索来确定相等性。

但是，这给出了：Error: Tactic failure.我的意图是，如果constructor选择了错误的构造函数，crush将无法解决目标，因此fail会触发回溯。但这似乎没有发生，它在第一次命中时就失败了fail。

我的问题

我可以使用哪些策略让证明搜索找到存在变量的值？如何使用constructor's 回溯来找到使存在存在的价值？

我正在尝试编写如下所示的 Ltac 代码：

问题是，试图匹配上下文中有值的情况，以及关于该值的一些事实。所以我混合了假设名称和假设类型的命名空间。(is_v_of_expr e)最终目标是在上下文中为每个循环破坏expr，但要确保它不会通过连续破坏相同的表达式来循环。

是否可以为这样的事情编写 Ltac 匹配表达式？

ordType我对其布尔比较运算符==,<b和的 an 和中缀表示法有以下定义 <=b。

现在考虑下面的 Ltac 定义，show_H它打印类型为 形式的假设x == y。

但是，当我使用此定义在以下引理中显示假设的名称时，它会失败并显示以下消息。

为什么解析器无法检测==假设中的符号？

在证明中，如果我对非最终论证进行归纳，我会得到普遍量化的归纳假设。我发现自己反复写这样的策略：

也就是说，我寻找一个归纳假设，并寻找与它统一的论点来专门化它。然后我做specialize (Hypothesis Arg1 Arg2...)

这感觉就像样板，但我一直不得不为我使用它的每个引理编写不同的版本。有没有办法：

1. 自动执行此操作？
2. 自动执行此操作，仅针对归纳假设？（这样我们就不会陷入将每个参数应用于每个可能的函数的无限循环中）