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: Adam Koprowski <adam.koprowski AT gmail.com>
To: zell08v AT orange.fr
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Beginner's question: how to prove m+n = n+m
Date: Mon, 1 Mar 2010 11:58:51 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=nZ5rZiDyV0dbjK1A9g5EXgn5VWoXVJ5W/gFaP0pQ812CXQGmhNJSLnh+tDtdGVQ8rW ShiF8BtflACOwQZf5BbUCz+BzRuPTOkDWP6wbPT1VgcY7x9eRdNohvJCUZfESp1ESj57 PzB1Jm4bgZyUqpQT2gEstaaauQJJ3zcfQspbk=

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.

��Best,

��Adam

--
Adam Koprowski � [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate � �[http://mlstate.com, 15 rue Berlier, 75013 Paris, France]

[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