ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発 › Lean における同値性

TL;DR

• 命題 $P$ と $Q$ が同値であるとは、$P\to Q$ と $Q\to P$ がともに成り立つことで、Lean では ↔ で表す。
• 同値を示すときは constructor で 2 つのゴールに分け、仮定にある同値は rw で書き換えに使う。

内容

同値の表し方

命題 $P$ と $Q$ が同値であるとは、$P\to Q$ と $Q\to P$ がともに成り立つことを指す。Lean では同値を ↔ で表す。なお、Lean では同値な命題を基本的に区別しない。これを命題外延性と呼ぶ。

constructor タクティク

ゴールが $P⟺Q$ のときは、$⊢P\to Q$ と $⊢Q\to P$ の 2 つのゴールを示せばよい。このためのタクティクが constructor である。· は、ゴールが複数あるときに、それぞれのゴールの証明を見やすく分けるための記法である。

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

タクティク結合子 <;>

constructor を使うと、続けて intro を使うことが多い。

example (P Q : Prop) (hq : Q) : (Q → P) ↔ P := by
  constructor
  -- (Q → P) → P を証明する
  case mp =>
    intro h
    exact h hq
 
  -- P → Q → P を証明する
  case mpr =>
    intro hp hq
    exact hp

このような場合は、タクティク結合子 <;> を使うと記述量を減らせる。<;> は、直前のタクティクで生まれたすべてのゴールに、後ろのタクティクを適用する。

example (P Q : Prop) (hq : Q) : (Q → P) ↔ P := by
  constructor <;> intro h
  case mp =>
    exact h hq
 
  case mpr =>
    intro hq
    exact h

rw タクティク

仮定に同値が含まれるときは、rw を使って同値なものに書き換えられる。たとえば h : P ↔ Q が仮定にあれば、rw [h] で $P$ を $Q$ に書き換えられる。

example (P Q : Prop) (h : P ↔ Q) (hq : Q) : P := by
  -- P ↔ Q が仮定にあるので、P の代わりに Q を示す
  rw [h]
  exact hq

逆に $Q$ を $P$ に書き換えるときは、← を付けて rw [← h] と書く。

example (P Q : Prop) (h : P ↔ Q) (hp : P) : Q := by
  rw [← h]
  exact hp

キーワード

• Lean
• タクティク
• 命題外延性