如何解决我如何从错误的假设中证明错误?
我有一个明显错误的假设,我想用它来证明错误。在这种情况下,我的目标中有 Hx: 0 * 0 = 2
和 False
。我将如何开始这样做?
解决方法
您可以使用 easy
策略:
Goal 0 * 0 = 2 -> False. Proof. easy. Qed.
,
手动方法,为了完整性:
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
and x = 2
!由于 0 = O
和 2 = S (S O)
由完全不同的构造函数组成,因此 Coq 认为这是矛盾的,并认为您的证明是完整的。
另一种完整性解决方案:cbn ; congruence
。实际上0 * 0
减少到0(即O
),这与2(S (S O)
)的不同在于构造函数的不相交类型 nat
。第一种策略减少(简化)目标,第二种策略利用不相交性来推导矛盾。
Goal 0 * 0 = 2 -> False.
cbn. congruence.
Qed.
,
还有另一种解决方案,适用于此特定示例:lia
。 lia
代表L线性I整数A算术。这种强大的策略考虑了由线性整数算术(无论是方程还是不等式)组成的所有假设,并使用它们来解决算术目标,或者如果算术假设相互矛盾的任何目标。
您必须加载一个库。
Require Import Coq.micromega.Lia.
Goal 0 * 0 = 2 -> False.
lia.
Qed.
Coq 总是有很多选择。
,如果您想了解它在“幕后”是如何工作的,this answer 可能会很有用。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。