The Coq mailing list

[t x <txrev319 AT gmail.com>]

I think you're missing the point of the "solve from fundamentals" group since you're using auto, apply <existing lemma>, and ring.

These theorems can be solved by examining "Print nat. Print plus. Print mult." then doing "induction n; < solve n = 0 case > ; solve < n = S n' case >"

Personally, I found reasoning through nat / plus / mult quite enlightening on how "low level" Coq is -- in that natural numbers, +, and * are libraries rather than core of the language.

On Thu, Sep 5, 2013 at 6:17 PM, soham chakraborty <soham4you AT gmail.com> wrote:

Hi all,

This was my first post in Coq club forum and I appreciate you all for the discussions to understand the problem (thanks Nick) and suggesting possible techniques. Thank you all for the same.

My goal has been to use the basic constructs(theorem/lemma/axiom) to learn as beginner. Additionally came to know about some powerful constructs(ring, auto with arith) which can make the job easier. Using them I have found following ways to solve the theorem 1 * n = n. Please review and provide your feedback.

Thanks & Regards,
soham

Solutions

-----------------------------------------

Theorem plus_n_O_theorem : forall n : nat,

       n + 0 = n.
Proof.

intros n. auto. Qed.

Theorem mult_1_l : forall n:nat,
           1 * n = n.
Proof.

     intros n. simpl. apply plus_n_O_theorem.
Qed.

----------------------------------------

Axiom plus_n_O_axiom : forall n : nat,
       n + 0 = n.

Theorem mult_1_l : forall n:nat,
           1 * n = n.
Proof.

     intros n. simpl. apply plus_n_O_axiom.
Qed.

-----------------------------------------

Lemma plus_n_O_lemma : forall n : nat,
       n + 0 = n.
Proof. auto. Qed.

Theorem mult_1_l : forall n:nat,
           1 * n = n.
Proof.

     intros n. simpl. apply plus_n_O_lemma.
Qed.

------------------------------------------

Require Import Arith.

Theorem mult_1_l : forall n:nat,
           1 * n = n.
Proof.
intros n.

auto with arith.
Qed.

-----------------------------------------

Require Import Arith.

Theorem mult_1_l : forall n:nat,
           1 * n = n.
Proof.

    intros n. ring.
Qed.

-----------------------------------------

Require Import Arith.

Lemma plus_n_O_lemma : forall n : nat,
       n + 0 = n.
Proof. auto. Qed.

Theorem mult_1_l : forall n:nat,
           1 * n = n.
Proof.

     intros n. simpl. apply plus_comm.
Qed.

---------------------------------------

On Thu, Sep 5, 2013 at 10:01 PM, Kristopher Micinski <krismicinski AT gmail.com> wrote:

Mult should have been plus..

Theorem one_times_n : forall n, 1 * n = n.

  intros.

  simpl; rewrite plus_comm; reflexivity.

Qed.

Kris

On Thu, Sep 5, 2013 at 12:05 PM, Nick Benton <nick AT microsoft.com> wrote:

Err…no, actually. That won’t reduce.

 

From: Kristopher Micinski [mailto:krismicinski AT gmail.com]
Sent: 05 September 2013 16:55
To: Colm Bhandal
Cc: Valentin Robert; Nick Benton; soham chakraborty; coq-club AT inria.fr

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

 

I'm surprised that nobody has mentioned it, but while you absolutely *should* learn the induction way to do this, you also rewrite with the commutativity lemma for multiplication on the naturals and then reduce.

 

Kris

 

 

On Thu, Sep 5, 2013 at 11:45 AM, Colm Bhandal <bhandalc AT tcd.ie> wrote:

Absolutely agree. Induction on the naturals is an invaluable playground for learning Coq.

 

On 5 September 2013 16:14, Valentin Robert <valentin.robert.42 AT gmail.com> wrote:

Let the existence of powerful tactics not prevent you from learning
the basics of induction though, as this will be fairly ubiquitous if
you plan to achieve anything elaborate using Coq. :-)

- Valentin

On Thu, Sep 5, 2013 at 2:43 PM, Colm Bhandal <bhandalc AT tcd.ie> wrote:
> 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
>>
>>
>
>