The Coq mailing list

["N. Raghavendra" <raghu AT hri.res.in>]

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/