矛盾と背理法

by_cases h : P は，命題 P が成り立つ場合と成り立たない場合に分けます． 一般の命題 P : Prop に対する場合分けは，古典論理の排中律に依存します． P が計算で判定可能な命題なら，その判定手続きに基づく場合分けとしても読めます．

example (P : Prop) : P ∨ ¬ P := by
  by_cases h : P
  · left
    exact h
  · right
    exact h

Classical.byContradiction は背理法です． ¬ P → False から P を結論します． これは一般には古典論理の原理です． 構成的に証明したい場面では，¬ P を仮定して False を示す「否定の証明」と区別して使います．

example (P : Prop) (h : ¬¬ P) : P := by
  exact Classical.byContradiction h

否定が量化子の外側にある命題を扱うときも，Core Lean だけで証明できます． たとえば ¬ ∀ n, P n から ∃ n, ¬ P n を得るには，古典論理の背理法を使います． Mathlib では push Not がこの種の変形を自動化してくれますが，ここでは明示的に証明します．

example (P : Nat → Prop) (h : ¬ ∀ n, P n) : ∃ n, ¬ P n := by
  exact Classical.byContradiction (fun hNoExists =>
    h (fun n =>
      Classical.byContradiction (fun hn =>
        hNoExists ⟨n, hn⟩)))

exfalso は，現在のゴールを False に変えます． 矛盾を導けば任意のゴールが閉じる，という規則を使うための tactic です． False.elim を tactic モードで使いやすくしたものと考えるとよいです．

example (P Q : Prop) (hP : P) (hNotP : ¬ P) : Q := by
  exfalso
  exact hNotP hP

contradiction は，コンテキストにある矛盾を探してゴールを閉じます．

example (P Q : Prop) (hP : P) (hNotP : ¬ P) : Q := by
  contradiction