Theorem ev_ev__ev_full : forall n m,
even (n+m) <-> (even n <-> even m).
Proof.
intros n m. split.
- intros H. split.
+ intros H1. apply (ev_ev__ev n m H H1).
+ intros H1. rewrite plus_comm in H. apply (ev_ev__ev m n H H1).
- intros H.
Output:
n, m : nat
H : even n <-> even m
============================
even (n + m)
Now n can be either even or not even.
if n is even, m is also even. Then by ev_sum theorem (n+m) is also even.
if n is not even, it has the form (n' + 1), where n' is even. m is also not even, and has the form (m' + 1), where m' is even. So their sum is equal to:
n + m = n' + 1 + m' + 1 => n + m = (n' + m') + 2.
even ((n' + m') + 2). After apply ev_SS we get even (n' + m'). As we know that n' is even and m' is even, we apply ev_sum. And this proves the theorem.
How to write this informal proof in coq?
Start with these lemmas:
Theorem even_S (n : nat) : (~even n <-> even (S n)) /\ (even n <-> ~even (S n)). Admitted.
Theorem contra {A B : Prop} (prf : A -> B) : ~B -> ~A. Admitted.
even_S is proven with induction, and I think it's one of the examples of theorems where making the conclusion stronger than you might expect makes it easier to prove (dropping either side of the /\ makes the remaining side difficult). contra is a tautology.
Knowing even_S, the decidability of even n follows straightforwardly from induction on n.
Theorem even_dec (n : nat) : {even n} + {~even n}. Admitted.
This is a decision procedure: even_dec n tells you whether n is even or not, depending on whether it returns the left or right alternative. { _ } + { _ } is the notation for sumbool. It's basically like a bool (it's in Set and so can be destructed in computationally relevant contexts) except it also witnesses one of the two given Props depending on the alternative. In your proof, the first step is branching on this property:
destruct (even_dec n) as [prf_n | prf_n].
If even n, the proof is trivial.
+ admit.
Otherwise, the contrapositive of the backwards implication tells us ~even m. We can also eliminate the nots:
+ pose proof (contra (proj2 H) prf_n) as prf_m.
apply even_S in prf_n.
apply even_S in prf_m.
The rest of the proof (asserting that n = S n', m = S m', even n', even m' and thus even (n + m)) follows with some work (with inversion).
admit.
(I have filled in the admits myself and this path does successfully lead to the proof, but just spilling all the answers is no fun :).)