Leanにおける論理２

前回に引き続き、Lean 4 における論理の証明を学んでいきます。今回は同値・論理積・論理和の三つを取り上げます。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。

同値（↔）

命題 P と Q が同値であるとは、P → Q と Q → P がどちらも成立することを意味します。Lean 4 では ↔ 演算子で表現します。

#eval True ↔ True   -- true
#eval True ↔ False  -- false

constructor タクティク

P ↔ Q を証明するには constructor タクティクを使います。適用すると「P → Q を示す」「Q → P を示す」という二つのゴールに分割されます。各ゴールの開始は ·（\. + Tab）で宣言します。

example (P Q: Prop) (h1 : P → Q) (h2 : Q → P) : P ↔ Q := by
  constructor
  · apply h1
  · apply h2

case mp / case mpr

· の代わりに case mp => と case mpr => を使うことで、どちらのゴールを証明しているかを明示できます。mp（modus ponens 方向）が P → Q、mpr（逆方向）が Q → P に対応します。

example (P Q: Prop) (h1 : P → Q) (h2 : Q → P) : P ↔ Q := by
  constructor
  case mp =>
    apply h1
  case mpr =>
    apply h2

constructor <;> による一括宣言

constructor <;> と書くと、分割された両方のゴールに対して同じタクティクをまとめて適用できます。たとえば、どちらの証明でも最初に intro h が必要な場合は次のように書けます。

-- constructor <;> intro h で両ゴールに一括して intro を適用
example (P Q : Prop) (h1 : P → Q) (h2 : Q → P) : P ↔ Q := by
  constructor <;> intro h
  · exact h1 h
  · exact h2 h

constructor で生成された二つのゴール（P → Q と Q → P）に対して intro h が同時に適用され、それぞれのコンテキストに h が追加されます。繰り返しを減らせるのが便利です。

rw（rewrite）タクティク

rw（rewrite）タクティクを使うと、ゴールを書き換えることができます。仮定 h : P ↔ Q があるとき、rw [h] でゴール中の P を Q に置き換えられます。

-- h : P ↔ Q を使ってゴールの P を Q に書き換える
example (P Q : Prop) (h : P ↔ Q) (hq : Q) : P := by
  rw [h]
  exact hq

上の例では、ゴール P に rw [h] を適用すると Q に書き換わります。そのあと exact hq で閉じることができます。

論理積（∧）

論理積は、二つの命題が同時に成り立つことを表す命題です。Lean 4 では ∧ 演算子で表現します。

P	Q	P ∧ Q
true	true	true
true	false	false
false	true	false
false	false	false

#eval True ∧ True   -- true
#eval True ∧ False  -- false
#eval False ∧ True  -- false
#eval False ∧ False -- false

constructor タクティク

論理積の証明にも constructor タクティクを使います。P ∧ Q のゴールが「P を示す」「Q を示す」の二つに分割されます。

example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  constructor
  · exact hp
  · exact hq

case left / case right

論理積の場合、case 文では left と right を指定します。

example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  constructor
  case left =>
    exact hp
  case right =>
    exact hq

論理和（∨）

論理和は、二つの命題のうち少なくともどちらかが成り立つことを表す命題です。Lean 4 では ∨ 演算子で表現します。

P	Q	P ∨ Q
true	true	true
true	false	true
false	true	true
false	false	false

#eval True ∨ True   -- true
#eval True ∨ False  -- true
#eval False ∨ True  -- true
#eval False ∨ False -- false

left タクティク / right タクティク

論理和 P ∨ Q を証明する場合、left タクティクまたは right タクティクを使います。left は ∨ の左側（P）を証明するときに、right は右側（Q）を証明するときに使います。

-- P ∨ Q を左側（P）で証明する
example (P Q : Prop) (hp : P) : P ∨ Q := by
  left
  exact hp

-- P ∨ Q を右側（Q）で証明する
example (P Q : Prop) (hq : Q) : P ∨ Q := by
  right
  exact hq

cases タクティク（論理和を仮定として使う場合）

論理和を仮定として使うときは、cases タクティクを使います。h : P ∨ Q という仮定に対して cases h with を適用すると、「P が成立する場合（inl）」と「Q が成立する場合（inr）」の二つに分岐して証明を進めることができます。

example (P Q : Prop) (h : P ∨ Q) : Q ∨ P := by
  cases h with
  | inl hp =>
    right
    exact hp
  | inr hq =>
    left
    exact hq

上の例では、P ∨ Q を仮定にして Q ∨ P（順序を逆にした論理和）を証明しています。inl hp では P が得られるので、ゴール Q ∨ P の右側（P）を right で示します。inr hq では Q が得られるので、左側（Q）を left で示します。

まとめ

今回学んだタクティクをまとめます。

論理	記号	証明タクティク	case 名
同値	↔	constructor	mp / mpr
論理積	∧	constructor	left / right
論理和（証明）	∨	left / right	—
論理和（仮定）	∨	cases ... with	inl / inr