## Stream: new members

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

#### 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?

#### 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


#### 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.

#### 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.

#### Patrick Massot (Aug 31 2018 at 07:36):

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

#### Kenny Lau (Aug 31 2018 at 07:42):

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

#### 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')


#### Patrick Massot (Aug 31 2018 at 07:43):

Why don't you like my solution?

#### Johan Commelin (Aug 31 2018 at 07:43):

you might as well use classical

This conclusion doesn't need any hypotheses.

#### 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


#### 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.

#### Andrew Skiba (Aug 31 2018 at 07:48):

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

#### 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)))


#### 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)))


#### Sean Leather (Aug 31 2018 at 07:52):

Are these cries for hhhhhhelp, Kenny? :wink:

#### Kenny Lau (Aug 31 2018 at 07:52):

I just like to name my hypotheses h

#### Sean Leather (Aug 31 2018 at 07:53):

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

#### 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.

#### Sean Leather (Aug 31 2018 at 08:06):

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

#### 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.

#### 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.

#### Patrick Massot (Aug 31 2018 at 09:53):

constructive math is crazy...

#### Bryan Gin-ge Chen (Aug 31 2018 at 13:39):

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

#### 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