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