Zulip Chat Archive

Stream: new members

Topic: prove ¬(p ↔ ¬p) without classical


view this post on Zulip Andrew Skiba (Aug 31 2018 at 07:07):

The examples at the end of chapter 3 of tutorial "Theorem proving in Lean" are very easy, except the one in subj. If I try to construct it as is, I have to construct false from two functions, which I can get by iff.mp and iff.mpr - but I have no objects to apply these functions. I found propext constant, which allowed me to convert iff to an equality of p = ¬p, but I don't see how to prove (p = ¬p) → false. In Idris language such proofs are built by "impossible" keyword, but I cannot find anything similar in Lean. Am I missing something basic?

view this post on Zulip Sean Leather (Aug 31 2018 at 07:19):

Here's what I came up with:

example {p : Prop} [h : decidable p] (q : p  ¬p) : false :=
match h with
| is_true  p  := iff.mp q p p
| is_false np := np (iff.mpr q np)
end

view this post on Zulip Sean Leather (Aug 31 2018 at 07:26):

Perhaps the key to remember here is that ¬ p means p → false, so both iff.mp q p : p → false and np : p → false. Then you just have to fill in the p.

view this post on Zulip Andrew Skiba (Aug 31 2018 at 07:28):

Is not the idea of not using classical that I cannot prove by cases? I'm still at the beginning of the tutorial and did not learn what is decidable, but it looks too similar to excluded middle. I suppose it should also allow to prove ¬¬p → p which should not work in constructive reasoning.

view this post on Zulip Patrick Massot (Aug 31 2018 at 07:36):

https://github.com/leanprover/lean/blob/master/library/init/logic.lean#L343

view this post on Zulip Kenny Lau (Aug 31 2018 at 07:42):

@Sean Leather if you use decidable you might as well use classical

view this post on Zulip Sean Leather (Aug 31 2018 at 07:43):

True. Attempt # 2:

example {p : Prop} (q : p  ¬p) : false :=
have h' : ¬p, from λ h, (iff.mp q h) h,
h' (iff.mpr q h')

view this post on Zulip Patrick Massot (Aug 31 2018 at 07:43):

Why don't you like my solution?

view this post on Zulip Johan Commelin (Aug 31 2018 at 07:43):

you might as well use classical

This conclusion doesn't need any hypotheses.

view this post on Zulip Kenny Lau (Aug 31 2018 at 07:44):

example {p : Prop} (q : p  ¬p) : false :=
q.1 (q.2 $ λ H, q.1 H H) (q.2 $ λ H, q.1 H H)

example {p : Prop} (q : p  ¬p) : false :=
(λ H, q.1 H H) $ q.2 $ λ H, q.1 H H

view this post on Zulip Sean Leather (Aug 31 2018 at 07:46):

@Kenny Lau I was trying to avoid “shortcuts” like .1 and $, which may not have been covered, yet.

view this post on Zulip Andrew Skiba (Aug 31 2018 at 07:48):

Thanks, guys! Excellent examples, will try to understand where did I miss the point.

view this post on Zulip Kenny Lau (Aug 31 2018 at 07:48):

example {p : Prop} : ¬(p  ¬p) :=
λ q, iff.rec_on q (λ h1 h2, h1 (h2 (λ H, h1 H H)) (h2 (λ H, h1 H H)))

view this post on Zulip Kenny Lau (Aug 31 2018 at 07:51):

example {p : Prop} : ¬(p  ¬p) :=
assume q : p  ¬p, iff.rec_on q
(assume h1 : p  ¬p,
 assume h2 : ¬p  p,
 h1 (h2 (λ H, h1 H H)) (h2 (λ H, h1 H H)))

view this post on Zulip Sean Leather (Aug 31 2018 at 07:52):

Are these cries for hhhhhhelp, Kenny? :wink:

view this post on Zulip Kenny Lau (Aug 31 2018 at 07:52):

I just like to name my hypotheses h

view this post on Zulip Sean Leather (Aug 31 2018 at 07:53):

Too bad there's only one h in the Latin alphabet.

view this post on Zulip Andrew Skiba (Aug 31 2018 at 08:01):

@Patrick Massot I did like your solution, because the tutorial only states that there are implementations of these proofs in the standard library, but does not mention where to find them. But the easiest to follow is Sean's one, because I can see what I missed: although it's impossible to construct a p, it is still possible to construct ¬p, and the last line is trivial. I still did not completely understand, how it's done by λ h, (iff.mp q h) h, but it's a small piece to resolve already.

view this post on Zulip Sean Leather (Aug 31 2018 at 08:06):

@Andrew Skiba You know that λ and assume are the same?

view this post on Zulip Sean Leather (Aug 31 2018 at 08:09):

When looking again at Theorem Proving in Lean, I realized that it mostly used assume. I use λ more myself, since it's shorter.

view this post on Zulip Andrew Skiba (Aug 31 2018 at 09:52):

@Andrew Skiba You know that λ and assume are the same?

Sure, this one is clear. I missed another point: although it's impossible to construct p from ¬¬p without em, it is easy to construct ¬p from ¬¬¬p. This is the key to solving this exercise.

view this post on Zulip Patrick Massot (Aug 31 2018 at 09:53):

constructive math is crazy...

view this post on Zulip Bryan Gin-ge Chen (Aug 31 2018 at 13:39):

This problem seems to be a fairly popular question here 1 2.

view this post on Zulip Kevin Buzzard (Aug 31 2018 at 13:53):

Yeah, for some reason it's tripping up a lot of people working through TPIL. We need a FAQ!


Last updated: May 16 2021 at 05:21 UTC