问题标签 [logical-foundations]

玩 nostutter excersizes 我发现了另一种奇怪的行为。这是代码：

展开后的状态是这样的：

当我specialize (H2 eq_refl).在加载其他逻辑基础文件的 IndProp.v 中运行时，它可以工作。不知何故，它明白需要将“1”作为参数。IndProp.v 的标题是这样的：

当我将代码移动到另一个文件“nostutter.v”中时，同样的代码给出了预期的错误：

术语“eq_refl”的类型为“RelationClasses.Reflexive Logic.eq”，而预期的类型为“1 = 1”。

nostutter.v 的标头：

我必须明确添加一个参数eq_refl：specialize (H2 (eq_refl 1)).

我认为这与专业无关。它是什么？怎么修？

我来到了这一点：

输出：

我的计划是使用传递性le：

a <= b -> b <= c -> a <= c

并替换 a := a, b := (S b') 和 c := a。

所以我们会得到：

a <= (S b') -> (S b') <= a -> a <= a

我将使用 H1 和 H2 作为所需的 2 个假设并得到 Ha：a <= a。然后对其进行反演，得到构造 this is a = a 的唯一方法。

但是我应该使用什么语法来应用我的 2 个假设的传递性来得到 Ha？

来自逻辑基础的 Rel 章节。我得到了我试图理解的 excersize 的解决方案：

我不明白，介绍模式如何[| b' H1]工作？介绍后显示：

第二个子目标：

我知道它相当于破坏，但是什么样的破坏呢？这绝对不是一个简单的destruct b.

我也试图理解使用absurd (S b' <= b')战术背后的逻辑。这是否意味着，如果我们a = S b'在这种情况下证明这一点，就意味着我们在 H1 中重写后，我们得到：a，这是一个普遍错误的陈述（荒谬）？S b'S b' <= b'

I am currently learning coq thanks to the Software Fondation's ebook. I successfully wrote the addition as follow:

But I'm stuck with exp because of the following error:

Since they wrote:

If you hit a "Universe inconsistency" error, try iterating over a different type. Iterating over cnat itself is usually problematic. I tried using the definition of cnat:

But then I have:

I do not ask for a solution, but I'd really like to understand these errors. Thanks for your lights !

我们得到这个：

我们还有一个先前证明的定理：

我们知道那(n+m)是偶数而且(n+p)是偶数。如何通过将 ev_sum 应用于 Hnm 和 Hnp 在上下文中创建新假设：

?

输出：

现在 n 可以是偶数也可以不是偶数。

• 如果 n 是偶数，则 m 也是偶数。那么由ev_sum定理 (n+m) 也是偶数。

• 如果 n 不是偶数，它的形式为 (n' + 1)，其中 n' 是偶数。m 也不是偶数，形式为 (m' + 1)，其中 m' 是偶数。所以它们的总和等于：

  n + m = n' + 1 + m' + 1 => n + m = (n' + m') + 2。

偶数 ((n' + m') + 2)。在apply ev_SS我们得到偶数 (n' + m') 之后。我们知道 n' 是偶数并且 m' 是偶数，我们apply ev_sum. 这证明了这个定理。

如何在 coq 中编写这个非正式的证明？

任务。

假设我们给 Coq 定义如下：

以下哪个命题是可证明的？

我证明了三分之二。

第三个是不可证明的，因为c3只会增加n，永远不会等于list的头部+1。但是如何正式证明它是不可证明的呢？

更新 1

在软件基础“QuickChick”的第 4 卷中，我们进行了以下练习：

但是得到一个错误：

它突出了match opt1 with.

• 也许，我的解决方案非常原始：它只是模式匹配所有可能的情况。有更好的吗？

• 是什么导致此语法错误？

任务：编写一个将自然数转换为二进制数的函数。

第二个函数给出错误，因为它在结构上不是递归的：

我应该怎么做才能证明它总是终止，因为 q 总是小于 n。

从软件基础通过 Quick Chick 课程我陷入了以下定理：

在这里我们得到：

证明true = true -> (eqb f1 f2) = true似乎是不可能的，因为(eqb f1 f2)可能是错误的，在这种情况下，我们进入false = true了空的上下文，这是无法证明的。

这个定理是不正确的还是我遗漏了什么？