Mathis Bouverot-Dupuis (May 09 2024 at 20:05): 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).
Notification Bot (May 09 2024 at 20:05):Mathis Bouverot-Dupuis has marked this topic as resolved.
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
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.
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?
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: Oct 13 2024 at 01:02 UTC