gcongr unfold DFunLike.coe

Stream: mathlib4

[Yaël Dillies]

In #18959, I am hitting a very weird behavior from gcongr. By adding the lemma a ≤ b → Additive.toMul a ≤ Additive.toMul b and alike as gcongr lemmas, gcongr now turns the goal μ s ≤ μ t into inst✝².1 μ s ≤ inst✝².1 μ t.

[Yaël Dillies]

Does anyone know why that might be happening? cc @Heather Macbeth

[Yaël Dillies]

See MeasureTheory.OuterMeasure.Basic for the precise failure

[Floris van Doorn]

Based on your comment in the OuterMeasure file I'll hazard a guess that gcongr only looks at the head of a function application and use that as the key for the lemma. So toMul_mono and all other lemmas you added probably have the same key, namely DFunLike.coe, and one of these lemmas will be tried whenever gcongr sees DFunLike.coe.

[Yaël Dillies]

Hmm, that looks bad. How should I fix this?

[Eric Wieser]

Probably it should be using a DiscrTree instead

[Heather Macbeth]

I notice with_reducible gcongr still works on that measure theory example, even though gcongr doesn't. I wonder whether gcongr's apply step should be at reducible transparency -- and how many of the current library uses it would break if we made that change. I'll investigate at some point.

[Heather Macbeth]

Even so, it seems a bit dangerous to be tagging gcongr lemmas with the key DFunLike.coe -- seems like it could lead to bad performance (since it's an obvious place where there could be multiple lemmas with the same key). I'm not convinced that either of these two lemmas (Additive.toMul_mono and measure_mono) need a gcongr tag in their current form. The to_additive stuff could be handled by hand, and the measure_mono (which invokes the obscure docs#OuterMeasureClass) could be replaced by two lemmas for the two use cases of that class: outer measures and measures.

[Yaël Dillies]

Heather Macbeth said:

it seems a bit dangerous to be tagging gcongr lemmas with the key DFunLike.coe

Heather Macbeth said:

measure_mono (which invokes the obscure docs#OuterMeasureClass) could be replaced by two lemmas for the two use cases of that class: outer measures and measures.

But the two lemmas would still have a DFunLike.coe key, right?

[Heather Macbeth]

OK, running the apply in gcongr at a stricter reducibility

• breaks nothing in mathlib
• infinitesimally speeds up mathlib
• fixes Yael's bug

I propose we merge this! #19262

[Heather Macbeth]

At the same time I think it would be good to investigate how many "gcongr" lemmas in mathlib have the DFunLike.coe key. For a long time I've wished we had a linter or tooling to query what gcongr lemmas are stored with the same key. That would be a good place to start an investigation ... maybe one of our linter experts would be interested in collaborating with me on this?

[Heather Macbeth]

I was not very precise in my comments about measure_mono -- what I think I'm trying to get at is that the pattern of the lemma seems different between Additive.toMul_mono (which I have a vaguely bad feeling about)

@DFunLike.coe
  (Equiv (Additive α) α)
  (Additive α)
  (fun x ↦ α)
  (@Equiv.instFunLike (Additive α) α)
  (@toMul α)

and my proposed variant of measure_mono (which I have a more positive gut feeling about):

@DFunLike.coe
  (@Measure X inst)
  (Set X)
  (fun x ↦ ENNReal)
  (@Measure.instFunLike X inst)
  μ

I don't want to speculate too far in advance of the facts, but if we were to special-case DFunLike.coe as a gcongr key, we might do something like requiring that the gcongr lemma's invocation of DFunLike.coe be with a free variable in the a slot ... and possibly also not have a free variable in the F slot.

[Yaël Dillies]

Thanks Heather! Works great

[Yaël Dillies]

Heather Macbeth said:

we might do something like requiring that the gcongr lemma's invocation of DFunLike.coe be with a free variable in the a slot ...

That means we wouldn't be able to use gcongr on any concrete bundled hom, like docs#Multiset.card and similar. Seems sad