Filter.generate

Stream: mathlib4

[Yury G. Kudryashov]

Given docs#Filter.generate_eq_biInf do we really need Filter.generate? Most of the library uses ⨅ i, 𝓟 (s i), not generate (Set.range s). I know that it's used to define the complete lattice instance, but it's easy to rewrite it using the "complete lattice from SetSup" constructor. @Patrick Massot

[Jireh Loreaux]

I think it's nice because it gives it in terms of the inductive docs#Filter.GenerateSets.

[Patrick Massot]

The theory is definitely cleaner without Filter.generate. You can do everything without ever knowing what the elements of an inf look like. The way we get a complete lattice instance here and elsewhere is actually a bit ridiculous. We could use instead that fact that, in an ordered set, if every set has a sup then every set has inf (and vice-versa).

[Jireh Loreaux]

But sometimes don't we want to know what the elements of an inf look like? And in that case, why not prefer Filter.GenerateSets?

[Yury G. Kudryashov]

My main argument is that it's better to have 1 normal form.

[Yury G. Kudryashov]

Otherwise we either (almost) ignore one of the forms or have random parts of API build around different forms.

[Yury G. Kudryashov]

@loogle Filter.generate

[loogle]

:search: Filter.generate, Filter.mkOfClosure, and 25 more

[Yury G. Kudryashov]

As you can see, Filter.generate is mentioned less than 30 times in defs/theorems.

[Yury G. Kudryashov]

For the other outcome see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.28simp.29.20normal.20forms.20for.20expressions.20about.20.60Filter.60s

[Patrick Massot]

Jireh Loreaux said:

But sometimes don't we want to know what the elements of an inf look like? And in that case, why not prefer Filter.GenerateSets?

My claim is that we actually don’t want to know. Sometimes we think we want it, but this is an illusion.

[Eric Wieser]

Patrick Massot said:

Jireh Loreaux said:

But sometimes don't we want to know what the elements of an inf look like? And in that case, why not prefer Filter.GenerateSets?

My claim is that we actually don’t want to know. Sometimes we think we want it, but this is an illusion.

Do we actually just want the induction principle it provides?

[Yury G. Kudryashov]

Please don't start any refactors here until #17552 is merged or rejected (moving many defs to a new file).

[Johan Commelin]

[Yury G. Kudryashov]

Patrick Massot said:

The way we get a complete lattice instance here and elsewhere is actually a bit ridiculous. We could use instead that fact that, in an ordered set, if every set has a sup then every set has inf (and vice-versa).

That's why I PRd this construction (one of two) in !3#2359 4.5 years ago (the other one was added a year later by @Kim Morrison ).

[Yury G. Kudryashov]

@Patrick Massot See #17799 for an experiment. One side effect is that sInf (e.g., atTop or cocompact) is now something Lean can try to unfold while unifying expressions, so I had to add type hints here and there.

[Yury G. Kudryashov]

!bench reports slowdowns here and there and a speedup in a file that failed to compile with the new definitions, then I fixed it.

[Yury G. Kudryashov]

What should I do? Make it irreducible? Something else?

[Patrick Massot]

I would try irreducibility, yes.

[Yury G. Kudryashov]

What's the difference between @[irreducible] def and irreducible_def?

[Matthew Ballard]

My understanding:

• The former is built into core.
• The latter is irreducible to the kernel also.

[Yury G. Kudryashov]

Do we prefer one of them to the other in Mathlib?

[Matthew Ballard]

I would prefer the former unless there is a demonstrated problem with the kernel unfolding it.

[Jireh Loreaux]

Unless I'm mistaken, irreducible_def also provides a rewrite lemma giving you access to the underlying unWrapped definition.

[Yury G. Kudryashov]

I used @[irreducible] def, it works. #17799 is ready for review!

[Michael Rothgang]

0.5% speed-up on overall instruction in mathlib :tada:

[Yury G. Kudryashov]

Should we make more complicated definitions irreducible?

[Yury G. Kudryashov]

E.g., sInf on TopologicalSpace.

[Yury G. Kudryashov]

I'll try this once #17799 is merged.

[Eric Wieser]

Yury G. Kudryashov said:

Patrick Massot said:

The way we get a complete lattice instance here and elsewhere is actually a bit ridiculous. We could use instead that fact that, in an ordered set, if every set has a sup then every set has inf (and vice-versa).

That's why I PRd this construction (one of two) in !3#2359 4.5 years ago (the other one was added a year later by Kim Morrison ).

Perhaps we should make the Inf field of this construction irreducible too? That is, extract it to a def and make it irreducible.

[Yury G. Kudryashov]

We should split this construction into *.ofCompleteSemilatticeSup, with some of them using irreducible defs, so that we can cherry-pick parts of the construction.

[Yury G. Kudryashov]

I won't have time for this for at least a week.