The Coq mailing list

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

At 2013-09-06T16:06:03+05:30, soham chakraborty wrote:

> Thanks Valentin for the reference. Yes, these commands solve the
> problem and Raghu's solution works :)
>
> One query. In theorem n + 0 = n is not accepted (guess it is due to
> recursion as Nick suggested earlier). But "simpl in IHp." allows "p +
> 0 = p". Any particular reason?

"simpl in IHp" just simplifies IHp using the relevant definitions.  The
induction hypothesis IHp is only a hypothesis available in the given
context, and not a theorem that can be used outside that context.  In
particular, IHp is not the theorem

forall p : nat, p + O = p.

which needs a separate proof.

----------------------------------------------------------------------
Print mult.

mult = 
fix mult (n m : nat) {struct n} : nat :=
  match n with
  | 0 => 0
  | S p => m + mult p m
  end
     : nat -> nat -> nat

Argument scopes are [nat_scope nat_scope]
----------------------------------------------------------------------

IHp : 1 * p = p

By definition,

1 * p = mult 1 p = mult (S O) p = p + mult O p = p + O

So IHp is simplified as

IHp : p + O = O

Best regards,
Raghu.

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