Stream: Coq devs & plugin devs

Topic: Unify local + global context

Lasse Blaauwbroek (Sep 17 2022 at 17:53):

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:

1. Section variables seem to exist in some kind of Heisenberg state between global and local. Definitions from the section can refer to them, but to the user it looks like they are part of the local context. This is especially strange when the user unfolds a definition depending on a section variable.
2. The abstract tactic 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 Qed or Defined was used, these objects either stay in the global context or are removed again and inlined into the proof term.
3. Schemes have a similar effect like 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 clear, 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).

Pierre-Marie Pédrot (Sep 17 2022 at 18:02):

Some quick remarks:

• Don't take abstract as an example of something that makes sense in the current implementation.
• The evarmap is also another kind of environment, and it's not clear where it lives with your definition.
• There is a difference of use between local contexts and global environments, namely the former is "reader"-like whereas the latter is "state"-like. There is a notion of scope for bound variables, but you can't pop a global def.

Lasse Blaauwbroek (Sep 17 2022 at 18:30):

• The abstract tactic 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...
• I'd think that the evar-map can be maintained just like the mask that I described can be maintained.
• Yes, the global context being reader-like and the local context being state-like is a good point. Thanks.

Last updated: Oct 12 2024 at 11:01 UTC