existential binding

Stream: mathlib4

[Jireh Loreaux]

In mathlib4#993 I ran into an issue which seems like a bug. The statement of SetLike.exists had massaged from ∃ x ∈ p, q ⟨x, ‹_›⟩ to ∃ (x : B) (h : x ∈ p), q ⟨x, ‹_›⟩. The former worked in Lean 3 (and it expands to the latter).

[Jireh Loreaux]

@Scott Morrison do you know what the expected behavior is here?

[Scott Morrison]

As far as I'm aware we aspire in mathport to translate from ∃ x ∈ p to ∃ (x : B) (h : x ∈ p), but don't always succeed, and don't currently have support for the former in lean4/mathlib4.

[Mario Carneiro]

It's rather the opposite: mathport will expand all binders by default but it tries to use the existing binder collection support where possible for things like exists

[Mario Carneiro]

import Std
#check ∀ s, ∃ x ∈ s, x = x

[Scott Morrison]

Indeed, grepping for ∃.*:.*∈ turns up less than I remembered, and all the ones I looked at are necessary.

[Mario Carneiro]

The reason why the original example doesn't work is because ∃ x ∈ p, q x is now sugar for ∃ x, x ∈ p /\ q x, not ∃ x, ∃ h : x ∈ p, q

[Winston Yin]

Why was this syntactic sugar changed from mathlib3 to 4? I imagine it’ll break a lot of proofs during porting.

How will Lean elaborate ∃ (x : A) (p x) (y : B) (q y), r x y now? Will it be ∃ (h : p x) or p x ∧ ...?

[Yaël Dillies]

Hmm, this is a bit annoying indeed, because there are some proofs that rely on swapping pairs of existential quantifiers.