coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Valentin Robert <valentin.robert.42 AT gmail.com>
To: soham chakraborty <soham4you AT gmail.com>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Error: 1 * n = n.
Date: Thu, 5 Sep 2013 08:44:27 +0100

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