Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Merlin Göttlinger <megoettlinger AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] eta-expansion of Program Fixpoints
  • Date: Sat, 20 Jan 2018 17:30:08 +0000
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=megoettlinger AT gmail.com; spf=Pass smtp.mailfrom=megoettlinger AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f50.google.com
  • Ironport-phdr: 9a23:PzQSXxBm6+A8dvGqRLh/UyQJP3N1i/DPJgcQr6AfoPdwSPv5pMbcNUDSrc9gkEXOFd2Cra4c0qyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUmTaxe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoIODA5/2PXhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YBCPQOPfxcr4n8oVsBtRqwHQ+wBOPzzj9Ih3n23aIk3OQ7DArL2wkgEMwBsHTTstr1KLsSUeS0zKnOwjXMcelW1Czy6IjNaB8hoPWMUahsfsrWzEkiDgXIhUiTp4z9Jz6ZyPgBvmyB4+djVe+jkXArpxx+rzS1xsoglo/EjZ8PxF/e7yV22oM1KMW4SEFlZd6kF4NdtySAOIt3RsMuWmBouDomxrEft562fDQGxI4oxx7YbPyHfIyI7Qz5WOmNJjd4gWppeLO5hxms7Uit0vPwWtWw3VpQrSdIksPAum4Q2xHc8MSKSudx8l+k2TmV1gDT7u9EIVozlareM5Mhx6A/lpUUsUvdAi/2hEH2jK6QdkUr5Oeo8f/qYrrjppCGNo90jhvyPbgpmsy6Geg4KBQBX3CH+eSg073u5VH2QLJTjvEvjqbZtI3aKt8Aq66iAw5V154j5AylAzen1tQYh3gHI0hfdBKJlYi6c23Jdfv/FLK0h0mmuDZt3fHPeLP7UbvXKX2Wtbr7ebd73GHC1BY3zNZQ6ogcXrQML/X+RlP1tdrXAwURPAm9wuKhA9J4gNBNEVmTC7OUZfuB+WSD4fgidrHVNd0l/Q3lIv1g3MbAyHowmFsTZ66shMJFZ3WxH/AgKEKcMyO13oUxVFwStw97d9TEzUWYWGcKNXm3VqM4oDo8DdD+VNqRdsWWmLWEmRyDMNhWa2RBUA3eFH7pc8CFR69JZn/KZMBmlTMAWP6qTIpzjRw=

Hi Matthieu,

no that doesn't seem to change things.

Cheers,
Merlin

Matthieu Sozeau <mattam AT mattam.org> schrieb am Sa., 20. Jan. 2018 um 18:25 Uhr:
Hi Merlin,

I guess it’s a type inference issue here, what if you explicitly do [@map A demo] instead?
Cheers,
- Matthieu
Le sam. 20 janv. 2018 à 14:15, Merlin Göttlinger <megoettlinger AT gmail.com> a écrit :
Hi,

when using Program Fixpoint with a measure function the following works (typeckecks):

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

whereas the version where demo should be eta-expanded automatically does not work because of the added parameters of the measure function:

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.

Is there a trick to have Coq expand this automatically or a specific reason why it doesn't?

Cheers,
Merlin



Archive powered by MHonArc 2.6.18.

Top of Page