パンの木を植えて

主として数学の話をするブログ

トップ > Lean4 でフィボナッチ数列の２つの表現が同値であることを示す

Lean4 でフィボナッチ数列の２つの表現が同値であることを示す

\[ %%% 黒板太字 %%% \newcommand{\A}{\mathbb{A}} %アフィン空間 \newcommand{\C}{\mathbb{C}} %複素数 \newcommand{\F}{\mathbb{F}} %有限体 \newcommand{\N}{\mathbb{N}} %自然数 \newcommand{\Q}{\mathbb{Q}} %有理数 \newcommand{\R}{\mathbb{R}} %実数 \newcommand{\Z}{\mathbb{Z}} %整数 %%% 2項演算 %%% \newcommand{\f}[2]{ \frac{#1}{#2} } \]

Lean4 は Haskell のような純粋関数型言語ですが，より型システムが強力なので，定義した関数が望ましい性質を満たすことを証明することができます．

その１例として，ここでは（何番煎じかわかりませんが）フィボナッチ数列を取り上げます．*1


まずはフィボナッチ数列を関数として定義しましょう．

/-- フィボナッチ数列の通常の定義をそのまま Lean の関数として書いたもの -/
def fibonacci : Nat → Nat
| 0 => 0
| 1 => 1
| n + 2 => fibonacci n + fibonacci (n + 1)

example : [0, 1, 2, 3, 4, 5].map fibonacci = [0, 1, 1, 2, 3, 5] := rfl

この定義は素直ですが，同じ計算を何度も繰り返してしまうので計算時間がかかりすぎることで知られています．

より効率的にしたものを定義しましょう．ここではヘルパー関数を使うことで定義します．

/-- フィボナッチ数列の速いバージョン -/
def fib (n : Nat) : Nat :=
  (loop n).1
where
  loop : Nat → Nat × Nat
    | 0   => (0, 1)
    | n+1 => ((loop n).2, (loop n).1 + (loop n).2)

example : [0, 1, 2, 3, 4, 5].map fib = [0, 1, 1, 2, 3, 5] := rfl

このヘルパー関数 loop には，fib.loop という名前でアクセスすることが可能です．

通常のプログラミング言語であればここで２つの関数をテストして一致することを確認し，話は終わりなのですが，Lean4 では一致することを証明することができます．

せっかくなのでやってみましょう．鍵となるのは，高速版の fib が同じ漸化式を満たすということです．それを補題として示しましょう．

theorem fib_add (n : Nat) : fib n + fib (n + 1) = fib (n + 2) := by
  -- ヘルパー関数について示せば十分
  suffices fib.loop n + fib.loop (n + 1) = fib.loop (n + 2) from by
    simp [fib]
    rfl

  let α := fib.loop (n + 1)
  let β := fib.loop n
  have :=
    calc fib.loop (n + 2)
      _ = (α.2, α.1 + α.2) := by rfl
      _ = (β.1 + β.2, β.2 + (β.1 + β.2)) := by rfl
      _ = (β.1, β.2) + (β.2, β.1 + β.2) := by rfl
      _ = β + α := by rfl
  assumption

同じ漸化式を満たすことさえ示せてしまえば，あとは帰納法で関数の一致を示すことができます．

example : fibonacci = fib := by
  funext n
  induction' n using Nat.strong_induction_on with n ih
  match n with
  | 0 => rfl
  | 1 => rfl
  | n + 2 =>
    rw [←fib_add, fibonacci]
    simp_all

終わりです．形式的に「機械可読な」証明を書いているにしては，短いと思いませんか？simp などの強力なタクティクがあるおかげです．


今回のコードですが，Lean4 Web で触ることができます．気になったらぜひ自分で編集してみてください．(はてな記法と衝突するのでコード片としてURLを共有します)

https://lean.math.hhu.de/#code=import%20Mathlib%0D%0A%0D%0A%2F--%20%E3%83%95%E3%82%A3%E3%83%9C%E3%83%8A%E3%83%83%E3%83%81%E6%95%B0%E5%88%97%E3%81%AE%E9%80%9A%E5%B8%B8%E3%81%AE%E5%AE%9A%E7%BE%A9%E3%82%92%E3%81%9D%E3%81%AE%E3%81%BE%E3%81%BE%20Lean%20%E3%81%AE%E9%96%A2%E6%95%B0%E3%81%A8%E3%81%97%E3%81%A6%E6%9B%B8%E3%81%84%E3%81%9F%E3%82%82%E3%81%AE%20-%2F%0D%0Adef%20fibonacci%20%3A%20Nat%20%E2%86%92%20Nat%0D%0A%7C%200%20%3D%3E%200%0D%0A%7C%201%20%3D%3E%201%0D%0A%7C%20n%20%2B%202%20%3D%3E%20fibonacci%20n%20%2B%20fibonacci%20(n%20%2B%201)%0D%0A%0D%0Aexample%20%3A%20%5B0%2C%201%2C%202%2C%203%2C%204%2C%205%5D.map%20fibonacci%20%3D%20%5B0%2C%201%2C%201%2C%202%2C%203%2C%205%5D%20%3A%3D%20rfl%0D%0A%0D%0A%0D%0A%2F--%20%E3%83%95%E3%82%A3%E3%83%9C%E3%83%8A%E3%83%83%E3%83%81%E6%95%B0%E5%88%97%E3%81%AE%E9%80%9F%E3%81%84%E3%83%90%E3%83%BC%E3%82%B8%E3%83%A7%E3%83%B3%20-%2F%0D%0Adef%20fib%20(n%20%3A%20Nat)%20%3A%20Nat%20%3A%3D%0D%0A%20%20(loop%20n).1%0D%0Awhere%0D%0A%20%20loop%20%3A%20Nat%20%E2%86%92%20Nat%20%C3%97%20Nat%0D%0A%20%20%20%20%7C%200%20%20%20%3D%3E%20(0%2C%201)%0D%0A%20%20%20%20%7C%20n%2B1%20%3D%3E%20((loop%20n).2%2C%20(loop%20n).1%20%2B%20(loop%20n).2)%0D%0A%0D%0Aexample%20%3A%20%5B0%2C%201%2C%202%2C%203%2C%204%2C%205%5D.map%20fib%20%3D%20%5B0%2C%201%2C%201%2C%202%2C%203%2C%205%5D%20%3A%3D%20rfl%0D%0A%0D%0A%0D%0Atheorem%20fib_add%20(n%20%3A%20Nat)%20%3A%20fib%20n%20%2B%20fib%20(n%20%2B%201)%20%3D%20fib%20(n%20%2B%202)%20%3A%3D%20by%0D%0A%20%20--%20%E3%83%98%E3%83%AB%E3%83%91%E3%83%BC%E9%96%A2%E6%95%B0%E3%81%AB%E3%81%A4%E3%81%84%E3%81%A6%E7%A4%BA%E3%81%9B%E3%81%B0%E5%8D%81%E5%88%86%0D%0A%20%20suffices%20fib.loop%20n%20%2B%20fib.loop%20(n%20%2B%201)%20%3D%20fib.loop%20(n%20%2B%202)%20from%20by%0D%0A%20%20%20%20simp%20%5Bfib%5D%0D%0A%20%20%20%20rfl%0D%0A%0D%0A%20%20let%20%CE%B1%20%3A%3D%20fib.loop%20(n%20%2B%201)%0D%0A%20%20let%20%CE%B2%20%3A%3D%20fib.loop%20n%0D%0A%20%20have%20%3A%3D%0D%0A%20%20%20%20calc%20fib.loop%20(n%20%2B%202)%0D%0A%20%20%20%20%20%20_%20%3D%20(%CE%B1.2%2C%20%CE%B1.1%20%2B%20%CE%B1.2)%20%3A%3D%20by%20rfl%0D%0A%20%20%20%20%20%20_%20%3D%20(%CE%B2.1%20%2B%20%CE%B2.2%2C%20%CE%B2.2%20%2B%20(%CE%B2.1%20%2B%20%CE%B2.2))%20%3A%3D%20by%20rfl%0D%0A%20%20%20%20%20%20_%20%3D%20(%CE%B2.1%2C%20%CE%B2.2)%20%2B%20(%CE%B2.2%2C%20%CE%B2.1%20%2B%20%CE%B2.2)%20%3A%3D%20by%20rfl%0D%0A%20%20%20%20%20%20_%20%3D%20%CE%B2%20%2B%20%CE%B1%20%3A%3D%20by%20rfl%0D%0A%20%20assumption%0D%0A%0D%0A%0D%0Aexample%20%3A%20fibonacci%20%3D%20fib%20%3A%3D%20by%0D%0A%20%20funext%20n%0D%0A%20%20induction'%20n%20using%20Nat.strong_induction_on%20with%20n%20ih%0D%0A%20%20match%20n%20with%0D%0A%20%20%7C%200%20%3D%3E%20rfl%0D%0A%20%20%7C%201%20%3D%3E%20rfl%0D%0A%20%20%7C%20n%20%2B%202%20%3D%3E%0D%0A%20%20%20%20rw%20%5B%E2%86%90fib_add%2C%20fibonacci%5D%0D%0A%20%20%20%20simp_all%0D%0A%0D%0A

あとシンタックスハイライトが効いてなくて見づらかったと思うので， gist も貼っておきます

*1:すでに記事を書かれてる方が何人もいらっしゃいますが，証明方法はあまり被ってないと思います