coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] eta-expansion of Program Fixpoints

From: Merlin Göttlinger <megoettlinger AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] eta-expansion of Program Fixpoints
Date: Sat, 20 Jan 2018 13:15:38 +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-f54.google.com
Ironport-phdr: 9a23:BgKDHRTl2d1BwTW7w2KXanZwatpsv+yvbD5Q0YIujvd0So/mwa69YBWN2/xhgRfzUJnB7Loc0qyK6/mmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfa5+IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/27XhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YBCPQOPfxcr4n8oVsBtRqwHQ+wBOPzzj9Ih3n23aIk3OQ7DArL2wkgEMwBsHTTstr1KLsSUeS0zKnOwjXMcelW1Czy6IjNaB8hoPWMUahsfsrWzEkiDgXIhUiTp4z9Jz6ZyPgBvmyB4+djVe+jkXArpxx+rzS1xsohhY/EjZ8PxF/e7yV22oM1KMW4SEFlZd6kF4NdtySAOIt3RsMuWmBouDomxrEft562fCcHxI4oxx7YbPyHfIyI7Qz5WOmNJjd4gWppeLO5hxms7Uit0vPwWtWw3VpQrSdIksPAum4Q2xHc8MSKSvRw8l+k2TmV1gDT7u9EIVozlareM5Mhx6A/lpUUsUvdAi/2hEH2jK6QdkUr5Oeo8f/qYrrjppCGNo90jhvyPbgpmsy6Geg4KBQBX3CH+eSg073u5VH2QLJTjvEvjqbZtI3aKt8Aq66iAw5V154j5AylAzen1tQYh3gHI0hfdBKJlYi6c23JdbrzCu76iFCxmh9qwerHN/vvGN+FenPEifLqeat3w09a0gs6i95FscF6ELYEddf+QEvwsuv3kAMlNw2yzOv9QIF424wZVH6TBq6fP67ImVCN7+MrZeKLYdlG637GN/E56qu23jcCklgHcPzxhMpFWDWDBv1jZn6hTz/pi9YFH30Nu1NnHuPvgVyGFzVUYiTrBv5u1nQAEIujSLz7aMW1mrXYhXW0G5RXYiZNDVXeSS61JbXBYO8FbWepGuEkkjEAUuL8GYoo1BXrtROijrQ6cqzb/SoXsZ+l399wtbXe

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

[Coq-Club] eta-expansion of Program Fixpoints, Merlin Göttlinger, 01/20/2018
- Re: [Coq-Club] eta-expansion of Program Fixpoints, Matthieu Sozeau, 01/20/2018
  - Re: [Coq-Club] eta-expansion of Program Fixpoints, Merlin Göttlinger, 01/20/2018