The Coq mailing list

[soham chakraborty <soham4you AT gmail.com>]

Hi Raghu,

Good to hear from you. I have also started with the same book but yet to study the case analysis part :)

On the solution you sent Coq is getting stuck at

Case "n = O". Error: No interpretation for string "n = O".

Can you please check.

Best Regards,

soham

On Fri, Sep 6, 2013 at 1:39 PM, N. Raghavendra <raghu AT hri.res.in> wrote:

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/