contradiction

矛盾からはどんな命題でも証明することができます．これを爆発律(principle of explosion)と呼びますが，contradiction は，この爆発律を使ってゴールを閉じるタクティクです．

ローカルコンテキストに P と ¬ P が同時にあるなど，矛盾した状況にあるときにゴールを閉じます．

import Mathlib.Algebra.Algebra.Basic -- `not_lt` などが使えるようにする

variable (P Q : Prop)

-- `False`
example (h : False) : P := by contradiction

-- 明らかに偽な等式
example (h : 2 + 2 = 3) : P := by contradiction

-- 明らかに偽な等式
example (x : Nat) (h : x ≠ x) : P := by contradiction

-- 矛盾する仮定
example (hP : P) (hnP : ¬ P) : Q := by contradiction

爆発律を利用するタクティクには他に exfalso もありますが，あちらはゴールを False に書き換えるだけで，ゴールを閉じるところまでは行いません．

補足

以下の例では，contradiction がいかにも通りそうに見えるのですが，通りません．contradiction にはあまり強力な前処理は備わっていないので，注意が必要です．

variable (n m : ℕ)

example (hl : n ≤ m) (hg : m < n) : False := by
  -- 明らかに矛盾に見えるが， 通らない
  fail_if_success contradiction

  -- 通らない理由は， `n ≤ m` が `¬ m < n` を意味することを
  -- `contradiction` は知らないから．

  -- 次のようにして教えてあげると…
  have := hl.not_lt

  -- `contradiction` が通るようになる
  contradiction