【LEAN学習メモ】基本文法と簡単な証明をやってみる

こんにちは！
今数学界で話題のLEANに入門してみました
学習メモとして備忘録的に書きます

文法

値の定義

def x : Nat := 3

defは定義
Natは自然数
:= は定義

関数定義

def add (a b : Nat) : Nat :=
  a + b

引数として自然数a, bを受け取って、自然数を返す
自動的にカリー化されている

let式

def squarePlusOne (n : Nat) : Nat :=
  let m := n * n
  m + 1

letは式であり副作用はない

パターンマッチ

def isZero (n : Nat) : Bool :=
  match n with
  | 0 => true
  | _ => false

Haskellのガードに似ているパターンマッチがある

再帰

def factorial : Nat → Nat
  | 0 => 1
  | Nat.succ n => (Nat.succ n) * factorial n

Leanは再帰の停止性を自動チェックできるらしい

帰納法

theorem add_zero (n : Nat) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
      simp [Nat.add_succ, ih]

自然数nに0を足しても変わらない、を帰納法で上のように書ける

calc

calc
  a = b := by ...
  _ = c := by ...
  _ = d := by ...

calcを使うとa = b = c = dのような式を段階的に書ける

IOモナド

def main : IO Unit :=
  IO.println "Hello, Lean!"

純粋関数型言語なので、IOなど副作用ある処理はモナドを使う

簡単な証明をやってみる

奇数の和は平方数になる、という定理を証明してみます

数式で書くとこんな感じ

$ \displaystyle \sum_{ i = 1 }^{ n } (2n - 1) = n ^ 2 $

-- oddSum n = 1 + 3 + ... + (2n - 1)
def oddSum : Nat -> Nat
  | 0 => 0
  | Nat.succ n => oddSum n + (n + n + 1)

theorem oddSum_eq_square (n : Nat) : oddSum n = n * n := by
  -- n について帰納法を使う
  induction n with
  | zero =>
      -- oddSum 0 = 0 かつ 0 * 0 = 0
      rfl
  | succ n ih =>
      -- 帰納法の仮定:
      -- ih : oddSum n = n * n
      -- これを使って oddSum (n+1) = (n+1)^2 を示す
      calc
        -- oddSum の定義を 1 段だけ展開
        oddSum (Nat.succ n)
            = oddSum n + (n + n + 1) := by
                rfl
        -- ih で oddSum n を n * n に置き換える
        _ = n * n + (n + n + 1) := by
              rw [ih]
        -- 足し算の並びを整理して、
        -- n*n + n と n+1 の形にする
        _ = (n * n + n) + (n + 1) := by
              simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
        -- n*n + n の部分を (n+1)*n と見直す
        _ = (Nat.succ n) * n + Nat.succ n := by
              rw [Nat.succ_mul]
        -- a*b + a = a*(b+1) を使って (n+1)^2 にする
        _ = (Nat.succ n) * Nat.succ n := by
              rw [Nat.mul_succ]

calcを使って式変形を追いかけていくことで、丁寧に証明していけた気がします
よくある数学書だと、途中が省略されたりしますが、LEANはそれがないので、数学の学習に向いているかもしれません

まとめ

LEAN、とても面白い言語ですね！
次にやってみたいこと

1. 代数学と相性良さそうなので、群論など代数学の定理をLEANで書いてみたい
2. アルゴリズムの検証にLEANが使えないか試してみたい
3. システム設計を代数的に表現して、システムアーキテクチャをLEANで記述してみたい

特に最後のはぜひやってみたい...
代数的アーキテクチャ論
AIエージェントにアーキテクチャ設計してもらって、LEANで検証し、実装、なんていう流れができたら嬉しいですね