Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


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



Archive powered by MhonArc 2.6.16.

Top of Page