power-up for ext

Stream: mathlib4

[Scott Morrison]

!4#5191 and https://github.com/leanprover/std4/pull/156 provide a power-up to the ext tactic, restoring mathlib3-like capability.

!4#5191 is far from exhaustive in the changes we would then be able to make in mathlib4, but it is indicative of what we'd be able to do. (Maybe it represents fixing 10% of the ext regressions?)

The PR to std4 works by keeping tracking of two discrimination trees. The first behaves just as with the current behaviour of ext. The second uses whnf both when generating the tree and looking up theorems. Then ext preferentially uses any available results from looking up in the first tree, falling back to looking up in the second tree.

(Previously it had been suggested that we just fall back to Lean3's behaviour of having a single giant bucket. This should be much more performant than that.)

I don't think there is any performance concern (on the assumption that we want this behaviour: certainly this results in ext trying more theorems, but the lookup itself should be very fast still), but !bench hasn't done anything 12 hours later so I can't prove this to you. If we'd like, there's an easy performance improvement of not doing the second discrimination tree lookup until we've exhausted all (any?) results from the first one. But I doubt this is actually relevant in practice.

[Mario Carneiro]

I don't really like this change, it is doing full whnf on the term without "asking for permission" first, which has been known to cause problems in the past (the most recent example being this) and it eventually seems to come up no matter where we do it. It is also not very principled to only whnf the head of the term and not everything else; this is basically reverting to the lean 3 behavior of indexing only on the head which causes problems when the head is something uninteresting and the actual dispatch is somewhere in a subterm.

[Mario Carneiro]

Could you give an example of a prototypical problem where this extra strong ext would help?

[Scott Morrison]

Mario, all of the changes in 5191 are undoing regressions caused by this change in the behavior in ext, and there are many many more.

[Scott Morrison]

I'm away from the computer at the moment so won't pick out a concrete example from those, but the two situations that most annoy me in the category theory library are:

[Scott Morrison]

1. Every category instance needs a new ext lemma for the morphisms, as ext won't look through the category.Hom definition.

[Scott Morrison]

2. We have ext lemmas for morphisms out of a categorical limit, or into a colimit. We then make (hundreds?) of definitions of something as a limit or colimit, and with the current design we need to restate these ext lemmas every time.

[Scott Morrison]

Much of the automation in the category theory library is predicated on having effective ext lemmas, so having to write so many boilerplate ext lemmas (or give up on the automation, which has happened too often during the port) is frustrating.

[Scott Morrison]

I'm very happy if there's an alternative change on the ext implementation side, but I'd really like to be able to merge something like !4#5191 on the mathlib4 side.

[Yury G. Kudryashov]

In Lean 3, ext was regularly trying to apply docs#option.ext to docs#ennreal's, thus to docs#measure_theory.measure's unless you stop it with : n or ext1.

[Yury G. Kudryashov]

You don't see this in the diff because we didn't drop those : _ while porting.

[Yury G. Kudryashov]

I mean, you didn't have to fix these because :up:

[Yury G. Kudryashov]

Can we have ext and ext! to work in both cases?

[Scott Morrison]

How about ext- and ext? :-) No, that would be fine.

[Scott Morrison]

aesop_cat would want to use the more powerful one by default, however.

[Scott Morrison]

I guess an alternative would be to keep just one tactic, but have two variants of the attribute, @[ext] and @[ext!], and only in the later case do we put that lemma in "using whnf discrimination tree".

[Scott Morrison]

Surely we can come up with something that is sufficiently principled, but avoids the current situation which is pretty bad...

[Reid Barton]

I'm not sure I quite understand the alternative suggestion

[Reid Barton]

What about marking definitions that ext should be allowed to unfold when trying to find ext-lemma applications? Is that what you meant?
For example, in your situation 1 above, it would be the Category (or Quiver or whatever) instance.

[Scott Morrison]

I was thinking instead that NatTrans.ext would be labelled by @[ext!], as it is by far one of the more common ext lemmas that currently fails to be applied because it is behind a definition. Similarly (co)limit.hom_ext.

Then lemmas labelled with ext! (and only those) would be put into the second discrimination tree, for which indexing and looking is done underneath a whnf.

Essentially, I'm proposing only enabling the new behaviour for a subset of lemmas.

[Scott Morrison]

Something that allows labelling Category seems quite complicated to implement. I'd love to see how that would work concretely. :-)

[Kevin Buzzard]

I certainly agree that something needs to be done. I hit this issue yesterday about an hour before Scott posted and I'd put it on my job list to highlight non-existence of ext!. One thing that one could have is a "Try this!" output of ext!? meaning that the ext! could be replaced by what it found.

[Scott Morrison]

I'm not sure that "Try this" solves the problem --- aesop_cat really needs the aggressive version (or something functionally equivalent, even it takes extra labelling) in many places.

[Reid Barton]

Scott Morrison said:

Something that allows labelling Category seems quite complicated to implement. I'd love to see how that would work concretely. :-)

Hmm, I think it would be much simpler, in principle--just do the reduction to whnf with some custom set of definitions regarded as transparent.
In contrast, I don't understand how you implement "unfold only if it will allow us to apply an ext! lemma".

[Reid Barton]

Oh wait, just to make sure--I meant writing @[ext] instance Category MyType, not annotating the class Category itself.

[Reid Barton]

FWIW I hit exactly your situation 1 recently, and I just assumed that I was meant to write an ext lemma spelled in terms of \hom if I also wanted ext to work for that spelling.

[Scott Morrison]

Wouldn't it need to be something like @[ext_reducible], not the @[ext] attribute itself?

[Scott Morrison]

Reid Barton said:

In contrast, I don't understand how you implement "unfold only if it will allow us to apply an ext! lemma".

Just as with the current implementation: if we don't find a lemma from the main discrimination tree, we do the whnf unfolding and look up in the second discrimination tree (which either has all @[ext] lemmas, as in the current PR, or some subset).

[Reid Barton]

Probably it should be yes, although we already merge two meanings into @[ext]--"this is an ext lemma", "generate an ext lemma".

[Eric Wieser]

Can this be resolved by instead adding ext lemmas that unfold hom into the actual morphism?

[Scott Morrison]

Yes -- the current solution is to add lots of extra ext lemmas.

[Scott Morrison]

That's what we're doing in today's mathlib4, and unhappy about.

[Scott Morrison]

I don't think there's any way to write an ext lemma that does nothing but unfold (as opposed to just applying the ext lemma for the underlying type), and it doesn't seem like this would gain anything much over the present situation. It's still an extra ext lemma that needs to be written for almost every category instance, and every definition that is a limit or colimit.

[Eric Wieser]

"nothing but unfold" would take a hypothesis of the form h : (show A →* B, from f) = (show A →* B, from g) to conclude f = g

[Eric Wieser]

The ugly shows are sort of an indication that either hom should be reducible, or that we need some type-cast functions (or that they already exist and I don't know what they're called!)

[Kevin Buzzard]

I was initially on board with the "let's write all the extra ext lemmas" thing, until I saw what this actually meant on the ground, where I would have had to write really obscure and ugly lemmas to deal with the syntactic abuse that lean 3 ext deals with so well

[Eric Wieser]

I think we should be trying to avoid the syntactic abuse in the first place; we put up with it in lean3 because reducible/semireducible was dealt with pretty randomly by tactics / TC search anyway. Lean 4 appears to be more principled, and teaching tactics to ignore the difference again feels like the wrong direction to go in

[Eric Wieser]

@Kevin Buzzard, the ext lemmas I describe above could be easily generated by a category_ext attribute

[Scott Morrison]

Okay: https://github.com/leanprover-community/mathlib4/pull/5228 goes in the opposite direction of my proposal starting this thread, and instead doubles down on adding repetitions of NatTrans.ext, and then performs the resulting available cleanups.

I certainly think we should do this, regardless of how we eventually either generate or obviate the need for the extra lemmas, so review and merge welcome. :-)

[Eric Wieser]

I think these might be worth a library note, so that they're easy to find again if we come up with a nicer solution later

[Scott Morrison]

Okay, tracking issue created at https://github.com/leanprover-community/mathlib4/issues/5229, and all the new lemmas in !4#5228 link to it. There are probably another 100 in library, but ... later!