Zulip Chat Archive

Stream: Is there code for X?

Topic: symmetric difference / disjunctive union of sets


view this post on Zulip Eric Wieser (Feb 25 2021 at 17:26):

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

view this post on Zulip Adam Topaz (Feb 25 2021 at 17:27):

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

view this post on Zulip Adam Topaz (Feb 25 2021 at 17:28):

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

view this post on Zulip Eric Wieser (Feb 25 2021 at 17:28):

Even a method of set would be fine for me

view this post on Zulip Adam Topaz (Feb 25 2021 at 17:30):

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

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

notation A `Δ` B := symmetric_difference A B

view this post on Zulip Eric Wieser (Feb 25 2021 at 17:30):

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

view this post on Zulip Adam Topaz (Feb 25 2021 at 17:31):

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

view this post on Zulip Eric Wieser (Feb 25 2021 at 17:32):

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

view this post on Zulip Gabriel Ebner (Feb 25 2021 at 17:32):

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

view this post on Zulip Adam Topaz (Feb 25 2021 at 17:32):

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

view this post on Zulip Adam Topaz (Feb 25 2021 at 17:32):

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?

view this post on Zulip Eric Wieser (Feb 25 2021 at 17:33):

Do we have sdiff on arbitrary lattices?

view this post on Zulip Bryan Gin-ge Chen (Feb 25 2021 at 17:34):

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?

view this post on Zulip Adam Topaz (Feb 25 2021 at 17:34):

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

view this post on Zulip Adam Topaz (Feb 25 2021 at 17:34):

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

view this post on Zulip Eric Wieser (Feb 25 2021 at 17:35):

You literally just used it!

view this post on Zulip Eric Wieser (Feb 25 2021 at 17:35):

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

view this post on Zulip Adam Topaz (Feb 25 2021 at 17:35):

What is sdiff?

view this post on Zulip Adam Topaz (Feb 25 2021 at 17:35):

s doesn't stand for symmetric?

view this post on Zulip Eric Wieser (Feb 25 2021 at 17:36):

I think s stands for "set"

view this post on Zulip Eric Wieser (Feb 25 2021 at 17:38):

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

view this post on Zulip Adam Topaz (Feb 25 2021 at 17:41):

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

view this post on Zulip Gabriel Ebner (Feb 25 2021 at 17:41):

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

view this post on Zulip Adam Topaz (Feb 25 2021 at 17:43):

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

view this post on Zulip Eric Wieser (Feb 25 2021 at 17:54):

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.

view this post on Zulip Eric Wieser (Feb 25 2021 at 17:56):

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

view this post on Zulip Mario Carneiro (Feb 25 2021 at 18:06):

heh, I think I would read them all as delta

view this post on Zulip Mario Carneiro (Feb 25 2021 at 18:06):

unicode is nuts

view this post on Zulip Gabriel Ebner (Feb 25 2021 at 18:08):

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

view this post on Zulip Eric Wieser (Feb 25 2021 at 18:12):

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

view this post on Zulip Johan Commelin (Feb 25 2021 at 18:22):

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.

view this post on Zulip Eric Wieser (Feb 25 2021 at 18:45):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 25 2021 at 18:58):

sup would let this work for boolean algebras, right?

view this post on Zulip Eric Wieser (Feb 25 2021 at 19:00):

True

view this post on Zulip Kevin Buzzard (Feb 25 2021 at 20:57):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 25 2021 at 21:12):

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

view this post on Zulip Bhavik Mehta (Feb 25 2021 at 23:28):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 27 2021 at 02:51):

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.

view this post on Zulip Bryan Gin-ge Chen (Feb 27 2021 at 19:15):

@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

view this post on Zulip Eric Wieser (Feb 27 2021 at 19:49):

No, I don't

view this post on Zulip Eric Wieser (Feb 27 2021 at 19:49):

Feel free to add it though

view this post on Zulip Eric Wieser (Feb 27 2021 at 19:50):

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

view this post on Zulip Bhavik Mehta (Feb 27 2021 at 19:55):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 27 2021 at 19:56):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 28 2021 at 08:22):

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.


Last updated: May 16 2021 at 05:21 UTC