Lean4 学習4 - ushumpei’s blog

n 番目の fibonacci 数を求める 2 つの関数が等しいこと (全ての引数に対し等しい戻り値を返すか) を証明してみた。

まず fib1 は素朴な実装

open Nat

def fib1 (n : Nat) :=
  match n with
  | 0 => 0
  | 1 => 1
  | n + 2 => fib1 n + fib1 (n + 1)

#eval fib1 12 -- 144 ok

fib2 は末尾再帰関数を用いて無駄な計算を省く実装

def fib_inner (n0 n1 n : Nat) :=
    match n with
    | 0 => n0
    | n + 1 => fib_inner n1 (n0 + n1) n
def fib2 (n : Nat) := fib_inner 0 1 n

#eval fib2 12 -- 144 ok

(雑に挙動を確かめる時に 12 を入れて 144 を確かめがち、12 x 12 = 144 で 12th fibonacci = 144 なのが印象的だったので)

末尾再帰関数に関する補題を示す (theorem って書いちゃってるけど)

theorem fib_inner_rule : ∀ n n0 n1 : Nat, fib_inner (n0 + n1) (n0 + n1 + n1) n
    = (fib_inner n0 n1 n) + (fib_inner n1 (n0 + n1) n) :=
  fun n : Nat =>
  Nat.recOn (
    motive := fun n =>
    ∀ n0 n1 : Nat, fib_inner (n0 + n1) (n0 + n1 + n1) n = (fib_inner n0 n1 n) + (fib_inner n1 (n0 + n1) n)
  ) n (
    fun n0 n1 =>
    calc fib_inner (n0 + n1) (n0 + n1 + n1) 0
        = n0 + n1                                          := by simp [fib_inner]
      _ = fib_inner n0 n1 0 + n1                           := by simp [fib_inner]
      _ = (fib_inner n0 n1 0) + (fib_inner n1 (n0 + n1) 0) := by simp [fib_inner]
  ) (
    fun n ih n0 n1 =>
    calc fib_inner (n0 + n1) (n0 + n1 + n1) (n + 1)
        = fib_inner (n0 + n1 + n1) (n0 + n1 + (n0 + n1 + n1)) n                 := by rw [fib_inner]
      _ = fib_inner (n1 + (n0 + n1)) (n1 + (n0 + n1) + (n0 + n1)) n             := by simp [Nat.add_assoc, Nat.add_comm]
      _ = (fib_inner n1 (n0 + n1) n) + (fib_inner (n0 + n1) (n1 + (n0 + n1)) n) := by rw [(ih n1 (n0 + n1))]
      _ = (fib_inner n0 n1 (n + 1)) + (fib_inner n1 (n0 + n1) (n + 1))          := by simp [fib_inner]
  )

fib1、fib2 が等しいことの証明を行う。強い数学的帰納法を使った。この辺全然正しいやり方がわかっていない。

theorem fib1_eq_fib2 : ∀ n : Nat, fib1 n = fib2 n :=
  fun n =>
  Nat.strongInductionOn (motive := fun n => fib1 n = fib2 n) n (
    fun n H =>
    match n with
    | 0 => rfl
    | 1 => rfl
    | n + 2 =>
      have _ : fib1 n = fib2 n :=
        have _ : n < n + 1 := lt_succ_of_le (Nat.le_refl n)
        have _ : n < n + 2 := Nat.lt_trans ‹n < n + 1› (lt_succ_of_le (Nat.le_refl (n + 1)))
        H n ‹n < n + 2› 
      have _ : fib1 (n + 1) = fib2 (n + 1) := H (n + 1) (lt_succ_of_le (Nat.le_refl (n + 1)))

      calc
        fib1 (n + 2)
          = fib1 n + fib1 (n + 1)                   := by simp [fib1]
        _ = fib2 n + fib1 (n + 1)                   := by rw [‹fib1 n = fib2 n›]
        _ = fib2 n + fib2 (n + 1)                   := by rw [‹fib1 (n + 1) = fib2 (n + 1)›]
        _ = fib_inner 0 1 n + fib_inner 0 1 (n + 1) := by simp [fib2]
        _ = fib_inner 0 1 n + fib_inner 1 1 n       := by simp [fib_inner]
        _ = fib_inner 1 2 n                         := by simp [fib_inner_rule n 0 1]
        _ = fib_inner 0 1 (n + 2)                   := by simp [fib_inner]
        _ = fib2 (n + 2)                            := by simp [fib2]
  )

ひとまず証明できた。

感想

by simp, by rw は何が起こっているかわからなくなるので使いたくなかったが、無いと全然進まないので使った。Eq の理解が曖昧なのが原因っぽい。
証明した後に書き直そうと思ったがうまくいかない
fib_inner を証明しているときに、証明しやすい実装を書かないといけないことに気がつき、ある既存の実装と新しい実装が同じことを数学的に証明する、といったことが結構困難なことだと分かった
- 例えば fib_inner が内部に隠蔽されていたら？とか、そういったことは文法上不可能になっているのだろうか？(let rec で定義した場合は fib2.fib_inner でアクセスできたので大丈夫だが)
- 証明を行う対象をどういったものにすべきか考えなければいけない
- リファクタリングの際に証明毎回行うのヤバそう
- 逆に証明されている定理に基づいて安全に行える？
  - 安全って何？
  - 今回は関数に対して証明を行ったが、型に対して証明がされている場合、その型を壊さない限りリファクタリングは自由に行える、とか良い面がある？
    - 型を壊すって何？
recOn も match も calc も by simp も by rw もだいぶ曖昧にやってる
- calc は have と this のシンタックスシュガー？
とはいえ関数の等号を示せた経験は、どう使っていくかのイメージが湧いてと思う
n < n + 2 くらい証明なしで使いたい、多分方法ある？見つけるのが難しい