set vs lattice operations

Stream: mathlib4

[Yury G. Kudryashov]

We have ∪, ∩, ∅, univ for sets (and finsets) and ⊔, ⊓, ⊥, ⊤ for general lattices. Can we teach Lean 4 to parse ∪ as ⊔ and show ⊔ as ∪ for certain types?

[Yury G. Kudryashov]

This would remove lots of code duplication.

[Yury G. Kudryashov]

We discussed this in Lean 3 but decided to postpone the decision till after the port.

[Yaël Dillies]

Yes, @Kyle Miller and I discussed it. It's very possible but I haven't had time to finish it.

[Yury G. Kudryashov]

If you do the meta-programming part, then I can take care of deduplication.

[Adam Topaz]

Can we just train mathematicians not to worry about ⊔, ⊓, ⊥, ⊤?

[Yury G. Kudryashov]

Last time we discussed this, the answer was "no".

[Yury G. Kudryashov]

I don't understand why since using Lean for, e.g., submodules needs lattice notation anyway.

[Yaël Dillies]

Okay, I dug up my DMs with Kyle and the branch is branch#kmill_set_use_lattice. Feel free to work on it. Kyle is busy doing other things.

[Yury G. Kudryashov]

Two previous discussions: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Set.20notation.20in.20lattices and https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/3083.20finset.20lattice

[Yury G. Kudryashov]

An important argument from one of these discussions: sometimes we want to have both ⊆ and ≤. Example: docs#Multiset

[Yury G. Kudryashov]

Another example when ⊆ makes more sense than ≤: docs#List

[Yury G. Kudryashov]

So, what should we do with ⊆?

[Yaël Dillies]

I would say don't touch it for now

[Yury G. Kudryashov]

If we don't touch ⊆, then changing ∪ to ⊔ in lemmas like docs#Set.union_subset makes no sense.

[Yaël Dillies]

Sorry, but why?

[Johan Commelin]

@Yury G. Kudryashov we could still do "parse $\cup$ as $\sqcup$, and deduplicate many lemmas", right? Even if we don't do the same thing for $\subseteq$.

[Johan Commelin]

How about this: if a lattice is SetLike then the set-like symbols are notation for the lattice-like symbols. And the pretty printer can use the set-like symbols whenever an instance of SetLike is available.
Exceptional types like Multiset and List can still use the set-like symbols however they want.

[Johan Commelin]

That would mean that all the lattice lemmas would be duplicated to provide set-like versions. But the duplication would be only once, and could probably be automated using an analogue of to_additive.

[Johan Commelin]

And it means that subgroups and submodules can use set-like notation, which is not too bad, I think.

[Johan Commelin]

The downside is maybe that $\bigcup H_i$ would depend on whether you take the supremum as subsets or as subgroups. But the place of the coe arrow should make that clear.

[David Loeffler]

IMHO, I think the issue Johan raises is serious enough that we shouldn't go for this proposal. For the lattice of subgroups of a group, subspaces of a vector space, ideals of a ring, etc it will be really weird and confusing if $\cup$ means something other than the usual mathematical meaning.

[Kevin Buzzard]

What is wrong with the status quo? Mathematicians are not going to be dropping standard notation any time soon and our goal as formalisers should be to be mimicking the notation in the books even if it's crap, because that's what people are used to

[Johan Commelin]

I agree with Kevin. With the caveat that we shouldn't ignore options to genuinely improve upon established mathematics. We're proud of how filters do that. And I can imagine that we can sometimes also come up with better/unifying notation compared to established maths. But we shouldn't create roadbumps if we can't show that their benefits clearly outweight the downsides.