Exists elaboration and bUnion

Stream: mathlib4

[Anatole Dedecker]

As you may now, ∃ x ≤ y, p x now elaborates as ∃ x, x ≤ y ∧ p x. While this is super nice for readability, it causes some problems when mixed with all of our other double binders. For example, the proof of docs#set.mem_accumulate is no longer a direct appication of docs#set.mem_Union₂. Is there any plan to mitigate that?

[Anatole Dedecker]

One possible solution there is to use the bunionᵢ/unionᵢ₂ distinction to make the difference, but that requires more care in the way we name lemmas (e.g docs#set.mem_Union₂ and docs#set.mem_bUnion are not the same)

[Kevin Buzzard]

I had heard that this change had been made -- is it in core Lean or mathlib? Definitely "exists x, exists (h : x <= y)" is more confusing but do we want to make the refactor now or do we want to put it off?

[Eric Wieser]

This doesn't change the meaning of ⋃ x ≤ y, s x does it?

[Kevin Buzzard]

That's defined in mathlib and as far as I can see it was faithfully ported (I was looking at this recently but I don't really understand notation3)

[Anatole Dedecker]

Eric Wieser said:

This doesn't change the meaning of ⋃ x ≤ y, s x does it?

No and that is precisely the problem, because docs4#set.mem_unionᵢ₂ gives nested exists intead of ∃ x ≤ y, ...

[Eric Wieser]

Right, and presumably the problem is that that lemma is supposed to be rfl?

[Anatole Dedecker]

No it was never rfl I think

[Eric Wieser]

Can you replace your doc links above with manual ones? Zulip doesn't like the names

[Anatole Dedecker]

Sorry. In Lean3 this is https://leanprover-community.github.io/mathlib_docs/data/set/lattice.html#set.mem_Union%E2%82%82 and in Lean4 it's not yet in the docs but in the source it's https://github.com/leanprover-community/mathlib4/blob/ea82bbc6dbcd23f2f29bdf7715f6ced3d0e9e9c5/Mathlib/Data/Set/Lattice.lean#L150

[Anatole Dedecker]

It's not rfl because indexed union is defined as indexed sup which is the sup of the image

[Eric Wieser]

So I guess the question becomes "should mathport translate to the defeq thing, or the most similar syntax which might not have the same meaning any more"

[Anatole Dedecker]

Yes if by "the defeq thing" you mean the nested existential vs "exists+and" (because iirc we purposefully traded the bad-defeq of indexed union with the defeq between union and sup, so this one should be kept as is)

[Mario Carneiro]

I don't think that this is a mathport problem. Mathport should definitely be using the thing with the similar syntax; the question is whether the similar syntax should be defeq to what it was in lean 3

[Mario Carneiro]

As I've said elsewhere, I don't think mathport should ever try to write the ugly thing to make things typecheck, since then people won't even notice the regression. Mathport could add those noisy warnings, but they have a tendency to confuse people or be ignored and they generally don't have the desired effect compared to a manually written Porting note

[Reid Barton]

Is there a lemma that rewrites the new desugaring of e.g. ∃ x ≤ y, p x to the old one?

[Reid Barton]

aha, exists_prop but I need to simp_rw it of course