Destruct/induction treat section variables uniformly, fixes #2901

[herbelin]

Kind: bug fix / enhancement

Edit: points 2 below moved to #6833 and points 3 and 4 to #6866. However the PR continues to include #6833 and #6866. Title changed to reflect that this is now for discussion about "destruct/induction treating section variables normally".

This PR implements 2 uniformization of the behavior of destruct and induction in unusual cases + 2 improvement about error/warning messages:

1. Removing the special non-clearing of section variables in destruct/induction (see [destruct H] in a section can fail to clear [H] #2901)
2. Using dependent elimination scheme in case of a dependent proposition when using induction
3. Improving error message when asking to clear a section hypothesis implicitly dependent in a definition of the section
4. Warning when destruct/induction cannot remove a section hypothesis because it is dependent in a definition of the section

Both 1. and 2. introduce incompatibilities.

1. The clearing can be unset by calling Unset Section Variables Clearing Compat
2. The use of dependent induction can be unset by calling Unset Dependent Propositions Induction

An example of application of 2. is (Edit: see the corresponding subset of the current PR at PR #6833):

Goal forall H : True/\False, H = H.
induction H. (* now works *)

An indirect consequence of 2. is that intuition succeeds more often since it now destructs dependent proposition. I guess we should prevent this impact on intuition (see #6558 and the possibility to use the assert_succeds (clear id) trick mentioned there).

An example of 3. is the change of error message in the following case (Edit: see the corresponding subset of the current PR at PR #6866):

Section A. Variable a:nat. Definition b:=a=a.
Goal b=b. clear a.
(* before: a is used in conclusion *)
(* after: a is used implicitly in b in conclusion *)

An example of 4. is the warning in the following case (Edit: see the corresponding subset of the current PR at PR #6866):

Section A. Variable a:nat. Definition b:=a=a.
Goal b=b. destruct a.
(* Cannot remove a, it is used implicitly in b *)

Fixes #7518.

• Corresponding documentation was added / updated.
• Entry added in CHANGES.

[gares]

Removing the special non-clearing of section variables in destruct/induction

The fact that clearing Section variables breaks many things is well known. Am I right that this patch does clear section variable more often?

[herbelin]

Am I right that this patch does clear section variable more often?

Yes.

[Zimmi48]

The more systematic clearing breaks lots of stuff! Most of the failing jobs are because of an hypothesis not found anymore. Some errors are a bit different, for instance compcert fails with:

Error: symbols_preserved depends on the variable TRANSL which is not declared
in the context.

Could it be a section variable bug?

One thing that would be interesting to check is whether relying on this PR could make the scripts better / simpler or not. I'm afraid that it risks making the scripts more complex instead. I personally was never a fan of the behavior of destruct which removes the hypothesis it is called on. So I'm reluctant to extend this behavior, even if it makes the tactic more uniform.

[herbelin]

I personally was never a fan of the behavior of destruct which removes the hypothesis it is called on.

Why don't you like it?

The more systematic clearing breaks lots of stuff!

I shall report on a more precise analysis of the failures later on.

[maximedenes]

I've always thought clearing sections variables was a bad idea™. So I don't understand why it would be good to do it more often. I guess seeing use cases would help understanding why it is important. #2901 doesn't seem convincing to me, because the fix I would have in mind there would be to always refuse to clear or rename section variables.

[herbelin]

Sorry, I don't understand neither why you say that it is a bad idea to clear sections variables in general nor how it would solve #2901 which precisely asks that destruct behaves with section variables as it does for non-section variables. Or are you saying that you think that this is a bad idea that destruct clears non-section variables?

Please explain, because I don't understand what you have in mind. Maybe can you give concrete examples?

[Zimmi48]

Why don't you like it?

I think I already mentioned this but it can be very confusing to beginners to lose information without really intending to nor realizing it. Moreover the current situation is inconsistent: compare for instance the situation with destruct and apply in. We already have the clear tactic; we could also automatically clear an hypothesis when its name is reused in the as clause.

E.g. in these two cases:

Parameters A B : Prop.
Goal (A \/ B) -> False.
intros H.
destruct H as [H | H].
Abort.

Goal (A -> B) -> A -> False.
intros H1 H2.
apply H1 in H2 as H2.
Abort.

but not in any of these two cases:

Parameters A B : Prop.
Goal (A \/ B) -> False.
intros H.
destruct H as [H1 | H1].
Abort.

Goal (A -> B) -> A -> False.
intros H1 H2.
apply H1 in H2 as H3.
Abort.

BTW this should work as well (but it doesn't):

Goal (A -> B) -> A -> False.
intros H1 H2.
apply H1 in H2 as H1.

---

FTR here is a real mistake made by many beginners too eager to use destruct on all their hypotheses:

Axiom not_not_elim : forall A, ~~A -> A.

Goal forall A, A \/ ~A.
intro. (* Show A \/ ~ A with no hypothesis *)
apply not_not_elim.
intro H.
apply H.
destruct H. (* Loop back to showing A \/ ~ A with no hypothesis *)

[maximedenes]

Sorry, I don't understand neither why you say that it is a bad idea to clear sections variables in general

Are you saying you recall none of the previous discussions on that topic? If so, I guess we need to collect such information somewhere easy to find and point to.

[herbelin]

Are you saying you recall none of the previous discussions on that topic? If so, I guess we need to collect such information somewhere easy to find and point to.

I know the issues with section variables which occur in the body of definitions. I know the issues with section variables occurring in hints and similar other "objects". But I don't see why this makes clearing a section variable bad. If you clear a section variable, of course, you make unavailable everything that depends on it, but as soon as bindings are properly treated, what problems do you see?

[maximedenes]

Well I see the implementation complexity, but I don't see the use cases. To me it means that the user incorrectly fixed a logical context and later on realizes they want to make it vary. Do you have pointers to actual use cases?

[herbelin]

Do you have pointers to actual use cases?

I believe we do that very commonly.

Section S.
Variables n m p : nat.
(* Some lemmas using n, m, or p or a mix of them *)
End S.

In such situations, the variables n, m and p de facto vary from the moment you need induction on them.

So, if I understand correctly, you'd like that users use sections only for "parametric" contexts, which behave uniformly in the proofs?

[maximedenes]

That's not what I meant. You can write a match on a variable in a context without modifying the context. Doing a case analysis or an induction is the same, so I don't see why it should be prevented. Clearing, however, is really modifying the context. So I don't see why it should be allowed, since the user has fixed the context.

[herbelin]

@Zimmi48: I agree that in a pedagogical context, clearing automatically is somehow not low-level enough, and if Coq had a flag say -beginner, it might not clear by default. On the other side, destruct is an inversible step, so you don't loose information by clearing the variable/hypothesis (even though the case with indices is more delicate as you would need inversion or dependent induction and the reconstruction of the original information can be tedious). So, keeping the information is only making the context more complex, and it mobilizes names which could be otherwise reused.

[herbelin]

@maximedenes: Then, your view is that what you see above the ============================ line in a goal is not a local copy of the section context in the goal but the section context itself?

But, if so, why to copy it above the ============================ line if it is supposed to be fixed?

[maximedenes]

if Coq had a flag say -beginner

Btw, I think a "beginner" profile (as in set of options) would be something interesting to consider. Implicit arguments, for example, could qualify as on by default for regular users but off in the beginner profile. I believe there are many other such options.

[maximedenes]

@maximedenes: Then, your view is that what you see above the ============================ line in a goal is not a local copy of the section context in the goal but the section context itself?

But, if so, why to copy it above the ============================ line if it is supposed to be fixed?

I guess you mean initially, at the beginning of the proof. And this is in fact a very good point. I've often heard complaints from users (not just ssr users FTR) working in very large logical contexts, that they didn't want the context to be repeated in the goals. So have it fixed would also fix this problem, because we could simply remove it (with maybe a way to print it on demand, I haven't thought much about it).

[Zimmi48]

On the other side, destruct is an inversible step, so you don't loose information by clearing the variable/hypothesis

What? No, that is not true. See the example I gave with proving the excluded middle.

[herbelin]

What? No, that is not true. See the example I gave with proving the excluded middle.

Well, you're right. Or, more precisely, destructing an inductive type is reversible but when the hypothesis is not purely inductive and includes a dependent product or an implication, the additional application step (i.e. the negative step, since it is fashionable to think in term of positive and negative types) is not inversible (unless being classical and in the implication case). At the end the resulting destruct tactic is not inversible either.

So, this should indeed be clarified, the reversibility argument applies only to a destruct on a purely inductive type.

[herbelin]

I guess you mean initially, at the beginning of the proof. And this is in fact a very good point. I've often heard complaints from users (not just ssr users FTR) working in very large logical contexts, that they didn't want the context to be repeated in the goals. So have it fixed would also fix this problem, because we could simply remove it (with maybe a way to print it on demand, I haven't thought much about it).

Actually, I tried to do this very long time ago, when I was about your age but I had problems with auto which sees goal variables but does not see section variables. I don't know why I renounced to go further. It would probably not have taken so much time to elaborate a solution so that the section context could be explicitly dissociated from the goal context, while still having auto working as before, but I was not courageous enough, or too cautious in too heavy changes at this time, or too afraid of changing existing habits, but if I had gone further, that would probably have simplified things for the future.

It still can be done now, and my experiment with distinct section contexts and named contexts in the kernel is going into this direction. Typical issues shall continue to be (at least) with auto (how to control which section variables it is supposed to use), with naming (how to tell which section variables name should not be used to name goal variables), ...

[herbelin]

To dissociate discussion and to dissociate the impact of the two different semantic changes on tested packages, I open #6833 for parts 2, 3 and 4 of this PR.

So, the current PR now relies on #6833 and is restricted to only provide part 1 of the initial text.

[herbelin]

Report on the failures:

• VST: destruct jm. simpl in *. clear jm. fails because clear is already done.
• UniMath: A destruct in a section-local Ltac erases a section variables used in a definition of the section. Moving this destruct ic to destruct (ic) makes the whole contribution succeeds.
• CoLoR: failure 1: an induction on section variable l releases the name l so that next name l0 should now be l; failure 2: suspectingly related to intuition and part 2 of the PR. I'm testing separately; I stopped investigating.
• CompCert: a variable is cleared and a definition using it is called: case where asking explicitly to keep the hypothesis is enough (in particular answer to "Could it be a section variable bug?" in this comment is "no it is not a bug").
• fiat-parsers: destruct Henum as [ls Hls]; clear Henum fails because the clear is not needed any more (then a compatibility problem with CAst.t).
• fiat-crypto: to be investigated.
• elpi: seems unrelated (merlin problem??).
• ltac2: change in API.
• geocoq: suspectingly related to intuition, so, to Use dependent induction for elim and induction whenever needed on dependent proof #6833. I did not investigate yet
• math-classes: a section variable c is cleared which needs to be kept for type classes to work properly; then, a section variable is cleared which is used in the body of a needed lemma.

No other failures, so not as bad as I thought: total number of failures is suspectingly < 10, with at least a third of them producing the expected behavior (expected = "do the expected clear" and "do not uselessly rename a variable") and the remaining ones producing equivalent behavior.
Side question: do we know what makes vst so slow to compile?

[ejgallego]

Clear and section variables is a very complicate discussion, I would just like to add a nit: please let's be careful of confusing UI shortcomings [how to properly display large contexts] with real concerns [as to what tactics / automation see].

[JasonGross]

The compatibility flags should be appropriately set in the Compat/Coq88.v file.

[ppedrot]

What is the likelihood of this PR getting merged? It has currently more colourful labels than the archetypical Holywood general in a Vietnam war movie.

[herbelin]

What is the likelihood of this PR getting merged?

I'm not good at probabilities but I can at least rebase it and #6833 and update their status.

[ppedrot]

Given that there was not activity in more than a year, I believe we can safely close this PR. Not necessarily that the changes shouldn't make in into master, but I think that the integration should be more progressive. In particular, given that the handling of section variables is a sensitive matter, we should at the very least agree on a vague mid-to-long-term plan.

[herbelin]

In particular, given that the handling of section variables is a sensitive matter, we should at the very least agree on a vague mid-to-long-term plan.

It seemed there was in #coq/ceps#51 an agreement on "treating section variables as constants". Is this a good basis to elaborate on?

[ppedrot]

I think so.

[herbelin]

But then, there was the question of the compatibility of the current Var-based implementation of tactics, with the possible idea of starting a proof with a sequence of x : T := S.x for each section variable, with deactivation of the printing of the body. Maybe should this be experimented?