isEmpty_subtype

Stream: mathlib4

[Violeta Hernández]

docs#isEmpty_subtype makes it so that for s : Set α, IsEmpty s simplifies to ∀ x, x ∉ s instead of the expected s = Ø.

[Violeta Hernández]

Is this desirable? Or should the simp set be tweaked?

[Kevin Buzzard]

That's a 404 for me, but I guess you could add the lemma saying that the forall statement is true iff s is empty, tag it simp, stick it on a branch, make a PR, mark it draft, get the green tick and then benchmark it to see if it makes things better or worse

[Violeta Hernández]

Had the theorem name wrong, fixed

[Kyle Miller]

Yeah, that seems like a problematic simp lemma. (Do I have it right that there's nonconfluence? If the simp set is nonconfluent, then it ought to be fixed on way or another.)

Maybe it would be better to have IsEmpty (Subtype p) <-> SetOf p = Ø as a simp lemma, which would match up with docs#Set.isEmpty_coe_sort, if it should be a simp lemma at all. Note that Set.isEmpty_coe_sort is not a simp lemma.

A version of isEmpty_subtype that could definitely be a simp lemma would be a conditional version, namely ∀ (x : α), ¬p x -> IsEmpty (Subtype p). This seems like it could be useful, at a bit of cost of having simp trying to discharge this hypothesis.

[Violeta Hernández]

The reason for isEmpty_coe_sort not being simp is that it competes with isEmpty_subtype.

[Violeta Hernández]

I'll try making the former simp and the latter not simp to see what happens

[Violeta Hernández]

#19918

[Violeta Hernández]

The PR now builds. There was barely any breakage, and in fact I was able to make two simp sets smaller.

[Yuyang Zhao]

It took me some time to figure out why #5901 build failed.

[Violeta Hernández]

What happened? Is this a bad simp lemma after all?