Stream: Coq devs & plugin devs

Topic: Unify local + global context

view this post on Zulip 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).

view this post on Zulip Pierre-Marie Pédrot (Sep 17 2022 at 18:02):

Some quick remarks:

view this post on Zulip Lasse Blaauwbroek (Sep 17 2022 at 18:30):

Last updated: Nov 29 2023 at 17:01 UTC