Set notation in lattices

Stream: general

[Rémy Degenne]

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]

Note that the original motivation for the instances onsubtype 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 and, or, and 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]

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]

The finset.basic file contains many lemmas that are consequences of a lattice structure, but are restated to use set notation.

[Eric Wieser]

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 rw sup_comm, unions would turn into sups

[Rémy Degenne]

And now that I think of it, the file data.set.basic imports order.boolean_algebra and then basically states again every lemma in the order files to adapt them to set notation.

[Bryan Gin-ge Chen]

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]

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]

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]

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]

You can write \ss for \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]

How about open_locale set_notation?

[Eric Wieser]

What would having that locale open do?

[Yakov Pechersky]

Note that there are some cases where subset does mean something different than le, like list.subset

[Patrick Massot]

What about using \inter and \union in lattices? Using \subset everywhere we use \le would definitely be weird, but \inf and \sup are symbols that I never saw before using Lean.

[Patrick Massot]

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]

(deleted)

[Eric Wieser]

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]

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]

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