Zulip Chat Archive

Stream: new members

Topic: Exists

Thomas Brooks (Jul 04 2020 at 22:29):

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 :=
        (assume (h:  x, p x  r),
            exists.elim h
                (assume (hx: α) (hpxr: p hx  r),
        (assume (h: ( x, p x)  r),
                (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 (Jul 04 2020 at 22:30):

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

Kevin Buzzard (Jul 04 2020 at 22:31):

This is much easier in tactic mode

Thomas Brooks (Jul 04 2020 at 22:33):

I haven't gotten to tactics yet!

Thomas Brooks (Jul 04 2020 at 22:34):

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

Thomas Brooks (Jul 04 2020 at 22:36):

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 (Jul 04 2020 at 22:36):

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

Thomas Brooks (Jul 04 2020 at 22:45):

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 (Jul 04 2020 at 23:02):

@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 (Jul 04 2020 at 23:21):

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

Kevin Buzzard (Jul 04 2020 at 23:45):

#print prefix exists

Jason Orendorff (Jul 04 2020 at 23:45):

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

Last updated: Dec 20 2023 at 11:08 UTC