问题标签 [coq-tactic]

我有一个函数count可以计算给定谓词在应用于列表元素时可证明的次数。定义如下：

然后我使用这个函数来陈述引理，如下所示：

我对这些引理的证明往往非常乏味：

我可以做些什么来自动化这些涉及使用我的count函数进行计算的乏味证明？

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

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

我试过这个：

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

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

这是我正在使用的 coq 版本：

这是我要证明的定理：

请注意，我将在证明中使用这个定理（我已经证明了）：

好的，现在这是我尝试通过通常的归纳方式证明定理：

但是在执行该rewrite策略时，它给了我以下错误：

但是如果我使用symmetry策略，我实际上可以通过相同的代码来证明它：

那么，为什么在没有对称的情况下重写它是行不通的呢？

我很好奇discriminate幕后的战术是如何运作的。因此我做了一些实验。

首先是一个简单的归纳定义：

然后是一个可以通过discriminate策略证明的简单引理：

让我们看看证明是什么样子的：

这看起来相当复杂，我不明白这里发生了什么。因此，我试图更明确地证明相同的引理：

让我们再次看看 Coq 用这个做了什么：

现在我完全糊涂了。这还是比较复杂的。谁能解释这里发生了什么？

我有一个归纳定义如下的公式：

和假设：

我想证明：

我尝试induction在类型上使用该策略world但失败了，因为它不是归纳类型。

它在 Coq 中是否可以证明，如果可以，你能建议如何做吗？

I have this code:

And I want to rewrite the current subgoal by using the is_eq definition. How can I do this ?

我已经开始学习 Coq，并试图证明一些看起来相当简单的事情：如果一个列表包含 x，那么该列表中 x 的实例数将 > 0。

我定义了 contains 和 count 函数如下：

我试图证明：

我知道证明将涉及展开计数和包含的定义，但我想说“列表不能为零，因为包含是真的，所以必须有一个元素是x真的”，我'玩了一会儿，但不知道如何使用战术来做到这一点。任何指导将不胜感激。lbeq_nat h x

我想通过添加一个定理来扩展 Coq'Art 中的练习 6.10，即对于所有非一月的月份，is_January 将等于 false。

我对月份的定义如下：

我对 is_January 的定义如下：

我正在执行以下操作以测试它是否正确。

我对这个定理的证明不是很满意。

无论如何，Coq 中是否有在- intro H; simpl; reflexivity.非 1 月份重复案例证明（所以我只有两个 - 或类似的东西，所以我不必重复自己）？还是我只是以错误的方式完全解决这个证明？

假设我有H: 0 = 1范围。我怎样才能用这个来得出结论False？