The Coq mailing list

[Sidi Ould_biha <sidi.ould_biha AT inria.fr>]

Hi!

You need to give more details about your proof script, how did u get to this 
goal.
I tried to guess your proof, I got the following script :

Theorem ev_test : forall n m, ev n -> ev m -> ev (n+m).
Proof. 
intros n m H.
induction H as [| n' En']; auto.
intro. generalize (IHEn' H); intro Em. clear H.
generalize (ev_SS _ Em); clear Em; intro Em.
assert (H : S (S n') + m = S (S (n' + m))). auto.
rewrite -> H. apply Em.
Qed.

Regards.

----- Mail original -----
> De: "Eric Tanter" 
>Â <etanter AT dcc.uchile.cl>
> À: 
>Â coq-club AT inria.fr
> Envoyé: Samedi 25 Décembre 2010 06:11:25
> Objet: [Coq-Club] Beginner's question: rewrite
> 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