Skip to Content.
Sympa Menu

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

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


chronological Thread 
  • 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



Archive powered by MhonArc 2.6.16.

Top of Page