coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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/
- Re: [Coq-Club] Error: 1 * n = n., (continued)
- Re: [Coq-Club] Error: 1 * n = n., Colm Bhandal, 09/05/2013
- Re: [Coq-Club] Error: 1 * n = n., Kristopher Micinski, 09/05/2013
- Message not available
- Re: [Coq-Club] Error: 1 * n = n., Kristopher Micinski, 09/05/2013
- Re: [Coq-Club] Error: 1 * n = n., soham chakraborty, 09/05/2013
- Re: [Coq-Club] Error: 1 * n = n., t x, 09/05/2013
- Re: [Coq-Club] Error: 1 * n = n., soham chakraborty, 09/06/2013
- [Coq-Club] Re: Error: 1 * n = n., N. Raghavendra, 09/06/2013
- Re: [Coq-Club] Re: Error: 1 * n = n., soham chakraborty, 09/06/2013
- Re: [Coq-Club] Re: Error: 1 * n = n., Valentin Robert, 09/06/2013
- Re: [Coq-Club] Re: Error: 1 * n = n., soham chakraborty, 09/06/2013
- [Coq-Club] Re: Error: 1 * n = n., N. Raghavendra, 09/06/2013
- Re: [Coq-Club] Re: Error: 1 * n = n., soham chakraborty, 09/06/2013
- Re: [Coq-Club] Error: 1 * n = n., Colm Bhandal, 09/05/2013
- [Coq-Club] Re: Error: 1 * n = n., N. Raghavendra, 09/06/2013
Archive powered by MHonArc 2.6.18.