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: "gallais @ EnsL" <guillaume.allais AT ens-lyon.fr>
To: "Zhoulai.FU AT X.org" <zhoulai.fu AT polytechnique.org>
Cc: coq-club <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:49:23 +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:cc:content-type; b=XtdPmScm4TkvqAnbCZvFaR9NSWW9nH8zSvNcNzSWjxWEpiFbbc/cEIcwcAU80ZqvAL dy0Tw9kOx62zVSvALwyxmFoekT1Z44g6ja/a/p2Ldv/MCDHq7ls2i3K1o0cQrKgHrwaL kjeLsuGJeqSfgTxm4JwoFaXwuJjr5GbKN1hcw=

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.

[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