Zulip Chat Archive

Stream: maths

Topic: set tactic


view this post on Zulip 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.

view this post on Zulip Chris Hughes (Jan 27 2020 at 22:26):

by finish [set.ext_iff]

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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   :=

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 18:42):

ooh Chris has just done it :-)

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 18:42):

except he cheated

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 20:40):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 21:25):

Thanks to @Chris Hughes for helping me debug this one

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 21:26):

Yes inter_self_left is exactly what is missing

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jan 30 2020 at 21:27):

ext, split ; finish

view this post on Zulip Patrick Massot (Jan 30 2020 at 21:27):

No idea why that split seems needed.

view this post on Zulip 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

view this post on Zulip Jesse Michael Han (Jan 30 2020 at 21:29):

by tidy

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 21:30):

Chris suggests that this is a bug with finish

view this post on Zulip Patrick Massot (Jan 30 2020 at 21:30):

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

view this post on Zulip Jesse Michael Han (Jan 30 2020 at 21:31):

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

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 21:34):

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

view this post on Zulip 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 :-)

view this post on Zulip Mario Carneiro (Jan 30 2020 at 21:37):

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

view this post on Zulip Patrick Massot (Jan 30 2020 at 21:37):

Kevin's bare hand are still in tactic mode.

view this post on Zulip 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)

view this post on Zulip 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