Zulip Chat Archive

Stream: PR reviews

Topic: 3083 finset lattice


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 15 2020 at 20:52):

Oh I see Gabriel also likes round notations.

view this post on Zulip Patrick Massot (Jun 15 2020 at 20:54):

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

view this post on Zulip Patrick Massot (Jun 15 2020 at 20:55):

I would very much prefer having integrals that work.

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Jun 15 2020 at 21:25):

I was thinking about definitions, not notation.

view this post on Zulip Yury G. Kudryashov (Jun 15 2020 at 21:27):

The only question about using ant for lattice is what to do with /</ vs //.

view this post on Zulip Yury G. Kudryashov (Jun 15 2020 at 21:28):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 16 2020 at 01:27):

what about \sqcap and \sqcup?

view this post on Zulip Jeremy Avigad (Jun 16 2020 at 01:36):

Yeah, that works for me.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 16 2020 at 03:02):

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

view this post on Zulip 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.

view this post on Zulip 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. (-;

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Jun 16 2020 at 07:19):

Yury G. Kudryashov said:

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

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 16 2020 at 17:28):

Gabriel Ebner said:

Yury G. Kudryashov said:

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

2π=π\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?

view this post on Zulip Gabriel Ebner (Jun 16 2020 at 17:34):

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

view this post on Zulip Johan Commelin (Jun 16 2020 at 17:35):

Gabriel Ebner said:

I'm 60% serious. 2π=π\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...)

view this post on Zulip 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.).

view this post on Zulip Johan Commelin (Jun 16 2020 at 17:36):

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

view this post on Zulip Johan Commelin (Jun 16 2020 at 17:37):

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

view this post on Zulip Johan Commelin (Jun 16 2020 at 17:37):

We definitely don't want 0 \subset 1.

view this post on Zulip Gabriel Ebner (Jun 16 2020 at 17:38):

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

view this post on Zulip Johan Commelin (Jun 16 2020 at 17:42):

I think I prefer to go full lattice notation everywhere.

view this post on Zulip Reid Barton (Jun 16 2020 at 17:52):

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

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Jun 17 2020 at 04:50):

Proof state will always use one notation.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 17 2020 at 05:07):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 26 2020 at 23:30):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 29 2020 at 19:28):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 19:30):

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

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 19:31):

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

view this post on Zulip 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)

view this post on Zulip Sebastien Gouezel (Jun 29 2020 at 19:35):

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

view this post on Zulip Sebastien Gouezel (Jun 29 2020 at 19:36):

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

view this post on Zulip 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??).

view this post on Zulip 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:

view this post on Zulip 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!

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Jun 29 2020 at 19:44):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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)?

view this post on Zulip Sebastien Gouezel (Jun 29 2020 at 19:53):

I was faster :)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Floris van Doorn (Jun 29 2020 at 20:01):

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

view this post on Zulip 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].

view this post on Zulip Sebastien Gouezel (Jun 29 2020 at 20:01):

Exactly.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Sebastien Gouezel (Jun 29 2020 at 20:05):

It is exactly the same statement.

view this post on Zulip 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)

view this post on Zulip Floris van Doorn (Jun 29 2020 at 20:06):

ah ok. that would make it easier.

view this post on Zulip 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.

view this post on Zulip 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 XYX\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.

view this post on Zulip Johan Commelin (Jun 29 2020 at 20:08):

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

view this post on Zulip Alex J. Best (Jun 29 2020 at 20:08):

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

view this post on Zulip 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?

view this post on Zulip Sebastien Gouezel (Jun 29 2020 at 20:18):

I think we should just have one class.

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 20:19):

Then what should @[to_set] do?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Floris van Doorn (Jun 29 2020 at 20:25):

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

view this post on Zulip 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

view this post on Zulip 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].

view this post on Zulip Floris van Doorn (Jun 29 2020 at 20:29):

we don't necessarily care about defeq.

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 20:33):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (Jun 29 2020 at 20:42):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 20:48):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 21:00):

(done locally)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 30 2020 at 06:55):

We still can have good notation in the input.

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Sebastien Gouezel (Jun 30 2020 at 07:09):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 07:23):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 30 2020 at 14:42):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 30 2020 at 16:29):

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

view this post on Zulip 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