Zulip Chat Archive

Stream: new members

Topic: Exists


view this post on Zulip 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 :=
    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)))

view this post on Zulip Reid Barton (Jul 04 2020 at 22:30):

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

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 22:31):

This is much easier in tactic mode

view this post on Zulip Thomas Brooks (Jul 04 2020 at 22:33):

I haven't gotten to tactics yet!

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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....

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Thomas Brooks (Jul 04 2020 at 23:21):

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

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 23:45):

#print prefix exists

view this post on Zulip Jason Orendorff (Jul 04 2020 at 23:45):

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


Last updated: May 08 2021 at 03:17 UTC