coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] eta-expansion of Program Fixpoints

From: Lars Rasmusson <lars.rasmusson AT ri.se>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] eta-expansion of Program Fixpoints
Date: Wed, 21 Feb 2018 10:37:21 +0000
Accept-language: en-US, sv-SE
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lars.rasmusson AT ri.se; spf=Pass smtp.mailfrom=lars.rasmusson AT ri.se; spf=None smtp.helo=postmaster AT se-out1.mx-wecloud.net
Ironport-phdr: 9a23:y3geZR+a8gCkov9uRHKM819IXTAuvvDOBiVQ1KB42uMcTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaKz43/mLZisJyg6JavB2uqAdyw4HIbIGQLvdyYr/RcNEcSGFcXshRTStBAoakYoUJFeUBJ/1YpJThqVQUthu+ABSsBPj0yj9PgH/9wKo30+A7HgHcxwwsBcgOv27PrNXwKacSSvu1zK7OzTjYdfNW2C3x6JPWfR04p/yHQLF+cdLJxEQsEw7JlEucpZL4Mz+PyOgAs2iW4/BkWO+hk2Irth19riKyysswloXFnJ4ZxkrF+Ch72Io1K8O3RU1nbdOhFZZdtTyVOol1T84nQGxnpT01x7wDtJKmciUF1ZonyhvcZvObb4eF4BTuX/uLLzhinnJqYre/ig6y8Ue+zu38UdG50E1UoSZcldnMq2wN2wHJ5siCRfpx50mg1iiT2ADX7eFEPF07mbDdK5E/3r48jpsTsULdES/qgEj7j6ubel869uS29ujreKvqq5+cOoNujgzzPLwimsmlDuQ5NggOUXKb+eO51LD7+U32Wq9KjuYsnqnDqp/aPsEbprOiAw9O1YYj7Q2yDy2n0NgChnkIMkpJeAibgIjxJ1HOPPf4AO+jjFSriTdn3uzJPrn8AprWNXXDi7fgfbNl60FG0gYzzNZf54hVCr4bOv7zVFXx55TkCUpzOAuthu3jFd9V14UEWGvJDLXTePfZtkbN7eYyKcGNYpUUsXDzMa52yeTpiCodkEUGNZOgxp4Kc2u/GLwyJ0yDejz2i8wEDHwRuQwWVu2sk1DUAm0bXGq7Q69pvmJzM4mhF4qWHtn80ozE5z+yG9htXk4DD1mNFXnycIDbCe0NLjmfcJY4zm40EIO5Qopk7imA8RfgwuU1NOuS4SBK7cu+hugw3PXakFQJzRIxD8mZ1DvRHXp522QVW2Zw2bA6vkF2zlCe3e5+juAKTdE=

On 20 Jan 2018, at 14:15 , Merlin Göttlinger <megoettlinger AT gmail.com> wrote:

Program Fixpoint demo {A} (l : list A) {measure (length l)} : nat :=
match l with
| nil => 0
| cons x x0 => fold_right plus 0 (map demo [[x]; x0])
end.

I don't know if this helps, but since (H)

fold_right plus 0 (map demo [[x]; x0]) = demo [x] + demo x0

a call to (demo [a]) will turn into (demo [a] + demo nil), so it is an infinite loop,

and shouldn't be provable anyway...

Require Import List Psatz. Import ListNotations.
Lemma H: forall A (x:A) x0 demo,

fold_right plus 0 (map demo [[x]; x0]) = demo [x] + demo x0.

Proof. intros; compute; fold plus; lia. Qed.

Attachment: smime.p7s
Description: S/MIME cryptographic signature

Re: [Coq-Club] eta-expansion of Program Fixpoints, Lars Rasmusson, 02/21/2018