Lean4 学習9'

Lean4 学習9 - ushumpei’s blog こちらで定義した range' : (n : Nat) → Vector (Fin n) n という関数、もっと簡単に定義できた。

range を定義してから型の対応関係を考えるというのが逆で、型の対応関係を考えたら自然と range に相当するものが出てきた感じ。

Fin n → α から Vector α n への自然変換から range 関数 (n ⊢> [0, 1, ..., n-1]) を得る話

対応関係

以下を定義する。fin_fun_to_vec は複雑に考えていたがそんなに難しいものではなかった。

• fin_fun_to_vec: f: Fin n → α を Vector α n に [f 0, f 1, ..., f (n-1)] という感じで対応させる関数
• vec_to_fin_fun: v: Vector α n を Fin n → α に i ⊢> v[i] という感じで対応させる関数

def Vector (α: Type) (n: Nat) := { l : List α // l.length = n }

def fin_fun_to_vec {n: Nat} {α : Type} (f: Fin n → α): Vector α n := match n with
  | 0 => ⟨[], rfl⟩ 
  | m+1 =>
    let a: α := f ⟨0, Nat.zero_lt_succ m⟩ 
    let as: Vector α m := fin_fun_to_vec (fun j : Fin m =>
      have hj: j.val + 1 < m + 1 := Nat.add_lt_add_right j.isLt 1
      f ⟨j.val + 1, hj⟩)
    have h : (a::as.val).length = m + 1 := calc
      (a::as.val).length = as.val.length + 1 := rfl
      _                  = m + 1             := congrArg (· + 1) as.property
    ⟨a::as.val, h⟩ 

def vec_to_fin_fun {n: Nat} {α : Type} (v: Vector α n): Fin n → α := fun i =>
  have h : i.val < v.val.length := calc
    i.val < n            := i.isLt
    _     = v.val.length := Eq.symm v.property
  v.val.get ⟨i.val, h⟩

定義

fin_fun_to_vec により Fin n → Fin n の恒等写像が range n に変換される

def range (n: Nat) : Vector (Fin n) n := fin_fun_to_vec id

#eval range 3  -- [0, 1, 2]
#check range 3 -- range 3 : Vector (Fin 3) 3

感想

• まじか
• すごい圏論っぽい話だと思うので時間がある時に考えてみる
  • 圏は Hask 圏 (とかいうやつ)、n は固定
  • Fin n → α が関手であることは、f: X → Y を f ∘ _: (Fin n → X) → (Fin n → Y) に移すことからわかる (∘: 関数の合成)
  • Vector α n へ関手であることは、f: X → Y を _.map f: Vector X n → Vector Y n に移すことからわかる
  • fin_fun_to_vec が Fin n → α から Vector α n への自然変換であることは、f: X → Y、a: Fin n → X として可換図式の２経路を計算すると [f ∘ a 0, f ∘ a 1, ..., f ∘ a n-1] で一致することからわかる
• 多分関手とか自然変換とかそれ用のクラスとかがあるはず (だけど一旦放置)