问题标签 [coq-tactic]

如果我有这样的谓词：

然后我可以简单地使用归纳法来证明一些虚拟引理：

但是，对于具有产品类型参数的谓词：

几乎相同引理的类似证明被卡住了，因为所有关于变量的假设都消失了：

为什么会这样？如果我用 替换induction，inversion那么它的行为符合预期。

引理仍然可以证明，induction但需要一些解决方法：

不幸的是，这种方式的证明变得非常混乱，并且对于更复杂的谓词是不可能遵循的。

一个明显的解决方案是这样声明bar：

这解决了所有问题。然而，就我的目的而言，我发现以前的（“元组”）方法更加优雅。有没有办法保持谓词不变并且仍然能够进行可管理的归纳证明？问题甚至来自哪里？

我将用一个例子来说明。

子目标：

所以我的问题是如何提取（P-> Q）。我已经有了 R，但是当我“在 H0 中应用 H”时，它会评估所有内容并给我 Q。

我是 Coq 的新手，我遇到了死胡同。我有一个大致像这样的归纳定义（我之前已经定义了归纳接受）：

我需要证明的是：

当然，在开始我得到的证明时

我花了很长时间阅读有关战术的文章，试图找到某种方法可以将 h 插入我的 fn2 或类似的东西，但我就是找不到方法。有人可以在这里指导我并给我一些想法吗？我也尝试过将有趣的 A 简化为 A，但我也没有成功。非常感谢您的帮助！

我想证明以下定理：

我已经得到了以下证明：

但现在我处于一种我不知道该怎么办的情况。以下内容可供我使用：

我想证明以下子目标：

如何在给定前提下消除 forall 量词

那就是：我怎样才能插入我的具体 x ： A 以便我可以推断： px ？

给定一个使用战术的有效 Coq 证明;，是否有一个通用公式可以将其转换为有效的等效证明，并.替换为;？

许多 Coq 证明使用;或 策略 排序 策略。作为初学者，我想观察各个步骤的执行情况，所以我想替换.，;但令我惊讶的是，我发现这可能会破坏证明。

关于的文档;很少，我还没有找到.任何地方的明确讨论。我确实看到了一篇论文，上面写着非正式的意思t1; t2是

适用于在当前证明上下文中t2由执行产生的每个子目标，t1

我想知道是否.只对当前子目标进行操作并解释不同的行为？但特别想知道是否有通用的解决方案来修复替换.为;.

给定以下对 和 的否定定义以及三个参数，我可以轻松地证明不同的情况，但我想以某种方式使用 Coq 将这个证明写在一个 forall 语句中。Forall b1 b2 b3 : bool 其中一个为假返回真，三个为真返回假。我如何在 Coq 中编写这个前提，以便我可以使用拆分之类的策略来分解连词等？

This seems like a really simple question, but I wasn't able to find anything useful.

I have the statement

and would like to prove

I haven't been able to find what theorem allows for this.

我有以下证明状态：

所以我想

然后用证明无关性来证明这一点。不幸的是，pF = pG这是无效的，因为它们具有不同的类型，即使我知道类型相同，因为H. 说rewrite H或rewrite H in pF导致匹配失败，我认为是因为in pF指的是值而不是类型。

是否有等价于rewritefor 类型？

这是我要完成的定理（带有所有必要的定义）。

在 Coq 中，我经常发现自己在做以下事情：我有证明目标，例如：

而且我真的只需要证明a = b，因为无论如何其他一切都是相同的，所以我这样做：

然后证明那个子目标，然后

完成证明。

但是，让那些在我的证明底部徘徊似乎只是不必要的混乱。

Coq 中是否有一个通用策略来获取构造函数的相等性并将其拆分为构造函数参数的相等性，有点像 asplit但用于等式而不是连词。

我多次遇到这个问题：我在 Coq 中有一个证明状态，其中包括相同等式两边的匹配项。

是否有一种标准方法可以将多个匹配项重写为一个匹配项？

例如。

如果我破坏expresion_evaling_to_Z我会得到两个相同的目标。我想找到一种方法来实现其中一个目标。