Zulip Chat Archive

Stream: mathlib4

Topic: Exists elaboration and bUnion


Anatole Dedecker (Dec 24 2022 at 22:32):

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 (Dec 24 2022 at 22:34):

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 (Dec 24 2022 at 22:45):

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 (Dec 24 2022 at 22:47):

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

Kevin Buzzard (Dec 24 2022 at 23:12):

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 (Dec 24 2022 at 23:46):

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 (Dec 24 2022 at 23:48):

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

Anatole Dedecker (Dec 24 2022 at 23:49):

No it was never rfl I think

Eric Wieser (Dec 24 2022 at 23:49):

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

Anatole Dedecker (Dec 24 2022 at 23:52):

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 (Dec 24 2022 at 23:53):

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

Eric Wieser (Dec 24 2022 at 23:54):

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 (Dec 24 2022 at 23:57):

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 (Dec 25 2022 at 00:34):

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 (Dec 25 2022 at 00:37):

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 (Jan 02 2023 at 19:48):

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

Reid Barton (Jan 02 2023 at 19:50):

aha, exists_prop but I need to simp_rw it of course


Last updated: Dec 20 2023 at 11:08 UTC