Zulip Chat Archive

Stream: general

Topic: Diamond of complete boolean algebras on sets


Oliver Nash (Oct 10 2022 at 13:16):

We seem to have a diamond as follows:

import data.set.lattice

variables {α : Type*}

-- Succeeds
example : @set.boolean_algebra α = pi.boolean_algebra := rfl

-- Fails
example : @set.complete_boolean_algebra α = pi.complete_boolean_algebra := rfl

Is this known?

Yaël Dillies (Oct 10 2022 at 13:29):

Hmm that's something I thought I had fixed. I'll investigate

Oliver Nash (Oct 10 2022 at 13:29):

Thanks, I'd be very grateful!

Yaël Dillies (Oct 10 2022 at 13:31):

Note that this does not morally need fixing (because set is a type synonym) but in this case I know that this working is related to defeqs we do care about.

Oliver Nash (Oct 12 2022 at 13:59):

@Yaël Dillies Did you find time to investigate this? If not, I'm happy just to open an issue for it and move on.

Oliver Nash (Oct 12 2022 at 14:00):

I appreciate the point about set being a type synonym but if it helps here is an example where this comes up for me:

import measure_theory.measure.measure_space

open filter measure_theory

lemma limsup_sdiff
  {α β : Type*} [complete_boolean_algebra α] (l : filter β) (u : β  α) (a : α) :
  (l.limsup u) \ a = l.limsup (λ b, (u b) \ a) :=
begin
  simp only [limsup_eq_infi_supr, sdiff_eq],
  rw binfi_inf (⟨set.univ, univ_mem :  (i : set β), i  l),
  simp_rw [inf_comm, inf_bsupr_eq, inf_comm],
end

variables {α : Type*} [measurable_space α] {μ : measure α}

lemma limsup_ae_eq_of_forall_ae_eq (s :   set α) {t : set α} (h :  n, s n =ᵐ[μ] t) :
  -- limsup at_top s =ᵐ[μ] t :=
  @limsup (set α)  _ at_top s =ᵐ[μ] t :=
begin
  simp_rw ae_eq_set at h ,
  split,
  { rw limsup_sdiff at_top s t,
    apply measure_limsup_eq_zero,
    simp [h], },
  { sorry, }, -- Omitting this proof to keep MWE short
end

Oliver Nash (Oct 12 2022 at 14:00):

The point is that I am forced to write @limsup (set α) ℕ _ at_top s rather than limsup at_top s because of the diamond.

Oliver Nash (Oct 12 2022 at 14:02):

I believe the reason this is happening is that in the hypothesis h : ∀ n, s n =ᵐ[μ] t, Lean is required to see through the set type synonym and so then it continues doing that for the conclusion.

Yaël Dillies (Oct 12 2022 at 14:02):

That's what's bad, right? You should never write s n but instead n ∈ s

Eric Wieser (Oct 12 2022 at 14:04):

s here is a family of sets

Eric Wieser (Oct 12 2022 at 14:04):

Should it be h : ∀ n, (∈ s n) =ᵐ[μ] (∈ t)?

Oliver Nash (Oct 12 2022 at 14:04):

What's happening is that we have a design decision in our measure theory library to define almost-equal sets as almost-equal functions.

Yaël Dillies (Oct 12 2022 at 14:05):

Hmm... That goes against the general design decision of making set α a proper type synonym.

Oliver Nash (Oct 12 2022 at 14:05):

Yes it does.

Oliver Nash (Oct 12 2022 at 14:06):

But it's been done.

Yaël Dillies (Oct 12 2022 at 14:06):

And when we eventually make set a structure your trick doesn't work anymore and we have to change even more files to fix it.

Eric Wieser (Oct 12 2022 at 14:06):

Can you remind me what the notation above unfolds to?

Eric Wieser (Oct 12 2022 at 14:06):

I'm not familiar with measure theory notation

Sebastien Gouezel (Oct 12 2022 at 14:07):

It means that, for a full measure set of points x, then x belongs to s n iff it belongs to t.

Eric Wieser (Oct 12 2022 at 14:07):

What's the declaration behind the notation though?

Sebastien Gouezel (Oct 12 2022 at 14:07):

And yes, we are abusing defeq to avoid duplicating the API. And yes, it's bad :-)

Oliver Nash (Oct 12 2022 at 14:08):

Eric Wieser said:

Can you remind me what the notation above unfolds to?

It's ∀ n, ∀ᶠ x in μ.ae, s n x = t x

Eric Wieser (Oct 12 2022 at 14:08):

I think we should just add the s

Eric Wieser (Oct 12 2022 at 14:09):

We did that for a bunch of decidable arguments a while ago and it was generally an improvement

Oliver Nash (Oct 12 2022 at 14:10):

Eric Wieser said:

I think we should just add the s

Can you clarify what this means?

Eric Wieser (Oct 12 2022 at 14:10):

I mean do what I said in the message above

Eric Wieser (Oct 12 2022 at 14:11):

The canonical way to view a set as a function is (∈ s)

Eric Wieser (Oct 12 2022 at 14:12):

Which as a bonus, works for finset, submonoid, ... too

Sebastien Gouezel (Oct 12 2022 at 14:12):

I am trying that randomly in some files, and it doesn't seem to break anything. So I agree it's probably a good idea. Let me try to complete this.

Oliver Nash (Oct 12 2022 at 14:13):

Oh I see. If I do that then Lean still uses pi.complete_boolean_algebra which is a problem when I try to apply limsup_sdiff because t is a set.

Eric Wieser (Oct 12 2022 at 14:14):

What's your full modified version?

Oliver Nash (Oct 12 2022 at 14:14):

import measure_theory.measure.measure_space

open filter measure_theory

lemma limsup_sdiff
  {α β : Type*} [complete_boolean_algebra α] (l : filter β) (u : β  α) (a : α) :
  (l.limsup u) \ a = l.limsup (λ b, (u b) \ a) :=
begin
  simp only [limsup_eq_infi_supr, sdiff_eq],
  rw binfi_inf (⟨set.univ, univ_mem :  (i : set β), i  l),
  simp_rw [inf_comm, inf_bsupr_eq, inf_comm],
end

variables {α : Type*} [measurable_space α] {μ : measure α}

lemma limsup_ae_eq_of_forall_ae_eq (s :   set α) {t : set α} (h :  n, ( s n) =ᵐ[μ] t) :
  limsup at_top s =ᵐ[μ] t :=
  -- @limsup (set α) ℕ _ at_top s =ᵐ[μ] t :=
begin
  -- change (∀ n, ∀ᶠ x in μ.ae, s n x = t x) at h,
  simp_rw ae_eq_set at h ,
  split,
  { rw limsup_sdiff at_top s t,
    apply measure_limsup_eq_zero,
    simp [h], },
  { sorry, }, -- Omitting this proof to keep MWE short
end

Eric Wieser (Oct 12 2022 at 14:14):

The conclusion needs s too

Eric Wieser (Oct 12 2022 at 14:15):

As does t, as in my above comment

Oliver Nash (Oct 12 2022 at 14:17):

Hmm, I'm trying this but failing. One moment.

Oliver Nash (Oct 12 2022 at 14:23):

OK using this idea make progress. Indeed the following allows me to avoid mangling the hypothesis and conclusion:

lemma limsup_ae_eq_of_forall_ae_eq (s :   set α) {t : set α} (h :  n, s n =ᵐ[μ] t) :
  limsup at_top s =ᵐ[μ] t :=
  -- @limsup (set α) ℕ _ at_top s =ᵐ[μ] t :=
begin
  simp_rw ae_eq_set at h ,
  split,
  { erw limsup_sdiff at_top (λ n, ( s n)) t,
    simp only,
    apply measure_limsup_eq_zero, -- This now fails because it expects `set`s
    simp [h], },
  { sorry, }, -- Omitting this proof to keep MWE short
end

but then I have the problem that measure_limsup_eq_zero expects sets.

Oliver Nash (Oct 12 2022 at 14:26):

More precisely, measure_limsup_eq_zero is a statement about a limsup in the complete lattice of sets, which is (unfortunately) definitionally different from what I have if I make a statement about the pi.complete_lattice.

Yaël Dillies (Oct 12 2022 at 14:28):

Okay, I don't understand what's going on. I thought this would be fine given that docs#set.Sup_eq_sUnion is defeq.

Oliver Nash (Oct 12 2022 at 14:37):

It's this failure, right:

example : @pi.has_Sup α (λ a, Prop) _ = @set.has_Sup α := rfl -- Fails

Oliver Nash (Oct 12 2022 at 14:37):

(likewise Inf)

Eric Wieser (Oct 12 2022 at 15:41):

Currently it seems that Sup s on sets is defined as

{a : α |  (t : set α) (H : t  s), a  t}

Eric Wieser (Oct 12 2022 at 15:43):

Whereas on pi types it's

λ (i : α),  (f : s), f i

Eric Wieser (Oct 12 2022 at 15:45):

My hunch is that changing that to one of ⨆ (f ∈ s), ↑f i or Sup (eval i '' s) would fix that

Oliver Nash (Oct 12 2022 at 15:45):

I've opened an issue #16932 for now at least.

Oliver Nash (Oct 12 2022 at 15:46):

(mostly to give me something to reference in a PR which is forced to include the @ characters)

Eric Wieser (Oct 12 2022 at 15:46):

I agree that we should fix this diamond, but I also think that separately we should fix this measure theory defeq abuse

Oliver Nash (Oct 12 2022 at 15:46):

Yes, agreed on both points.

Sebastien Gouezel (Oct 12 2022 at 16:40):

It's not just measure theory, unfortunately, it's also used for general filters. See docs#filter.eventually_eq_set. I'm gonna try to fix all these, but it might take longer than I was expecting naively.

Oliver Nash (Oct 12 2022 at 16:41):

Oh! Well if you have the appetite, such a heroic effort would be great.

Oliver Nash (Oct 13 2022 at 13:38):

I just looked at the complete lattice diamond issue and it seems to me that we would need to change the definition of both set.has_Sup and pi.has_Sup.

Oliver Nash (Oct 13 2022 at 13:38):

I think the following might work:

import data.set.lattice

variables {α : Type*}

def pi.has_Sup' {β : α  Type*} [Π i, has_Sup (β i)] : has_Sup (Π i, β i) :=
λ s i,  f  s, (f : Π i, β i) i

def set.has_Sup' : has_Sup (set α) :=
λ s, {a : α |  t  s, a  t}⟩

example : @pi.has_Sup' α (λ a, Prop) _ = @set.has_Sup' α := rfl

Oliver Nash (Oct 13 2022 at 13:40):

It's actually a one-character change in each case:

  • For pi.has_Sup: f : s becomes f ∈ s
  • For set.has_Sup: ∃ t ∈ s becomes ⨆ t ∈ s

Oliver Nash (Oct 13 2022 at 13:41):

I'm tempted to try this but first I thought I'd see if anyone who has been more involved in the order hierarchy can see an obvious reason why this is doomed?

Oliver Nash (Oct 13 2022 at 13:41):

(same remarks for Infs ofc)

Floris van Doorn (Oct 13 2022 at 13:59):

Maybe it's easier to make such instances definitionally equal if we consistently define Sup in terms of Sup of the "lower" structure, instead of defining it using bsupr (which is a Sup of an image over another Sup)?

Floris van Doorn (Oct 13 2022 at 14:02):

i.e.

import data.set.lattice

variables {α : Type*}

def pi.has_Sup' {β : α  Type*} [Π i, has_Sup (β i)] : has_Sup (Π i, β i) :=
λ s i, Sup (function.eval i '' s)⟩

def set.has_Sup' : has_Sup (set α) :=
λ s, {a : α | Sup ((λ t, a  t) '' s)}⟩

example : @pi.has_Sup' α (λ a, Prop) _ = @set.has_Sup' α := rfl

Oliver Nash (Oct 13 2022 at 14:05):

Thanks, this might indeed be better! If I take this up I'd be tempted to go with whichever change is easier to implement given what we already have in place but if its a tie, I think I'll go for this.

Yaël Dillies (Oct 13 2022 at 14:05):

We explicitly prefer ⨆ i ∈ s, f i over Sup (f '' s), though.

Yaël Dillies (Oct 13 2022 at 14:07):

See for example, docs#with_top.coe_Sup, docs#lower_set.coe_Sup, ...

Yaël Dillies (Oct 13 2022 at 14:10):

We rely a lot on the defeq of set.has_Sup, so changing this would be a pain.

Sebastien Gouezel (Oct 13 2022 at 14:12):

Note that ⨆ i ∈ s, f i almost always returns garbage in a conditionally complete lattice (because when i is not in syou are looking at the Sup of the empty set, which might be anything), while Sup (f '' s) is typically better behaved.

Yaël Dillies (Oct 13 2022 at 14:13):

Yes, that's the one reason we use it, but we avoid it completely in complete lattices.

Sebastien Gouezel (Oct 13 2022 at 14:14):

This might be a historical accident, by the way: at the beginning there were only complete lattices, and conditionally complete ones were added much later on.

Floris van Doorn (Oct 13 2022 at 14:15):

Yaël Dillies said:

We explicitly prefer ⨆ i ∈ s, f i over Sup (f '' s), though.

In lemma statements about complete lattices I agree, but on the basic plumbing in definitions like pi.has_Sup I think it's weird to define Sup in terms of a more complicated (but equal) operation in the β i.
We probably do (ab?)use the defeq of set.has_Sup though...

Sebastien Gouezel (Oct 13 2022 at 14:15):

⨆ (i : s), f i is good also in conditionally complete lattices, and maybe better defeqwise than Sup (f '' s).

Floris van Doorn (Oct 13 2022 at 14:16):

I think those two are defeq?

Floris van Doorn (Oct 13 2022 at 14:16):

oh no, the former is in terms of set.range...

Yaël Dillies (Oct 13 2022 at 14:16):

No, they are one docs#subtype.exists away from each other.

Sebastien Gouezel (Oct 13 2022 at 18:36):

Eric Wieser said:

The canonical way to view a set as a function is (∈ s)

I did the experiment to change the measure theory folder to replace the defeq abuse s =ᵐ[μ] t with the more correct (∈ s) =ᵐ[μ] (∈ t). You can see the outcome in #16960. Personally, I am not convinced: readability is really worse, and the gain is virtually null (and the linter is not happy). So unless some people insist they like the new version better, I'll just close this in a few days.

Yaël Dillies (Oct 13 2022 at 19:24):

There's always the option of making an abbreviation to turn (∈ s) =ᵐ[μ] (∈ t)into s =ᵐˢ[μ] t (ot somet other notation) and restore readability.

Floris van Doorn (Oct 13 2022 at 20:19):

Oh, I now see that #16960 is related to this thread (I didn't read the whole thread before). I agree that that PR makes the readability worse, but we have been avoiding the set-defeq as much as we could. So I'm not sure if we should go further with it...

Patrick Massot (Oct 13 2022 at 20:22):

The readability loss is really horrible.

Mario Carneiro (Oct 13 2022 at 20:24):

It makes more sense to define another variation on eq_on instead of using these lambdas everywhere

Junyan Xu (Oct 13 2022 at 21:35):

Another systematic abuse is around presieves and sieves in category theory / Grothendieck topology /sites: docs#category_theory.presieve is defined to be set but you can see it's used like a function as in S f in docs#category_theory.presieve.bind. There is even a docs#category_theory.sieve.has_coe_to_fun instance.

There are some implicit arguments involved so maybe you can't directly write ∈ S but it should be possible to define a set_like instance to a sigma type like we did in the subgroupoid PR.

But then you have to write ⟨Y, f⟩ ∈ S instead of just f ∈ S but you may define another notation like f ∈' S that is more succinct.

Bhavik Mehta (Oct 14 2022 at 19:38):

For what it's worth, if someone can make ∈ S work here, then I'm in favour of removing the coe_to_fun and removing the defeq abuse. Alternatively we could change presieves to be phrased in terms of predicates, and enforce set_of

Eric Wieser (Jul 21 2023 at 16:53):

Yaël Dillies said:

There's always the option of making an abbreviation to turn (∈ s) =ᵐ[μ] (∈ t)into s =ᵐˢ[μ] t (ot somet other notation) and restore readability.

I would guess this option is much more viable in lean4?


Last updated: Dec 20 2023 at 11:08 UTC