ushumpei’s blog

生活で気になったことを随時調べて書いていきます。

Lean4 学習9

Lean4 で有限個の要素をいい感じに扱いたくてどうすればいいか悩んでいて、Fin n → α がそれに当たるかなーとか考えたのですが、プログラミングにおいては Vector α n (長さ固定の List α) が使いやすいのでその間を埋めることができないかなと色々しています。

とりあえずなんかに使えそうなので range' : (n : Nat) → Vector (Fin n) n を定義しました。

追記: もっといい方法があった

ushumpei.hatenablog.com

range 定義

まずは List.range を真似て、行き先が List (Fin n) の range を定義します。range n は [0, 1, ..., n-1] を返します。適当に実装したら逆順 [n-1, n-2, ..., 0] となってしまったり、一個不足した [0, 1, ..., n-2] となってしまったりして苦労しました。

-- Fin n := {i: ℕ | i < n} = {0, 1, ..., n-1}
def range (n: Nat): List (Fin n) := match n with
  | 0   => []
  | i+1 =>
    let fin := ⟨i, (Nat.lt_succ_self i)⟩
    loop fin (fin::[])
where
  loop {n: Nat} : Fin n → List (Fin n) → List (Fin n)
  | ⟨0, _⟩,   ns => ns
  | ⟨i+1, h⟩, ns =>
    have hh : i < n := calc i < i + 1 := Nat.lt_succ_self i
                            _ < n     := h
    loop ⟨i, hh⟩ (⟨i, hh⟩ :: ns)
#eval range 4  -- [0, 1, 2, 3]
#check range 4 -- range 4 : List (Fin 4)

証明1

次に長さに関する定理を証明します。range 内部の再帰関数 loop に関する補題 loop_length という名前で range.loop nn (nn:nns) の長さが nn.val + nns.length + 1 と等しいことを示します。ここで最初に躓いたのが n = 0 の時ですが Fin 0 は要素を持たないことに気がつき absurd で解決できました。他の部分は気合いでいきました。

theorem loop_length: ∀ n, ∀ nn: Fin n, ∀ nns: List (Fin n), (range.loop nn (nn::nns)).length = nn.val + nns.length + 1
  | 0, nn       , nns => absurd nn.isLt (Nat.not_lt_zero _)
  | _, ⟨0, h⟩   , nns =>
    calc
      (range.loop ⟨0, h⟩ (⟨0, h⟩::nns)).length = (⟨0, h⟩::nns).length := rfl
      _                                        = nns.length + 1       := rfl
      _                                        = 0 + nns.length + 1   := Eq.symm (Nat.zero_add (nns.length + 1))
  | n, ⟨i+1, h⟩, nns =>
    let nn' := ⟨i+1, h⟩
    have hh : i < n := calc i < i + 1 := Nat.lt_succ_self i
                            _ < n     := h
    let nn := ⟨i, hh⟩
    calc
      (range.loop nn' (nn'::nns)).length = (range.loop nn (nn::nn'::nns)).length := rfl
      _                                  = nn.val + (nn'::nns).length + 1        := loop_length n nn (nn'::nns)
      _                                  = nn.val + 1 + (nn'::nns).length        := Nat.add_right_comm nn.val (nn'::nns).length 1
      _                                  = nn.val + 1 + nns.length + 1           := rfl
      _                                  = nn'.val + nns.length + 1              := rfl

証明2

この補題を使用して range n の長さが n であることを証明します。congrArg とか忘れかけています、Eq.refl の部分は勘で書きました。そろそろ体系的に学ぶべき時が来た気がします。

theorem range_length: ∀ n, (range n).length = n
  | 0   => rfl
  | i+1 =>
    let fin := ⟨i, (Nat.lt_succ_self i)⟩
    calc (range (i+1)).length = (range.loop fin (fin::[])).length := congrArg List.length (Eq.refl (range (i+1)))
      _                       = fin.val + 1                       := loop_length (i+1) fin []
      _                       = i+1                               := rfl

range' 定義

range' : (n : Nat) → Vector (Fin n) n を定義します。多分この関数を range にして、前のやつを range' にした方が良い。Vector は Mathlib にあるようですが、何が起こっているか分かりにくかったので一旦自前で用意しました。

def Vector (α: Type) (n: Nat) := { l : List α // l.length = n }
def range' (n: Nat): Vector (Fin n) n := ⟨range n, range_length n⟩

感想

  • range' を使用して Fin n → α と Vector α n の双方向の変換を書くことができる
    • もしかしたらもっと簡単で使いやすくかける方法があるかもしれない
    • 準同型的なことを示したいが全然分からない、関数や部分集合の等値性はどのように示す？
      • そもそも何の同型？α は型、Fin n → α と Vector α n は関手だとして、その間の自然同型とかいうやつ？
  • そろそろ体系的に学ぶべき時が来た気がします
  • ライブラリを探す能力が不足している
    • 新しめな言語を触ることが減っているので、ググれば何かしらのコードがある状況に慣れてしまっている
  • ゲーム理論的な話を Lean4 でやりたくて、プレイヤーが n 人いて、戦略が m 個あって、みたいなことを議論するための道具として Fin n → α をいじった
    • 単に Vector を使えば事足りたのだろうか？
      • 各プレイヤーが戦略を決めた場合のプレイヤーごとの点数は (Fin n → Fin m) → Fin n → ℝ で与えられる感じで良いか？
        • これを Vector で書く場合は？
  • calc がインデントの位置によって失敗するようになった？
    • _ を行頭の方に寄せて書くことで回避できたが、何が何だか分からなくて混乱した