The Coq mailing list

[Eric Tanter <etanter AT dcc.uchile.cl>]

Hi,

I'm just starting to learn Coq, going through Pierce's & co Software 
Foundations.

In a proof, I have the following situation:
(ev is an inductively defined property of evenness)

1 subgoal
Case := "E = ev_SS n' En'" : String.string
m : nat
n' : nat
En' : ev n'
IHEn' : ev m -> ev (n' + m)
Em : ev (S (S (n' + m)))
H : S (S n') + m = S (S (n' + m))
______________________________________(1/1)
ev (S (S n') + m)


one way to reach the goal is:
rewrite <- H in Em. apply Em.

However, it seems to me that I could also reach the goal by using rewrite in 
the goal, not in Em.
I therefore tried the following:
rewrite -> H. apply Em. But the rewrite fails with:
Error: Found no subterm matching "S (S n') + m" in the current goal.

I would have expected rewrite to transform the goal to ev (S (S (n' + m))), 
which is exactly Em.

I don't understand why the rewrite fails in the goal, while it succeeds in Em.

Any explanation is more than welcome!

Thanks,

-- Éric