Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Re: Error: 1 * n = n.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: Error: 1 * n = n.


Chronological Thread 
  • From: "N. Raghavendra" <raghu AT hri.res.in>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Re: Error: 1 * n = n.
  • Date: Fri, 06 Sep 2013 13:39:41 +0530
  • Cancel-lock: sha1:NhfExLpjnZ43q6QbwcCMqYcxAaQ=

At 2013-09-05T23:47:34+05:30, soham chakraborty wrote:

> Using them I have found following ways to solve the theorem 1 * n =
> n. Please review and provide your feedback.

I've also just begun to learn Coq. This is an exercise in Pierce's
software foundations book:

http://www.cis.upenn.edu/~bcpierce/sf/Induction.html

At the level of that chapter, I'd solve this exercise as follows:

Theorem mult_1_l :
forall n : nat,
1 * n = n.

Proof.
intros n.
induction n as [ | p IHp].
{
Case "n = O".
reflexivity.
}
{
Case "n = S p".
simpl.
simpl in IHp.
rewrite -> IHp.
reflexivity.
}
Qed.

Best regards,
Raghu.

--
N. Raghavendra
<raghu AT hri.res.in>,
http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/




Archive powered by MHonArc 2.6.18.

Top of Page