Fixes #10812: tactic subst failure with section variables indirectly dependent in goal

[herbelin]

Kind: bug fix

To decide if rewriting is needed, don't consider implicitly depending section variables as occurring since there are invisible from unification (i.e. use local_occur_var)

This is a potential source of incompatibilites, but it also has to be fixed.

Fixes #10812
Fixes #12139

• Added / updated test-suite
• Entry added in the changelog

[ppedrot]

@herbelin can you rebase to get a clean CI?

[JasonGross]

This seems extremely strange to me. It breaks subject reduction in the context of the goal, right? Or else it is not reversible (if it clears the equation but not a) or else repeat subst will infinite loop (if it clears neither the equation nor a)? If subst a succeeds, what happens when I unfold b? I think the proper fix for the bug is to make subst not consider section variable occuring indirectly, not to make subst a succeed when a occurs indirectly.

[herbelin]

I think the proper fix for the bug is to make subst not consider section variable occuring indirectly, not to make subst a succeed when a occurs indirectly.

Your arguments make sense. I will rethink about the PR.

[herbelin]

I consider this PR pending on the question of what subst a should do when a is a section variable with dependencies via a global declaration in the goal:

Section A.                                                  
Variable a:nat.       
Definition b := a.
Goal a=1 -> b=1. 
intros. 
subst a.

Should it fail with something like "This section variable occurs indirectly in the goal and cannot be substituted further." or "This section variable has an implicit occurrence in foo which could not be substituted" or "Cannot substitute a section variable with implicit occurrences"? Same question with a rewritable occurrence of a in the goal (e.g. if it had been a=1 -> a+a=2 -> b=1).

See discussion at #12139.

[herbelin]

@ppedrot: several tactics have to decide at some time whether a variable is a section variable or not. This is the case also of this PR. However, we have no way at the current time to assert for sure that a goal variable is the exact original instance of a section variable or an homonym with same type.

One way to fix this (actually critical) issue would be to add to evar_info an Id.Set.t field which tells which ids of the named context are a copy of a genuine section variable. Would it be ok for you? Or would you have another propositions in mind?

[herbelin]

For the record, here is an example of the section variable homonymy problem:

Section A.
Variable a:nat.
Definition b:=a.
Goal a = a.
revert a; intro a.
change a with b. (* should not succeed *)
Fail clear a. (* should not be forbidden *)

[ppedrot]

One way to fix this (actually critical) issue would be to add to evar_info an Id.Set.t field which tells which ids of the named context are a copy of a genuine section variable. Would it be ok for you? Or would you have another propositions in mind?

Without a clear specification of what it means to be a section variable, I think this is doomed. What if you revert and intro a section variable? What if you perform a change that leaves the type untouched? My take is that this is only going to introduce new issues because the underlying problem of what sections are is still there.

[ppedrot]

Forgot to add that I think that the proper fix is to separate the two representations in the constr syntax. We should have one node for section variables, and one node for goal variables. It's not going to be pretty in terms of backwards compatibility though.

[herbelin]

Without a clear specification of what it means to be a section variable, I think this is doomed.

Ah sorry, I thought it was clear what is the specification I'm referring to. It is the following:

• Locally, from the point of view of a goal, a section variable is like a constant (it is not done, but we could typically give it a name of the form Top.SectionName.name if ever we had to refer to it... but we generally arrange so that we don't need to refer to it)
• A goal lives in a context of the form Global-env ; Section marker; Section-Env; Begin-of-proof-marker; Extra-variables-introed-since-the-beginning-of-the-proof
• A goal comes with an information of what subset of variables from the context are visible: this is what is above the ===== line
• At the beginning of a proof only the section variables are visible; each intro adds new variables to the typing context which are by default visible.
• These variables can be hidden by using clear (the precondition is that no dependency is broken)
• Any newly introduced variable can take any name which is not already used in the set of visible names; in particular, it can reuse any name of the current spine of binders if this name has been cleared.

What if you revert and intro a section variable?

This is a different variable, i.e. a different binder (but possibly with the same name, in which case this will typically exhibits an alpha-conversion at Show Proof time).

What if you perform a change that leaves the type untouched?

I don't understand the question.

My take is that this is only going to introduce new issues because the underlying problem of what sections are is still there.

There is no underlying problem with sections. Think at section variables like global objects with a qualified name + a discharge (= distributivity + strengthening) operation over contexts and the question of what sections are is clear.

The missing information I was talking about in my previous comment is: when I have a name foo in my list of visible names and a global constant bar depending on a section name foo, is the foo of the list of visible names a reference to this very section name or to a unrelated goal-introduced eponynous name foo.

[herbelin]

Forgot to add that I think that the proper fix is to separate the two representations in the constr syntax. We should have one node for section variables, and one node for goal variables. It's not going to be pretty in terms of backwards compatibility though.

Yes, this would be much cleaner. My proposal is exactly to do that but without changing the internal representation, i.e. by keeping an indication in the typing context telling if a Var node in this context has to be interpreted as a section variable or as an intro-ed goal variable.

[herbelin]

@Zimmi48 : I'm a bit lost. Unreleased.rst fails with a :tacn:`subst @ident` but there is a .. tacn:: subst @ident in tactics.rst. There is apparently something which I still don't understand well. Similarly, what is the correct way to write :tacn:rewrite in *`?

[Zimmi48]

@herbelin :tacn: creates links for the name of the tactic only (it takes the prefix before the first @). So in this case it should be :tacn:`subst`. If you want not just to link to the tactic but write it with argument, you can use :n:`subst @ident`, which will not link to the definition of the tactic, or :tacn:`subst` :n:`@ident` which will.

Concerns taken into account

[herbelin]

@ppedrot: This seems to have reached a consensus among the persons having taken part to the discussion, as well as a green CI. Only the (backward-compatible) MetaCoq overlay has not been merged yet (MetaCoq/metacoq#415).

[ppedrot]

@herbelin how come the CI passed if the fix has not been merged yet?

[herbelin]

how come the CI passed if the fix has not been merged yet?

The PR also includes the overlay.

[ppedrot]

@herbelin I think you should then remove the overlay from the PR. I'll try to get my private informants to merge the MetaCoq PR meanwhile.

[herbelin]

OK, done.

[ppedrot]

@herbelin people are complaining that the MetaCoq PR is breaking their CI, can you investigate?

[herbelin]

Can you get more information about what fails with what? It works for me with MetaCoq/metacoq#415 (17a84730) on Coq master (e4bfbdf).

[JasonGross]

The CI fails with

File "./theories/PCUICPrincipality.v", line 313, characters 35-47:
Error: Not an inductive goal with 1 constructor.

On Coq 8.11. You can see the build log by clicking on the red x next to the commit, https://travis-ci.org/github/MetaCoq/metacoq/jobs/683270751
But it looks like it's also failing the CI here, with the overlay.

[herbelin]

The CI fails with

File "./theories/PCUICPrincipality.v", line 313, characters 35-47:
Error: Not an inductive goal with 1 constructor.

On Coq 8.11. You can see the build log by clicking on the red x next to the commit, https://travis-ci.org/github/MetaCoq/metacoq/jobs/683270751
But it looks like it's also failing the CI here, with the overlay.

OK, I think I got the explanation. MetaCoq is not testing the MetaCoq PR against the master branch of MetaCoq but against the branch of MetaCoq called coq-8.11. This is because when I submitted the MetaCoq PR, the base was coq-8.11 and I did not pay attention that it was wrong. I changed it to master only afterwards, but the CI apparently did not take it into account (or maybe should it be restarted maually).

The MetaCoq PR is ok on top of MetaCoq master with both Coq master and with this Coq PR (as tested by me locally and by Coq CI).

[Zimmi48]

@ppedrot The overlay has been merged now. This PR seems ready to merge.

[ppedrot]

Right, sorry, forgot to merge it.