## Stream: new members

### Topic: example : ¬(p ↔ ¬p)

#### Eduardo Cavazos (Oct 22 2019 at 04:15):

Question posted to stackoverflow:

https://stackoverflow.com/q/58496954/268581

Thanks for any suggestions!

#### Mario Carneiro (Oct 22 2019 at 04:40):

are you sure you can't prove the precondition of hppf2?

#### Eduardo Cavazos (Oct 22 2019 at 04:49):

are you sure you can't prove the precondition of hppf2?

Hi @Mario Carneiro !

Given what is shown on the question so far:

example : (p ↔ (p → false)) → false :=

(assume hppf : (p ↔ (p → false)),

have hppf1 : p → (p → false), from iff.elim_left hppf,
have hppf2 : (p → false) → p, from iff.elim_right hppf,

)


by "precondition of hppf2", I'm guessing you mean: (p → false)?

yes

try to prove it

#### Eduardo Cavazos (Oct 22 2019 at 05:47):

yes

try to prove it

    (assume hp : p, ...)


but then I'd have to have a way to generate a value of type false. It's not clear how to do so.

It certainly is

#### Johan Commelin (Oct 22 2019 at 05:49):

After all p ↔ ¬ p

#### Johan Commelin (Oct 22 2019 at 05:49):

And you know p

#### Eduardo Cavazos (Oct 22 2019 at 05:53):

Hmm... something like this?

(assume hp : p, false.elim ((hppf1 hp) hp))

#### Johan Commelin (Oct 22 2019 at 05:54):

Does it typecheck? If so, you won.

#### Eduardo Cavazos (Oct 22 2019 at 06:02):

This seems to typecheck:

example : (p ↔ (p → false)) → false :=

(assume hppf : (p ↔ (p → false)),

have hppf1 : p → (p → false), from iff.elim_left hppf,
have hppf2 : (p → false) → p, from iff.elim_right hppf,

have hpf : (p → false), from (assume hp : p, ((hppf1 hp) hp)),

have hp : p, from (hppf2 hpf),

(hppf1 hp) hp)


#### Johan Commelin (Oct 22 2019 at 06:03):

Here's my version:

example (p : Prop) : ¬(p ↔ ¬p) :=
begin
assume H,
have hp : p := H.mpr (λ hp, _),
all_goals
{ have hp_copy := hp,
rw H at hp_copy,
end


#### Johan Commelin (Oct 22 2019 at 06:05):

@Eduardo Cavazos and here is a golfed version:

example (p : Prop) : ¬(p ↔ ¬p) :=
by finish


#### Eduardo Cavazos (Oct 22 2019 at 06:08):

@Johan Commelin ,

Your earlier hint helped me, thank you!

Here I was aiming for a solution that doesn't use the techniques mentioned in section 3.5 "Classical Logic". Indeed, exercise 3.7.2 asks for this.

#### Eduardo Cavazos (Oct 22 2019 at 06:15):

Thank you @Mario Carneiro! Your hint along with Johan's helped me come up with something that appears to work.

#### Kevin Buzzard (Oct 22 2019 at 08:33):

Doesn't finish use classical stuff? Someone should check the axioms used in that proof

#### Kenny Lau (Oct 22 2019 at 08:33):

unfortunately we do not have an intuitionistic 0th order logic automator yet

#### Rob Lewis (Oct 22 2019 at 08:35):

by ifinish solves it without choice.

#### Kenny Lau (Oct 22 2019 at 08:35):

oh what it's there now! oh how fast time flies

#### Rob Lewis (Oct 22 2019 at 08:36):

I think the i versions of the finish family have been there since the beginning, no?

#### Chris Hughes (Oct 22 2019 at 09:08):

import tactic.finish

lemma X (p : Prop): ¬(p ↔ ¬ p) := by ifinish
#print X
/-
λ (p : Prop),
eq.mpr
(id
(eq.trans ((λ (a a_1 : Prop) (e_1 : a = a_1), congr_arg not e_1) (p ↔ ¬p) false (propext (iff_not_self p)))
(propext not_false_iff)))
(λ (a : ¬true), (λ (p : Prop) (a : ¬true), false.rec false (false_of_true_eq_false (eq_false_intro a))) p a))
-/


I like how the proof term uses decidable.by_contradiction to prove true.

#### Rob Lewis (Oct 22 2019 at 09:35):

Yeah, that's a very long way to write (iff_not_self p).1.

#### Kevin Buzzard (Oct 22 2019 at 10:34):

I explicitly tell the maths UGs here that proof by contradiction is the most powerful way to prove P -> Q because you get to assume both P and not Q so you have a lot to play with. As a consequence I've been marking perfectly constructive-doable scripts last weekend, with P -> Q proofs of the form "Assume P. Assume for a contradiction not Q. Now here's a proof of Q. But not Q! Contradiction!". I just give them full marks, it's my job to train people to think this way.