coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Beginner's question: how to prove m+n = n+m

From: "Zhoulai.FU AT X.org" <zhoulai.fu AT polytechnique.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Beginner's question: how to prove m+n = n+m
Date: Mon, 1 Mar 2010 12:36:20 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:content-type; b=bzvo5w57oQrv/47I2vrSZkxAgIz+jMW1vV6/5p/fXffP5KCdDAqTPOy8qr8rTwS7iC /KJPDdTs74Iyj9yUtrmIUZDDsx3ZJcY7fLVkD09xPA2m2TuD4NveC0dS6bvlG8efAYy7 rwkgI5KpXrbSXIhBYl+nMbCcaquksxJZaaqWU=

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.

[Coq-Club] Beginner's question: how to prove m+n = n+m, zell08v
- Re: [Coq-Club] Beginner's question: how to prove m+n = n+m, Adam Koprowski
  - Re: [Coq-Club] Beginner's question: how to prove m+n = n+m, Zhoulai.FU AT X.org
    - Re: [Coq-Club] Beginner's question: how to prove m+n = n+m, gallais @ EnsL
      - Re: [Coq-Club] Beginner's question: how to prove m+n = n+m, Zhoulai.FU AT X.org
        
        Re: [Coq-Club] Beginner's question: how to prove m+n = n+m, Guilhem Moulin
        
        Re: [Coq-Club] Beginner's question: how to prove m+n = n+m, Adam Koprowski
- Re: [Coq-Club] Beginner's question: how to prove m+n = n+m, Jean-Marc Notin