Lean4 学習10

Lean4 を数学の証明以外で使ってみたい気持ちがあり、しかし現実にある複雑なプログラムを検証する方法がわかっていないため、とりあえず FizzBuzz の証明を書いてみました。

import Std

def fizz_buzz : Nat → String := fun n =>
  if n % 15 = 0 then "FizzBuzz"
  else if n % 3 = 0 then "Fizz"
  else if n % 5 = 0 then "Buzz"
  else toString n

 -- 15 の倍数で FizzBuzz になることを証明する
theorem fizz_buzz_mul_15 (n : Nat) : n % 15 = 0 → fizz_buzz n = "FizzBuzz" := fun mod_15 =>
  by simp [fizz_buzz, mod_15]

-- 3 の倍数で 5 の倍数じゃないものは Fizz になることを証明する
theorem fizz_buzz_mul_3 (n : Nat) : n % 3 = 0 ∧ (¬ n % 5 = 0) → fizz_buzz n = "Fizz" := fun ⟨mod_3, not_mod_5⟩ =>
  have not_mod_15 : ¬ n % 15 = 0 := fun mod_15 =>
    have mod_5 : n % 5 = 0 :=
      have h : 5 ∣ 15 := by simp -- 書きたくない
      have dvd_15 : 15 ∣ n := (Nat.dvd_iff_mod_eq_zero 15 n).mpr mod_15
      (Nat.dvd_iff_mod_eq_zero 5 n).mp (Nat.dvd_trans h dvd_15)
    absurd mod_5 not_mod_5
  by simp [fizz_buzz, not_mod_15, mod_3]

-- 5 の倍数で 3 の倍数じゃないものは Buzz になることを証明する
theorem fizz_buzz_mul_5 (n : Nat) : n % 5 = 0 ∧ (¬ n % 3 = 0) → fizz_buzz n = "Buzz" := fun ⟨mod_5, not_mod_3⟩ =>
  have not_mod_15 : ¬ n % 15 = 0 := fun mod_15 =>
    have mod_3 : n % 3 = 0 :=
      have h : 3 ∣ 15 := by simp -- 書きたくない
      have dvd_15 : 15 ∣ n := (Nat.dvd_iff_mod_eq_zero 15 n).mpr mod_15
      (Nat.dvd_iff_mod_eq_zero 3 n).mp (Nat.dvd_trans h dvd_15)
    absurd mod_3 not_mod_3
  by simp [fizz_buzz, not_mod_15, not_mod_3, mod_5]

-- 3 の倍数でも 5 の倍数でもないものはそのままの数になることを証明する
theorem fizz_buzz_n (n: Nat) : (¬ n % 3 = 0) ∧ (¬ n % 5 = 0) → fizz_buzz n = toString n := fun ⟨not_mod_3, not_mod_5⟩ =>
  have not_mod_15 : ¬ n % 15 = 0 := fun mod_15 =>
    have mod_3 : n % 3 = 0 :=
      have h : 3 ∣ 15 := by simp -- 書きたくない
      have dvd_15 : 15 ∣ n := (Nat.dvd_iff_mod_eq_zero 15 n).mpr mod_15
      (Nat.dvd_iff_mod_eq_zero 3 n).mp (Nat.dvd_trans h dvd_15)
    absurd mod_3 not_mod_3
  by simp [fizz_buzz, not_mod_15, not_mod_3, not_mod_5]

def main: IO Unit :=
  let fizz_buzz_list := List.map fizz_buzz (List.range 100)
  IO.println fizz_buzz_list

#eval main

感想

• 色々と課題がある
  • Std は勝手にインポートされたりしないのか
  • 自明な式を示すために使っている by simp を書かない方法、実はありそう
  • % だけで書きたかったが (FizzBuzz 書く時大体は % で書くと思うので) ∣ の方が定理が証明されていて楽だったので使った、敗北感ある
  • IO わかっていない
  • if に式 (Prop) を渡しているので、型レベルでのパターンマッチ？みたいなことをしている？依存型がわかっていない
• 状態を型で定義すれば何らかの証明が書けそう？
  • 基本的なプログラムである TODO リストとか書けるだろうか？
    • 状態として考えられるのは有限の TODO アイテムのリスト
      • でもそんなに面白くないな...
  • そもそも証明が必要になるプログラムはどんなものか？
    • 簡単なプロトコルでも実装してみる？
      • 具体的にどう役に立つ？
    • 証明が必要なもの、必要じゃないものはある
    • 日付の変換、単位の読み替え、何らかのちゃんとした (式等で記述可能な) 定義があるもの？