问题标签 [logical-foundations]

这是来自 Software Foundations 的 5 星练习。

我花了太多时间试图拆分它H，却发现尽管为此做了一天半的工作，但我对不平等如何发挥作用的许多假设都被证明是错误的。昨晚我有一些很棒的想法，现在它们被丢弃了，这让我比以往任何时候都更加困惑这个问题。在过去的两天里，我似乎只是在忘记代数。

s如果答案是我需要在s 或length ss 或s上匹配，我会非常尴尬，pumping_constant re因为我找不到通过那里的方法。

这个问题的设置方式强烈建议H应该以某种方式拆分以便进行归纳。我仍然对此持怀疑态度。

这是书中的任务：

证明 Coq 与一般排中公理的一致性需要复杂的推理，而 Coq 本身无法进行。然而，下面的定理暗示对于任何特定的Prop [P] ，假设一个可判定性公理（即排中的一个实例）总是安全的。为什么？因为我们无法证明对这样一个公理的否定。如果可以，我们将同时拥有 [~ (P / ~P)] 和 [~ ~ (P / ~P)] （因为 [P] 意味着 [~ ~ P]，通过下面的练习），这将是矛盾。但既然我们不能，添加 [P / ~P] 作为公理是安全的。

据我了解的任务，我必须介绍排中公理。但我不确定我是否正确地做到了：

现在我们得到了(P \/ ~ P)，但是当我尝试时apply decidability.，它给出了一个错误：

该怎么办？

这是我得到的：

我已经证明了前面的定理：

并想将其应用于 H1，但是

给出一个错误：

为什么在表达式中找不到“m” even (n + m)？怎么修？

更新

给出了一个非常奇怪的结果：

我认为它会将 H1 转换为 2 假设：

但相反，它给出了 2 个子目标，我们需要证明的第二个子目标比最初的更复杂：

这里发生了什么事？

Im trying to prove the following lemma:

Here is what I got at the end:

I want coq to evaluate "even 0" to true and "even 1" to false. I tried simpl, apply ev_0 in H. but they give an error. What to do?

不幸的是，我再次陷入困境：

结果如下：

据我所知，我可以用文字来证明：

(n' + 1) 根据 H 不是偶数。因此根据 IHn，n' 不是偶数是不正确的（双重否定）：

展开双重否定，我们得出结论 n' 是偶数。

但是如何在 coq 中编写呢？

使用 IndProp 中的 leb_complete 定理，我发现了以下奇怪之处：

它产生以下内容：

一切安好。现在，当我运行apply IHn'.它并产生以下内容时：

为什么它有效？在 IHn' 我们有

变量 m 和m'不同，但它仍然有效。当我尝试

它给出了一个错误：

但是 IHn' 中有变量“m”！我很困惑，请解释一下这里发生了什么。

到目前为止，这是我们所得到的：

现在我需要将 H1 和 H2 组合成exists s : list T, s =~ App re1 re2或将目标分解为 2 个子目标，并使用 H1 和 H2 分别证明它们。但我不知道，该怎么做。

The authors of the book have provided proofs for some unit tests for nostutter exercise. Unfortunately, they didn't provide explanations how they work. I was able to understand all the proofs but one:

After intro we have the following:

When I remove repeat and run match once, I get this:

So it tries to recursively find, where the list in H2 doesn't match any of nostutter constructors.

Can somebody explain me, how does this match work step by step? What is goal variable and |- symbol?

深入test_nostutter_1研究 excersize 我找到了一种无需重复即可解决的方法：

我决定更多地使用它，并且在 coq 参考手册中我发现do tactical可以多次循环一个策略。

expr 被评估为 v ，它必须是一个策略值。这个策略值 v 被应用了 num 次。假设 num > 1，在第一次应用 v 之后，至少一次将 v 应用到生成的子目标，依此类推。如果在 num 个应用程序完成之前 v 的应用程序失败，它就会失败。

所以我尝试了这个：

但不幸的是它失败了。只有这个有效：

是否可以使用do使其工作？

为了理解@keep_learning的答案，我一步一步地浏览了这段代码：

这是我们在执行specialize之前所拥有的

这是 eq Prop，其构造函数eq_refl用于specialize：

我无法解释，这个命令是如何工作的：

我阅读了有关专业参考手册的信息，但是那里的解释太宽泛了。据我了解，H2 中的“1 = 1”表达式满足eq_refl构造函数，因此 eq 命题为 True。然后它简化了表达式：

我们得到

有人可以为我提供一个解释正在specialize做什么的最小示例，以便我可以自由使用它吗？

更新

尝试使用 apply 来模仿 special 的工作原理，我做了以下操作：

这给出了：

几乎相同specialize，只是假设名称不同。

在 test_nostutter_4 定理中，我尝试了这个并且它起作用了：

它给了我们：

这个比较复杂，我们不得不引入一个新的假设 Heq。但是我们得到了我们需要的东西——最后是 H3。

专业化内部是否使用记住之类的东西？或者是否可以用 apply 但不记得来解决它？