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):

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 (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 tidyworks.

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)[b,c)[c,a)=[a,c)[b,a)[c,b)[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):

iZ/3χXi(1χXi+1)=χXiχXiχXi+1=χXiχXiχXi1=iZ/3χXi(1χXi1)\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: Dec 20 2023 at 11:08 UTC