Zulip Chat Archive

Stream: new members

Topic: contradiction question

view this post on Zulip PV (Apr 11 2020 at 23:17):

Curious if you create the following premise so your goal state ends up like:
n : mynat,
hn : n = succ n,
h0 : succ n ≠ 0
⊢ succ n = 0

Is there a way to use the premise h0 and the goal state contradiction statements to return a proof of the goal?

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:18):

you don't need h0 if the other hypotheses are already contradictory

view this post on Zulip Mario Carneiro (Apr 11 2020 at 23:19):

however the proof that n = succ n is false is not completely trivial so you may not have it on mynat. You have to prove it by induction

view this post on Zulip Patrick Stevens (Apr 12 2020 at 07:09):

The exfalso tactic will destroy the goal so that you only have to prove false, if that's what you're asking; but you can't generally take a hypothesis of the form "not A" and a goal of "A", and create a proof. After all, you could prove false that way: take a hypothesis of the form true, and a goal of the form false. If you notice that your goal is incompatible with your hypotheses, you have only two real paths to victory (one of them classically valid and one not): exfalso and prove that your hypotheses are inconsistent, or proof-by-contradiction of assuming the negation of the false goal and then proving that the hypotheses with that extra assumption are inconsistent. (There are niche cases where it's actually easier to prove the false goal from the false assumptions, but in my experience those are rare.)

view this post on Zulip PV (Apr 12 2020 at 14:38):

That makes sense. Still getting used to reading a neq 0 as a = 0 -> false and the use of the exfalso tactic to move along.

Last updated: May 12 2021 at 03:23 UTC