example : ¬(p ↔ ¬p)

Stream: new members

[Eduardo Cavazos]

Question posted to stackoverflow:

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

Thanks for any suggestions!

[Mario Carneiro]

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

[Eduardo Cavazos]

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]

yes

[Mario Carneiro]

try to prove it

[Eduardo Cavazos]

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]

It certainly is

[Johan Commelin]

After all p ↔ ¬ p

[Johan Commelin]

And you know p

[Eduardo Cavazos]

Hmm... something like this?

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

[Johan Commelin]

Does it typecheck? If so, you won.

[Eduardo Cavazos]

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]

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]

@Eduardo Cavazos and here is a golfed version:

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

[Eduardo Cavazos]

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

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

[Kevin Buzzard]

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

[Kenny Lau]

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

[Rob Lewis]

by ifinish solves it without choice.

[Kenny Lau]

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

[Rob Lewis]

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

[Chris Hughes]

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]

It thinks like an undergraduate

[Rob Lewis]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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.