3083 finset lattice

Stream: PR reviews

[Yury G. Kudryashov]

#3083 makes finset use lattice operations instead of "set" operations. What do you think about this? data.finset now compiles but I don't want to waste time on porting the rest of mathlib if this is not going to be merged.

[Bhavik Mehta]

What's the advantage of this? I think it would be slightly more confusing for newbies who want to use finsets but don't want to think about a lattice, and if I remember correctly the lattice operations already work on finsets anyway

[Chris Hughes]

I think it's a good idea. It just means you don't need duplicates of all lemmas on lattice operations and set operations. Occasionally I can't rw with a lattice lemma because I've got set operations or vice versa.

[Patrick Massot]

Does it mean you want to use the obscure lattice notations for set/finset intersection and union?

[Patrick Massot]

If you want to unify everything I would rather drop the lattice notations and use round intersection and union everywhere instead of the lattice square versions

[Patrick Massot]

Oh I see Gabriel also likes round notations.

[Patrick Massot]

Either way it sounds like a drastic change that is not drastically motivated.

[Patrick Massot]

I would very much prefer having integrals that work.

[Kevin Buzzard]

We have the zany lattice notation for ideals and I got used to it in the end. There are advantages of a unified approach. I get annoyed that set.preimage isn't called comap nowadays

[Yury G. Kudryashov]

I was thinking about definitions, not notation.

[Yury G. Kudryashov]

The only question about using ∪ ant ∩ for lattice is what to do with ≤/</⊥ vs ⊆/⊂/∅.

[Yury G. Kudryashov]

I know only one type with different interpretation of ≤ and ⊆: multiset.

[Scott Morrison]

I think having any types with both ≤ and ⊆ is probably a bad idea: just a recipe for confusion. (I remember being dismayed stumbling on this one.) I would propose picking the important one to receive notation (whether it's ≤ and ⊆) and just dealing with being more verbose for the other.

[Jeremy Avigad]

Whenever I have to do anything with lattices I struggle a lot with typing \lub and \glb because I have to mentally reconstruct which is which. It doesn't help that we think of them as union and inter, and the lattice names are sup and inf. Maybe it would help if we could also use \lunion and \linter for "lattice union" and "lattice inter", or something like that.

[Mario Carneiro]

what about \sqcap and \sqcup?

[Jeremy Avigad]

Yeah, that works for me.

[Kevin Buzzard]

I must confess I feel the same as Jeremy about these funny words. I guess I recognise cup as union though

[Jeremy Avigad]

Oh, yeah, and when talking about lattices in ordinary mathematics I use "meet" and "join." We give the dictionary here: https://avigad.github.io/mathematics_in_lean/basics.html#proving-facts-about-algebraic-structures
I put the translations there to help myself sort them out more than anyone else.

[Yury G. Kudryashov]

Changing sup to join and inf to meet should not be too hard.

[Yury G. Kudryashov]

But I don't want to start any of these refactors until we'll agree on the goal.

[Johan Commelin]

I would like to maintain readability as much as possible. But uniformity pays off in the long run. And I think the symbols are similar enough that we can explain to anyone that \sqcup is the symbol for union of "set-like" things. Then we only need to tell them that in names

• subset becomes le
• union becomes meet
• inter becomes join
  and I think all of those are pretty self-explanatory.
  The hardest thing might be empty becomes bot...
  And of course univ was already confusing to begin with, so replacing it with top doesn't change anything. (-;

[Yury G. Kudryashov]

We can use union and inter for meet and join though in some contexts (e.g., supr in reals or ennreals) this looks funny.

[Gabriel Ebner]

Jeremy Avigad said:

I use "meet" and "join."

I mix up meet and join pretty often always, I guess mostly because these words don't exist in German. In German we typically use supremum and infimum, so I prefer the current naming.

[Gabriel Ebner]

Yury G. Kudryashov said:

in some contexts [...] this looks funny.

$\sqrt{2} \cup \pi = \pi$ doesn't look so bad, it reminds me of Dedekind cuts.

[Jeremy Avigad]

I didn't mean to suggest that meet and join are better than sup and inf. It would help if we could reclaim \sup and \inf in VS Code. We already have \supseteq and \infty for the symbols they are assigned to now. It might help to be able to type \sqcap and \sqcup when working with finsets, because \cap and \cup are used in Latex for intersections and unions. But I can probably get used to the fact that intersection is \inf because it is smaller and union is \sup because it is bigger. It's just that \glb and \lub are horrible, because e.g. "greatest" and "lower" go in opposite directions, and I have to stop to think about which one wins.

[Johan Commelin]

Gabriel Ebner said:

Yury G. Kudryashov said:

in some contexts [...] this looks funny.

$\sqrt{2} \cup \pi = \pi$ doesn't look so bad, it reminds me of Dedekind cuts.

I guess this is tongue in cheek? I'm not a fan :wink: I guess that for linear orders we want to simp this away to max a b as soon as possible?

[Gabriel Ebner]

I'm 60% serious. $\sqrt{2} \sqcup \pi = \pi$ doesn't look any better to me. But $1 \in \pi$ would be too much, even for me.

[Johan Commelin]

Gabriel Ebner said:

I'm 60% serious. $\sqrt{2} \sqcup \pi = \pi$ doesn't look any better to me.

But it also doesn't look any worse, right? (At least to me...)

[Gabriel Ebner]

I completely agree. That's why I think ${}\cup{}$ is the best choice if we want to standardize, because it looks right half of the time (with sets, multisets, etc.).

[Johan Commelin]

But on an abstract lattice, it looks "wrongish".

[Johan Commelin]

And the problem remains with \le vs \subset, right?

[Johan Commelin]

We definitely don't want 0 \subset 1.

[Gabriel Ebner]

Yes, ⊆ vs. ≤ is the hard one. How about ∅ ≤ A ∩ B? ducks

[Johan Commelin]

I think I prefer to go full lattice notation everywhere.

[Reid Barton]

$\cup$/$\cap$ look really wrong when they are wrong, for example, filters ordered by reverse inclusion.

[Scott Morrison]

Is it insane to have all the notations mean the same thing (i.e. lattice operations), and let people use different ones in different contexts?

[Yury G. Kudryashov]

Proof state will always use one notation.

[Bryan Gin-ge Chen]

Is this sort of thing why we have to prove everything for both additive groups and multiplicative groups?

[Yury G. Kudryashov]

For multiplicative and additive groups we also have rings. They use both multiplicative and additive structures.

[Yury G. Kudryashov]

One possible solution is to write a to_additive-style attribute and add it to all the lattice lemmas.

[Yury G. Kudryashov]

But then we'll have to decide which notation is better in each case.

[Floris van Doorn]

I wouldn't mind using lattice notation everywhere.
I'm not in favor using set notation for lattices.
The current status quo means we have to redo everything about lattices separately for sets and finsets, which is not great. There have been plenty of cases where I needed a lemma that existed for exactly one of {bUnion, supr} and I needed it for the other one.

[Yury G. Kudryashov]

Even worse, we need to redo lots of stuff separately for sets, finsets, and lattices.

[Yury G. Kudryashov]

Let me revive this thread. What are the reasons against migration of sets, multisets and finsets to lattice?

[Yury G. Kudryashov]

I remember the following:

• $\sqcup$ and $\sqcap$ look worse than $\cup$ and $\cap$;
• it's hard to remember \lub for $\sqcup$.

What else?

[Johan Commelin]

The second point is no longer valid after all the new additions to the translations file.

[Floris van Doorn]

point 2 has been resolved: there are now many ways to input ⊔ and ⨆.
I think a point that is close to point 1: lattice notation is beginner unfriendly.

[Yury G. Kudryashov]

And defining $f'(x)$ using normed spaces and filters is very beginner friendly ;)

[Yury G. Kudryashov]

BTW, when I first saw Lean the fact that ⊂ means $\subsetneq$ was very surprising.

[Floris van Doorn]

There is a difference: with a good enough API you don't need to know about normed spaces & filters to work with the derivative on functions real -> real. The lattice operations on set is the API.
(just to be clear: I'm in favor of using lattice notation for sets over the status quo)

[Sebastien Gouezel]

Can we have local notation : ∪ := ⊔, and use it in the set files?

[Sebastien Gouezel]

Or even have it globally as an input notation in all files?

[Floris van Doorn]

I'm afraid that might make things even more confusing if the lemmas you use are called sup_comm and image_sup (or sup_comm and image_union??).

[Johan Commelin]

image and preimage should clearly be renamed to map and comap... ...
... :confused: :rolling_on_the_floor_laughing:

[Sebastien Gouezel]

Floris van Doorn said:

I'm afraid that might make things even more confusing if the lemmas you use are called sup_comm and image_sup (or sup_comm and image_union??).

Good point!

[Floris van Doorn]

Also, what does s ≤ t mean to a mathematician (if anything)? Is it pointwise inequalities: ∀ x ∈ s, ∀ y ∈ t, x ≤ y? Using lattice notation means that it has to mean subset...

[Johan Commelin]

I guess it could mean pointwise ineqs, but I think that's very rare.

[Alex J. Best]

I don't think the idea that sets form a partial order w.r.t. inclusion is so alien to mathematicians, so I'd say most would guess it means subset.

[Johan Commelin]

It definitely helps that the lattice notation is just a pointy-squary version of the set notation.

[Floris van Doorn]

But it might take some time to get used to names like le_image_sup : f '' (s ⊔ f ⁻¹' t) ≤ f '' s ⊔ t (or le_map_sup). I do feel like we're losing something when moving from the current notation/naming to the lattice versions...

[Sebastien Gouezel]

We would need an attribute like to_additive to create union lemmas from sup lemmas, and a notation union = sup. Then it would be mostly transparent to the user, but with better defeq properties.

[Jeremy Avigad]

How about having something like the to_additive trick, so that we can batch-duplicate lattice theorems with set names and set notation (for types that have that notation defined)?

[Sebastien Gouezel]

I was faster :)

[Alex J. Best]

As a small experiment, I just asked two grad students (in number theory) what X \le Y for X, Y sets means with no hints, one guessed the partial order by inclusion, and one guessed an inequality of cardinals (i.e. exists an injection from X \to Y. It might have been more realistic to pose it as X, Y subsets of Z, what does X\le Y mean.

[Yury G. Kudryashov]

If we try the to_additive trick, then which notation should we use for submonoids etc?

[Sebastien Gouezel]

I would say: don't touch existing files. Both notations should be completely equivalent, so you can even use \le at one line and \subseteq at the next one.

[Floris van Doorn]

I guess lattice operations are fine on submonoids, opens, ...
For submonoids you don't even have ↑(s ⊔ t) = ↑s ∪ ↑t in general

[Floris van Doorn]

@Sebastien Gouezel As an temporary solution? Eventually we will want to name our lemmas in a consistent way (which probably means using _sup_ instead of _union_ everywhere)

[Floris van Doorn]

But if we use ∪ for set, we probably also want it for finset...

[Johan Commelin]

I think that @Sebastien Gouezel is proposing to throw away set/basic.lean and instead tag every lemma in order/lattice.lean with @[to_set].

[Sebastien Gouezel]

Exactly.

[Sebastien Gouezel]

In more specialized domains, we should settle on one of the choices. I'd say use union and subset for sets and finsets (and more generally if there is a coercion to sets satisfying coe (a sup b) = coe a union coe b), and order notation otherwise.

[Floris van Doorn]

is the statement of lemma union_comm the same as sup_comm, or is it specialized to sets?

[Sebastien Gouezel]

It is exactly the same statement.

[Sebastien Gouezel]

(Possibly with a different pretty printer setting so that the sup is shown as a union in the tooltip)

[Floris van Doorn]

ah ok. that would make it easier.

[Floris van Doorn]

yeah, you probably still want different has_union and has_sup classes, and let to_set modify the classes as well, so that the goal/lemmas are printed the way you wrote them.

I guess that could work.

[Kevin Buzzard]

@Alex J. Best I agree: if you don't know X and Y are subsets of Z then $X\subseteq Y$ doesn't make much sense. If they're both subsets of Z then there's at most one canonical injection from X to Y and so now you're more likely to guess the inclusion.

[Johan Commelin]

This is going to be a refactor so big that :head_bandage: :head_bandage: :head_bandage:

[Alex J. Best]

I agree, it was a flawed experiment! But someone still got it right!

[Yury G. Kudryashov]

If we have different has_sup and has_union classes, then how can union_comm and sup_comm be the same?

[Sebastien Gouezel]

I think we should just have one class.

[Yury G. Kudryashov]

Then what should @[to_set] do?

[Yury G. Kudryashov]

And I guess we won't be able to tell pretty-printer to consistently use ∪ for sets and finsets.

[Sebastien Gouezel]

@[to_set] theorem le_sup_right : b ≤ a ⊔ b

should create a theorem subset_union_rightwhich is defeq to le_sup_right, but in which notation union := sup and notation subseteq := \le are activated so that the tooltip shows right.

[Sebastien Gouezel]

Yury G. Kudryashov said:

And I guess we won't be able to tell pretty-printer to consistently use ∪ for sets and finsets.

I agree, but I think this is only a minor annoyance. (And it might be solvable in Lean 4).

[Yury G. Kudryashov]

What do you mean by "notation ... are activated"? AFAIK, Lean doesn't store notation with lemma statements. It uses currently active notation in #print etc.

[Floris van Doorn]

Yury G. Kudryashov said:

If we have different has_sup and has_union classes, then how can union_comm and sup_comm be the same?

with two different classes, they are not syntactically equal.
My idea (to get the pretty printing right) is to have separate has_sup and has_union classes. Given a lattice you have instances to both has_sup and has_union, and the underlying maps are definitionally equal.
Then @[to_set] replaces all sups with unions, in the same way that to_additive does it.

[Floris van Doorn]

The lemmas will be definitionally equal, but not syntactically equal.

[Sebastien Gouezel]

Yury G. Kudryashov said:

What do you mean by "notation ... are activated"? AFAIK, Lean doesn't store notation with lemma statements. It uses currently active notation in #print etc.

ok, too bad

[Yury G. Kudryashov]

If we use different classes, why should we care about defeq? We can make @[to_set] do the same as @[to_additive].

[Floris van Doorn]

we don't necessarily care about defeq.

[Sebastien Gouezel]

I don't remember the start of the thread: wasn't your goal to get union defeq to to \sup to start with?

[Yury G. Kudryashov]

Let's say we consider different options. The goal is to reduce code duplication.

[Yury G. Kudryashov]

Currently we prove quite a few lattice lemmas for (a) sets; (b) finsets; (c) all other lattices.

[Yury G. Kudryashov]

Technically the simplest solution is to start using ≤, $\sqcap$ etc everywhere but this is bad for new users.

[Yury G. Kudryashov]

Other solutions include: (a) use a @[to_additive]-like attribute to transfer lemmas from lattice operations to set operations; (b) allow ∪ as a (local?) alternative syntax for $\sqcup$ and use it for sets and finsets.

[Sebastien Gouezel]

From the discussion, (a) looks like the nicest solution, albeit not the easiest to implement.

[Yury G. Kudryashov]

The main drawback of (a) is that we'll need class names for set versions of everything up to complete_boolean_algebra and, e.g., monotone won't work automatically unless we define has_le as well.

[Yury G. Kudryashov]

I hope that with Lean 4 we'll be able to define a pretty-printer that uses ∪ for some types and $\sqcup$ for all other types.

[Yury G. Kudryashov]

So we have option (c): wait for Lean 4.

[Sebastien Gouezel]

Even with Lean 4, we would need @[to_set] to create lemma names with union and subset instead of sup and le.

[Jeremy Avigad]

Is it a problem that order.complete_lattice depends on properties of sets, through order.bounds? On a quick look, order.bounds only uses finite unions and intersections, subset, empty and univ. So maybe it is o.k.

[Yury G. Kudryashov]

It's easy to reorder imports so that data/set/basic will know the definition of complete_boolean_algebra and lemmas about bounded_lattice.

[Yury G. Kudryashov]

(done locally)

[Yury G. Kudryashov]

Sebastien Gouezel said:

Even with Lean 4, we would need @[to_set] to create lemma names with union and subset instead of sup and le.

It's easier to add aliases with custom names than to modify types.

[Johan Commelin]

Yury G. Kudryashov said:

The main drawback of (a) is that we'll need class names for set versions of everything up to complete_boolean_algebra and, e.g., monotone won't work automatically unless we define has_le as well.

Well, to_set wouldn't have to replay the proofs (like to_additive) does, if we make sure that things are defeq. Then it just has to modify the name and statement, and can prove the resulting lemma by directly calling the lattice version.
So it generates

lemma subset_union_right : the-statement :=
le_sup_right _ _ _

To make this work, we have to give set some low-priority has_le and has_sup instances, but it would save us from duplicating the entire lattice class hierarchy for set-like notation.

[Yury G. Kudryashov]

What's wrong with the approach "make \cup and \sqcup two notations for the same operation and make @[to_set] work as alias + autogen name"? This way we can't have good notation in the proof state but we can be sure that any lemma about lattices work for sets even without a @[to_set] alias.

[Yury G. Kudryashov]

We still can have good notation in the input.

[Yury G. Kudryashov]

(and I hope that we'll be able to have a good notation in the proof state in Lean 4)

[Yury G. Kudryashov]

How exactly should the "defeq" based @[to_set] work? Should we add some instances like has_subset.to_has_le and use them when transforming the statement? Will it play nice with diamonds?

[Sebastien Gouezel]

Shouldn't we remove completely has_subset, and use subset as a notation for le?

[Yury G. Kudryashov]

With the "make \cup and \sqcup two notations for the same operation" approach yes, we should. But I'm trying to understand what other options do we have, and can't understand the "defeq" approach @Johan Commelin is talking about.

[Kevin Buzzard]

Sebastien Gouezel said:

Shouldn't we remove completely has_subset, and use subset as a notation for le?

Shouldn't we completely remove has_mul, and use * as a notation for has_add?

[Kevin Buzzard]

I guess there might be some edge cases where a type has two monoid structures

[Yury G. Kudryashov]

@Kevin Buzzard Let's discuss lattices, not monoids. Currently there is only one rarely used type (multiset) with both has_subset and has_le and has_le.le ≠ has_subset.subset.

[Kevin Buzzard]

So rather fewer edge cases than in the */+ case.

[Yury G. Kudryashov]

And I'm not aware of good structures involving has_subset on multiset, so we can just add a custom notation for this.

[Yury G. Kudryashov]

One more type with sensible has_subset different from has_le: list.

[Gabriel Ebner]

IIRC there is more than one reasonable (non-subset) definition of ≤ on lists. And only one of them is well-founded (if the order on the elements is well-founded). Maybe these should be different relations (i.e., not ≤) anyhow.