Make box a definition and prove it contractive

This also allows us to get rid of ctx_eq.

However, I have the feeling that some things got significantly slower; CI will tell us. Also, some of the automation does not work any more, as can be seen by my changes in the respective type-checking proofs. @jjourdan could you help me with that? I don't even understand why these things used to work, or what changed about them now...

Unfortunately this exactly confirms what I dislike about these eauto-based proofs... if they fail, it is pretty much impossible to debug what is going on unless you are the person that carefully designed these hint dbs in the first place. For example, it took me more than 30 minutes to even realize that there is a second hint db lrust_typing_merge. Until then I had used Print HintDb lrust_typing, and then focused only on the lemmas that came up there. @jjourdan any chance you could document which pieces are working together how, and which priorities have been carefully tuned? And by "document" I mean "written down in some file in the project root"; not "half a dozen comments spread across the entire development". Right now, solve_typing is to a large extend a mystery to me (at least to the extend that it is broken after I introduced box as a definition).

added 1 commit

• 9b92a3cf - Make box a definition and prove it contractive

Compare with previous version

added 1 commit

• 03fdb63e - Fix [solve__typing] by changing the hint on [tctx_extract_hasty_here_eq] into a …

Compare with previous version

I fixed the problem: it was because of the Hint Extern that you introduced for tctx_extract_hasty_here_eq. This makes Coq use apply's unification and hence ignore the Hint Opaque declarations. Theses declarations are important, because they prevent the types definitions to be unfolded and unified with each others.

Could you explain a bit more why you did this change? At least in this state of the repo, it seems that this change does not change anything.

Some help for debugging what is happening with these kinds of tactics. First, you can use Typeclasses eauto := debug. in order to see what is being tried. It may also be a good idea to look at the definition of the tactic, where it the existence of lrust_typing_merge is clear. I also give there a brief explanation. In the current case, Typeclasses eauto := debug. showed that only a few tactics were tried, and I then deduced that there were a problem with unification.

Independently from this, I have to admit that the way the priorities have been chosen for [tctx_extract_hasty] are not documented enough, and I can add somewhere a summary of all these. I can also give a list of all the goals that can be solved by [solve_typing], and their intuitive meaning. Is this what you expect?

Could you explain a bit more why you did this change? At least in this state of the repo, it seems that this change does not change anything.

A bunch of files failed to compile before I added that -- for example, option.v. I have no idea why they suddenly work again now... Thanks for fixing this, I am going to merge then!

It may also be a good idea to look at the definition of the tactic, where it the existence of lrust_typing_merge is clear.

Fair enough. ;) I think I had seen it a while ago, and back then it was just a single "eauto", and didn't realize it has changed since then.

In the current case, Typeclasses eauto := debug. showed that only a few tactics were tried, and I then deduced that there were a problem with unification.

Well, but then you fixed it by actually using weaker unification, such that fewer things can be applied. I was aware I changed unification behavior by making that Hint a Hint Extern (that was the entire point), but it didn't occur to me that this could have the "opposite" effect.

Independently from this, I have to admit that the way the priorities have been chosen for [tctx_extract_hasty] are not documented enough, and I can add somewhere a summary of all these. I can also give a list of all the goals that can be solved by [solve_typing], and their intuitive meaning. Is this what you expect?

The priorities should be enough; which goals can be solved is fairly clear from where it is used and from looking at the hint dbs.

More generally speaking, I also still don't have a mental model for what exactly making things opaque in the typeclass db does. Originally I thought this was just about the head symbol (where eauto organizes hint dbs by head symbol and if the head symbol is marked opaque, it won't try to unfold it). But clearly, it's having a larger effect than that, and is also used by unification when applying Hint Resolve.

mentioned in commit 5d6f2eda

merged

Well, but then you fixed it by actually using weaker unification, such that fewer things can be applied. I was aware I changed unification behavior by making that Hint a Hint Extern (that was the entire point), but it didn't occur to me that this could have the "opposite" effect.

Right. Except that if you make it too strong, it fails to terminate and it therefore becomes weaker...

More generally speaking, I also still don't have a mental model for what exactly making things opaque in the typeclass db does. Originally I thought this was just about the head symbol (where eauto organizes hint dbs by head symbol and if the head symbol is marked opaque, it won't try to unfold it). But clearly, it's having a larger effect than that, and is also used by unification when applying Hint Resolve.

When you are using eauto, opaque and transparent hints are completely unpredictable. When using typeclasses eauto, my mental model is the following: all the hints are tried one after the other, in the order of priorities. The conclusions of the lemmas are unified with the goal, by following the transparency hints (for everything in the goal, including the head symbol and the others).

Moreover, this is documented nowhere, but a "discriminated" hintdb is one where all the symbols are transparent by default. By default, hintdb are non-discriminated.

One last thing: when several hintdb are given, they are tried one after the other, regardless of the priorities.

Moreover, this is documented nowhere, but a "discriminated" hintdb is one where all the symbols are transparent by default. By default, hintdb are non-discriminated.

Wait, per default not everything is transparent? So where is lrust_typing set to default-transparent then? (I saw in Print HintDb that it says it will unfold "all constants except ...".)

One last thing: when several hintdb are given, they are tried one after the other, regardless of the priorities.

Wtf?!? I sure assumed that it would take the union of the hintdbs, and then merge them. This makes no sense.

Still I am wondering about the actual code of solve_typing:

(typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
  (typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail)

What is the advantage of this over just the second clause? Are there cases where the first one succeeds quickly but the second one takes long to succeed? Because for failure, this will actually make things much worse by doing eauto search twice.

Wait, per default not everything is transparent? So where is lrust_typing set to default-transparent then? (I saw in Print HintDb that it says it will unfold "all constants except ...".)

That's specified by the discriminated keyword here:

Create HintDb lrust_typing discriminated.
Create HintDb lrust_typing_merge discriminated.

Wtf?!? I sure assumed that it would take the union of the hintdbs, and then merge them. This makes no sense.

Yes. I discussed with Matthieu about that, and he agreed that this is a bug. This should be corrected soon (I hope).

Yes. I discussed with Matthieu about that, and he agreed that this is a bug. This should be corrected soon (I hope).

Good :) Is there a bug report for this?

What is the advantage of this over just the second clause? Are there cases where the first one succeeds quickly but the second one takes long to succeed? Because for failure, this will actually make things much worse by doing eauto search twice.

This is explained just above:

The reason is that we want we want the search proof search for [tctx_extract_hasty] to suceed even if the type is an evar, and merging makes it diverge in this case.

Hm, yeah, I should have read that indeed -- though of course this makes me wonder whether the merging hint db couldn't be tweaked not to diverge. After all, Hint Mode and Hint Cut are all per-db. But you know that stuff way better than I do, so whatever^^

though of course this makes me wonder whether the merging hint db couldn't be tweaked not to diverge

I thought a bit about how I could do this, but I found the two-hintdbs solution simpler. If you can think of a simple tweak that would prevent it diverge but still allow merging and inferring the type of a variable when no merging is involved, please go ahead.

That's specified by the discriminated keyword here:

Well, actually, we've just checked: the discriminated keyword seems to have a different (unknown) purpose. What make the hintdb transparent by default is the very fact of creating it. I'll create a bug report about this.

Good :) Is there a bug report for this?

Yes: https://coq.inria.fr/bugs/show_bug.cgi?id=5304