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