Zulip Chat Archive

Stream: Is there code for X?

Topic: Tactic for unions, intersections


view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 24 2020 at 19:22):

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

view this post on Zulip 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

view this post on Zulip Bjørn Kjos-Hanssen (Oct 24 2020 at 19:23):

Awesome, I had not heard of finish

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Reid Barton (Oct 24 2020 at 19:32):

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

view this post on Zulip 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!

view this post on Zulip 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)

view this post on Zulip 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:)

view this post on Zulip 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...

view this post on Zulip Adam Topaz (Oct 24 2020 at 19:41):

tidy?

view this post on Zulip Kyle Miller (Oct 24 2020 at 19:43):

ext, simp, tauto! works

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Oct 24 2020 at 19:43):

It should!

view this post on Zulip Heather Macbeth (Oct 24 2020 at 19:43):

Kyle Miller said:

ext, simp, tauto! works

nonterminal simp! :(

view this post on Zulip Kyle Miller (Oct 24 2020 at 19:44):

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

view this post on Zulip Heather Macbeth (Oct 24 2020 at 19:45):

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

view this post on Zulip 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...

view this post on Zulip Reid Barton (Oct 24 2020 at 19:47):

There was an oddly similar question discussed here before

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Reid Barton (Oct 24 2020 at 19:56):

Right, because there is a multiplicity problem.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 24 2020 at 20:03):

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

view this post on Zulip 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}

view this post on Zulip Heather Macbeth (Oct 24 2020 at 20:09):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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