Associativity of append

3/4 ~35 minlean

Prove append associativity without using the library theorem.

3 lines · Lean 4

theorem append_assoc_local (xs ys zs : List α) :
    (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by
  sorry

Objectifs

Prove append associativity without using the library theorem.

Indices

Voir la solution

theorem append_assoc_local (xs ys zs : List α) :
    (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by
  induction xs with
  | nil => rfl
  | cons x xs ih => simp [ih]