Contrapositive theorem

Stream: lean4

[Omnikar]

What is the name of the theorem for (p → q) → ¬q → ¬p?

[Scott Morrison]

import Mathlib.Logic.Basic

example : (p → q) → (¬q → ¬p) := Function.mt

[Omnikar]

What does mt stand for?

[Mac Malone]

@Omnikar modus tollens

[Jireh Loreaux]

Scott Morrison said:

import Mathlib.Logic.Basic

example : (p → q) → (¬q → ¬p) := Function.mt

Scott, I think you mean:

import Mathlib.Tactic

example : (p → q) → (¬q → ¬p) := by exact? -- Try this: Function.mt

[Jireh Loreaux]

Omnikar, exact? is a tactic that searches the library for the lemma that closes the goal.

[Scott Morrison]

Haha!!! I promise I tried that (aiming to post that was why I copied and pasted into a new window!) but mysteriously it didn't work for me. :-)

[Jireh Loreaux]

I didn't try it, so maybe it wouldn't have worked for me either!

[Kevin Buzzard]

It doesn't work for me either:

import Mathlib.Tactic

example : (p → q) → (¬q → ¬p) := by exact?
/-
`exact?` could not close the goal. Try `apply?` to see partial suggestions.
-/

@David Renshaw can you do your black magic again?

[David Renshaw]

weird. If I do

set_option trace.Tactic.librarySearch.lemmas true in
example : (p → q) → (¬q → ¬p) := by
  exact?

then I see both mt and Function.mt show up as candidates:

[Tactic.librarySearch.lemmas] Candidate library_search lemmas:
    [(mt, ),
     (asymm, ),
     (irrefl, ),
     (Iff.not, mp),
     (Not.imp, ),
     (Iff.not, mpr),
     (asymm_of, ),
     (not_congr, mpr),
     (imp_false, mp),
     (not_congr, mp),
     (irrefl_of, ),
     (Not.intro, ),
     (Eq.mpr_not, ),
     (Function.mt, ),
...

[David Renshaw]

but for some reason neither is selected