Set notation

Stream: general

[Yaël Dillies]

I am getting annoyed at the duplication around set, finset, multiset and ⊆, disjoint, ∪, ∩. What do people think of a has_set_notation class which states that s ⊆ t ↔ s ≤ t, s ∪ t = s ⊔ t, s ∩ t = s ⊓ t, ... Along with Yury's proposed refactor of ⊆, this means we can prove set notation variants of lemmas once and for all.

[Yaël Dillies]

Of course, it shouldn't get abused (so for example I would not want docs#topological_space.opens to have it, because the set notation is not the simp normal form), but I feel like it's a good compromise to keep mathematician notation in the game without driving me insane.

[Yaël Dillies]

We could maybe even extend it to docs#has_insert and docs#set.erase, docs#finset.erase (eh, disparity already :sad:)

[Kevin Buzzard]

I must confess there have been times when I've got annoyed at this notation and the fix I'd come up with involved simply deleting the notation on the basis that lattice notation worked fine :-) The proposed idea is probably much better than this. I don't really understand about opens though -- even if it's not simp normal form you're saying we can't use it?

[Yaël Dillies]

If we forbid has_set_notation for types whose simp normal form is not set notation, we can have s ⊔ t = s ∪ t, s ⊓ t = s ∩ t, etc... be polymorphic simp lemmas.

[Yaël Dillies]

I'm also thinking that such a class would make a to_set attribute moderately easy to write. It would turn all ⊔ into ∪, ⊓, into ∩, ..., add [has_set_notation α] to all types that appeared in such expressions, change the lemma name and the proof à la to_additive.

[Yaël Dillies]

It wouldn't work work for everything, but it certainly would for the entirety of file#order/boolean_algebra, which is somewhat the epitomy of the annoying file whose existence is crucial but underknowledged.

[Yury G. Kudryashov]

Possibly, we need separate classes for different set operations. E.g., finsets have complement only in a finite type and many types have good inf but not sup (e.g., subgroup).

[Yaël Dillies]

Note that ᶜ is not a problem because there's no set-specific notation.