## Stream: maths

### Topic: set tactic

#### Kevin Buzzard (Jan 27 2020 at 22:18):

Is there a tactic which does goals like this:

example (X : Type*) (U₁ U₂ : set X) (h₁ : U₁ ≠ ∅) (h₂ : U₂ ≠ ∅)
(h : -U₁ ∪ -U₂ = univ → -U₁ = univ ∨ -U₂ = univ) : U₁ ∩ U₂ ≠ ∅ :=
begin
intro h1,
have h2 : -U₁ ∪ -U₂ = univ,
rw eq_univ_iff_forall,
intro x,
rw eq_empty_iff_forall_not_mem at h1,
replace h1 := h1 x,
revert h1,
simp, tauto!,
replace h := h h2,
cases h with h3 h4,
apply h₁, exact compl_univ_iff.1 h3,
apply h₂, exact compl_univ_iff.1 h4,
end


? It's just easy stuff from logic.basic but disguised as sets.

#### Chris Hughes (Jan 27 2020 at 22:26):

by finish [set.ext_iff]

#### Kevin Buzzard (Jan 29 2020 at 19:18):

import data.set.basic

example (X : Type*)
(Y U₁ U₂ : set X)
(h : U₁ ∩ U₂ ∩ Y = ∅) :
-U₁ ∩ Y ∪ -U₂ ∩ Y = Y := sorry


finish [set.ext_iff] doesn't do this one :-( Any idea why not?

#### Kevin Buzzard (Jan 30 2020 at 14:34):

import data.set.basic tactic.tauto

example (X : Type*)
(Y U₁ U₂ : set X)
(h : U₁ ∩ U₂ ∩ Y = ∅) :
-U₁ ∩ Y ∪ -U₂ ∩ Y = Y :=
begin
ext x,
rw set.eq_empty_iff_forall_not_mem at h,
replace h := h x,
revert h,
simp [set.mem_union, set.mem_inter_iff]; tauto!,
end


Best I can do so far

#### Joe (Jan 30 2020 at 15:25):

A little better but maybe still too much...

example (X : Type*)
(Y U₁ U₂ : set X)
(h : U₁ ∩ U₂ ∩ Y = ∅) :
-U₁ ∩ Y ∪ -U₂ ∩ Y = Y :=
begin
simp [set.ext_iff] at *,
assume x, replace h := h x,
tauto
end


#### Alex J. Best (Jan 30 2020 at 18:40):

Would be fun to have a way to move these goals into equality in a boolean ring and call ring.

#### Kevin Buzzard (Jan 30 2020 at 18:41):

I'm currently struggling with this:

import topology.basic

namespace topology

open set

/-- A subspace Y of a topological space X is *irreducible* if it is non-empty,
and for every cover by two closed sets C₁ and C₂, one of the Cᵢ has to be Y. -/
def is_irreducible {X : Type*} [topological_space X] (Y : set X) : Prop :=
(∃ x, x ∈ Y) ∧ ∀ C₁ C₂ : set X,
is_closed C₁ → is_closed C₂ → (C₁ ∩ Y) ∪ (C₂ ∩ Y) = Y → C₁ ∩ Y = Y ∨ C₂ ∩ Y = Y

lemma irred_iff_nonempty_open_dense {X : Type*} [topological_space X] (Y : set X):
is_irreducible Y ↔ (∃ x, x ∈ Y) ∧
∀ U₁ U₂ : set X, is_open U₁ → is_open U₂ →
U₁ ∩ Y ≠ ∅ → U₂ ∩ Y ≠ ∅ → U₁ ∩ U₂ ∩ Y ≠ ∅ :=


#### Kevin Buzzard (Jan 30 2020 at 18:42):

for me the proof is completely content-free -- I am surprised I can't just tactic my way to the end.

#### Kevin Buzzard (Jan 30 2020 at 18:42):

ooh Chris has just done it :-)

#### Kevin Buzzard (Jan 30 2020 at 18:42):

except he cheated

#### Sebastien Gouezel (Jan 30 2020 at 20:23):

The current preferred way to express that a set s is nonempty in mathlib is to write s.nonempty (gives you access to a nice API with dot notation).

#### Kevin Buzzard (Jan 30 2020 at 20:40):

We need to get Johannes back to fix up topology.subset_properties :-)

#### Kevin Buzzard (Jan 30 2020 at 21:23):

I have a fabulous challenge :-)

import data.set.basic

open set

-- hint
example (X : Type*) (U₁ U₂ V S : set X) :
U₁ ∩ U₂ ∩ (V ∩ S) = V ∩ U₁ ∩ (V ∩ U₂) ∩ S :=
begin
simp [inter_left_comm, inter_comm, inter_assoc],
end

-- challenge
example (X : Type*) (S V U₁ U₂ : set X) :
U₁ ∩ U₂ ∩ (V ∩ S) = V ∩ U₁ ∩ (V ∩ U₂) ∩ S :=
sorry


#### Kevin Buzzard (Jan 30 2020 at 21:25):

Thanks to @Chris Hughes for helping me debug this one

#### Kevin Buzzard (Jan 30 2020 at 21:25):

I don't know any way of solving the second goal without simply doing it by hand

#### Mario Carneiro (Jan 30 2020 at 21:26):

theorem inter_self_left {α} (U V : set α) : U ∩ (U ∩ V) = U ∩ V :=
by rw [← inter_assoc, inter_self]

-- challenge
example (X : Type*) (S V U₁ U₂ : set X) :
U₁ ∩ U₂ ∩ (V ∩ S) = V ∩ U₁ ∩ (V ∩ U₂) ∩ S :=
by simp [inter_left_comm, inter_comm, inter_assoc, inter_self_left]


#### Kevin Buzzard (Jan 30 2020 at 21:26):

Yes inter_self_left is exactly what is missing

#### Kevin Buzzard (Jan 30 2020 at 21:27):

but I had no idea that the behaviour of simp would depend on the order which the variables were introduced. I was tearing my hair out until Chris pointed this out.

#### Patrick Massot (Jan 30 2020 at 21:27):

ext, split ; finish

#### Patrick Massot (Jan 30 2020 at 21:27):

No idea why that split seems needed.

#### Kevin Buzzard (Jan 30 2020 at 21:28):

In fact the reason I didn't find this one was precisely because it didn't occur to me to use split

#### Jesse Michael Han (Jan 30 2020 at 21:29):

by tidy

#### Kevin Buzzard (Jan 30 2020 at 21:30):

Chris suggests that this is a bug with finish

#### Patrick Massot (Jan 30 2020 at 21:30):

tidy is definitely the best answer so far. Too bad it's so slow.

#### Jesse Michael Han (Jan 30 2020 at 21:31):

don't look at the proof trace it emits :^)

#### Kevin Buzzard (Jan 30 2020 at 21:34):

ha ha it's even longer than my bare hands proof :-)

#### Kevin Buzzard (Jan 30 2020 at 21:35):

I was supposed to be proving results about Noetherian topological spaces this evening and all I've done is spent hours proving logical trivialities :-)

#### Mario Carneiro (Jan 30 2020 at 21:37):

it's always longer than your bare hands proof, that's what tactics do

#### Patrick Massot (Jan 30 2020 at 21:37):

Kevin's bare hand are still in tactic mode.

#### Jesse Michael Han (Jan 30 2020 at 21:52):

finish makes no progress on the problem (you can see where it gets stuck by examining the goal state after safe; in this case it just negates the goal and nothing else triggers)

if you change the intersections to lattice.inf, finish will instead time out (there are too many possible rewrites)

#### Jesse Michael Han (Jan 31 2020 at 00:09):

we frequently had to deal with this kind of reasoning in boolean algebras in flypitch; here's an example of our tools used for two of the problems in this thread

-- requires flypitch
import data.set.basic
import .to_mathlib
import .bv_tauto

namespace tactic
namespace interactive
open lean.parser interactive interactive.types

meta def bblast (hs : parse simp_arg_list) : tactic unit :=
do
simp_flag ← succeeds \$ pure hs,
if simp_flag then
(do s ← mk_simp_set tt [] hs,
simp_all s.1 s.2 { fail_if_unchanged := ff })
else skip,
is_eq <- target >>= λ e, succeeds (expr.is_eq e),
if is_eq then [refine le_antisymm _ _] else skip,
all_goals tidy_context,
done <|> all_goals (try bv_tauto)

end interactive
end tactic

open set

lemma to_infs {X : Type*} {S₁ S₂ : set X} : S₁ ∩ S₂ = S₁ ⊓ S₂ := rfl

example (X : Type*) (S V U₁ U₂ : set X) :
U₁ ∩ U₂ ∩ (V ∩ S) = V ∩ U₁ ∩ (V ∩ U₂) ∩ S :=
by bblast[to_infs]

lemma foo {α : Type*} [lattice.boolean_algebra α]
(Y U₁ U₂ : α)
(h : U₁ ⊓ U₂ ⊓ Y = ⊥) :
(-U₁ ⊓ Y) ⊔ (-U₂ ⊓ Y) = Y :=
begin
bblast, have : Γ ≤ -(U₁ ⊓ U₂ ⊓ Y), by simp*, bv_tauto
end

example (X : Type*)
(Y U₁ U₂ : set X)
(h : U₁ ∩ U₂ ∩ Y = ∅) :
(-U₁ ∩ Y) ∪ (-U₂ ∩ Y) = Y :=
foo _ _ _ h
`

Last updated: May 19 2021 at 02:10 UTC