contrapose

contrapose は対偶を取るタクティクです。

ローカルコンテキストに h : P という仮定があるときに contrapose h を実行すると、ゴールの否定がローカルコンテキストに追加されて、同時にゴールが ⊢ ¬ P に変わります。

import Mathlib.Tactic

variable {f : Int → Int} {a b : Int}

/-- 自前で定義した単調性 -/
def MyMonotone (f : Int → Int) : Prop :=
  ∀ ⦃a₁ a₂⦄, a₁ ≤ a₂ → f a₁ ≤ f a₂

example (h : MyMonotone f) (h' : f a < f b) : a < b := by
  -- 対偶をとる
  contrapose h'

  -- ゴールと仮定が否定になって入れ替わる
  show ¬f a < f b

  simp_all only [not_lt]
  apply h
  assumption

contrapose!

contrapose! は、対偶をとった後に簡略化を実行します。

example (h : MyMonotone f) (h' : f a < f b) : a < b := by
  -- 対偶をとる
  contrapose! h'

  -- 不等号の否定を逆向きの不等号に簡略化してくれる
  show f b ≤ f a

  apply h
  assumption