0

我有一个明显错误的假设，我想用它来证明错误。在这种情况下，我有Hx: 0 * 0 = 2而且我有False我的目标。我该如何开始呢？

图片来自 CoqIDE： 在此处输入图像描述

4

5 回答 5

0

为了完整性，手动方法：

Goal 0 * 0 = 2 -> False.
Proof.
  intro H.
  inversion H.
Qed.

（免责声明：我自己是 Coq 的初学者，所以如果我得到任何不正确的细节，请道歉 - 请让我知道，以便我改进答案！）

这是有效的，因为0 * 0 = 2计算结果为0 = 2，并且反转该假设将其分解为不同的可能构造函数（如更智能的版本destruct）。唯一可能的构造函数eq是eq_refl : forall a, a = a。因此，Coq 意识到这eq_refl是唯一可能的构造函数，可以用来对形式进行假设0 = 2。因此，Coq 将尝试找出 的值a，作为反演过程的一部分。但是，将其应用于0 = 2，它得到x = 0 和 x = 2！因为0 = O和2 = S (S O)由完全不同的构造函数组成，Coq 认为这是一个矛盾，并认为你的证明是完整的。

于 2021-03-29T03:22:41.423 回答
0

您可以使用以下easy策略：

Goal 0 * 0 = 2 -> False. Proof. easy. Qed.
于 2021-03-28T23:26:59.543 回答
0

如果您想了解它是如何“在幕后”工作的，这个答案可能会很有用。

于 2021-03-29T15:47:48.320 回答
0

还有另一种解决方案，适用于这个特定的例子：lia. lia代表线性整数A算法。_ 这种强大的策略考虑了所有由线性整数算术（无论是方程还是不等式）组成的假设，并使用它们来解决算术目标，或者如果算术假设相互矛盾，则可以解决任何目标。

您必须加载一个库。

Require Import Coq.micromega.Lia.

Goal 0 * 0 = 2 -> False.
  lia.
Qed.

Coq 总是有很多选择。

于 2021-03-29T09:12:59.073 回答
0

另一个完整性解决方案：cbn ; congruence. 确实0 * 0 减少到 0（即O），这与 2（S (S O)）的不同之处在于 type的构造函数的不相交性nat。第一种策略减少（简化）目标，第二种策略利用不相交来推断矛盾。

Goal 0 * 0 = 2 -> False.
  cbn. congruence.
Qed.
于 2021-03-29T08:17:41.587 回答