Zulip Chat Archive

Stream: general

Topic: Newb question / not-true example in TPIL?


view this post on Zulip Ben Weinstein-Raun (Jun 04 2018 at 03:27):

Hi, I'm a total newb to Lean and to proof assistants generally. I'm working through Chapter 4 of TPIL, and in particular the example statements in 4.4. I haven't been able to prove the last two of them, and I'm beginning to suspect that the last one, at least, is actually false.

example : (∃ x : α, r → p x) ↔ (r → ∃ x : α, p x) := sorry.

If r is false and α is uninhabited, the left side of this equivalence is false while the right side is true, no?

view this post on Zulip Ben Weinstein-Raun (Jun 04 2018 at 03:29):

(sorry if there's a better place to ask this)

view this post on Zulip Simon Hudon (Jun 04 2018 at 03:29):

that's the right place to come

view this post on Zulip Simon Hudon (Jun 04 2018 at 03:31):

I think you may be right

view this post on Zulip Simon Hudon (Jun 04 2018 at 03:33):

As you say, if r is false, the statement reduces to (∃ x, true) ↔ true which is another way of saying that α is inhabited, which does not seem to be an assumption

view this post on Zulip Simon Hudon (Jun 04 2018 at 03:35):

Sorry, I take it back: I just saw variable a : α which means that α is inhabited

view this post on Zulip Ben Weinstein-Raun (Jun 04 2018 at 03:35):

oh, wait, there is a line
variable a : α
further up; I hadn't noticed this. Is that equivalent to an assumption that α is inhabited?

view this post on Zulip Ben Weinstein-Raun (Jun 04 2018 at 03:35):

ah, yeah, sorry about that

view this post on Zulip Simon Hudon (Jun 04 2018 at 03:35):

No worries

view this post on Zulip Ben Weinstein-Raun (Jun 04 2018 at 03:39):

(also, thanks!)

view this post on Zulip Simon Hudon (Jun 04 2018 at 03:39):

:smile: :thumbs_up:


Last updated: May 13 2021 at 06:15 UTC