The Coq mailing list

["Zhoulai.FU AT X.org" <zhoulai.fu AT polytechnique.org>]

Hello Guillaume,

Thank you for your answer. 

I agree that it is not a hard work if we introduce a lemma as you said. However to do that,  if I understand well , you may probably have to use something like this 
**************
[rewrite] [lemma_name]
**************
But the "rewrite" learned till now does not have that syntax. It can only rewrite 
syntactically something following a rule indicated by a hypothesis. 

Thus, finally my question turns to:
"Can we work around more primitively with 
-simpl. reflexivity.  intros. Case. Eval. 
-induction
-rewrite with the syntax: [rewrite] [<-]/[->] [hypothesis]
?"

or can we fullfil the case "n=S n', m = S m'" in the follwing part?
----------------------
Theorem plus_comm : forall n m : nat,
  plus n m = plus m n.
Proof.
  intros n m.
  induction n as [|n'].
  induction m as [|m'].
  Case "n=0 m=0".
  reflexivity.
  Case "n=S n' m=0'".
  simpl. rewrite <- IHm'. simpl. reflexivity.
  induction m as [|m'].
  Case "n=Sn' m=0".
  simpl. rewrite -> IHn'.  reflexivity.
  Case"n=Sn' m= S m'".
(*Can we fullfil this case with a primitive way????*)
Admitted.
 --------------------------------------------

I hope it's clear. Thanks in advance.

Z.

On Mon, Mar 1, 2010 at 12:49 PM, gallais @ EnsL <guillaume.allais AT ens-lyon.fr> wrote:

Hi,

You should just try to prove it by induction : the generated goals are quite easy to prove (even for a beginner) once you know that there exists a lemma `plus_n_Sm` stating that `forall n m : nat, S (n + m) = n + S m`.

You can try to prove plus_n_Sm as a sublemma (the induction proof is also quite easy) and you will be able to proove plus_comm using only intro, induction, reflexivity, rewrite and simpl.

Cheers,

guillaume

On 1 March 2010 12:36, Zhoulai.FU AT X.org <zhoulai.fu AT polytechnique.org> wrote:

On Mon, Mar 1, 2010 at 11:58 AM, Adam Koprowski <adam.koprowski AT gmail.com> wrote:

On Mon, Mar 1, 2010 at 11:53, <zell08v AT orange.fr> wrote:

Hello,

I am a total beginner on Coq. Here is an exercise from the introduction cours
of Pierce. To prove:
**********************
Theorem plus_comm : forall n m : nat,
 plus n m = plus m n.
Proof.
 (* FILL IN HERE *) Admitted.
********************

How can I prove it with only the several keywords that  leaarned so far:
simpl. reflexivity. rewrite. intros. Case. Eval.

 

  Indeed, as the proof goes by induction, you will have to extend this list with the [induction] tactic.

Thanks. You are right. I had forgetten [induction]. In fact, my question should have been:

How can I prove it with only the several keywords that  learned so far: Induction

simpl. reflexivity. rewrite. intros. Case. Eval.

I mean I still hope to know the answer with this extended list:) Thanks in advance.

-- 
Zhoulai FU

INRIA Rennes - Bretagne Atlantique
Campus Universitaire de Beaulieu
35042 RENNES Cedex - FRANCE