# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Tactic for unions, intersections

#### Bjørn Kjos-Hanssen (Oct 24 2020 at 19:17):

Is there a tactic that will solve things like: `(X ∪ Z ∪ Y) \ (X ∩ Z ∩ Y) = (X ∪ Y ∪ Z) \ (X ∩ Y ∩ Z)`

? I wrote a rather long proof of it, which hopefully wasn't necessary...

#### Heather Macbeth (Oct 24 2020 at 19:18):

You could see if `mfld_set_tac`

, written by @Sebastien Gouezel, will work. You might need to import some of the manifolds files to get access to it.

#### Kyle Miller (Oct 24 2020 at 19:22):

Is this what you want?

```
example {α : Type*} (X Y Z : set α) : (X ∪ Z ∪ Y) \ (X ∩ Z ∩ Y) = (X ∪ Y ∪ Z) \ (X ∩ Y ∩ Z) :=
by finish
```

#### Adam Topaz (Oct 24 2020 at 19:22):

It seems that `finish`

can take care of a lot of these small facts about sets.

#### Adam Topaz (Oct 24 2020 at 19:23):

#### Bjørn Kjos-Hanssen (Oct 24 2020 at 19:23):

Awesome, I had not heard of `finish`

#### Kyle Miller (Oct 24 2020 at 19:24):

When that doesn't work, it can be useful to use `ext, simp`

to turn things into a theorem of logic. (And then later use `squeeze_simp`

to remove a non-terminal `simp`

.)

#### Adam Topaz (Oct 24 2020 at 19:24):

In the conversation linked above you will find an example which finish can't solve, but for which `tidy`

works.

#### Heather Macbeth (Oct 24 2020 at 19:28):

Actually, `mfld_set_tac`

does exactly this :). Heres the code:

https://github.com/leanprover-community/mathlib/blob/cae77dc794ad18c1bc6ed361b7902aa9b1fb2fda/src/data/equiv/local_equiv.lean#L88

and basically it's `ext, split; simp`

using a simp-set that contains a few extra set lemmas.

#### Kyle Miller (Oct 24 2020 at 19:29):

Another proof:

```
example {α : Type*} (X Y Z : set α) : (X ∪ Z ∪ Y) \ (X ∩ Z ∩ Y) = (X ∪ Y ∪ Z) \ (X ∩ Y ∩ Z) :=
by simp only [set.union_left_comm, set.union_comm, set.inter_left_comm, set.inter_comm]
```

Mario's pointed out that `simp`

puts things into a normal form, and these `left_comm`

lemmas are useful for this purpose.

#### Bjørn Kjos-Hanssen (Oct 24 2020 at 19:31):

On the other hand, if I already have a proof written out, will replacing it by simply `by finish`

make Lean take longer to check the proof?

#### Reid Barton (Oct 24 2020 at 19:32):

Well, that depends on your proof :upside_down: but yes, probably.

#### Heather Macbeth (Oct 24 2020 at 19:34):

I would argue that one should prioritize speed of human comprehension over speed of computer comprehension, and writing `by finish`

for a trivial lemma is the right way to get human comprehension!

#### Kyle Miller (Oct 24 2020 at 19:36):

I wonder if the lemmas in the `simp only`

proof I gave should be added to `mfld_set_tac`

(I've never used this tactic, so I don't know if that's in scope)

#### Kyle Miller (Oct 24 2020 at 19:38):

Also, you might consider the `simp only`

proof because it says "this lemma follows by commutativity of unions and intersections", is only one line, and appears to be orders of magnitude faster than `finish`

. (But like @Heather Macbeth says, writing `by finish`

is a great way to say "the proof is trivial"! :smile:)

#### Bjørn Kjos-Hanssen (Oct 24 2020 at 19:41):

Hmm... I wrote an even longer proof for `(X \ Y) ∪ (Y \ Z) ∪ (Z \ X) = (X ∪ Y ∪ Z) \ (X ∩ Y ∩ Z)`

, for that one `finish`

is not enough...

#### Adam Topaz (Oct 24 2020 at 19:41):

tidy?

#### Kyle Miller (Oct 24 2020 at 19:43):

`ext, simp, tauto!`

works

#### Heather Macbeth (Oct 24 2020 at 19:43):

There doesn't seem to be a `comm_ring`

instance on `boolean_algebra`

. But if there were, would `by ring`

solve this?

#### Adam Topaz (Oct 24 2020 at 19:43):

It should!

#### Heather Macbeth (Oct 24 2020 at 19:43):

Kyle Miller said:

`ext, simp, tauto!`

works

nonterminal simp! :(

#### Kyle Miller (Oct 24 2020 at 19:44):

It's left as an exercise to the reader to `squeeze_simp`

:smile:

#### Heather Macbeth (Oct 24 2020 at 19:45):

I am introducing an alternate meaning of the emoji :pray: to refer to squeezing :)

#### Bjørn Kjos-Hanssen (Oct 24 2020 at 19:46):

I guess it's too much to ask for a tactic proof of `|X\Y| + |Y\Z| + |Z\X| = |X\Z| + |Z\Y| + |Y\X|`

? (where `|X|`

is a `local notation`

for `X.card`

) :pray: I wrote a very long proof of that...

#### Reid Barton (Oct 24 2020 at 19:47):

There was an oddly similar question discussed here before

#### Reid Barton (Oct 24 2020 at 19:53):

I can't figure out how to search for it but it was to prove that $[a, b) \cup [b, c) \cup [c, a) = [a, c) \cup [b, a) \cup [c, b)$

#### Bjørn Kjos-Hanssen (Oct 24 2020 at 19:55):

Sort of similar... although that one generalizes to n>3, whereas mine doesn't readily.

#### Reid Barton (Oct 24 2020 at 19:56):

Right, because there is a multiplicity problem.

#### Reid Barton (Oct 24 2020 at 19:58):

Wait, isn't yours also true for n>3 (if we use one cyclic order and the reverse cyclic order)?

But it's no longer "equivalent" to the interval version

#### Adam Topaz (Oct 24 2020 at 20:03):

Why isn't there a comm_ring instance on `set X`

?

#### Heather Macbeth (Oct 24 2020 at 20:04):

$\begin{aligned} \sum_{i\in \mathbb{Z}/3}\chi_{X_i}(1-\chi_{X_{i+1}}) &=\sum\chi_{X_i}-\sum\chi_{X_i}\chi_{X_{i+1}}\\ &=\sum\chi_{X_i}-\sum\chi_{X_i}\chi_{X_{i-1}}\\ &=\sum_{i\in \mathbb{Z}/3}\chi_{X_i}(1-\chi_{X_{i-1}}) \end{aligned}$

#### Heather Macbeth (Oct 24 2020 at 20:09):

and maybe the above can be automated after rewriting using docs#set.indicator_finset_sum

#### Bjørn Kjos-Hanssen (Oct 24 2020 at 20:16):

Oh right, @Reid Barton @Heather Macbeth , it just doesn't have the internal version like `(X ∪ Y ∪ Z) \ (X ∩ Y ∩ Z)`

#### Kyle Miller (Oct 24 2020 at 20:31):

A slow proof:

```
import data.finset.basic
import algebra.big_operators.basic
open_locale big_operators
open finset
variables {α : Type*} [decidable_eq α]
def indicate (X : finset α) : α → ℕ := λ x, if x ∈ X then 1 else 0
def count (X Y Z : finset α) : α → ℕ := λ x, indicate (X \ Y) x + indicate (Y \ Z) x + indicate (Z \ X) x
lemma count_eq (X Y Z : finset α) : count X Y Z = count X Z Y :=
begin
ext x,
dsimp [count, indicate],
simp only [mem_sdiff],
by_cases hx : x ∈ X; simp [hx]; by_cases hy : x ∈ Y; simp [hy]; by_cases hz : x ∈ Z; simp [hz],
end
lemma card_rot (X Y Z : finset α) : card (X \ Y) + card (Y \ Z) + card (Z \ X) = card (X \ Z) + card (Z \ Y) + card (Y \ X) :=
begin
have key : ∑ x in X ∪ Y ∪ Z, count X Y Z x = ∑ x in X ∪ Y ∪ Z, count X Z Y x,
{ simp only [count_eq] },
dsimp [count, indicate] at key,
simp only [sum_add_distrib] at key,
simp only [←sum_filter] at key,
simp only [sum_const, nsmul_eq_mul, mul_one, nat.cast_id] at key,
convert key; ext; simp only [mem_union, mem_filter, mem_sdiff, union_assoc]; tauto!,
end
```

#### Kyle Miller (Oct 24 2020 at 20:54):

A more satisfying proof:

```
import data.finset.basic
open finset
variables {α : Type*} [decidable_eq α]
lemma disj₁ (X Y Z : finset α) : disjoint ((X \ Y) ∪ (Y \ Z)) (Z \ X) :=
by { rw disjoint_iff, ext, simp only [mem_union, mem_sdiff, inf_eq_inter, mem_inter], tauto! }
lemma disj₂ (X Y Z : finset α) : disjoint (X \ Y) (Y \ Z) :=
by { rw disjoint_iff, ext, simp only [mem_sdiff, inf_eq_inter, mem_inter], tauto! }
lemma union_rot_sdiff (X Y Z : finset α) : (X \ Y) ∪ (Y \ Z) ∪ (Z \ X) = (X \ Z) ∪ (Z \ Y) ∪ (Y \ X) :=
by { ext, simp only [mem_union, mem_sdiff, union_assoc], tauto! }
lemma card_rot (X Y Z : finset α) : card (X \ Y) + card (Y \ Z) + card (Z \ X) = card (X \ Z) + card (Z \ Y) + card (Y \ X) :=
begin
have key := congr_arg card (union_rot_sdiff X Y Z),
rwa [card_disjoint_union (disj₁ X Y Z), card_disjoint_union (disj₁ X Z Y),
card_disjoint_union (disj₂ X Y Z), card_disjoint_union (disj₂ X Z Y)] at key,
end
```

#### Bjørn Kjos-Hanssen (Oct 24 2020 at 21:20):

These are great @Kyle Miller ... I guess the second one has fewer exotic imports

Last updated: May 16 2021 at 05:21 UTC