Programmers <socalfp@googlegroups.com>
Received: by 10.236.168.70 with SMTP id j46mr35141034yhl.2.1320616516094;
        Sun, 06 Nov 2011 13:55:16 -0800 (PST)
X-BeenThere: socalfp@googlegroups.com
Received: by 10.150.35.17 with SMTP id i17ls8118641ybi.1.gmail; Sun, 06 Nov
 2011 13:55:15 -0800 (PST)
Received: by 10.236.175.225 with SMTP id z61mr34358637yhl.9.1320616515548;
        Sun, 06 Nov 2011 13:55:15 -0800 (PST)
Received: by 10.236.175.225 with SMTP id z61mr34358636yhl.9.1320616515537;
        Sun, 06 Nov 2011 13:55:15 -0800 (PST)
Return-Path: <thomashartm...@googlemail.com>
Received: from mail-gx0-f174.google.com (mail-gx0-f174.google.com [209.85.161.174])
        by gmr-mx.google.com with ESMTPS id f3si1607463ybi.0.2011.11.06.13.55.15
        (version=TLSv1/SSLv3 cipher=OTHER);
        Sun, 06 Nov 2011 13:55:15 -0800 (PST)
Received-SPF: pass (google.com: domain of thomashartm...@googlemail.com designates 209.85.161.174 as permitted sender) client-ip=209.85.161.174;
Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thomashartm...@googlemail.com designates 209.85.161.174 as permitted sender) smtp.mail=thomashartm...@googlemail.com; dkim=pass (test mode) header...@googlemail.com
Received: by ggnb2 with SMTP id b2so6513479ggn.33
        for <socalfp@googlegroups.com>; Sun, 06 Nov 2011 13:55:15 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=googlemail.com; s=gamma;
        h=mime-version:in-reply-to:references:from:date:message-id:subject:to
         :cc:content-type:content-transfer-encoding;
        bh=pMxCyk06+0C0Ntf5Q6cuFvca8j2TB/amoPgXvZSKVhM=;
        b=mZiE63Hc6jdyhy/idCzpdODBTEV4ZoS5BAUCqu2b1hGaY95woYlyPfxAWfKk+bEGnW
         gmGIm1nBOCDlwnfXvgbwl0hWDKm3gyaKrE67x2wtkHZD8tJuNXE3EavIv/cZ3J3x5Y/y
         slAeyK9NludGorzt3DCIVqMZ+rUOzkkaE6AiU=
Received: by 10.50.104.137 with SMTP id ge9mr36767572igb.38.1320616515290;
 Sun, 06 Nov 2011 13:55:15 -0800 (PST)
MIME-Version: 1.0
Received: by 10.142.135.20 with HTTP; Sun, 6 Nov 2011 13:54:54 -0800 (PST)
In-Reply-To: <CAHAXnDXVTwiYaurEnRH1jh6V+wWvLpeXkWBqoOfZPLApEYs...@mail.gmail.com>
References: <CAHAXnDXd0kXmhkMuba=8nBdkGyrSo03Gkv+omiQ_Cx_hEfZ...@mail.gmail.com>
 <CAHAXnDXVTwiYaurEnRH1jh6V+wWvLpeXkWBqoOfZPLApEYs...@mail.gmail.com>
From: Thomas Hartman <thomashartm...@googlemail.com>
Date: Sun, 6 Nov 2011 13:54:54 -0800
Message-ID: <CAHAXnDWBuSvWKpq9mLuuj=TkPaBLVo9kdLzbRMKHP2Tb6_G...@mail.gmail.com>
Subject: Re: Who can prove plus_assoc without using simpl tactic? And what
 does simpl tactic REALLY do?
To: socalfp@googlegroups.com
Cc: Michael Vanier <mvanie...@gmail.com>
Content-Type: text/plain; charset=windows-1252
Content-Transfer-Encoding: quoted-printable

Correction: On second thought, the following Definition is not valid.
You need to use Fixpoint.

NOT VALID:
Definition plus (n0 m0 : nat) : nat :=3D
     match n0 with
     | 0 =3D> m0
     | S p =3D> S (plus p m0)
end.

I was fooled into thinking it was okay by the fact that I had made the
definition in a Module Playground segment, which was ignored further
on.

Where I used plus in the proof, I guess it was coming from coq prelude.


On Sun, Nov 6, 2011 at 1:20 PM, Thomas Hartman
<tho...@marketpsychdata.com> wrote:
> As a side note, I then tried to prove
>
> Theorem plus_Sn_m_here : forall n m : nat, plus (S n) m =3D S (plus n m).
>
> in a way that was more "convincing" to me than just citing
> reflexivity. Because actually, it wasn't obvious to me that the above
> is reflexively true, though appparently it is to coq.
>
> Theorem plus_Sn_m_here : forall n m : nat, plus (S n) m =3D S (plus n m).
> =A0reflexivity.
> Qed.
>
> Finally, I wound up with the following
>
> Theorem plus_Sn_m_here : forall n m : nat, plus (S n) m =3D S (plus n m).
> =A0unfold plus. (* Can be skipped. The proof pane is a mess, but both
> sides of the mess are identical, see below*)
> =A0reflexivity.
> Qed.
>
> First, here is the mess you get in the proof pane from unfold plus:
>
> 1 subgoal
> ______________________________________(1/1)
> forall n m : nat,
> S
> =A0((fix plus (n0 m0 : nat) : nat :=3D
> =A0 =A0 =A0match n0 with
> =A0 =A0 =A0| 0 =3D> m0
> =A0 =A0 =A0| S p =3D> S (plus p m0)
> =A0 =A0 =A0end) n m) =3D
> S
> =A0((fix plus (n0 m0 : nat) : nat :=3D
> =A0 =A0 =A0match n0 with
> =A0 =A0 =A0| 0 =3D> m0
> =A0 =A0 =A0| S p =3D> S (plus p m0)
> =A0 =A0 =A0end) n m)
>
> This is a mess to look at, but note that both sides of the mess is
> identical, which to me at least is "convincing" enough with regards to
> applying reflexivity.
>
> So... what is fix doing here? It appears that
>
> (fix plus (n0 m0 : nat) : nat :=3D
> =A0 =A0 =A0match n0 with
> =A0 =A0 =A0| 0 =3D> m0
> =A0 =A0 =A0| S p =3D> S (plus p m0)
> =A0 =A0 =A0end)
>
> is an internal desugaring of the plus function defined earlier as
>
> Fixpoint plus (n : nat) (m : nat) : nat :=3D
> =A0match n with
> =A0 =A0| O =3D> m
> =A0 =A0| S n' =3D> S (plus n' m)
> =A0end.
> *)
>
> I confirmed this by commenting out the first definition and replacing
> with the second Basics.v loads just fine, through =A0the end of the
> file.
>
> ***********************
> (*
> Fixpoint plus (n : nat) (m : nat) : nat :=3D
> =A0match n with
> =A0 =A0| O =3D> m
> =A0 =A0| S n' =3D> S (plus n' m)
> =A0end.
> *)
>
> Definition plus (n0 m0 : nat) : nat :=3D
> =A0 =A0 =A0match n0 with
> =A0 =A0 =A0| 0 =3D> m0
> =A0 =A0 =A0| S p =3D> S (plus p m0)
>
> end.
> ***********************
>
> Cheers, thomas.
>
>
> On Sun, Nov 6, 2011 at 11:39 AM, Thomas Hartman
> <tho...@marketpsychdata.com> wrote:
>> Theorem plus_assoc : forall n m p : nat,
>> =A0n + (m + p) =3D (n + m) + p.
>> Proof.
>> =A0intros n m p. induction n as [| n'].
>> =A0Case "n =3D 0".
>> =A0 =A0reflexivity.
>> =A0Case "n =3D S n'".
>> =A0 =A0simpl. (* <<<--- what is simpl doing here ?????? ?*)
>> =A0 =A0rewrite -> IHn'.
>> =A0 =A0reflexivity.
>> Qed.
>>
>> Who can prove this without using simpl? (Spoiler below.)
>>
>> Hint 1:
>>
>> SearchRewrite...
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>> Hint 2:
>>
>> SearchRewrite ( (S _) + _).
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>> Solution:
>>
>> Theorem plus_assoc_nosimpl : forall n m p : nat,
>> =A0n + (m + p) =3D (n + m) + p.
>> Admitted.
>> Proof.
>> =A0intros n m p.
>> =A0induction n as [|n']. reflexivity.
>> =A0rewrite -> plus_Sn_m.
>> =A0rewrite -> plus_Sn_m.
>> =A0rewrite -> plus_Sn_m.
>> =A0rewrite -> IHn'.
>> =A0reflexivity.
>> Qed.
>>
>
>
>
> --
> --
> _____________________
> Thomas Hartman
> MarketPsych LLC
> MarketPsy Capital =A0LLC
> 2400 Broadway, Suite 220
> Santa Monica, CA, USA
> Tel: =A0+1.310.573.8523
> ______________________
>
> This e-mail message and any attachments may contain information that
> is confidential, proprietary or privileged, and is for the named
> person=92s use only. =A0No confidentiality or privilege is waived or lost
> by any mistransmission. =A0If you are not the intended recipient or
> agent responsible for delivering it to the intended recipient, you are
> hereby notified that any dissemination, distribution, copying or other
> use of this message or its attachments is strictly prohibited. =A0If you
> have received this message in error, please notify us immediately and
> destroy all copies of this message and attachments without disclosing
> the contents to anyone. =A0Neither this message nor any information
> included herein constitute an offer to sell or the solicitation of an
> offer to buy any securities or investment product, or legal, tax,
> accounting, or investment advice.
>