After having some experience with Coq internally treats the global context and local context I have some questions about why things are designed the way they are.
Coq has two pretty separate notions of contexts. The global context and the local context. At first sight, this seems to make sense: The global context contains "permanent" objects, while the local context contains temporary hypotheses and changes frequently while proving a lemma. However, there are quite a few features in Coq that blur the line between these two notions:
abstracttactic adds objects to the global context. This has the immediate consequence that the global context needs to be threaded through the tactic monad (even though at first sight one would expect only the local context to be threaded). Then, depending on whether
Definedwas used, these objects either stay in the global context or are removed again and inlined into the proof term.
abstract. They magically generate definitions which are sometimes inlined and sometimes not.
All this makes me wonder what the advantage of two notions of contexts are. Why not simply have one context. Then, while interactively proving a lemma, a mask can be maintained that determines which assumptions/definitions are shown to the user and in what order. Tactics like
move and such can interact with this mask to modify the view for the user.
I'm having a hard time coming up with conceptual reasons why this would be a bad idea (ignoring the practical issue regarding the amount of work it would take to actually pull this off).
Some quick remarks:
abstracttactic may be considered as mis-behaved, but as far as I know, the 'auto-generating-schemes' thing is not considered bad right? And that has very similar behavior...
Last updated: Jun 08 2023 at 04:01 UTC