(** **** Exercise: 3 stars, standard, optional (ev_plus_plus)
This exercise just requires applying existing lemmas. No
induction or even case analysis is needed, though some of the
rewriting may be tedious. *)
Theorem ev_plus_plus : forall n m p,
even (n+m) -> even (n+p) -> even (m+p).
Proof.
intros n m p H1 H2.
Here is what I got:
1 subgoal (ID 89)
n, m, p : nat
H1 : even (n + m)
H2 : even (n + p)
============================
even (m + p)
I have proven the previous theorem:
Theorem ev_ev__ev : forall n m,
even (n+m) -> even n -> even m.
And wanted to apply it to H1, but
apply ev_ev__ev in H1.
gives an error:
Error: Unable to find an instance for the variable m.
Why can't it find "m" in the expression even (n + m)? How to fix?
Update
apply ev_ev__ev with (m:=m) in H1.
gives a very strange result:
2 subgoals (ID 90)
n, m, p : nat
H1 : even m
H2 : even (n + p)
============================
even (m + p)
subgoal 2 (ID 92) is:
even (n + m + m)
I thought that it will transform H1 to 2 hypothesis:
H11 : even n
H12 : even m
But instead it gave 2 subgoals, the second that we need to prove is more complicated than the initial one:
even (n + m + m)
What's happening here?
The statement forall n m, even (n+m) -> even n -> even m. does not mean "if we have that (n + m) is even then we have both that n is even and that m is even" (this is false, consider n = m = 1). Instead it means "if we have that (n+m) is even, and we have that n is even, then we have that m is even".
There is no way to get H11 : even n and H12 : even m just from H1 : even (n + m) without assuming a contradiction. I would suggest figuring out how to prove your theorem with pen and paper before trying to prove it in Coq.