An `EmptyCollection` instance for Prop-valued functions

Stream: general

[Oliver Nash]

In various places, but especially in the measure theory library, we abuse definitional equality and regard a set as a function α → Prop. Mostly this is fine but one thing that does not work is the following:

import Mathlib

variable {α : Type _} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}

#check s =ᵐ[μ] ∅ -- failed to synthesize instance EmptyCollection (α → Prop)

[Oliver Nash]

I propose fixing this as follows:

instance PiProp.instEmptyCollection {α : Type _} : EmptyCollection (α → Prop) :=
  ⟨fun _ ↦ False⟩ -- Or even `Set.instEmptyCollectionSet`

#check s =ᵐ[μ] ∅ -- works :-)

[Oliver Nash]

Any objections?

[Eric Wieser]

There was a discussion about =ᵐ[μ] and sets somewhere else, right?

[Eric Wieser]

I assume you don't want to use \bot, which should already work here

[Oliver Nash]

Eric Wieser said:

There was a discussion about =ᵐ[μ] and sets somewhere else, right?

There was a discussion which ultimately resulted in this issue !3#16932 for which the history is here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Diamond.20of.20complete.20boolean.20algebras.20on.20sets

[Oliver Nash]

(I actually plan to fix that issue at some point when I'm feeling patient.)

[Oliver Nash]

Eric Wieser said:

I assume you don't want to use \bot, which should already work here

I hadn't considered this but I'd prefer to use ∅ and it looks like I can unless there's an objection to my proposal here.

[Yury G. Kudryashov]

I think that we should add a notation for docs#Filter.EventuallyEq for sets which unfolds to (· ∈ s) =ᶠ[l] (· ∈ t)

[Yury G. Kudryashov]

And add ⊆ᶠ[l] which unfolds to (· ∈ s) ≤ᶠ[l] (· ∈ t)

[Yury G. Kudryashov]

These should be notations, not (semireducible) definitions so that we can continue using lemmas about EventuallyLE and EventuallyEq.

[Yury G. Kudryashov]

But this should wait till we reopen Mathlib for refactors.

[Eric Rodriguez]

Yury G. Kudryashov said:

But this should wait till we reopen Mathlib for refactors.

this isn't the case yet?

[Oliver Nash]

Is it definitely a win to have more notation? I mean s =ᵐ[μ] t is completely clear already, it's just that we haven't supported it fully.

[Kyle Miller]

I think using sets as functions is a design mistake. Elsewhere we're careful to write (· ∈ s) for s as a function.

[Yury G. Kudryashov]

@Kyle Miller I agree and I'm to blame for introducing this abuse of defeq.

[Yury G. Kudryashov]

@Oliver Nash Empty set is not the only operation. We get similar errors with all set operations.

[Oliver Nash]

Is there a downside to this design decision beyond the burden it creates to ensure that we have definitionally equal constructions on Set α and α → Prop?

[Oliver Nash]

Yury G. Kudryashov said:

Oliver Nash Empty set is not the only operation. We get similar errors with all set operations.

I know.

[Yury G. Kudryashov]

I think that =ᵐˢ or =ˢᵐ is short and readable too.

[Kyle Miller]

Once you accidentally get terms like s x there's no theory about it, and you can't write any simp lemmas to get you out of the situation.

[Yury G. Kudryashov]

Also, Lean 4 simp uses discrimination trees and a similar abuse of defeq in manifolds leads to situations when simp fails to apply a theorem because it is about Prod while the arguments are of type ModelProd.

[Yury G. Kudryashov]

BTW, I think that we should add notation =ˢ for docs#Set.EqOn

[Oliver Nash]

Yury G. Kudryashov said:

I think that =ᵐˢ or =ˢᵐ is short and readable too.

Fair enough; I don't have strenuous objections. But it does seem the same argument could almost be used to justify separate notations for addition on ℤ versus ℚ or something. For me if we add a new notation for this, it's a slight capitulation to the computer. I'd never use it on the blackboard.

[Kyle Miller]

It'd be nice if Set were a structure. One cool thing would be that we could have a CoeFun instance that makes it so s as a function is (· ∈ s)

[Oliver Nash]

With the above remarks in mind, it sounds like my need for:

instance PiProp.instEmptyCollection {α : Type _} : EmptyCollection (α → Prop) := ⟨fun _ ↦ False⟩

will ultimately disappear (maybe soon). Nevertheless, am I right in thinking there is no objection to adding this anyway?

[Yury G. Kudryashov]

@Kyle Miller Though we would need an unexpander to avoid fun x ↦ x ∈ s =ᵐ[μ] fun x ↦ x ∈ t in the info view.

[Kyle Miller]

@Oliver Nash I don't think it's a good idea, because now if you see ∅ you can't be sure whether it's a true Set or a predicate

[Yury G. Kudryashov]

I think that you should write (∅ : Set _) in the RHS.

[Yury G. Kudryashov]

That's what we do for union and intersection.

[Oliver Nash]

OK I give in. Maybe I'm not persuaded but I'm in the minority!

[Yury G. Kudryashov]

Eric Rodriguez said:

Yury G. Kudryashov said:

But this should wait till we reopen Mathlib for refactors.

this isn't the case yet?

We're waiting for official pair of tags on mathlib3 and Mathlib4. We hope to have them today or tomorrow.

[Notification Bot]

María Inés de Frutos Fernández has marked this topic as resolved.

[Notification Bot]

María Inés de Frutos Fernández has marked this topic as unresolved.