Diamond of complete boolean algebras on sets

Stream: general

[Oliver Nash]

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]

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

[Oliver Nash]

Thanks, I'd be very grateful!

[Yaël Dillies]

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]

@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]

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]

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]

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]

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

[Eric Wieser]

s here is a family of sets

[Eric Wieser]

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

[Oliver Nash]

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]

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

[Oliver Nash]

Yes it does.

[Oliver Nash]

But it's been done.

[Yaël Dillies]

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]

Can you remind me what the notation above unfolds to?

[Eric Wieser]

I'm not familiar with measure theory notation

[Sebastien Gouezel]

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

[Eric Wieser]

What's the declaration behind the notation though?

[Sebastien Gouezel]

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

[Oliver Nash]

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]

I think we should just add the ∈s

[Eric Wieser]

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

[Oliver Nash]

Eric Wieser said:

I think we should just add the ∈s

Can you clarify what this means?

[Eric Wieser]

I mean do what I said in the message above

[Eric Wieser]

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

[Eric Wieser]

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

[Sebastien Gouezel]

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]

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]

What's your full modified version?

[Oliver Nash]

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]

The conclusion needs ∈s too

[Eric Wieser]

As does t, as in my above comment

[Oliver Nash]

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

[Oliver Nash]

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]

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]

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]

It's this failure, right:

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

[Oliver Nash]

(likewise Inf)

[Eric Wieser]

Currently it seems that Sup s on sets is defined as

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

[Eric Wieser]

Whereas on pi types it's

λ (i : α), ⨆ (f : ↥s), ↑f i

[Eric Wieser]

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

[Oliver Nash]

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

[Oliver Nash]

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

[Eric Wieser]

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

[Oliver Nash]

Yes, agreed on both points.

[Sebastien Gouezel]

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]

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

[Oliver Nash]

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]

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]

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]

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]

(same remarks for Infs ofc)

[Floris van Doorn]

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]

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]

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]

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

[Yaël Dillies]

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

[Yaël Dillies]

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

[Sebastien Gouezel]

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]

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

[Sebastien Gouezel]

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]

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]

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

[Floris van Doorn]

I think those two are defeq?

[Floris van Doorn]

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

[Yaël Dillies]

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

[Sebastien Gouezel]

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]

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]

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]

The readability loss is really horrible.

[Mario Carneiro]

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

[Junyan Xu]

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]

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]

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?