Lean4 学習

Lean が気になっているので Theorem Proving in Lean 4 の Propositions and Proofs にある演習問題を解いた。プログラムによる定理証明に触れるのは初なので、時々型を定理だと認識できなくなって迷走してしまうなど苦労した。

Lean4 が気になっている理由としては

• 定理証明支援系で堅牢なソフトウェアかけるんじゃないかなという期待
• Lean4 が関数型言語 + 定理証明支援系 という部分

定理証明支援系の使用例を調べてみたが、今回の学習からどう繋がっていくかイメージがまだついていない

• Hyper-V, Ironclad (契約管理？), ... など: https://leanprover.github.io/presentations/20150717_CICM/#/sec-6
• 自動運転の安全性: https://www.nii.ac.jp/news/release/2022/0707.html
• 例としてC言語コンパイラCompCert、オペレーティングシステムseL4が紹介されている: https://note.com/morikita/n/nf45b6e44964f
  • seL4 の開発で定理証明支援系によりコスト削減できたみたいな記事をどこかで見たが見失った...

問題を載せることに関しては Apache License 2.0 のため大丈夫な認識

以下

variable (p q r : Prop)

-- commutativity of ∧ and ∨
example : p ∧ q ↔ q ∧ p := Iff.intro
  (fun hpq => ⟨hpq.right, hpq.left⟩)
  (fun hqp => ⟨hqp.right, hqp.left⟩)
example : p ∨ q ↔ q ∨ p := Iff.intro
  (fun hpq => hpq.elim
    (fun hp => Or.inr hp)
    (fun hq => Or.inl hq))
  (fun hqp => hqp.elim
    (fun hq => Or.inr hq)
    (fun hp => Or.inl hp))

-- associativity of ∧ and ∨
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := Iff.intro
  (fun h => ⟨h.left.left, ⟨h.left.right, h.right⟩⟩)
  (fun h => ⟨⟨h.left, h.right.left⟩, h.right.right⟩)
example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := Iff.intro
  (fun h => h.elim
    (fun hpq => hpq.elim
      (fun hp => Or.inl hp)
      (fun hq => Or.inr (Or.inl hq)))
    (fun hr => Or.inr (Or.inr hr)))
  (fun h => h.elim
    (fun hp => Or.inl (Or.inl hp))
    (fun hqr => hqr.elim
      (fun hq => Or.inl (Or.inr hq))
      (fun hr => Or.inr hr)))

-- distributivity
example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := Iff.intro
  (fun h => have hp := h.left
    h.right.elim
    (fun hq => Or.inl (And.intro hp hq))
    (fun hr => Or.inr (And.intro hp hr)))
  (fun h => h.elim
    (fun hpq => And.intro hpq.left (Or.inl hpq.right))
    (fun hpr => And.intro hpr.left (Or.inr hpr.right)))
example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := Iff.intro
  (fun h => h.elim
    (fun hp => And.intro (Or.inl hp) (Or.inl hp))
    (fun hqr => And.intro (Or.inr hqr.left) (Or.inr hqr.right)))
  (fun h =>
    have hpq := h.left
    have hpr := h.right
    hpq.elim
      (fun hp => Or.inl hp)
      (fun hq => hpr.elim
        (fun hp => Or.inl hp)
        (fun hr => Or.inr (And.intro hq hr))))

-- other properties
example : (p → (q → r)) ↔ (p ∧ q → r) := Iff.intro
  (fun hpqr =>
    fun hpq =>
    hpqr hpq.left hpq.right)
  (fun h =>
    fun hp =>
    fun hq =>
    h (And.intro hp hq))
example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := Iff.intro
  (fun h =>
    And.intro
    (fun hp => h (Or.inl hp))
    (fun hq => h (Or.inr hq)))
  (fun h =>
    fun hpq => hpq.elim
    (h.left)
    (h.right))
example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := Iff.intro
  (fun hnpq => And.intro
    (fun hp => hnpq (Or.inl hp))
    (fun hq => hnpq (Or.inr hq)))
  (fun h =>
    have hnp := h.left
    have hnq := h.right
    fun hpq => hpq.elim hnp hnq)
example : ¬p ∨ ¬q → ¬(p ∧ q) :=
  fun h =>
  fun hpq => h.elim
    (fun hnp => hnp hpq.left)
    (fun hnq => hnq hpq.right)
example : ¬(p ∧ ¬p) :=
  fun h => h.right h.left
example : p ∧ ¬q → ¬(p → q) :=
  fun h₁ => fun h₂ => h₁.right (h₂ h₁.left)
example : ¬p → (p → q) :=
  fun hnp => fun hp => absurd hp hnp
example : (¬p ∨ q) → (p → q) := 
  fun h => fun hp => h.elim
    (fun hnp => absurd hp hnp)
    (fun hq => hq)
example : p ∨ False ↔ p := Iff.intro
  (fun h => h.elim (fun hp => hp) (fun hf => hf.elim))
  (fun hp => Or.inl hp)

example : p ∧ False ↔ False := Iff.intro
  (fun h => h.right.elim)
  (fun h => h.elim)
example : (p → q) → (¬q → ¬p) :=
  fun hpq => fun hnq => fun hp => hnq (hpq hp)

open Classical

variable (p q r : Prop)

example : (p → q ∨ r) → ((p → q) ∨ (p → r)) :=
  fun h => (em p).elim
    (fun hp => (h hp).elim
      (fun hq => Or.inl fun _ => hq)
      (fun hr => Or.inr fun _ => hr))
    (fun hnp => Or.inl (fun hp => absurd hp hnp))
example : ¬(p ∧ q) → ¬p ∨ ¬q :=
  fun h => (em p).elim
    (fun hp => (em q).elim
      (fun hq => (h (And.intro hp hq)).elim)
      (fun hnq => Or.inr hnq))
    (fun hnp => Or.inl hnp)
example : ¬(p → q) → p ∧ ¬q :=
  fun hn => 
    (em p).elim
    (fun hp =>
      have hnq : ¬q := fun hq =>
        have h : p → q := fun _ => hq
        absurd h hn
      And.intro hp hnq)
    (fun hnp =>
      have h : p → q := fun hp => absurd hp hnp
      absurd h hn)
example : (p → q) → (¬p ∨ q) :=
  fun hpq => (em p).elim
    (fun hp => Or.inr (hpq hp))
    (fun hnp => Or.inl hnp)
example : (¬q → ¬p) → (p → q) :=
  fun h => fun hp => (em q).elim
    (id)
    (fun hnq => absurd hp (h hnq))
example : p ∨ ¬p := em p
example : (((p → q) → p) → p) := (em p).elim
  (fun hp => fun _ => hp)
  (fun hnp => fun h =>
    have hpq : p → q := fun hp => absurd hp hnp 
    absurd (h hpq) hnp)

感想

• 排中律を使った証明が難しい
• have ... absurd で補題を示していく感じにしているがもっと良い書き方ありそう
• And.intro の方がカッコを使った書き方より見やすそう
• フォーマッター欲しい、ちゃんと読んでないけど話はある？(https://github.com/leanprover/lean4/issues/369)
• 関数型言語の側面をうまく使えていないかもしれない
• 依存型がわかってない
• Type と Prop の差異が曖昧、Prop : Type？
• そういえば定理証明支援系って言葉あまり意味を理解していないで使っている
  • 定理証明支援系を使って書かれたコードは証明？証明を使ったソフトウェア開発とかいうべき？