I want to prove the following :
1 subgoals
a : nat
b : nat
H0 : a + b = 0
______________________________________(1/1)
a = 0 /\ b = 0
It seems very easy, even trivial, but I dont know how to do it. I tried induction
, case
, unsuccessfully. Any idea ?
Thanks for your help.
You can prove forall n1 n2, n1 + n2 = 0 -> n1 = 0
by case analysis on n1
.
If n1
is 0
, the conclusion is 0 = 0
, which you can prove because =
is reflexive.
If there's an n3
such that n1 = S n3
, then the hypothesis S n3 + n2 = 0
reduces to S (n3 + n2) = 0
and implies False
because 0
and S
are different constructors.
False
implies anything so you're done.
You can prove forall n1 n2, n1 + n2 = 0 -> n2 = 0
by using the previous fact and commutativity of addition. Then you're able to prove 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.
It's probably better to try to automate the proof as much as possible though.
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.
Either way, this fact has already been proved in the standard library.
Require Import Coq.Arith.Arith.
Check plus_is_O.