The Coq mailing list

[soham chakraborty <soham4you AT gmail.com>]

Hi Raghu,

Thanks for the explanation. Also your second solution(remove case) works without string.

Best Regards,

soham

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

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/