contradiction question

Stream: new members

[PV]

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?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Stevens]

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

[PV]

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.