The Coq mailing list

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

Hi Sidi,

Ok, here is my proof script:

Theorem ev_sum : forall n m,
   ev n -> ev m -> ev (n+m).
Proof.
  intros n m En.
  induction En as [|n' En'].
  Case "E = ev_0". simpl. intro Em. apply Em.
  Case "E = ev_SS n' En'".
   intro Em. apply IHEn' in Em.
   assert (H: S (S n') + m = S (S (n' + m))).
   simpl. reflexivity.
   apply ev_SS in Em.  
   rewrite <- H in Em.
   apply Em.
Qed.

(note that in your script you're using a number of tactics which I don't know 
about and are not used in the SF book at this point: auto, clear, generalize)

So, to recap my question: in the script above, I should also be able to 
proceed by rewrite H in the goal, but it does not work, and I don't 
understand why.

Thanks!

-- Éric


On Dec 25, 2010, at 1:05 AM, Sidi Ould_biha wrote:

> 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
>