set tactic

Stream: maths

[Kevin Buzzard]

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]

by finish [set.ext_iff]

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

ooh Chris has just done it :-)

[Kevin Buzzard]

except he cheated

[Sebastien Gouezel]

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]

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

[Kevin Buzzard]

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]

Thanks to @Chris Hughes for helping me debug this one

[Kevin Buzzard]

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

[Mario Carneiro]

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]

Yes inter_self_left is exactly what is missing

[Kevin Buzzard]

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]

ext, split ; finish

[Patrick Massot]

No idea why that split seems needed.

[Kevin Buzzard]

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]

by tidy

[Kevin Buzzard]

Chris suggests that this is a bug with finish

[Patrick Massot]

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

[Jesse Michael Han]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Patrick Massot]

Kevin's bare hand are still in tactic mode.

[Jesse Michael Han]

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]

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