Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Error: 1 * n = n.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Error: 1 * n = n.


Chronological Thread 
  • 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

Use the "ring" tactic. Just type "ring" and any ring equalities will be solved automatically, whether they be integers, Reals, naturals... This tactic has saved me an enormous amount of time. I highly recommend it.


On 5 September 2013 10:55, Nick Benton <nick AT microsoft.com> wrote:

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

 





Archive powered by MHonArc 2.6.18.

Top of Page