aesop and set inclusions

Stream: general

[Kevin Buzzard]

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]

I thought that @Peter Nelson had written such a tactic in Lean3?

[Kevin Buzzard]

Did it make it into mathlib?

[Jannis Limperg]

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]

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]

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]

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]

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]

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]

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]

It's a tactic, not a theorem.

[Yury G. Kudryashov]

I guess, you'll need more imports.

[Adam Kurkiewicz]

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!