Lean4 学習9' (original) (raw)

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 は複雑に考えていたがそんなに難しいものではなかった。

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

感想