Exists

Stream: new members

[Thomas Brooks]

Hi, I'm working through the documentation and exercises and I'm stuck on 4.4 (existential quantifier). I thought I could use exists.elim to go from \exists (x: \alpha), p x to x but I get a type error since x is not a Prop. I seem to need this to prove the reverse direction of the exercise example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r. Any guidance? My full attempt is:

example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
    iff.intro
        (assume (h: ∃ x, p x ∧ r),
            exists.elim h
                (assume (hx: α) (hpxr: p hx ∧ r),
                    (and.intro
                        (exists.intro
                            hx
                            hpxr.left)
                        hpxr.right)))
        (assume (h: (∃ x, p x) ∧ r),
            exists.intro
                (exists.elim h.left
                    (assume (hx: α) (hpx: p hx),
                        hx)) -- Problem here!! has type Π (hx : α), p hx → α : Type
                (exists.elim h.left
                    (assume (hx: α) (hpx: p hx),
                        show p hx ∧ r, from and.intro hpx h.right)))

[Reid Barton]

You should use exists.elim while your goal is still a Prop.

[Kevin Buzzard]

This is much easier in tactic mode

[Thomas Brooks]

I haven't gotten to tactics yet!

[Thomas Brooks]

@Reid Barton I'm not sure what you mean. Is exists.elim not appropriate here? Is there an alternative?

[Thomas Brooks]

And on this topic, how can I view everything in a namespace? Like to look at all everything that is exists.something to see if something fits my needs.

[Thomas Brooks]

Oh wait, I think I understand now. I should use exist.elim outside of the exists.intro....

[Thomas Brooks]

That fixed it, thanks for the help. So is there no way to get (\exists x: \alpha, p x) -> \alpha? I would have assumed that could be done

[Kyle Miller]

@Thomas Brooks It's sort of a coherence issue. You need to choose an term of \alpha in a consistent way so that substitution/rewriting works. One thing to think about is that, since every pair of proofs of a Prop are equal, you can't just take a proof ⟨x, h⟩ of existence and map it to x. What would you do for ⟨x', h'⟩? You'd need to ensure that whatever you did wouldn't give you the absurd conclusion that x = x'.

The library has classical.some to "give" you such a term (noncomputably). It uses Lean's version of the axiom of choice.

[Thomas Brooks]

@Kyle Miller That makes sense, thanks for the explanation!

[Kevin Buzzard]

#print prefix exists

[Jason Orendorff]

#print prefix is so darn useful, it should be mentioned earlier in the book