Using `gcongr` to prove `Monotone` on `Set`s

Stream: mathlib4

[Yury G. Kudryashov]

If I apply a theorem that assumes Monotone (s : _ → Set _), then after intro i j hle, the goals is s i ≤ s j, not s i ⊆ s j, so gcongr fails. @Heather Macbeth Is there an easy way to tell gcongr to auto simplify s i ≤ s j to s i⊆ s j?

[Heather Macbeth]

@Yury G. Kudryashov Interesting, how many such theorems are there in the library? I wonder whether it is worth phrasing such theorems in terms of a variant of Monotone which takes two named relations rather than looking for an order instance on the type? (rather than adjusting gcongr)

[Yury G. Kudryashov]

It's a common assumption in measure theory.

[Yury G. Kudryashov]

@loogle @Monotone _ (Set _)

[loogle]

:search: Set.monotone_setOf, Set.monotone_powerset, and 86 more

[Yury G. Kudryashov]

@loogle @Antitone _ (Set _)

[loogle]

:search: Set.antitone_setOf, Antitone.inter, and 52 more

[Yury G. Kudryashov]

@loogle @StrictMono _ (Set _)

[loogle]

:search: Function.Injective.image_strictMono, SetLike.coe_strictMono, and 1 more

[Heather Macbeth]

OK, I scrolled through those. So is docs#MeasureTheory.tendsto_setIntegral_of_monotone a canonical example of the situation you're describing? Measure theory lemma involving a sequence of sets, monotonicity of that sequence appears as a side condition?

[Heather Macbeth]

And you'd like the monotonicity side condition to be knocked off by fun i j hle ↦ by gcongr, but it isn't because gcongr sees s i ≤ s j rather than s i ⊆ s j?

[Heather Macbeth]

One approach could be to offer a configurable reducibility setting in gcongr -- many other tactics do offer such a setting, but currently gcongr hard-codes reducible transparency (because of potential performance issues like #8731).

(Not sure whether semireducible transparency would see through the LE instance on Set -- we should obviously check this first.)

[Yury G. Kudryashov]

gcongr can prove le from lt. Can we reuse this for le and subset?

[Heather Macbeth]

When gcongr proves le from lt, it stays in le-world all through the logic and then switches to lt at the leaf represented by the < hypothesis. In your example you want the relation-switch to happen at the root (the goal), not the leaf.

[Yury G. Kudryashov]

Thanks for the explanation.

[Heather Macbeth]

But it would certainly be nice to handle your use case. Do you think having a transparency configuration would fix it?

[Yury G. Kudryashov]

I'm afraid that this may be too much. If gcongr can see through semireducible definitions, then it will spend more time trying to unify lemmas with the goal.

[Heather Macbeth]

I wouldn't propose doing this in general (because of cases like the example in #8731 where this really affects performance), just that we could have a transparency config which you would set to "semireducible" in your use case.

[Yury G. Kudryashov]

I'll try to run some experiments this weekend.

[Heather Macbeth]

The other approach is just to make a new definition MonotoneFor with specified relations, and adjust the lemmas you mentioned to have MonotoneFor hypotheses ...

[Yury G. Kudryashov]

We have Relator.LiftFun

[Yaël Dillies]

Could we avoid overengineering a solution here? Bhavik and I are now making concrete plans for subset to be notation for le on Set and Finset

[Bhavik Mehta]

I will try to write more about these plans in the next few days, but in the meantime let me add that it would be nice if gcongr could work on Monotone lemmas even in the case where every relation is syntactically ≤. See eg lines 314-323 here: https://github.com/leanprover-community/mathlib4/pull/17694/files#diff-72ab2090c9a127e6bd5b4f0eb304fdb2ab1f475d7a78f0e37de446feb956b127R314. The change that Yaël and I are considering is orthogonal to this (and in fact would benefit from this)

[Heather Macbeth]

@Bhavik Mehta Do you mean that it should be possible to tag directly as gcongr a lemma whose conclusion is Monotone Foo, rather than writing a clone of the lemma with the form (h : x ≤ y) : Foo x ≤ Foo y? Yes, that would be a useful feature!

(This is not very closely related to Yury's use case, though.)

[Bhavik Mehta]

Yes, exactly! I agree it's not directly related to Yury's case, but it'd be useful now, and in conjunction with the change Yaël and I mention above would make Yury's case work automatically too edit: no longer quite so sure about this, I misread