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 16:31:28 +0530
  • Cancel-lock: sha1:ktZ2l12Pg9f9nWknJaXv4GaS4eE=

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/




Archive powered by MHonArc 2.6.18.

Top of Page