Length of append

2/4 ~30 minlean

Prove that length turns append into addition.

3 lines · Lean 4

theorem length_append_local (xs ys : List α) :
    (xs ++ ys).length = xs.length + ys.length := by
  sorry

Objectifs

Prove that length turns append into addition.

Indices

Voir la solution

theorem length_append_local (xs ys : List α) :
    (xs ++ ys).length = xs.length + ys.length := by
  induction xs with
  | nil => simp
  | cons x xs ih => simp [ih]