Zulip Chat Archive

Stream: new members

Topic: semialgebra setminus


view this post on Zulip Iocta (Mar 16 2021 at 20:27):

What's wrong here?

import data.finset.basic

open set

variables {α : Type*}

structure semialgebra (α : Type*) :=
(semialgebra' : set (set α)  Prop)
(semialgebra_empty : semialgebra' )
(semialgebra_inter :  (s : set (set α)) (hs : semialgebra' s) (s1 s2 : set α), s1  s  s2  s  (s1  s2)  s)
(semialgebra_difference :  (s t : set (set α)),  c : finset (set α), (finset.bUnion c) = s \ t)

-- type mismatch at application
--   has_sdiff.sdiff s
-- term
--   s
-- has type
--   set (set α) : Type ?
-- but is expected to have type
--   (set α → finset ?m_1) → finset ?m_1 : Type (max ? ?)

view this post on Zulip Alex J. Best (Mar 16 2021 at 20:45):

I think your definition has too many levels of nested sets, set X is the power set set (set X) is subsets of the power set but set (set X)) \to Prop is another condition on those, so a further power set.

import data.finset.basic

open set


structure semialgebra (α : Type*) :=
(in_semialgebra : set α  Prop)
(semialgebra_empty : in_semialgebra )
(semialgebra_inter :  (s1 s2 : set α), in_semialgebra s1  in_semialgebra s2  in_semialgebra (s1  s2))
(semialgebra_difference :  (s t : set α), in_semialgebra s  in_semialgebra t   c : finset (set α),  s'  c, in_semialgebra s'  (sUnion (c : set (set α))) = s \ t)

looks more like what I read on https://en.wikibooks.org/wiki/Measure_Theory/Basic_Structures_And_Definitions/Semialgebras,_Algebras_and_%CF%83-algebras if that's what youre trying.

view this post on Zulip Alex J. Best (Mar 16 2021 at 20:45):

I had to cast the finset to a set to take the set docs#set.sUnion and also deleted the repeated introduction of alpha.

view this post on Zulip Alex J. Best (Mar 16 2021 at 20:52):

I guess that page also includes a pairwise disjoint condition which is missing from what I wrote

view this post on Zulip Iocta (Mar 16 2021 at 21:05):

I see. That in_ naming scheme is very clarifying. I was confused thinking the first component's argument was the semialgebra instead of a member of it.

view this post on Zulip Iocta (Mar 16 2021 at 22:06):

image.png

is the "disjoint" condition actually doing any work or can I just delete it?

view this post on Zulip Iocta (Mar 16 2021 at 22:07):

import data.finset.basic

open set

variables {α : Type*}

structure semialgebra' (α : Type*) :=
(in_semialgebra : set α  Prop)
(semialgebra_empty : in_semialgebra )
(semialgebra_inter :  (s1 s2 : set α), in_semialgebra s1  in_semialgebra s2  in_semialgebra (s1  s2))
(semialgebra_compl :  (s : set α), in_semialgebra s   c : finset (set α), sUnion (c : set (set α)) = s)

view this post on Zulip Iocta (Mar 16 2021 at 22:13):

(Also, why is that definition so different from the one on wikibooks)

view this post on Zulip Iocta (Mar 17 2021 at 22:46):

I thought it was gonna ask me to show that empty is in I, but it's asking for nullset equals I. I guess I've made the same mistake again, but I don't see how.

import measure_theory.measure_space

open measure_theory measure_theory.measure_space classical set

structure semialgebra (α : Type*) :=
(in_semialgebra : set α  Prop)
(semialgebra_empty : in_semialgebra )
(semialgebra_inter :  (s1 s2 : set α), in_semialgebra s1  in_semialgebra s2  in_semialgebra (s1  s2))
(semialgebra_compl :  (s : set α), in_semialgebra s   c : finset (set α), sUnion (c : set (set α)) = s)

example (I : {s : set  //  (a b : ), s = Icc a b}) : semialgebra I := {
  in_semialgebra := heq I,
  semialgebra_empty := _,
  semialgebra_inter := _,
  semialgebra_compl := _
}

-- don't know how to synthesize placeholder
-- context:
-- I : {s // ∃ (a b : ℝ), s = Icc a b}
-- ⊢ I == ∅

view this post on Zulip Eric Wieser (Mar 17 2021 at 22:59):

Are you sure you want heq I as your in_semi_algebra?

view this post on Zulip Eric Wieser (Mar 17 2021 at 22:59):

It's very rare to want docs#heq unless you're really running into dependently-typed trouble

view this post on Zulip Eric Wieser (Mar 17 2021 at 23:01):

Is it possible you wanted this?

example : semialgebra  := {
  -- the semialgebra contains closed intervals of ℝ
  in_semialgebra := λ s,  (a b : ), s = Icc a b,
  semialgebra_empty := 0, 0, sorry⟩,
  semialgebra_inter := sorry,
  semialgebra_compl := sorry
}

view this post on Zulip Iocta (Mar 17 2021 at 23:03):

That looks more right, I'll try that

view this post on Zulip Iocta (Mar 17 2021 at 23:05):

I guess that's actually asking me to show [0,0]=[0,0] = \emptyset which probably isn't true. So maybe my statement of the problem is broken in the first place.

view this post on Zulip Eric Wieser (Mar 17 2021 at 23:51):

Oh yeah, I forgot what closed meant!

view this post on Zulip Iocta (Mar 18 2021 at 19:36):

What is this error?

import measure_theory.measure_space

open measure_theory measure_theory.measure_space classical set

structure semialgebra (α : Type*) :=
(in_semialgebra : set α  Prop)
(semialgebra_empty : in_semialgebra )
(semialgebra_inter :  (s1 s2 : set α), in_semialgebra s1  in_semialgebra s2  in_semialgebra (s1  s2))
(semialgebra_compl :  (s : set α), in_semialgebra s   c : finset (set α), sUnion (c : set (set α)) = s)


example : semialgebra  := {
  in_semialgebra := λ s, s =    (a b : ),  (a < b  s = (Ioc a b)),
  semialgebra_empty := or.inl rfl,
  semialgebra_inter := begin
    intros s1 s2 h1 h2,
    cases h1 with h1 h1,
    {
      cases h2 with h2 h2,
      {
        left,
        rw [h1, empty_inter],
      },
      {
        left,
        rw [h1, empty_inter],
      },
    },
    {
      cases h2,
      {
        left,
        rw [h2, inter_empty],
      },
      {
        right,
        cases h1 with a1 h1,
        cases h1 with b1 h1,
        rw h1,
        cases h2 with a2 h2,
        cases h2 with b2 h2,
        rw h2,
        {
          use a1  a2,
          use b1  b2,
          intro h,
          rw Ioc_inter_Ioc,
        },
        {
          apply (classical.em (a2 < b2)),
          -- invalid apply tactic, failed to unify
          --   a2 < b2
          -- with
          --   a2 < b2 ∨ ¬a2 < b2
          -- state:
          -- s1 s2 : set ℝ,
          -- a1 b1 : ℝ,
          -- h1 : a1 < b1 → s1 = Ioc a1 b1,
          -- a2 b2 : ℝ,
          -- h2 : a2 < b2 → s2 = Ioc a2 b2
          -- ⊢ a2 < b2
        },
        {
          sorry,
        },
      },
    }
  end,
  semialgebra_compl := begin
    sorry
  end
}

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 19:37):

Do you understand what the apply tactic does? It changes a goal of the form Q to a goal of the form P if you apply f : P -> Q.

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 19:37):

Where is your function of the form P -> Q which you're applying?

view this post on Zulip Iocta (Mar 18 2021 at 19:49):

It's in h2

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 19:49):

if h2 is of the form P -> Q then you should apply h2 instead, and it will work as long as your goal is Q. You are applying a theorem of the form "P or Q is true" and this isn't a function so you can't apply it.

view this post on Zulip Iocta (Mar 18 2021 at 19:52):

Er that's not right. h2 is P -> Q and I have P in goal. I think I should be able to say P is either true or it isn't. In case it's true, that's sufficient; in case it isn't I'm gonna try to find a contradiction.

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 19:53):

Sure you can do that but apply doesn't do that. Maybe you want the by_cases tactic?

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 19:54):

Oh if P is your goal then maybe by_contra is a quicker way to get where you want to go

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 19:54):

Aah -- you use cases to split P or Q into a P line and a Q line so maybe another approach is to just change your apply to a cases. But by_contra will get you there more quickly.

view this post on Zulip Eric Wieser (Mar 18 2021 at 19:58):

That goal looks untrue to me

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 20:00):

∃ (a b : ℝ), (a < b → s = (Ioc a b)) should surely be "a < b and s = ...". Otherwise such a and b always exist, just take a=1 and b=0.

view this post on Zulip Iocta (Mar 18 2021 at 20:03):

Like this? in_semialgebra := λ s, s = ∅ ∨ ∀ (a b : ℝ), (a < b ∧ s = (Ioc a b)),

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 20:05):

That looks right, but why not just drop a < b and the s = emptyset as well, because when a>=b Ioc a b is just the empty set anyway.

view this post on Zulip Iocta (Mar 18 2021 at 20:08):

Oh that's much nicer

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 20:09):

It's crazy how these things sometimes come out really super-nicely sometimes.

view this post on Zulip Iocta (Mar 18 2021 at 20:12):

I think I missed something. If the statement is just in_semialgebra := λ s, ∀ (a b : ℝ), s = (Ioc a b), then semialgebra_empty will ask me to show that forall a b, Ioc a b = emptyset, which doesn't seem true.

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 20:13):

There's something wrong with compl as well. Right now you can just let c = {s^compl}. If you restrict to all the elements of c being in your semialgebra then you can't make the complement of [0,1) because every set in your semialgebra has finite measure and so a finite union will do too. I think you might need the infinity versions of Ioc. I've forgotten what they're called though.

view this post on Zulip Iocta (Mar 18 2021 at 20:14):

Iic?

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 20:14):

yes it could well be that

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 20:15):

docs#set.Iic

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 20:15):

Yes, that. But I don't want to tell you what your semialgebra is -- it's your definition.

view this post on Zulip Iocta (Mar 18 2021 at 20:17):

I'm trying to copy image.png

view this post on Zulip Iocta (Mar 18 2021 at 20:18):

But one dimensional for now

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 20:19):

note the possibility that a and b can be infinity.

view this post on Zulip Iocta (Mar 18 2021 at 20:19):

Well I guess I was sorta mixing that with image.png from https://en.wikibooks.org/wiki/Measure_Theory/Basic_Structures_And_Definitions/Semialgebras,_Algebras_and_%CF%83-algebras

view this post on Zulip Iocta (Mar 18 2021 at 20:19):

But maybe those definitions are actually not talking about the same object

view this post on Zulip Iocta (Mar 18 2021 at 20:21):

(deleted)

view this post on Zulip Iocta (Mar 18 2021 at 20:26):

Yeah this can't be right

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

structure semialgebra (α : Type*) :=
(in_semialgebra : set α  Prop)
(semialgebra_empty : in_semialgebra )
(semialgebra_inter :  (s1 s2 : set α), in_semialgebra s1  in_semialgebra s2  in_semialgebra (s1  s2))
(semialgebra_compl :  (s : set α), in_semialgebra s   c : finset (set α), sUnion (c : set (set α)) = s)


example : semialgebra ereal := {
  in_semialgebra := λ s,  (a b : ereal), s = (Ioc a b),
  semialgebra_empty := begin
      intros a b,
  -- a b: ereal
  -- ⊢ ∅ = Ioc a b
  end,
  semialgebra_inter := begin
    sorry,
  end,
  semialgebra_compl := begin
    sorry
  end
}

view this post on Zulip Iocta (Mar 18 2021 at 20:32):

Gotta be

example : semialgebra ereal := {
  in_semialgebra := λ s,  (a b : ereal), s = (Ioc a b),
  semialgebra_empty := 0, 0, sorry⟩,
  semialgebra_inter := begin
    sorry,
  end,
  semialgebra_compl := begin
    sorry
  end

view this post on Zulip Eric Wieser (Mar 18 2021 at 20:44):

Isn't that what I posted earlier?

view this post on Zulip Eric Wieser (Mar 18 2021 at 20:45):

Ah, Ioc instead of Icc

view this post on Zulip Iocta (Mar 18 2021 at 20:49):

It's very close, also changed real to ereal

view this post on Zulip Iocta (Mar 19 2021 at 00:31):

I'm trying to make a finset with this these two elements but Lean doesn't know how to put the elements in the finset.

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

structure semialgebra (α : Type*) :=
(in_semialgebra : set α  Prop)
(semialgebra_empty : in_semialgebra )
(semialgebra_inter :  (s1 s2 : set α), in_semialgebra s1  in_semialgebra s2  in_semialgebra (s1  s2))
(semialgebra_compl :  (s : set α), in_semialgebra s   c : finset (set α), sUnion (c : set (set α)) = s)

example : semialgebra ereal := {
  in_semialgebra := λ s,  (a b : ereal), s = (Ioc a b),
  semialgebra_empty := 0, 0, sorry⟩,
  semialgebra_inter := begin
    intros s1 s2 h1 h2,
    cases h1 with a1 ha1,
    {
      cases ha1 with b1 hb1,
      {
        cases h2 with a2 ha2,
        {
          cases ha2 with b2 hb2,
          use a1  a2,
          use b1  b2,
          rw [hb1, hb2, Ioc_inter_Ioc],
        },
      },
    },
  end,
  semialgebra_compl := begin
    intros s hs,
    cases hs with a h,
    cases h with b h,
    rw h,
    have t : finset (set ereal) := {(Iic a) , (Ioi b)},
-- failed to synthesize type class instance for
-- s : set ereal,
-- a b : ereal,
-- h : s = Ioc a b
-- ⊢ has_insert ?m_1 (finset (set ereal))
-- state:
-- s : set ereal,
-- a b : ereal,
-- h : s = Ioc a b
-- ⊢ ∃ (c : finset (set ereal)), ⋃₀↑c = (Ioc a b)ᶜ
  end
}

view this post on Zulip Scott Morrison (Mar 19 2021 at 00:42):

Are you just missing decidable instances? What happens if you open_locale classical, or use classical at the beginning of the proof?

view this post on Zulip Iocta (Mar 19 2021 at 00:45):

Yeah that was it

view this post on Zulip Iocta (Mar 19 2021 at 08:44):

How can I solve this?

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

open_locale classical

lemma compl_Ioc (a b : ereal) : (Ioc a b)  = Iic a  Ioi b :=
begin
  sorry,
end

view this post on Zulip Iocta (Mar 19 2021 at 08:51):

I think it's true

view this post on Zulip Johan Commelin (Mar 19 2021 at 08:55):

Does ext get you started?

view this post on Zulip Eric Wieser (Mar 19 2021 at 11:01):

rw [mem_union_eq, mem_Ioi, mem_Iic, mem_compl_eq, mem_Ioc] will then get you most of the way to finished

view this post on Zulip Eric Wieser (Mar 19 2021 at 11:04):

I think it might be worth PRing that lemma, once golfed to:

lemma compl_Ioc (a b : ereal) : (Ioc a b) = Iic a  Ioi b :=
set.ext $ λ _, not_and_distrib.trans (or_congr not_lt not_le)

view this post on Zulip Eric Wieser (Mar 19 2021 at 11:04):

Along with the other three variants of o and c

view this post on Zulip Iocta (Mar 19 2021 at 21:52):

This works now. How can I make it shorter?

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

open_locale classical

structure semialgebra (α : Type*) :=
(in_semialgebra : set α  Prop)
(semialgebra_empty : in_semialgebra )
(semialgebra_inter :  (s1 s2 : set α), in_semialgebra s1  in_semialgebra s2  in_semialgebra (s1  s2))
(semialgebra_compl :  (s : set α), in_semialgebra s   c : finset (set α), sUnion (c : set (set α)) = s)


lemma compl_Ioc (a b : ereal) : (Ioc a b) = Iic a  Ioi b :=
set.ext $ λ _, not_and_distrib.trans (or_congr not_lt not_le)


example : semialgebra ereal := {
  in_semialgebra := λ s,  (a b : ereal), s = (Ioc a b),
  semialgebra_empty := 0, 0, by simp only [mem_empty_eq, forall_const, not_false_iff, Ioc_self],⟩,
  semialgebra_inter := begin
    intros s1 s2 h1 h2,
    cases h1 with a1 ha1,
    {
      cases ha1 with b1 hb1,
      {
        cases h2 with a2 ha2,
        {
          cases ha2 with b2 hb2,
          use a1  a2,
          use b1  b2,
          rw [hb1, hb2, Ioc_inter_Ioc],
        },
      },
    },
  end,
  semialgebra_compl := begin
    intros s hs,
    cases hs with a h,
    cases h with b h,
    rw h,
    let t : finset (set ereal) := {(Iic a) , (Ioi b)},
    use t,
    have: ⋃₀↑t =  (Iic a)  (Ioi b),
    from by simp only [finset.coe_insert, sUnion_singleton, finset.coe_singleton, sUnion_insert],
    rw [this],
    rw [compl_Ioc],
  end
}

view this post on Zulip Eric Wieser (Mar 19 2021 at 21:59):

Yours intros and four cases tactics can be combined into a single rintros

view this post on Zulip Eric Wieser (Mar 19 2021 at 22:00):

rintros s1 s2 ⟨a1, b1, rfl⟩ ⟨a2, b2, rfl⟩

view this post on Zulip Eric Wieser (Mar 20 2021 at 10:14):

Here's how I'd golf the whole thing:

example : semialgebra ereal := {
  in_semialgebra := λ s,  (a b : ereal), s = Ioc a b,
  semialgebra_empty := 0, 0, (Ioc_self _).symm⟩,
  semialgebra_inter := begin
    rintros s1 s2 a1, b1, rfl a2, b2, rfl⟩,
    exact a1  a2, b1  b2, Ioc_inter_Ioc⟩,
  end,
  semialgebra_compl := begin
    rintros s a, b, rfl⟩,
    refine ⟨{Iic a, Ioi b}, eq.trans _ (compl_Ioc _ _).symm⟩,
    simp only [finset.coe_insert, sUnion_singleton, finset.coe_singleton, sUnion_insert],
  end }

view this post on Zulip Iocta (Mar 20 2021 at 20:43):

rintros s1 s2 ⟨a1, b1, rfl⟩ ⟨a2, b2, rfl⟩, works but if I replace it with rintros s1 s2 ⟨a1, b1, _⟩ ⟨a2, b2, _⟩, then it doesn't work. What is the difference?

view this post on Zulip Eric Wieser (Mar 20 2021 at 20:50):

rfl is like introducing h then immediately doing rw h

view this post on Zulip Eric Wieser (Mar 20 2021 at 20:50):

Although that's a bit of a simplification

view this post on Zulip Iocta (Mar 20 2021 at 20:51):

Whereas the _ is just introducing h?

view this post on Zulip Iocta (Mar 20 2021 at 21:00):

rintros s1 s2 a1, b1, h1 a2, b2, h2⟩,
rw [h1, h2],

does work

view this post on Zulip Eric Wieser (Mar 20 2021 at 21:37):

Yeah, _ just tells lean to pick a name for you

view this post on Zulip Iocta (Mar 21 2021 at 04:46):

This works, what does a shorter version look like?

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

open_locale classical
noncomputable theory


structure algebra' (α : Type*) :=
(in_algebra : set α  Prop)
(algebra_empty : in_algebra )
(algebra_compl :  (s : set α), in_algebra s  in_algebra s)
(algebra_union :  (s1 s2 : set α), in_algebra s1  in_algebra s2  in_algebra (s1  s2))


lemma eq_compl_of_compl_eq (s1 s2: set ) (h : s1 = s2) : s1 = s2 :=
begin
ext,
split;
{
  intro h,
  simp only [mem_compl_eq] at *,
  finish,
},
end


example : algebra'  := {
  in_algebra := λs,  (t : finset ), (s = t)  (s = t),
  algebra_empty :=
  finset.empty, or.inl rfl⟩,
  algebra_compl := begin
    intros s hs,
    cases hs with t ht,
    cases ht with h ht,
    {
      use t,
      rw [compl_compl],
      right,
      exact h,
    },
    {
      use t,
      left,
      exact ht,
    }
  end,
  algebra_union := begin
    rintros s1 s2 t1, h1 t2, h2⟩,
    cases h1,
    {
      cases h2,
      {
        use t1  t2,
        left,
        simp only [finset.coe_union],
        simp only [*],
      },
      {
        use t2.filter (λx, x  s1),
        right,
        rw [compl_union],
        ext,
        simp only [mem_sep_eq, mem_inter_eq, finset.mem_coe, mem_compl_eq, finset.coe_filter],
        split,
        simp only [*, and_imp, finset.mem_coe] at *,
        {
          intros h h',
          split,
          {
            have: s2 = t2,
            from by {
              apply eq_compl_of_compl_eq,
              exact h2,
            },
            simp only [*, not_not, finset.mem_coe, mem_compl_eq] at *,
          },
          { exact h, },
        },
        {
          intros h,
          split,
          { exact h.2,  },
          {
            cases h,
            rw [mem_compl_eq],
            simp only [*, finset.mem_coe] at *,
          },
        },
      },
    },
    {
      cases h2,
      {
        use t1.filter (λx, x  s2),
        right,
        rw [compl_union],
        ext,
        split,
        {
          intro h,
          simp only [*, mem_sep_eq, mem_inter_eq, not_false_iff, and_self, mem_compl_eq, finset.coe_filter] at *,
        },
        {
          intro h,
          have: s1 = t1,
          from by {
            apply eq_compl_of_compl_eq,
            exact h1,
          },
          {
            simp only [*, mem_sep_eq, mem_inter_eq, not_false_iff, and_self, mem_compl_eq, finset.coe_filter] at *,
          },
        },
      },
      {
        use t1.filter (λx, x  t2),
        have h1': s1 = t1,
        from by {
          apply eq_compl_of_compl_eq,
          exact h1,
        },
        have: s2 = t2,
        from by {
          apply eq_compl_of_compl_eq,
          exact h2,
        },
        right,
        ext,
        simp only [*, mem_sep_eq, compl_union, mem_inter_eq, iff_self, finset.mem_coe, finset.coe_filter] at *,
      },
    },
  end
}

view this post on Zulip Kevin Buzzard (Mar 21 2021 at 08:04):

"have, from by apply exact" can all be done in one line, and one has to question whether it's even necessary given that you're about to close the goal with a simp * -- just throw the proof directly into the list of things in the list

view this post on Zulip Kevin Buzzard (Mar 21 2021 at 08:04):

intros, cases can be done with rintro

view this post on Zulip Kevin Buzzard (Mar 21 2021 at 08:05):

Did you try library_search for eq_compl_of_compl_eq?

view this post on Zulip Iocta (Mar 21 2021 at 08:16):

What is the rintros-only version of rintros s ⟨t, ht⟩, cases ht with h,?

view this post on Zulip Iocta (Mar 21 2021 at 08:17):

library_search didn't work for eq_compl_of_compl_eq ("excessive memory consumption")

view this post on Zulip Kevin Buzzard (Mar 21 2021 at 08:21):

Try looking for the iff version? The rintros version probably replaces ht with (h1 | h2)

view this post on Zulip Iocta (Mar 21 2021 at 08:25):

I tried replacing the have/from like simp only [*, not_not, finset.mem_coe, mem_compl_eq, eq_compl_of_compl_eq, h2] at *, but it said invalid simplification lemma 'eq_compl_of_compl_eq'

view this post on Zulip Kevin Buzzard (Mar 21 2021 at 08:27):

Indeed that is a useless simp lemma by itself. I'm suggesting you add the full proof ie eq_compl_of_compl_eq h1

view this post on Zulip Iocta (Mar 21 2021 at 08:28):

Replacing rintros s ⟨t, ht⟩, cases ht with h, with rintros s ⟨t, ⟨h1 | h2⟩⟩, leaves me with image.png

view this post on Zulip Kevin Buzzard (Mar 21 2021 at 08:28):

You can just use simp to close goals, you don't need all this simp only stuff

view this post on Zulip Iocta (Mar 21 2021 at 08:29):

I read somewhere that it's bad style to just use simp because the simp rules change over time, so I normally write squeeze_simp and just use whatever it says

view this post on Zulip Kevin Buzzard (Mar 21 2021 at 08:29):

You need round brackets like I used, not pointy ones. Sorry I can't help more, I'm not at lean right now.

view this post on Zulip Kevin Buzzard (Mar 21 2021 at 08:30):

It's bad style to use simp to not close a goal. If it's solving the goal it's fine.

view this post on Zulip Iocta (Mar 21 2021 at 08:33):

can all be done in one line

what are the rules for what's done in a single line?

view this post on Zulip Iocta (Mar 21 2021 at 08:34):

btw dunno what's wrong with those ()in the screenshot but it always wraps weird like that when there's a \compl

view this post on Zulip Iocta (Mar 21 2021 at 08:36):

Try looking for the iff version?

lemma eq_compl_of_compl_eq (s1 s2: set ) (h : s1 = s2) (x : ) : x  s1  x  s2 :=
begin
library_search,
end

didn't work either

view this post on Zulip Eric Wieser (Mar 21 2021 at 09:13):

I think Kevin is describing

lemma eq_compl_iff_compl_eq (s1 s2: set ) :
  s1 = s2  s1 = s2 :=
begin
  library_search,
end

does that work?

view this post on Zulip Iocta (Mar 21 2021 at 18:49):

No

view this post on Zulip Eric Wieser (Mar 21 2021 at 18:52):

How about the statement function.involutive (has_compl.compl : set X \to set X)?

view this post on Zulip Iocta (Mar 21 2021 at 18:58):

If you mean

example (X : Type) : function.involutive (has_compl.compl : set X  set X) := begin
  library_search,
end

then no

view this post on Zulip Kevin Buzzard (Mar 21 2021 at 19:08):

It's in there somewhere. Why not just read data.set.basic? Find the section on compl.

view this post on Zulip Iocta (Mar 21 2021 at 20:04):

Maybe it's in a form I don't recognize, but I don't see it. https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#lemmas-about-complement

view this post on Zulip Kevin Buzzard (Mar 21 2021 at 20:41):

There's also a bunch of stuff in order/boolean_algebra but I can't see it there either. Here are some shorter proofs:

import tactic
import data.set.basic

namespace set

variable {α : Type*}

lemma eq_compl_of_compl_eq {s1 s2: set α} : s1 = s2  s1 = s2 :=
begin
  rintro rfl,
  exact (compl_compl s1).symm,
end

lemma eq_compl_iff_compl_eq (s1 s2 : set α) : s1 = s2  s1 = s2 :=
eq_compl_of_compl_eq, λ h, (eq_compl_of_compl_eq h.symm).symm

end set

view this post on Zulip Bryan Gin-ge Chen (Mar 21 2021 at 20:48):

These should definitely be added to mathlib (in order/boolean_algebra).

view this post on Zulip Iocta (Mar 21 2021 at 21:11):

Why is the have necessary?

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

open_locale classical
noncomputable theory





structure algebra' (α : Type*) :=
(in_algebra : set α  Prop)
(algebra_empty : in_algebra )
(algebra_compl :  (s : set α), in_algebra s  in_algebra s)
(algebra_union :  (s1 s2 : set α), in_algebra s1  in_algebra s2  in_algebra (s1  s2))



lemma eq_compl_of_compl_eq (s1 s2: set ) (h : s1 = s2) : s1 = s2 :=
begin
ext,
split;
{
  intro h,
  simp only [mem_compl_eq] at *,
  finish,
},
end



example : algebra'  := {
  in_algebra := λs,  (t : finset ), (s = t)  (s = t),
  algebra_empty :=
  finset.empty, or.inl rfl⟩,
  algebra_compl := begin
    rintros s t, ht⟩, cases ht with h,
    { use t, rw [compl_compl], right, exact h, },
    { use t, left, exact ht, }
  end,
  algebra_union := begin
    rintros s1 s2 t1, (h11 |h12)⟩ t2, (h21 | h22)⟩,
    {
      use t1  t2,
      left,
      simp only [finset.coe_union, *],
    },
    {
      use t2.filter (λx, x  s1),
      right,
      rw [compl_union],
      ext,
      simp only [mem_sep_eq, mem_inter_eq, finset.mem_coe, mem_compl_eq, finset.coe_filter],
      split,
      simp only [*, and_imp, finset.mem_coe] at *,
      {
        intros h h',
        split,
        { -- have: s2 = t2ᶜ, from by {  apply eq_compl_of_compl_eq, exact h22, },
          simp [*, eq_compl_of_compl_eq s2, eq_compl_of_compl_eq t2] at *,  },
        { exact h, },
      },
      {
        intros h,
        split,
        { exact h.2,  },
        { cases h,
          rw [mem_compl_eq],
          simp only [*, finset.mem_coe] at *,   },
      },
    },
    {
        use t1.filter (λx, x  s2),
        right,
        rw [compl_union],
        ext,
        split,
        { intro h, simp [*] at *, },
        { intro h, { simp [*, eq_compl_of_compl_eq s1] at *,}, },
    },
    {
        use t1.filter (λx, x  t2),
        right,
        ext,
        simp [*, eq_compl_of_compl_eq s1, eq_compl_of_compl_eq s2] at *,
    },
  end
}


simp_all tactic failed to simplify
state:
s1 s2 : set ,
t1 : finset ,
h11 : s1 = t1,
t2 : finset ,
h22 : s2 = t2,
x : ,
h : x  t1,
h' : x  s2
 x  t2

view this post on Zulip Iocta (Mar 21 2021 at 21:13):

Anyway that's a good reduction in verbosity, but still pretty large

view this post on Zulip Damiano Testa (Mar 22 2021 at 14:16):

You may want to double-check, but I think that this is a simplified version of what you had:

lemma compl_eq_iff {α : Type*} (s1 s2 : set α) : s1 = s2  s2 = s1 :=
by refine _, _; rintros rfl; exact compl_compl _

example : algebra'  := {
  in_algebra := λs,  (t : finset ), (s = t)  (s = t),
  algebra_empty :=
  finset.empty, or.inl rfl⟩,
  algebra_compl := begin
    rintro s t, rfl | h⟩,
    { exact t, or.inr (compl_compl t)⟩ },
    { exact t, or.inl h }
  end,
  algebra_union := begin
    rintro s1 s2 t1, rfl | h t2, rfl | k⟩,
    { exact t1  t2, or.inl (finset.coe_union _ _).symm },
    { rw  (compl_eq_iff _ _).mp k,
      exact t2.filter (λx, x  t1), or.inr (ext (λ x, by simp [and_comm]))⟩ },
    { rw  (compl_eq_iff _ _).mp h,
      exact t1.filter (λ x, x  t2), or.inr (ext (λ x, by simp [and_comm]))⟩ },
    { rw  (compl_eq_iff _ _).mp h,
      exact t1.filter (λx, x  s2), or.inr (ext (λ x, by simp [and_comm]))⟩ },
  end }

view this post on Zulip Damiano Testa (Mar 22 2021 at 14:35):

Also, while I have not worked with it, it might be better to make implicit some of the inputs in your definition of algebra':

structure algebra' (α : Type*) :=
(in_algebra : set α  Prop)
(algebra_empty : in_algebra )
(algebra_compl :  {s : set α}, in_algebra s  in_algebra s)  -- made `s` implicit
(algebra_union :  {s1 s2 : set α}, in_algebra s1  in_algebra s2  in_algebra (s1  s2))  -- made `s1 s2` implicit

view this post on Zulip Iocta (Mar 22 2021 at 19:58):

That's quite an improvement! Thanks @Damiano Testa

view this post on Zulip Iocta (Mar 24 2021 at 19:14):

How can I express "the set of finite disjoint unions of sets in S"?
image.png

import measure_theory.measure_space
import data.real.ereal

open measure_theory measure_theory.measure_space classical set real

open_locale classical
noncomputable theory

structure algebra' (α : Type*) :=
(in_algebra : set α  Prop)
(algebra_empty : in_algebra )
(algebra_compl :  (s : set α), in_algebra s  in_algebra s)
(algebra_union :  (s1 s2 : set α), in_algebra s1  in_algebra s2  in_algebra (s1  s2))

structure semialgebra (α : Type*) :=
(in_semialgebra : set α  Prop)
(semialgebra_empty : in_semialgebra )
(semialgebra_inter :  (s1 s2 : set α), in_semialgebra s1  in_semialgebra s2  in_semialgebra (s1  s2))
(semialgebra_compl :  (s : set α), in_semialgebra s   c : finset (set α), sUnion (c : set (set α)) = s)

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 19:19):

You could define it recursively. Or you might want to check that the finite disjoint unions are just the same as the finite unions, which would be easier to define and work with -- I think they are.

view this post on Zulip Iocta (Mar 24 2021 at 19:26):

by 'check that ...' do you mean check that this result holds for finite unions in general?

view this post on Zulip Iocta (Mar 24 2021 at 19:27):

(deleted)

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 19:50):

I can't make sense of your lemma 1.1.3. How does one see that "the definition of S implies S_i^c \in S-bar"? I can't immediately see how to deduce it from your formal definition of semialgebra -- you know that the complement is a union of things in the semialgebra but you don't know the union is disjoint, right?

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 19:51):

For me, the algebra generated by the semialgebra seems to naturally be the finite union of elements of the semialgebra and then the proof that it's an algebra goes through; moreover it's clearly the smallest algebra containing the semialgebra, at least if we go via the definitions you have formalised.

view this post on Zulip Iocta (Mar 24 2021 at 20:51):

This text does use 'disjoint' in the definition of semialgebra image.png
so maybe I should try to include that in my lean semialgebra definition

view this post on Zulip Iocta (Mar 24 2021 at 20:51):

Or maybe that's unnecessary complication

view this post on Zulip Iocta (Mar 24 2021 at 21:06):

Is that like this?

structure semialgebra' (α : Type*) :=
(in_semialgebra : set α  Prop)
(semialgebra_empty : in_semialgebra )
(semialgebra_inter :  (s1 s2 : set α), in_semialgebra s1  in_semialgebra s2  in_semialgebra (s1  s2))
(semialgebra_compl :  (s : set α), in_semialgebra s   c : finset (set α), ( (x   c) (y  c),  x  y = )  sUnion (c : set (set α)) = s)

view this post on Zulip Kevin Buzzard (Mar 25 2021 at 08:12):

If you change the definition from the book then you'll have a different definition. Your definition of pairwise disjoint above is incorrect because you can have x=y. There might already be a way of saying "pairwise disjoint" in mathlib but I don't personally know it

view this post on Zulip Eric Wieser (Mar 25 2021 at 08:33):

docs#complete_lattice.independent I think is equivalent for sets?


Last updated: May 13 2021 at 00:41 UTC