Topic: Set notation in lattices
Rémy Degenne (Jun 05 2021 at 14:26):
I created a to_set_notation tactic (by modifying to_additive) and I am thinking that it may be something that we want in mathlib. The motivation is the following: let's say that we have a subtype of
set α, for example the recently created subtype of measurable sets. We can then prove that it is a boolean algebra. But then what we get is a lot of lemmas about inf, sup, Sup, bot, etc. Since intuitively the elements of the type are sets, we would like to have instead lemmas about inter, union, Union, empty, etc. In particular, we cannot even write the Union of such elements: it's not defined.
We could do the same as with mul/add, and have a tactic that translates all the lemmas about one notation to the other. We would prove that the measurable sets are a
set_boolean_algebra instead of a
boolean_algebra and have set notation available instead of lattice notation. Writing the tactic was incredibly easy, due to the fact that the to_additive tactic is superbly general: I just had to change the dictionary used to translate names. There is some work needed to add a
[to_set_notation] tag to all lemmas in the order folder, but that's it. I've done it up to boolean algebra to see if it worked well, and the only minor issue is that I need to find new names for the set versions of compl and sdiff (which already means set difference...).
Of course, an alternative solution is to drop set notation and use only inf and sup. I'd love to hear you thoughts on that!
Eric Wieser (Jun 05 2021 at 14:59):
Note that the original motivation for the instances on
subtype measurable_set (docs#measurable_set.subtype.boolean_algebra) came from absorbing bits of formal-ml, and there instead of using set notation, "prop" notation (
¬) is used, which seems to match how boolean algebras are usually written. In that repo this is a bit of a hack because those notations are not typeclasses but directly associated with
not, but if the motivation was there I think that could be adjusted.
I think in general either lean or mathlib needs a better approach to "these things are all the same but mathematicians like using different symbols for them"
Rémy Degenne (Jun 05 2021 at 15:06):
Yes, I saw that formal-ml uses prop notation; I prefer my events with set notation though :) . But personal preferences aside, I agree that it is not a very elegant solution. I was thinking that it was an easy way to do it and that it could be useful in that case if using set notation, and also for example to avoid stating all set lemmas again for finset
Rémy Degenne (Jun 05 2021 at 15:32):
The finset.basic file contains many lemmas that are consequences of a lattice structure, but are restated to use set notation.
Eric Wieser (Jun 05 2021 at 15:41):
I wonder if we can make
union reducible to the point that there is no need for both version of the lemma, and whether that's desirable - it would mean that after a
unions would turn into
Rémy Degenne (Jun 05 2021 at 15:41):
And now that I think of it, the file
order.boolean_algebra and then basically states again every lemma in the order files to adapt them to set notation.
Bryan Gin-ge Chen (Jun 05 2021 at 16:07):
I think something like this is worth trying in a PR. There have been a few long threads about set vs lattice notation here before, e.g. this one from last year, but I guess we never agreed on a course of action.
Rémy Degenne (Jun 05 2021 at 18:06):
Ok, I'll make it into a PR. Right now the tactic is a copy-and-paste of to_additive, so there is some work needed before it's PR worthy. And given how much of mathlib is affected by the files I will modify, I expect a lot of errors.
Scott Morrison (Jun 06 2021 at 01:18):
I think we should just abandon set notation entirely. It's not like being able to type
\subseteq instead of
\le is making life easier for anyone, and as far as I can tell the slight notation familiarity is the only advantage. It would be a pretty boring life if we could only talk about bare sets, and the separate notation classes are just useless burden for doing anything more interesting.
Yaël Dillies (Jun 06 2021 at 06:40):
There will just be some coercions to make more explicit, typically for subgroups which are then both less than G in terms of carriers and in terms of subgroups.
Rémy Degenne (Jun 06 2021 at 08:00):
You can write
\subseteq if you want to save a few keystrokes!
I would be perfectly happy myself with using inf, le and sup for everything, but what I strongly dislike is the current situation in which some things use set notation (sets, finsets), and at the same time have lattice instances, and the lemmas defined using set notation are incompatible with the ones available due to the instance. Also the business with subtypes not retaining the notation used by the type is bothering me.
I would be personally happy with having only one notation, but I am not sure that it is wise. One thing I liked about lean/mathlib when starting to learn it was that it felt not too far from math I could write on paper, and that involves being able to use the same notations. Now that I am used to it I don't care about a change in notation compared to paper math, but it would be one more hurdle for new people.
Overall, my point of view is that since set notation is there but not very convenient, I might as well try to ease its use. And if set notation goes away soon I won't regret spending time on it, since it's actually not a lot of work.
Kevin Buzzard (Jun 06 2021 at 08:01):
Eric Wieser (Jun 06 2021 at 08:14):
What would having that locale open do?
Yakov Pechersky (Jun 06 2021 at 08:15):
Note that there are some cases where
subset does mean something different than
Patrick Massot (Jun 06 2021 at 08:18):
What about using
\union in lattices? Using
\subset everywhere we use
\le would definitely be weird, but
\sup are symbols that I never saw before using Lean.
Patrick Massot (Jun 06 2021 at 08:19):
And it would be easier for beginner to simply get use to the fact that
\le can also mean
\subset than using totally new symbols for super familiar operations of union and intersection.
Eric Wieser (Jun 06 2021 at 08:23):
Eric Wieser (Jun 06 2021 at 08:45):
Is this something we can do better in lean4, by having set notation automatically used instead of lattice notation if a custom deelaborator finds a
has_mem for the type in question?
Eric Wieser (Jun 06 2021 at 08:47):
Currently notation printing is keyed by the head symbol in lean3 so there's no way to have the pretty printer print
@has_inf.inf (set X) _ differently to a general
has_inf.inf, but that feels like the sort of place where this should be handled.
Eric Wieser (Jun 06 2021 at 08:47):
You'd still have the awkwardness where you have to reach for
inf_comm instead of
inter_comm, but with that approach your goal state would always show things in terms of
inter and never
Last updated: Aug 03 2023 at 10:10 UTC