What do we do about https://github.com/coq/coq/issues/13834 ?
cc @Pierre-Marie Pédrot
Can't we move toward having the rewrite principles declared in advance? The lazy creation/declaration of these lemmas brings very little.
Error: you can't rewrite with foo unless you first run Whatever Scheme foo or decorate foo with #[rewrite].
I totally agree side effects are evil, but there are some which are kind of justified, and some others that look like they were added "for sport" like this one.
It's even worse than that: since the rewrite side-effects are globally visible inside a Defined proof, this is a source of non-determinism.
It's a terrible side-effect I think. And IIRC in a universe polymorphic proof it does generalize over unnecessary universes.
So, if we agree that we should generated these term ahead of time, maybe we should plan something. Still I have a memory of some cases in which there are many possible terms, and we don't know which ones (I think @Matthieu Sozeau told me this once). In any case we can design commands to generate the ones the user needs and have good error messages about what the user should run.
Last updated: Dec 01 2023 at 07:01 UTC