exists_prop

Stream: mathlib4

[Yaël Dillies]

Now that ∃ a ∈ s, p a means ∃ a, a ∈ s ∧ p a instead of ∃ a (ha : a ∈ s), p a, I wonder: Is it possible to have both the convenience of independent types and keep the parallel with forall?

In forall land, we have that ∀ h : p, q is the same as p → q. So back to exists land, we could define p ∧ q as ∃ h : p, q. Constructing/destructing an and would be done the same way, but this time ∃ a, a ∈ s ∧ p a is the same as ∃ a (ha : a ∈ s), p a, so there's no choice to be made between the old and new spelling!

[Yaël Dillies]

The drawbacks I see with this approach are

• It might lead to leakage, especially because and is such a common construct.
• I don't know how to geth.1 and h.2 working on h : p ∧ q. But hopefully a syntax/dot projection expert will.

[Eric Wieser]

A key difference here is you can't write Nat ∧ True but you can write ∃ n : Nat, True

[Eric Wieser]

So this is more than just merging dependent and non-dependent cases

[Yaël Dillies]

Sure, but you can bake such a restriction in the definition/notation, just as ite is a special case of dite.

[Eric Wieser]

But the reason you can't use .1 and .2 on exists but can on and is the fact that the formers arguments lives in Prop

[Yaël Dillies]

Sure:

variables {p q : Prop}

def new_and (p q : Prop) : Prop := ∃ h : p, q

lemma new_and.left : new_and p q → p := λ ⟨hp, hq⟩, hp
lemma new_and.right : new_and p q → q := λ ⟨hp, hq⟩, hq

[Yaël Dillies]

Now the question is how can you hack the .1/.2 notation to work where it shouldn't.

[Eric Wieser]

I also think this is only justifiable if we did the same thing to prod and sigma

[Yaël Dillies]

prod and sigma don't happen to stand in the middle of a Lean 3 vs 4 notation war, though.

[Floris van Doorn]

What are the advantages of defining p ∧ q as ∃ h : p, q? Is the disadvantage of the current situation only that it breaks some proofs during mathport?

[Mario Carneiro]

FYI .1 and .2 notation works on exists:

example (h : ∃ _x: True, True) : True ∧ True := ⟨h.1, h.2⟩

[Mario Carneiro]

(this was actually a source of unsoundness at one point, since it worked regardless of whether the first thing is a Prop. Now it checks that the projection is legal)

[Eric Wieser]

There's an easier "fix" to the current problem than the one that Yael is suggesting, and that's to have mathport output ∃ a, ∃ (ha : a ∈ s), p a instead of ∃ a (ha : a ∈ s), p a

[Eric Wieser]

Is there a zulip thread anywhere that discusses why the semantics of ∃ a (ha : a ∈ s), p a was changed in the first place?

[Mario Carneiro]

What is the difference between those options?

[Mario Carneiro]

they should be handled the same

[Eric Wieser]

∃ a (ha : a ∈ s), p a means ∃ a, a ∈ s ∧ p a in Lean 4

[Eric Wieser]

Maybe this is just mathlib?

[Eric Wieser]

Ah, it's just ∃ a ∈ s, p a

[Eric Wieser]

The precise claim is

import Mathlib.Data.Set.Basic

example (s : Set ℕ) (p : ℕ → Prop) :
  (∃ a ∈ s, p a) ↔ ∃ (a : ℕ) (ha : a ∈ s), p a := Iff.rfl -- fails

[Mario Carneiro]

I don't think there was a specific discussion about this, but it was a long requested feature, and mathlib has simp lemmas to rewrite this, and use rewrites to the exists-and form, so when the opportunity to actually do something about it came up we did

[Eric Wieser]

Arguably it would have made the port easier not to do it until after we were done, but I guess it's only a minor annoyance

[Eric Wieser]

Relatedly, is it deliberate that ∃ a (ha : a ∈ s), p a notation is no longer legal?

[Mario Carneiro]

No, it is an unfortunate side effect of the fact that binder predicates are not supported by the syntax defined in core. You can get the multiple binder syntax using \exists\0

[Mario Carneiro]

actually, I guess your example isn't even about binder predicates. Yes binders in lean 4 are way overcomplicated and it made my life miserable when generating them in mathport