coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Colm Bhandal <bhandalc AT tcd.ie>
- To: Nick Benton <nick AT microsoft.com>
- Cc: soham chakraborty <soham4you AT gmail.com>, Valentin Robert <valentin.robert.42 AT gmail.com>, "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Error: 1 * n = n.
- Date: Thu, 5 Sep 2013 14:43:13 +0100
The library version of multiplication actually does recurse on the left hand argument. If you type simpl when your goal is 1*n = n, you’ll see it reduces. But only to n+0 = n. Because addition recurses on the left argument too, that bit doesn’t reduce further. You need a lemma to finish it off, which is proved by induction on n, but is already proved in the Arith library (plus_n_O). Alternatively, “auto with arith.” will do this (or your original goal) automagically.
Nick
From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of soham chakraborty
Sent: 05 September 2013 10:40
To: Valentin Robert
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Error: 1 * n = n.
Dear Valentin Robert,
Thank you for the prompt suggestion. Does Coq requires put the _expression_ in certain sequence? Also what do you mean by the "shape of n"... Do you mean the type of n?
I went through the link but could not solve the issue I am facing.
No multiplication is defined in this context. The file contains only this theorem.
Also I tried these expressions with and without "Require Import Arith." to have the standard expressions.
I am using coqIde GUI for writing these expressions.
I tried few other expressions in different orders in the theorem mentioned in the earlier mail and here are the results.
0 = n * 0. - Error: Impossible to unify "n * 0" with "0".0 = 0 * n - pass. Why this _expression_ passes?
n = 1 * n - Error: Impossible to unify "1 * n" with "n".
n = n * 1. - Error: Impossible to unify "n * 1" with "n".
1 * n = n. Error: Impossible to unify "n" with "1 * n".
n * 1 = n. Error: Impossible to unify "n" with "n * 1".I also tried
Variable n : nat.
Check n * 1.
Check n.
Check 1 * n.Check 0.
Check 1.
and type of each _expression_ came out as nat, so the type mismatch should not be the issue.
Thanks a lot again.
Regards,
soham
On Thu, Sep 5, 2013 at 1:14 PM, Valentin Robert <valentin.robert.42 AT gmail.com> wrote:
My guess is that your definition of multiplication is defined by
case-analyzing its right argument, therefore the computation "1 * n"
is stuck waiting to know the shape of "n".
This is explained in this chapter:
http://www.cis.upenn.edu/~bcpierce/sf/Induction.html#lab41
- Valentin
On Thu, Sep 5, 2013 at 8:34 AM, soham chakraborty <soham4you AT gmail.com> wrote:
> Hi,
> I am a Coq beginner. I am trying the following theorem on coqIde
>
> Theorem mult_1_l : forall n:nat, 1 * n = n.
> Proof.
> intros n. reflexivity. Qed.
>
> But having follwing error message while hitting the tactic reflexivity.
> Error: Impossible to unify "n" with "1 * n".
>
> Can you please explain the problem.
>
> Thanks in advance.
>
> Best Regards,
> soham
- [Coq-Club] Error: 1 * n = n., soham chakraborty, 09/05/2013
- Re: [Coq-Club] Error: 1 * n = n., Valentin Robert, 09/05/2013
- Re: [Coq-Club] Error: 1 * n = n., soham chakraborty, 09/05/2013
- RE: [Coq-Club] Error: 1 * n = n., Nick Benton, 09/05/2013
- Re: [Coq-Club] Error: 1 * n = n., Colm Bhandal, 09/05/2013
- Re: [Coq-Club] Error: 1 * n = n., Valentin Robert, 09/05/2013
- 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] Error: 1 * n = n., Colm Bhandal, 09/05/2013
- Re: [Coq-Club] Error: 1 * n = n., Valentin Robert, 09/05/2013
- Re: [Coq-Club] Error: 1 * n = n., Colm Bhandal, 09/05/2013
- RE: [Coq-Club] Error: 1 * n = n., Nick Benton, 09/05/2013
- Re: [Coq-Club] Error: 1 * n = n., soham chakraborty, 09/05/2013
- Re: [Coq-Club] Error: 1 * n = n., Valentin Robert, 09/05/2013
Archive powered by MHonArc 2.6.18.