Zulip Chat Archive

Stream: new members

Topic: example : ¬(p ↔ ¬p)


view this post on Zulip Eduardo Cavazos (Oct 22 2019 at 04:15):

Question posted to stackoverflow:

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

Thanks for any suggestions!

view this post on Zulip Mario Carneiro (Oct 22 2019 at 04:40):

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

view this post on Zulip 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)?

view this post on Zulip Mario Carneiro (Oct 22 2019 at 05:42):

yes

view this post on Zulip Mario Carneiro (Oct 22 2019 at 05:42):

try to prove it

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 22 2019 at 05:49):

It certainly is

view this post on Zulip Johan Commelin (Oct 22 2019 at 05:49):

After all p ↔ ¬ p

view this post on Zulip Johan Commelin (Oct 22 2019 at 05:49):

And you know p

view this post on Zulip Eduardo Cavazos (Oct 22 2019 at 05:53):

Hmm... something like this?

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

view this post on Zulip Johan Commelin (Oct 22 2019 at 05:54):

Does it typecheck? If so, you won.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 22 2019 at 06:05):

@Eduardo Cavazos and here is a golfed version:

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 22 2019 at 08:33):

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

view this post on Zulip Kenny Lau (Oct 22 2019 at 08:33):

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

view this post on Zulip Rob Lewis (Oct 22 2019 at 08:35):

by ifinish solves it without choice.

view this post on Zulip Kenny Lau (Oct 22 2019 at 08:35):

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

view this post on Zulip Rob Lewis (Oct 22 2019 at 08:36):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 22 2019 at 09:13):

It thinks like an undergraduate

view this post on Zulip Rob Lewis (Oct 22 2019 at 09:35):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 22 2019 at 10:35):

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

view this post on Zulip 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