时间戳

首页 > 解决方案 > 这个 Coq 证明正确吗？

coq - 这个 Coq 证明正确吗？

问题描述

我正在学习软件基础第 1 卷中练习的解决方案。在线书籍： https ://x80.org/collacoq/ozavikeyeh.coq

Example and_exercise : forall n m : nat, n + m = 0 -> n = 0 /\ m = 0.
Proof. 
    intros [|n] m H.
    - split. 
        + reflexivity. 
        + apply H.
    - inversion H. 
Qed.

下面apply H是证明状态：

1 subgoal
n, m : nat
H : S n + m = 0
______________________________________(1/1)
S n = 0 /\ m = 0

假设H不成立，也无法S n = 0证明；这个证明仍然正确吗？

标签： coq

解决方案

你正在做一个案例。因此，您必须接受这一点，S n + m = 0否则您将无法提出诉讼。

更准确地说，您是S n = 0 /\ m = 0在假设成立的情况下证明S n + m = 0成立。S n + m = 0实际成立与否并不重要。

并S n = 0 /\ m = 0成立，因为S n + m = 0是一个矛盾。在逻辑上的矛盾下，任何事情都可能发生。你可以说任何事情，而你不在乎它是否不一致，对吧？

推荐阅读