Zulip Chat Archive
Stream: general
Topic: aesop and set inclusions
Kevin Buzzard (Sep 27 2024 at 21:59):
For years there's been no tactic which solves inequalities (or even equalities) with sets and unions/intersections etc. But maybe Aesop could be that tool? Here's an example shown to me by @Yagub Aliyev :
import Mathlib.Tactic
variable (U : Type) (A B C: Set U)
example : A ∩ B ⊆ (A ∩ C) ∪ (B ∩ Cᶜ) ∧ ((A ∩ C) ∪
(B ∩ Cᶜ)) ⊆ (A ∪ B) := by
have := fun u ↦ em (u ∈ C) -- is aesop constructive???
aesop
· intro x
aesop
· intro x
aesop
· intro x
aesop
I look at that code and think "it's nearly there"! How does one tweak aesop to get it over the line? The intro
issue is going from A ⊆ B
to \forall x, x \in A -> x \in B
.
Adam Topaz (Sep 27 2024 at 22:02):
I thought that @Peter Nelson had written such a tactic in Lean3?
Kevin Buzzard (Sep 27 2024 at 22:08):
Did it make it into mathlib?
Jannis Limperg (Sep 27 2024 at 22:20):
An Aesop solution:
import Mathlib.Tactic
add_aesop_rules simp Set.subset_def
add_aesop_rules safe apply em
variable (U : Type) (A B C : Set U)
example : A ∩ B ⊆ (A ∩ C) ∪ (B ∩ Cᶜ) ∧ ((A ∩ C) ∪
(B ∩ Cᶜ)) ⊆ (A ∪ B) := by
aesop
The first rule tells Aesop to use Set.subset_def
as a simp
lemma. The second rule tells Aesop to apply em
, which happens to suffice here.
Re constructivism: Aesop doesn't use classical logic by default (except possibly via core tactics), but classical rules can be added as above.
Jannis Limperg (Sep 27 2024 at 22:27):
It's not immediately clear to me what the best strategy to attack set goals would be in general. One possibility would be to just let Aesop unfold all the set definitions (∈
, ∩
, etc.), reducing the problem to pure logic, which Aesop is usually good at.
Heather Macbeth (Sep 27 2024 at 22:37):
It'd be nice to do this for finsets, too, where it's not literal "unfolding" but rather some combination of ext-ing and simp-ing.
Peter Nelson (Sep 27 2024 at 22:50):
By coincidence, @Edward Lee was in my office yesterday, talking about the prospect of dusting off that lean3 code. (He was the programmer at the time - I was just a cheerleader)
Yagub Aliyev (Sep 30 2024 at 04:33):
Jannis Limperg said:
add_aesop_rules simp Set.subset_def add_aesop_rules safe apply em variable (U : Type) (A B C : Set U)
Thank you. This seems to solve even harder problems:
import Mathlib.Tactic
import Mathlib.Data.Set.Defs
add_aesop_rules simp Set.subset_def
add_aesop_rules safe apply em
variable (U : Type) (A B C : Set U)
theorem lfelix2' (A B C: Set U) : ((A ∪ B) ∩ (Aᶜ ∪ C)) ∪ (A ∪ Bᶜ)ᶜ = ((A ∩ B ∩ C) ∪ (A ∩ Bᶜ ∩ C)) ∪ ((Aᶜ ∩ B ∩ C) ∪ (Aᶜ ∩ B ∩ Cᶜ)) := by
aesop
Earlier I solved this problem like this
import Mathlib.Tactic
import Mathlib.Data.Set.Defs
theorem lfelix2' (A B C: Set U) : ((A ∪ B) ∩ (Aᶜ ∪ C)) ∪ (A ∪ Bᶜ)ᶜ = ((A ∩ B ∩ C) ∪ (A ∩ Bᶜ ∩ C)) ∪ ((Aᶜ ∩ B ∩ C) ∪ (Aᶜ ∩ B ∩ Cᶜ)) := by
--first simplify the left side
rw[Set.compl_union] -- (A ∪ B) ∩ (Aᶜ ∪ C) ∪ Aᶜ ∩ Bᶜᶜ
rw[Set.inter_union_distrib_right] -- (A ∪ B ∪ Aᶜ ∩ Bᶜᶜ) ∩ (Aᶜ ∪ C ∪ Aᶜ ∩ Bᶜᶜ)
rw[Set.union_inter_distrib_left] -- (A ∪ B ∪ Aᶜ) ∩ (A ∪ B ∪ Bᶜᶜ) ∩ (Aᶜ ∪ C ∪ Aᶜ ∩ Bᶜᶜ)
rw[Set.union_union_distrib_right] -- (A ∪ Aᶜ ∪ (B ∪ Aᶜ)) ∩ (A ∪ B ∪ Bᶜᶜ) ∩ (Aᶜ ∪ C ∪ Aᶜ ∩ Bᶜᶜ)
rw[Set.union_compl_self] -- (Set.univ ∪ (B ∪ Aᶜ)) ∩ (A ∪ B ∪ Bᶜᶜ) ∩ (Aᶜ ∪ C ∪ Aᶜ ∩ Bᶜᶜ)
rw[Set.univ_union] -- Set.univ ∩ (A ∪ B ∪ Bᶜᶜ) ∩ (Aᶜ ∪ C ∪ Aᶜ ∩ Bᶜᶜ)
rw[Set.univ_inter] -- (A ∪ B ∪ Bᶜᶜ) ∩ (Aᶜ ∪ C ∪ Aᶜ ∩ Bᶜᶜ)
rw[Set.union_assoc] -- (A ∪ (B ∪ Bᶜᶜ)) ∩ (Aᶜ ∪ C ∪ Aᶜ ∩ Bᶜᶜ)
rw[compl_compl] -- (A ∪ (B ∪ B)) ∩ (Aᶜ ∪ C ∪ Aᶜ ∩ B)
rw[Set.union_self] -- (A ∪ B) ∩ (Aᶜ ∪ C ∪ Aᶜ ∩ B)
nth_rw 3 [Set.union_comm] -- (A ∪ B) ∩ (C ∪ Aᶜ ∪ Aᶜ ∩ B)
nth_rw 1 [Set.union_assoc] -- (A ∪ B) ∩ (C ∪ (Aᶜ ∪ Aᶜ ∩ B))
nth_rw 3 [Set.union_eq_compl_compl_inter_compl] -- (A ∪ B) ∩ (C ∪ (Aᶜᶜ ∩ (Aᶜ ∩ B)ᶜ)ᶜ)
nth_rw 2 [Set.inter_comm] -- (A ∪ B) ∩ (C ∪ ((Aᶜ ∩ B)ᶜ ∩ Aᶜᶜ)ᶜ)
nth_rw 2 [Set.compl_inter] -- (A ∪ B) ∩ (C ∪ ((Aᶜᶜ ∪ Bᶜ) ∩ Aᶜᶜ)ᶜ)
rw[Set.union_inter_cancel_left] -- (A ∪ B) ∩ (C ∪ Aᶜᶜᶜ)
rw[compl_compl] -- (A ∪ B) ∩ (C ∪ Aᶜ)
nth_rw 2 [Set.union_comm] -- (A ∪ B) ∩ (Aᶜ ∪ C)
-- For now we are done with the left hand side. now simplify the right hand side
nth_rw 1 [Set.inter_assoc] -- A ∩ (B ∩ C) ∪ A ∩ Bᶜ ∩ C ∪ (Aᶜ ∩ B ∩ C ∪ Aᶜ ∩ B ∩ Cᶜ)
nth_rw 1 [Set.inter_assoc] -- A ∩ (B ∩ C) ∪ A ∩ (Bᶜ ∩ C) ∪ (Aᶜ ∩ B ∩ C ∪ Aᶜ ∩ B ∩ Cᶜ)
nth_rw 1 [Set.inter_assoc] -- A ∩ (B ∩ C) ∪ A ∩ (Bᶜ ∩ C) ∪ (Aᶜ ∩ (B ∩ C) ∪ Aᶜ ∩ B ∩ Cᶜ)
nth_rw 1 [Set.inter_assoc] -- A ∩ (B ∩ C) ∪ A ∩ (Bᶜ ∩ C) ∪ (Aᶜ ∩ (B ∩ C) ∪ Aᶜ ∩ (B ∩ Cᶜ))
rw[← Set.inter_union_distrib_left] -- A ∩ (B ∩ C ∪ Bᶜ ∩ C) ∪ (Aᶜ ∩ (B ∩ C) ∪ Aᶜ ∩ (B ∩ Cᶜ))
rw[← Set.inter_union_distrib_left] -- A ∩ (B ∩ C ∪ Bᶜ ∩ C) ∪ Aᶜ ∩ (B ∩ C ∪ B ∩ Cᶜ)
rw[← Set.union_inter_distrib_right] -- A ∩ ((B ∪ Bᶜ) ∩ C) ∪ Aᶜ ∩ (B ∩ C ∪ B ∩ Cᶜ)
rw[← Set.inter_union_distrib_left] -- A ∩ ((B ∪ Bᶜ) ∩ C) ∪ Aᶜ ∩ (B ∩ (C ∪ Cᶜ))
rw[Set.union_compl_self] -- A ∩ (Set.univ ∩ C) ∪ Aᶜ ∩ (B ∩ (C ∪ Cᶜ))
rw[Set.union_compl_self] -- A ∩ (Set.univ ∩ C) ∪ Aᶜ ∩ (B ∩ Set.univ)
rw[Set.univ_inter] -- A ∩ C ∪ Aᶜ ∩ (B ∩ Set.univ)
rw[Set.inter_univ] -- A ∩ C ∪ Aᶜ ∩ B
-- now we arrived at a simpler equality (A ∪ B) ∩ (Aᶜ ∪ C) = (A ∩ C) ∪ (Aᶜ ∩ B)
-- more work is needed on the left side
nth_rw 1 [Set.inter_eq_compl_compl_union_compl] -- ((A ∪ B)ᶜ ∪ (Aᶜ ∪ C)ᶜ)ᶜ
nth_rw 2 [Set.compl_union] -- (Aᶜ ∩ Bᶜ ∪ (Aᶜ ∪ C)ᶜ)ᶜ
nth_rw 2 [Set.compl_union] -- (Aᶜ ∩ Bᶜ ∪ Aᶜᶜ ∩ Cᶜ)ᶜ
rw[compl_compl] -- (Aᶜ ∩ Bᶜ ∪ A ∩ Cᶜ)ᶜ
rw[Set.union_inter_distrib_left] -- ((Aᶜ ∩ Bᶜ ∪ A) ∩ (Aᶜ ∩ Bᶜ ∪ Cᶜ))ᶜ
rw[Set.inter_union_distrib_right] -- ((Aᶜ ∪ A) ∩ (Bᶜ ∪ A) ∩ (Aᶜ ∩ Bᶜ ∪ Cᶜ))ᶜ
rw[Set.inter_union_distrib_right] -- ((Aᶜ ∪ A) ∩ (Bᶜ ∪ A) ∩ ((Aᶜ ∪ Cᶜ) ∩ (Bᶜ ∪ Cᶜ)))ᶜ
rw[Set.union_comm] -- ((A ∪ Aᶜ) ∩ (Bᶜ ∪ A) ∩ ((Aᶜ ∪ Cᶜ) ∩ (Bᶜ ∪ Cᶜ)))ᶜ
rw[Set.union_compl_self] -- (Set.univ ∩ (Bᶜ ∪ A) ∩ ((Aᶜ ∪ Cᶜ) ∩ (Bᶜ ∪ Cᶜ)))ᶜ
rw[Set.univ_inter] -- ((Bᶜ ∪ A) ∩ ((Aᶜ ∪ Cᶜ) ∩ (Bᶜ ∪ Cᶜ)))ᶜ
rw[Set.compl_inter] -- (Bᶜ ∪ A)ᶜ ∪ ((Aᶜ ∪ Cᶜ) ∩ (Bᶜ ∪ Cᶜ))ᶜ
rw[Set.compl_inter] -- (Bᶜ ∪ A)ᶜ ∪ ((Aᶜ ∪ Cᶜ)ᶜ ∪ (Bᶜ ∪ Cᶜ)ᶜ)
rw[Set.compl_union] -- Bᶜᶜ ∩ Aᶜ ∪ ((Aᶜ ∪ Cᶜ)ᶜ ∪ (Bᶜ ∪ Cᶜ)ᶜ)
rw[Set.compl_union] -- Bᶜᶜ ∩ Aᶜ ∪ (Aᶜᶜ ∩ Cᶜᶜ ∪ (Bᶜ ∪ Cᶜ)ᶜ)
rw[Set.compl_union] -- Bᶜᶜ ∩ Aᶜ ∪ (Aᶜᶜ ∩ Cᶜᶜ ∪ Bᶜᶜ ∩ Cᶜᶜ)
rw[compl_compl] -- B ∩ Aᶜ ∪ (Aᶜᶜ ∩ Cᶜᶜ ∪ B ∩ Cᶜᶜ)
rw[compl_compl] -- B ∩ Aᶜ ∪ (A ∩ Cᶜᶜ ∪ B ∩ Cᶜᶜ)
rw[compl_compl] -- B ∩ Aᶜ ∪ (A ∩ C ∪ B ∩ C)
rw[← Set.union_assoc] -- (B ∩ Aᶜ ∪ A ∩ C) ∪ B ∩ C
-- we are done again with the left side. We need a small lemma to continue
have h : B ∩ C ⊆ B ∩ Aᶜ ∪ A ∩ C
rintro x
have := em (x ∈ A)
aesop
-- lemma proved.
have h1 : (B ∩ Aᶜ ∪ A ∩ C) ∪ (B ∩ C) = B ∩ Aᶜ ∪ A ∩ C -- more specialized 2nd lemma
ext x
constructor -- split the task into 2 parts
intro h0 -- first part
cases' h0 with h1 h2
exact h1
apply h at h2
exact h2
intro h3 -- second part
left
exact h3 -- second lemma is also proved.
rw[h1] -- let us use it on the left side
aesop
Yury G. Kudryashov (Sep 30 2024 at 05:15):
There is a mfld_set_tac
(AFAIR, written by @Sébastien Gouëzel) that solves this type of questions (possibly, not in the most efficient way).
Yagub Aliyev (Sep 30 2024 at 05:29):
Yury G. Kudryashov said:
There is a
mfld_set_tac
(AFAIR, written by Sébastien Gouëzel) that solves this type of questions (possibly, not in the most efficient way).
How do you use it? I couldn't.
import Mathlib.Tactic
import Mathlib.Data.Set.Defs
theorem lfelix2' (A B C: Set U) : ((A ∪ B) ∩ (Aᶜ ∪ C)) ∪ (A ∪ Bᶜ)ᶜ = ((A ∩ B ∩ C) ∪ (A ∩ Bᶜ ∩ C)) ∪ ((Aᶜ ∩ B ∩ C) ∪ (Aᶜ ∩ B ∩ Cᶜ)) := by
apply mfld_set_tac ?
Yury G. Kudryashov (Sep 30 2024 at 05:57):
It's a tactic, not a theorem.
Yury G. Kudryashov (Sep 30 2024 at 05:58):
I guess, you'll need more imports.
Adam Kurkiewicz (Oct 07 2024 at 14:22):
I've wanted to learn writing tactics at some point this year (closer to the end of the year though). If there was a 6-8 week project I could help with I'd be interested, especially if it helps @Kevin Buzzard/ wider community.
I've been using omega
tactic in IMO number theory problems, and it's incredible. It's sometimes surprising what it can solve!
Last updated: May 02 2025 at 03:31 UTC