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

它似乎很容易,甚至是微不足道的,但我不知道该怎么做.我试过了induction,case但没有成功.任何的想法 ？

谢谢你的帮助.

Answer 1

你可以forall n1 n2, n1 + n2 = 0 -> n1 = 0通过案例分析证明n1.

如果n1是0,结论是0 = 0,你可以证明,因为它=是反身的.

如果存在n3这样n1 = S n3的假设,那么假设S n3 + n2 = 0会减少S (n3 + n2) = 0并暗示False因为0并且S是不同的构造函数. False意味着什么,所以你已经完成了.

你可以forall n1 n2, n1 + n2 = 0 -> n2 = 0通过使用先前的事实和加法的可交换性来证明.然后你就能证明了forall 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.