# Zulip Chat Archive

## 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