coq - Coq 中的 a + b = 0 -> a = 0 且 b = 0

Question

我想证明以下事实:

1 subgoals
a : nat
b : nat
H0 : a + b = 0
______________________________________(1/1)
a = 0 /\ b = 0

看起来很简单，甚至微不足道，但我不知道该怎么做。我尝试了归纳、案例，但没有成功。有什么想法吗？

感谢您的帮助。

Answer 1

通过对n1进行案例分析，可以证明forall n1 n2, n1 + n2 = 0 -> n1 = 0。

如果n1为0，则结论为0 = 0，您可以证明这一点，因为=是反射性的。

如果存在 n3 使得 n1 = S n3，则假设 S n3 + n2 = 0 简化为 S (n3 + n2) = 0 并暗示 False 因为 0 和 S 是不同的构造函数。False 意味着任何事情，所以你就完成了。

您可以通过使用前面的事实和加法交换律来证明对于所有n1 n2，n1 + n2 = 0 -> n2 = 0。然后你就可以证明对于所有 n1 n2, n1 + n2 = 0 -> n1 = 0/\n2 = 0。

Check eq_refl.
Check O_S.
Check False_rect.
Conjecture plus_comm : forall n1 n2, n1 + n2 = n2 + n1.
Check conj.

不过，尝试尽可能自动化证明可能会更好。

Require Import Coq.Setoids.Setoid.

Set Firstorder Depth 0.

Create HintDb Hints.

Ltac simplify := firstorder || autorewrite with Hints in *.

Conjecture C1 : forall t1 (x1 : t1), x1 = x1 <-> True.
Conjecture C2 : forall n1, S n1 = 0 <-> False.
Conjecture C3 : forall n1, 0 = S n1 <-> False.
Conjecture C4 : forall n1 n2, S n1 = S n2 <-> n1 = n2.
Conjecture C5 : forall n1, 0 + n1 = n1.
Conjecture C6 : forall n1 n2, S n1 + n2 = S (n1 + n2).

Hint Rewrite C1 C2 C3 C4 C5 C6 : Hints.

Theorem T1 : forall n1 n2, n1 + n2 = 0 <-> n1 = 0 /\ n2 = 0.
Proof. destruct n1; repeat simplify. Qed.

Hint Rewrite T1 : Hints.

无论如何，这个事实已经在标准库中得到了证明。

Require Import Coq.Arith.Arith.

Check plus_is_O.