## Stream: PR reviews

### Topic: 3083 finset lattice

#### Yury G. Kudryashov (Jun 15 2020 at 20:24):

#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 (Jun 15 2020 at 20:27):

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 (Jun 15 2020 at 20:30):

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 (Jun 15 2020 at 20:51):

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

#### Patrick Massot (Jun 15 2020 at 20:52):

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 (Jun 15 2020 at 20:52):

Oh I see Gabriel also likes round notations.

#### Patrick Massot (Jun 15 2020 at 20:54):

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

#### Patrick Massot (Jun 15 2020 at 20:55):

I would very much prefer having integrals that work.

#### Kevin Buzzard (Jun 15 2020 at 21:07):

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 (Jun 15 2020 at 21:25):

I was thinking about definitions, not notation.

#### Yury G. Kudryashov (Jun 15 2020 at 21:27):

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

#### Yury G. Kudryashov (Jun 15 2020 at 21:28):

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

#### Scott Morrison (Jun 15 2020 at 23:09):

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 (Jun 16 2020 at 01:05):

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 (Jun 16 2020 at 01:27):

what about \sqcap and \sqcup?

#### Jeremy Avigad (Jun 16 2020 at 01:36):

Yeah, that works for me.

#### Kevin Buzzard (Jun 16 2020 at 01:36):

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

#### Jeremy Avigad (Jun 16 2020 at 02:42):

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 (Jun 16 2020 at 03:02):

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

#### Yury G. Kudryashov (Jun 16 2020 at 03:02):

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

#### Johan Commelin (Jun 16 2020 at 06:38):

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 (Jun 16 2020 at 06:40):

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 (Jun 16 2020 at 07:10):

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 (Jun 16 2020 at 07:19):

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 (Jun 16 2020 at 11:34):

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 (Jun 16 2020 at 17:28):

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 (Jun 16 2020 at 17:34):

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 (Jun 16 2020 at 17:35):

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 (Jun 16 2020 at 17:36):

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 (Jun 16 2020 at 17:36):

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

#### Johan Commelin (Jun 16 2020 at 17:37):

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

#### Johan Commelin (Jun 16 2020 at 17:37):

We definitely don't want 0 \subset 1.

#### Gabriel Ebner (Jun 16 2020 at 17:38):

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

#### Johan Commelin (Jun 16 2020 at 17:42):

I think I prefer to go full lattice notation everywhere.

#### Reid Barton (Jun 16 2020 at 17:52):

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

#### Scott Morrison (Jun 17 2020 at 04:47):

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 (Jun 17 2020 at 04:50):

Proof state will always use one notation.

#### Bryan Gin-ge Chen (Jun 17 2020 at 05:03):

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

#### Yury G. Kudryashov (Jun 17 2020 at 05:05):

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

#### Yury G. Kudryashov (Jun 17 2020 at 05:06):

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

#### Yury G. Kudryashov (Jun 17 2020 at 05:07):

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

#### Floris van Doorn (Jun 26 2020 at 22:45):

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 (Jun 26 2020 at 23:30):

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

#### Yury G. Kudryashov (Jun 29 2020 at 19:25):

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

#### Yury G. Kudryashov (Jun 29 2020 at 19:26):

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 (Jun 29 2020 at 19:28):

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

#### Floris van Doorn (Jun 29 2020 at 19:28):

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 (Jun 29 2020 at 19:30):

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

#### Yury G. Kudryashov (Jun 29 2020 at 19:31):

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

#### Floris van Doorn (Jun 29 2020 at 19:31):

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 (Jun 29 2020 at 19:35):

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

#### Sebastien Gouezel (Jun 29 2020 at 19:36):

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

#### Floris van Doorn (Jun 29 2020 at 19:37):

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 (Jun 29 2020 at 19:38):

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

#### Sebastien Gouezel (Jun 29 2020 at 19:39):

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 (Jun 29 2020 at 19:41):

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 (Jun 29 2020 at 19:44):

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

#### Alex J. Best (Jun 29 2020 at 19:44):

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 (Jun 29 2020 at 19:46):

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

#### Floris van Doorn (Jun 29 2020 at 19:50):

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 (Jun 29 2020 at 19:53):

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 (Jun 29 2020 at 19:53):

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)?

I was faster :)

#### Alex J. Best (Jun 29 2020 at 19:53):

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 (Jun 29 2020 at 19:55):

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

#### Sebastien Gouezel (Jun 29 2020 at 19:58):

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 (Jun 29 2020 at 19:58):

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 (Jun 29 2020 at 20:00):

@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 (Jun 29 2020 at 20:01):

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

#### Johan Commelin (Jun 29 2020 at 20:01):

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].

Exactly.

#### Sebastien Gouezel (Jun 29 2020 at 20:03):

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 (Jun 29 2020 at 20:04):

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

#### Sebastien Gouezel (Jun 29 2020 at 20:05):

It is exactly the same statement.

#### Sebastien Gouezel (Jun 29 2020 at 20:05):

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

#### Floris van Doorn (Jun 29 2020 at 20:06):

ah ok. that would make it easier.

#### Floris van Doorn (Jun 29 2020 at 20:06):

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 (Jun 29 2020 at 20:07):

@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 (Jun 29 2020 at 20:08):

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

#### Alex J. Best (Jun 29 2020 at 20:08):

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

#### Yury G. Kudryashov (Jun 29 2020 at 20:17):

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

#### Sebastien Gouezel (Jun 29 2020 at 20:18):

I think we should just have one class.

#### Yury G. Kudryashov (Jun 29 2020 at 20:19):

Then what should @[to_set] do?

#### Yury G. Kudryashov (Jun 29 2020 at 20:19):

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

#### Sebastien Gouezel (Jun 29 2020 at 20:21):

@[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 (Jun 29 2020 at 20:22):

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 (Jun 29 2020 at 20:25):

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 (Jun 29 2020 at 20:25):

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 (Jun 29 2020 at 20:25):

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

#### Sebastien Gouezel (Jun 29 2020 at 20:26):

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 (Jun 29 2020 at 20:27):

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 (Jun 29 2020 at 20:29):

we don't necessarily care about defeq.

#### Sebastien Gouezel (Jun 29 2020 at 20:32):

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 (Jun 29 2020 at 20:33):

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

#### Yury G. Kudryashov (Jun 29 2020 at 20:34):

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

#### Yury G. Kudryashov (Jun 29 2020 at 20:36):

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

#### Yury G. Kudryashov (Jun 29 2020 at 20:41):

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 (Jun 29 2020 at 20:42):

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

#### Yury G. Kudryashov (Jun 29 2020 at 20:44):

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 (Jun 29 2020 at 20:45):

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 (Jun 29 2020 at 20:48):

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

#### Sebastien Gouezel (Jun 29 2020 at 20:50):

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

#### Jeremy Avigad (Jun 29 2020 at 20:51):

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 (Jun 29 2020 at 20:52):

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

(done locally)

#### Yury G. Kudryashov (Jun 29 2020 at 21:01):

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 (Jun 30 2020 at 04:31):

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 (Jun 30 2020 at 06:54):

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 (Jun 30 2020 at 06:55):

We still can have good notation in the input.

#### Yury G. Kudryashov (Jun 30 2020 at 06:55):

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

#### Yury G. Kudryashov (Jun 30 2020 at 07:06):

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 (Jun 30 2020 at 07:09):

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

#### Yury G. Kudryashov (Jun 30 2020 at 07:12):

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 (Jun 30 2020 at 07:22):

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 (Jun 30 2020 at 07:23):

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

#### Yury G. Kudryashov (Jun 30 2020 at 14:36):

@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 (Jun 30 2020 at 14:42):

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

#### Yury G. Kudryashov (Jun 30 2020 at 14:57):

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 (Jun 30 2020 at 16:29):

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

#### Gabriel Ebner (Jun 30 2020 at 16:33):

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.

Last updated: May 09 2021 at 13:20 UTC