Stream: Coq users

Topic: ✔ Preserving binder names while manipulating functions


view this post on Zulip Mathis Bouverot-Dupuis (May 09 2024 at 20:05):

Yes I can preserve binder names using metaprogramming (for instance using Ocaml or Metacoq, and maybe also Ltac). The feature I would have liked is the ability to preserve binder names in pure Coq, so that I can prove properties about my functions. This feature does not seem to exist, so I guess I'll mark this topic as solved :(

In the end I did find a way to implement the tactic (https://github.com/MathisBD/coq-push-negs).

view this post on Zulip Notification Bot (May 09 2024 at 20:05):

Mathis Bouverot-Dupuis has marked this topic as resolved.

view this post on Zulip Thomas Lamiaux (May 09 2024 at 21:09):

Hum, controlling where to rewrite is a pain in Coq, but SSReflect one is supposed to be much better though I have never tried it myself

view this post on Zulip Théo Winterhalter (May 10 2024 at 00:14):

Please note that it is a feature that pure Coq is not able to distinguish binder names. You mention MetaCoq and in that case you would be able to prove properties about your functions.

view this post on Zulip Mathis Bouverot-Dupuis (May 10 2024 at 09:06):

For Metacoq, I believe I need to use quoting/unquoting to accomplish what I want, which (correct me if I'm wrong) makes proving things impossible.

I also understand that being able to distinguish binder names in Coq would not be a good thing, but would the ability to construct specific binders (without being able to destruct/inspect the binder afterwards) cause any theoretical issues?

view this post on Zulip Théo Winterhalter (May 10 2024 at 09:27):

For MetaCoq it's true that you would not be able to prove anything about the quote and unquote, but you can prove things about the rest. You can also produce a proof of an equality if that's what you need in the end. Something like that.

If I understand what you want, I guess it should be feasible to have some meta-programming involved at the level of binders, but I'm not sure you will get that feature request granted. If you think there is a feature that would make sense to be added to Coq and that you would willing to implement with the help of the Coq developers then I suggest you attend the next CUDW: https://github.com/coq/coq/wiki/Coq-Users-and-Developers-Workshop-2024
They would be able to advise you on what to do, but I'm not sure the feature you want, they would want. :smile:


Last updated: Jun 22 2024 at 15:01 UTC