我如何从错误的假设中证明错误？答案

【问题标题】：How do I prove false from a false hypothesis?我如何从错误的假设中证明错误？
【发布时间】：2021-06-25 01:01:49
【问题描述】：

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

来自 CoqIDE 的图片：

【问题讨论】：

trivial 应该可以工作
另一种解决方案：discriminate（如本文所述：stackoverflow.com/questions/66842087/…）

【解决方案1】：

您可以使用easy 策略：

Goal 0 * 0 = 2 -> False. Proof. easy. Qed.

【讨论】：

【解决方案2】：

为了完整性，手动方法：

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 认为这是一个矛盾并认为你的证明是完整的。

【讨论】：

【解决方案3】：

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

Goal 0 * 0 = 2 -> False.
  cbn. congruence.
Qed.

【讨论】：

【解决方案4】：

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

你必须加载一个库。

Require Import Coq.micromega.Lia.

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

Coq 总是有很多选择。

【讨论】：

【解决方案5】：

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

【讨论】：