Proving contradictions

Stream: new members

[Moti Ben-Ari]

The following proof is accepted but tauto seems to be too strong a tactic for a simple contradiction. contradiction h2 is what I want but it works only between two hypotheses and not between a hypothesis and a goal. Are there any other options?

theorem T1 (A : Prop) : (¬A → A) → A := by
  intro h1
  by_contra h2
  apply h2
  tauto
  done

Another proof would have

contrapose h1

as the second line. I expected to get ¬A →¬¬A but instead got ¬(¬A→A). Why? Is there any way to get from h1 to ¬A →¬¬A?

[Alex J. Best]

Your #mwe has no imports, are you using Mathlib?

[Alex J. Best]

import Mathlib
theorem T1 (A : Prop) : (¬A → A) → A := by
  intro h1
  by_contra h2
  apply h2
  apply h1
  exact h2

is a direct proof

[Alex J. Best]

You can use contrapose! to push the negation inwards. under the hood this calls push_neg

[Moti Ben-Ari]

Alex J. Best said:

Your #mwe has no imports, are you using Mathlib?

Yes, sorry, I used import Mathlib.Tactic.

I see that contrapose! works though I would prefer to simply replace a hypothesis by its contrapositive.

[Alex J. Best]

If h is a proof of P -> Q then mt h is the proof of not Q -> not P, I guess we dont have a tactic for exactly that because the term is so short!