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: Guilhem Moulin <guilhem.moulin AT ens-lyon.org>
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 17:00:27 +0100

Hello,

On Mon, 01 Mar 2010 at 16:25:08 +0100,
Zhoulai.FU AT X.org
wrote:
> ----------------------
> 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.
> --------------------------------------------

Your hypothesis IHm' isn't strong enough: you have to keep the "forall m"
in its body.

Theorem plus_comm : forall n m : nat,
plus n m = plus m n.
Proof.
intro n.
induction n as [|n'].
intro m.
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'".
...

Cheers,
Guilhem.

Attachment: signature.asc
Description: Digital signature

[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