coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: zell08v AT orange.fr
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Beginner's question: how to prove m+n = n+m
- Date: Mon, 1 Mar 2010 11:53:10 +0100
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.
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
--------------------------------
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,
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.