The Coq mailing list

[Nick Benton <nick AT microsoft.com>]

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