Proposing to associate a qualified name to section variables so as to distinguish them from (other) goal variables

[herbelin]

Rendered here.

[ppedrot]

I really like this idea, but as usual the devil is in the details. I wouldn't be surprised if we discovered while implementing the CEP that something prevents this to work.

[herbelin]

I really like this idea, but as usual the devil is in the details. I wouldn't be surprised if we discovered while implementing the CEP that something prevents this to work.

At least, there are a number of decisions to take!

To start with, there are two usages of the (current) named_context, even in the kernel:

• strictly as a section context, e.g. in Safe_typing.push_named, in Declarations.const_hyps, ...
• as a mix of section and goal variables to interpret the Var field in those general functions which the proof engine might use (e.g. the reduction)

The second case is delicate. From the moment the Var field can accept any section variable, even one which is not anymore listed in the current goal context, we need to find the information about this section variable somewhere.

Where to find it?

I see several solutions:

1. The goal context does not contain anymore the section variables that have been cleared. In this case, in the Var case, lookup searches first in the goal context, and if it does not find the variable, it searches in the section context
2. The goal context is a strict extension of the section context: each section variable is embedded in the goal context together with a flag telling if it is visible from the goal. In this case, in the Var case, lookup only needs to look in the goal context. If the variable is not found, it is an error.

Concretely, this means the two following options (in simplified informal code):
1.

type section_variable = Id.t
type section_context = section_variable declaration list

type goal_variable = {issecvar : bool; name : Id.t}
type goal_context = goal_variable declaration list
type env = {section_context : section_context; goal_context : goal_context; ...}
let lookup_named id env =
  try List.assoc id env.goal_context
  with Not_found -> if id.issecvar then List.assoc id.name env.section_context else raise Not_found

type section_variable = Id.t
type section_context = section_variable declaration list

type goal_variable = {issecvar : bool; name : Id.t}
type goal_context = {it : goal_variable declaration list; secinvisibility : bool Id.Map.t}
type env = {section_context : section_context; goal_context : goal_context; ...}
   (* invariant: each id in section_context occurs under the form {issecvar=true;name=id} in goal_context,
      possibly registered in the invisibility map *)
let lookup_named id env = List.assoc id env.goal_context.it

Any preference? Or alternative proposal?

[gares]

I like the idea too, and this is also what I simulate in Coq-Elpi by "identifying" the VarRef and ConstRef nodes in the GlobRef type.
This is IMO the simplest way top get a sound "tactic" system.

W.r.t. your question, I think that the displayed proof context should be made of section variables + proof variables.
I would not change the type Env.named_context, but rather have typing functions look up in 2 distinct "lists".
For backward compatibility I guess Goal.hyps (pf_hyps) should return the list of non cleared section variables + proof variables.
A cleared section variable x should display as Section.x as you propose if obtained by unfolding a constant for example.

IMO the big change (which is also the most tricky part in the simulation of this I do in Coq-Elpi) is that evars do not have section variables in their explicit substitution any more (being akin to global constants, ConstRef, they don't show up there). I've no idea if this can break code in the tactics (for sure there are few ssr lines which rely on that). If you don't change the type of Env.name_context then this happens naturally (since evars won't born in the union of the section and proof context, but just in the latter).

No idea what this means for vm (a recall a cache for section Let).

[herbelin]

IMO the big change (which is also the most tricky part in the simulation of this I do in Coq-Elpi) is that evars do not have section variables in their explicit substitution any more (being akin to global constants, ConstRef, they don't show up there).

Yes, the explicit substitution of evars does not need to give an instance for section vars since it is always the identity.

I've no idea if this can break code in the tactics

I would suspect that changing the explicit substitution would not break tactics. Of course, the presence of section variables or not in the defining context of an evar would modify the behavior of tactics.

I would not change the type Env.named_context, but rather have typing functions look up in 2 distinct "lists".

Two distincts lists is ok for typing. Then, the lookup for Var nodes would typically look like:

let lookup_named id env = List.assoc id.name (if id.issecvar then env.section_context else env.goal_context)

This is what I would consider as the default direction to go unless someone disagrees.

We still need somewhere (at latest in the evar_info), an explicit indication of the subset of section variables which tactics have to care about. Would it be ok for anyone if this is directly put in the evar_info rather than in the evar_hyps:named_context field of the evar_info?

About what list of variables is displayed (by Show), I have no strong preference.

Please tell if you have implementation plans, so that we can prevent doing twice the same work!

---

Another remark: I wonder whether rel_context shouldn't be moved out of safe_environment??? Then, once section_context and named_context are distinct, the named_context could be dropped too, couldn't it? Any opinion? In any case, this could be an easy step to propose as a PR, what do you think?

[gares]

This is what I would consider as the default direction to go unless someone disagrees.

Sorry if I was not clear.

I was suggesting to use the node Const of Constant.t for section variables, rather than a tagged Id.t and have in the section-context a list of Constant.t flagged with a boolean, so that we know what has to be displayed in the proof (clear could flip that boolean). The section-context is there merely to know which constants are part of the section, but is not really a context to be used for typing. And if you do so, then there is nothing to change in the typing code (I was wrong about this in my previous message, and misleading).

The command Variable has then to really mean Axiom, and Let is Definition, and section closing has to abstract Const nodes rather than Var nodes.
Print Assumptions, executed in the middle of a section, would also print section variables, because there they are really represented as axioms in the safe env!

As a result, I would keep Var for proof variables only.

I hope now it's more clear how I would implement it. Of course, I may miss some detail ;-)

PS: GlobRef could then drop the VarRef node, since Var is always local to a proof, never "global".
PS2: This is the encoding I do in Coq-Elpi

[herbelin]

@gares: Using Const for section variables would be easy for the typing part. What was worrying me a priori with this approach (but we need to make a precise evaluation) is that many tactics are used to treat hypotheses through the type variable/Id.t. This is why I was rather thinking at preserving the variable/lookup_named/mkVar/destVar/etc abstraction level, assuming that the tactic code would then go through without much trouble, rather than having to tell each individual tactic that hypotheses can now also be of the form Const (but again, I may be pessimistic and that may be simpler than what I think.)

and have in the section-context a list of Constant.t flagged with a boolean, so that we know what has to be displayed in the proof (clear could flip that boolean).

Yes, that's what I morally had in mind too (up to using Constant.t, KerName.t, or the basename of those, but this is equivalent).

[ppedrot]

I think that treating section variables as constants is the way to go. Instead of having two lists of contexts in the proof engine, we could simply instantiate the toplevel variables of the proof with the section "variables", with an (apparent) shadowing. This would be fully transparent for the user, we wouldn't even need to print stuff specially.

[herbelin]

I think that treating section variables as constants is the way to go. Instead of having two lists of contexts in the proof engine, we could simply instantiate the toplevel variables of the proof with the section "variables", with an (apparent) shadowing. This would be fully transparent for the user, we wouldn't even need to print stuff specially.

OK.

(But I would not mind also an extra unfolding of the artificial let-in introduced for the toplevel variables before passing the term to the kernel).

Concretely, @gares or @ppedrot, are you then expecting something from me on this topic or you have a roadmap (at least informally), and we just let things progress spontaneously?

[gares]

I don't have time for this myself, so I don't have a roadmap. Still I think having a design documented here is important for anyone, maybe some parts can be done by little steps (I don't know).

(But I would not mind also an extra unfolding of the artificial let-in introduced for the toplevel variables before passing the term to the kernel

I don't know exactly what @ppedrot had in mind, but I would not use the logic here, at all.
I would "display" in the goal windows also (for backward compatibility, unless set otherwise) the section axioms and local definitions (to avoid using the term variable). Then tactic "x" would resolve "x" to either a proof variable, or a global constant, as usual. I don't get why it can't be an Id.t. I recall some AST like SsrHyp of Id.t for example. I guess it's the interpretation function that has to change type, but not necessarily the AST.

[herbelin]

Then tactic "x" would resolve "x" to either a proof variable, or a global constant, as usual. I don't get why it can't be an Id.t.

Do you exclude that a goal mentions both a section variable S.x and a goal variable x of same base name?

[gares]

Yes, this can happen with something like

Seciton X.
Variable x : nat.
Definition foo := x.
Goal forall y, foo = y.
(* goal is: x |- forall y, foo = y *)
unfold foo; clear x; intro x.
(* goal is: x |- X.x = x *)
tactic x; tactic X.x.

I guess I don't know the internal of Coq vanilla tactic enough to see the problem with the second invocation.
The tactics I wrote take terms in input, and both x and X.x are terms.
I see X.x is a qualid and not an ident, but that seems all.

Do you have a specific tactic in mind?

[herbelin]

Actually, I got confused and asked something different that what I aimed at.

A typical question is what would be the type of the clear tactic. Would it take an Id.t and have to find by itself, in case this Id.t is not a goal variable, to what Const-like section variable it refers to? Or would it take a union type of either an Id.t or a Constant.t?

More generally, how much the code of each tactic possibly referring to names of the goal context would have to be modified to decide explicitly if the name refers to a not-cleared section variable or to a non-section goal variable?

I mean, all options are ok, but one has to be taken at some time.

[ppedrot]

We should probably schedule a meeting to talk about this CEP.

[herbelin]

We should probably schedule a meeting to talk about this CEP.

Next week is quite busy unless it is Thursday or Friday. Do you want me to set a poll? @gares, what would be your constraints, for, say, a 1h meeting?

[gares]

Would it take an Id.t

Yes. Section axiom "x" can only be cleared once, and the effect is to flip the boolean used by the pretty printer for the backward compatible "proof context from the section". After that point in time occurrences of it are displayed as "X.x" and can't be cleared. If the user introduces another x, then he can clear it.

[gares]

Thursday or Friday

they work for me

[herbelin]

I'm considering working back on this issue at some time, following this comment:

I was suggesting to use the node Const of Constant.t for section variables, rather than a tagged Id.t and have in the section-context a list of Constant.t flagged with a boolean, so that we know what has to be displayed in the proof (clear could flip that boolean). The section-context is there merely to know which constants are part of the section, but is not really a context to be used for typing. And if you do so, then there is nothing to change in the typing code.

Here is a preliminary sketch about how to proceed:

Step 1: section variables remain Var node but we remember which goal variables are the copy of a section context (i.e. which morally are definitions id' := Top.Section.id). [A concrete attempt]

• add to named_context_val a new field env_named_secvars : Id.t Id.Map.t which registers the section-variables-as-global-constants used in a goal, telling for each section variable available in the goal what its name is; each section variable in the map will have a copy in the field env_named_ctx to tell its position in the context
• clear id removes id from the table of section variable (since clear already needs a section var to be non dependent) in addition to clearing it from
• rename changes the name in env_named_secvars if the variable is a section variable
• lookup_named in a goal continues to failing on a cleared section variable

Step 2: Prepare Declare.declare_variable to be on top of Declare.declare_constant [A concrete attempt]

• move the calls to DeclareUniv.declare_univ_binders and DeclareUctx.declare_universe_context scattered here and there (especially in comAssumption.ml to Declare.declare_variable

Step 3: Use global constants for section variables

• Global.push_named_assum/Global.push_named_def take a definition_entry and have the same effect as add_constant except that they also register the assum/def to the section table
• remember the ordered list of qualified names and not only the number of elements in safe_env.sections.context and move this in Environ.env, accessible with a new Environ.section_context, so that we can replace the calls to named_context intending to see it as a section context?
• add another copy of LocalDef/LocalAssum with qualified name, or take the pair of a long name and a named declaration?
• adapt cooking so that it looks for Const instead of Var (in Cooking.abstract_context?)
• when starting a proof, replace the Const-based section variables with their Var name? (Or tweak tactics working on hypotheses so that when referring to id it may be resolved into Top.id?)
• removal of useless tests such as check_hyps_inclusion since the section context is now in full control of the kernel and a safe environment has by construction the correct dependencies (no more reset_with_named_context correctness hole).
• make Proof_using abstract over the representation of the section context and translate it to a constant-based section context
• use GlobRef.ConstRef everywhere we used VarRef, e.g. in implicit arguments, argument scopes, ... (many occurrences)
• ...

Step 4: Back to goals and tactics

• replace env_named_secvars : Id.t Id.Map.t with env_named_secvars : Constant.t Id.Map.t
• clear id allowed on section variables, replacing them with their expansion?
• accept unfold on section variables, replacing them with their expansion?
• remove code such as Equality.check_non_indirectly_dependent_section_variable, Termops.occur_in_global, ...

---

Related questions:

• named_context:
  • once section variables are constants, shouldn't the named_context (used only for goals) eventually go outside the kernel?
  • shouldn't actually named_context_val be the appropriate level of abstraction rather than named_context?

[Feel free to edit this comment to refine it/amend it]

[herbelin]

@gares, @ppedrot, @SkySkimmer: I'm currently working at using Const for section variables, which I believe was relatively consensual. This is going well, but this is quite a lot of work, and there are a few design choices which I would prefer are discussed earlier than sooner. Some implementation details are given in the previous comment.
The current experiments are in the following branches:

• Step 1: master+goal-knows-section-variables
• Step 2: 3 first commits of master+univs-ctx-and-binders-centralized
• Step 3, in progress: master+section-vars-are-consts

In any case, tell me if you want to take part to the design of the prototype, and at which step of the process.

[gares]

I'm currently working at using Const for section variables, which I believe was relatively consensual. This is going well

Great. I did a look at step3, but it is not clear to me which design choices you want to discuss. Can you write them here?

[herbelin]

Great. I did a look at step3, but it is not clear to me which design choices you want to discuss. Can you write them here?

There is the choice of names for the new datatypes and the organization of these datatypes. For instance, I'm currently moving Section.t directly in env and making some reorganization between Section and Safe_typing. But maybe should I work further first.