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

TL;DR

• Lean では含意を → で表す。→ は右結合である。
• 含意を使うときは apply、含意を示すときは intro タクティクを使う。

内容

含意の表し方

含意は、命題 $P$ と $Q$ に「$P$ ならば $Q$ が成り立つ」という命題を対応させる関数である。Lean では → で表す。→ は右結合なので、P → Q → R は P → (Q → R) と解釈される。

example (P Q R : Prop) : (P → Q → R) = (P → (Q → R)) := by
  rfl

apply タクティク

数学では、$P\to Q$ が成り立つと分かっていて、示したいことが $Q$ のとき、「よって $P$ を示せばよい」と推論する。Lean ではこの推論に apply を使う。

たとえば h : P → Q があり、ゴールが ⊢ Q のとき、apply h を実行するとゴールが ⊢ P に変わる。さらに hp : P があれば、apply hp でゴールを閉じられる。

example (P Q : Prop) (h : P → Q) (hp : P) : Q := by
  apply h
  apply hp

ただし、この場合は exact を使ったほうが証明が読みやすくなる。

example (P Q : Prop) (h : P → Q) (hp : P) : Q := by
  exact h hp

intro タクティク

数学では、$P\to Q$ を示したいとき、「$P$ を仮定して $Q$ を証明する」方法をよく取る。Lean ではこれに intro を使う。

example (P Q : Prop) (hq : Q) : P → Q := by
  intro hp
  exact hq

キーワード

• Lean
• タクティク