prove ¬(p ↔ ¬p) without classical

Stream: new members

[Andrew Skiba]

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]

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]

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]

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]

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

[Kenny Lau]

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

[Sean Leather]

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]

Why don't you like my solution?

[Johan Commelin]

you might as well use classical

This conclusion doesn't need any hypotheses.

[Kenny Lau]

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]

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

[Andrew Skiba]

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

[Kenny Lau]

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]

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]

Are these cries for hhhhhhelp, Kenny? :wink:

[Kenny Lau]

I just like to name my hypotheses h

[Sean Leather]

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

[Andrew Skiba]

@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]

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

[Sean Leather]

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]

@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]

constructive math is crazy...

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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