symmetric difference / disjunctive union of sets

Stream: Is there code for X?

[Eric Wieser]

Do we have an operator for this, or am I expected to write it out in terms of intersection / union / difference?

[Adam Topaz]

disjoin union is \sum (on the type level), but that's the best you can do in general.

[Adam Topaz]

The usual notation for symmetric difference is something like $A \Delta B$, I think? I haven't seen that in lean.

[Eric Wieser]

Even a method of set would be fine for me

[Adam Topaz]

variables {α : Type*} (A B : set α)

def symmetric_difference := (A ∪ B) \ (A ∩ B)

notation A `Δ` B := symmetric_difference A B

[Eric Wieser]

Whoops, used the wrong word in the title - it's specifically symmetric difference I'm after

[Adam Topaz]

i don't know how strongly this notation should bind though....

[Eric Wieser]

Would it be appropriate to add set.symm_diff (without notation) to mathlib?

[Gabriel Ebner]

If we add such a notation, it should probably be a type class and also be defined for finset.

[Adam Topaz]

I don't see why not. It's a common enough construction.

[Adam Topaz]

Gabriel Ebner said:

If we add such a notation, it should probably be a type class and also be defined for finset.

Maybe even make it something in an arbitrary lattice?

[Eric Wieser]

Do we have sdiff on arbitrary lattices?

[Bryan Gin-ge Chen]

You can define it in terms of join and meet and complementation per https://en.wikipedia.org/wiki/Boolean_ring#Relation_to_Boolean_algebras

edit: Maybe symmetric difference only really makes sense on boolean algebras?

[Adam Topaz]

We have a docs#has_sdiff class which I've never seen used...

[Adam Topaz]

Oh docs#set.has_sdiff but this is just defined as set.diff!

[Eric Wieser]

You literally just used it!

[Eric Wieser]

But docs#boolean_algebra.to_has_sdiff is the answer to my question

[Adam Topaz]

What is sdiff?

[Adam Topaz]

s doesn't stand for symmetric?

[Eric Wieser]

I think s stands for "set"

[Eric Wieser]

Unicode seems to think that ⊖ is the appropriate symbol for symmetric difference

[Adam Topaz]

We probably don't want to rely on compl because then we won't get it for finsets.

[Gabriel Ebner]

When I search for "symmetric" in the unicode character picker, I get U+2206 ∆ (which is of course different from Δ, or 𝚫, or even 𝞓).

[Adam Topaz]

But if we only use sdiff and sup in the definition, that would be okay for finsets:

import order.lattice

def symmetric_difference {α : Type*} [has_sup α] [has_sdiff α] (A B : α) := (A \ B) ⊔ (B \ A)

notation A `Δ` B := symmetric_difference A B

[Eric Wieser]

My comment was in reference to https://www.fileformat.info/info/unicode/char/2296/index.htm, which has "symmetric difference" in its index entries. Perhaps thats non-normative though.

[Eric Wieser]

2206 looks to be "increment", as in what I would normally read as "delta"

[Mario Carneiro]

heh, I think I would read them all as delta

[Mario Carneiro]

unicode is nuts

[Gabriel Ebner]

2206 also has "symmetric difference (in set theory)" in the comments

[Eric Wieser]

I don't feel strongly about the notation - a global symm_diff function with associated typeclass would be fine by me too

[Johan Commelin]

I certainly think that whatever version of Delta is used, it should be localized notation. It's good to be reminded that the notation is being used.

[Eric Wieser]

Do we want to use sup or union, given that the s in sdiff is set?

[Bryan Gin-ge Chen]

sup would let this work for boolean algebras, right?

[Eric Wieser]

True

[Kevin Buzzard]

This is the addition which, together with multiplication = intersection, gives us the ring structure on set X related to filters I guess.

[Bryan Gin-ge Chen]

It's the addition in boolean rings. Boolean rings and Stone's representation theorem would be nice projects...

[Bhavik Mehta]

Adam Topaz said:

But if we only use sdiff and sup in the definition, that would be okay for finsets:

import order.lattice

def symmetric_difference {α : Type*} [has_sup α] [has_sdiff α] (A B : α) := (A \ B) ⊔ (B \ A)

notation A `Δ` B := symmetric_difference A B

I used this notion as part of the proof in https://github.com/leanprover-community/mathlib/blob/e8c8ce914f4fbf23bfe25b4ae5083bdd8b6642fe/src/combinatorics/colex.lean#L164, and I'm pretty sure for a bunch of other things way back when I did kruskal-katona

[Bryan Gin-ge Chen]

I have some code now proving the equivalence between boolean algebras and boolean rings. The most annoying part, perhaps not surprisingly, was proving that the symmetric difference is associative. I'll try to break this up into PRs this weekend.

[Bryan Gin-ge Chen]

@Eric Wieser Do you have a branch in progress where you're using symmetric_difference? I'm thinking of adding it in a PR soon in the following form:

/-- The symmetric difference of a structure with `⊔` and `\` is `(A \ B) ⊔ (B \ A)`. -/
def symm_diff {α : Type*} [has_sup α] [has_sdiff α] (A B : α) := (A \ B) ⊔ (B \ A)

infix ` Δ `:100 := symm_diff

[Eric Wieser]

No, I don't

[Eric Wieser]

Feel free to add it though

[Eric Wieser]

(I have one line of a translation of some isabelle code that would use it, but that's it)

[Bhavik Mehta]

Eric Wieser said:

Do we have sdiff on arbitrary lattices?

Perhaps we should add a comment somewhere saying that sdiff means set difference, this certainly isn't the first time this confusion has happened

[Bryan Gin-ge Chen]

Good idea, I'll do that in one of my forthcoming PRs.

[Bryan Gin-ge Chen]

The PRs building up to the equivalence between Boolean algebras and Boolean rings are:

• #6460: "algebraic" constructors for (semi-)lattices
• #6464: Boolean rings (also has boolean_ring.to_boolean_algebra)
• #6469: symmetric difference operator
• #6476: boolean_algebra.to_boolean_ring

#6476 should probably have an equiv but I wasn't able to figure out how to prove equality between structures / classes. I'll start another thread about it.

[Yaël Dillies]

Bryan Gin-ge Chen said:

It's the addition in boolean rings. Boolean rings and Stone's representation theorem would be nice projects...

Guess who is reading this a year later :grinning:

[Yaël Dillies]

Kevin Buzzard said:

This is the addition which, together with multiplication = intersection, gives us the ring structure on set X related to filters I guess.

This is yet different from docs#set.set_semiring, right?