# Zulip Chat Archive

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

?

#### Mario Carneiro (Oct 22 2019 at 05:42):

yes

#### Mario Carneiro (Oct 22 2019 at 05:42):

try to prove it

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

yes

try to prove it

Well, I can start with this:

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

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

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, contradiction }, 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))) (decidable.by_contradiction (λ (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`

.

#### Mario Carneiro (Oct 22 2019 at 09:13):

It thinks like an undergraduate

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

It thinks like an undergraduate

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.

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

OK so I occasionally write a slightly sarcastic comment in the margin as well.

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

It's interesting that I still vividly remember figuring out myself that this was the correct way to think about every problem, as a first year undergraduate. As a result I rejected constructivism at 18 (without even understanding what this meant) and hence this is why I have very little feeling for it.

Last updated: May 17 2021 at 21:12 UTC