Lengthlemma.agda

_++_ : ∀ {A : Set} → List A → List A → List A
[]       ++ ys  =  ys
(x ∷ xs) ++ ys  =  x ∷ (xs ++ ys)

length : ∀ {A : Set} → List A → ℕ
length [] = 0
length (x ∷ xs) = 1 + length xs

length-lemma : ∀ {A : Set} → (xs ys : List A) →
  length (xs ++ ys) ≡ length xs + length ys  -- the theorem to be proven
length-lemma [] ys =
  begin
    length ([] ++ ys)
  ≡⟨⟩
    length ys
  ≡⟨⟩
    0 + length ys
  ∎
length-lemma (x ∷ xs) ys =
  begin
    length ((x ∷ xs) ++ ys)
  ≡⟨⟩
    length (x ∷ (xs ++ ys))
  ≡⟨⟩
    1 + length (xs ++ ys)
  ≡⟨ cong (1 +_) (length-lemma xs ys) ⟩ -- using the induction hypothesis here
    1 + (length xs + length ys)
  ∎