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: Jean-Marc Notin <Jean-Marc.Notin AT inria.fr>
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, 01 Mar 2010 17:25:44 +0100
Organization: INRIA

Especially, I am thinking of the proof with the standard schema from
high-school:
----------------
To prove:
forall m, n P(m,n) = true

It suffices to prove:
1. P(0.0) = true
2. P(m', n) = true ==> P( S m', n) = true
3. P(m, n') = true ==> P( m, S n') = true
--------------------------------

If you want to prove [plus_comm] this way, you will have to learn a new tactic (apply*) and search the standard library for some useful lemma (nat_double_ind**). Here is the proof:

Theorem plus_comm : forall n m : nat, plus n m = plus m n.
Proof.
  apply nat_double_ind; simpl;
    try (intros; rewrite <- plus_n_O; reflexivity).
  intros n m IH. repeat rewrite <- plus_n_Sm. rewrite IH. reflexivity.
Qed.

(*)
http://coq.inria.fr/refman/Reference-Manual011.html#@tactic20
(**) http://coq.inria.fr/stdlib/Coq.Init.Peano.html#nat_double_ind

[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