coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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,
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, Jean-Marc Notin
- Re: [Coq-Club] Beginner's question: how to prove m+n = n+m,
Adam Koprowski
Archive powered by MhonArc 2.6.16.