Tactic for unions, intersections

Stream: Is there code for X?

[Bjørn Kjos-Hanssen]

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]

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]

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]

It seems that finish can take care of a lot of these small facts about sets.

[Adam Topaz]

cf. https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Simple.20set.20theory.20nonsense/near/212441928

[Bjørn Kjos-Hanssen]

Awesome, I had not heard of finish

[Kyle Miller]

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]

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

[Heather Macbeth]

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]

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]

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]

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

[Heather Macbeth]

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]

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]

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]

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]

tidy?

[Kyle Miller]

ext, simp, tauto! works

[Heather Macbeth]

There doesn't seem to be a comm_ring instance on boolean_algebra. But if there were, would by ring solve this?

[Adam Topaz]

It should!

[Heather Macbeth]

Kyle Miller said:

ext, simp, tauto! works

nonterminal simp! :(

[Kyle Miller]

It's left as an exercise to the reader to squeeze_simp :smile:

[Heather Macbeth]

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

[Bjørn Kjos-Hanssen]

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]

There was an oddly similar question discussed here before

[Reid Barton]

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]

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

[Reid Barton]

Right, because there is a multiplicity problem.

[Reid Barton]

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]

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

[Heather Macbeth]

$$\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]

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

[Bjørn Kjos-Hanssen]

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

[Kyle Miller]

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]

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]

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