Proofs of the equality length(xs ++ ys) = length(xs) + length(ys)

José A. Alonso

07-08-2024

In Lean, the functions

    length : List α → Nat
    (++)   : List α → List α → List α

are defined such that

(length xs) is the length of xs. For example,
```
length [2,3,5,3] = 4
```
(xs ++ ys) is the list obtained by concatenating xs and ys. For example.
```
[1,2] ++ [2,3,5,3] = [1,2,2,3,5,3]
```

These functions are characterized by the following lemmas:

length_nil  : length [] = 0
length_cons : length (x :: xs) = length xs + 1
nil_append  : [] ++ ys = ys
cons_append : (x :: xs) ++ y = x :: (xs ++ ys)

To prove that

length (xs ++ ys) = length xs + length ys

To that end, complete the following Lean4 theory

import Mathlib.Tactic
open List

variable {α : Type}
variable (xs ys : List α)

example :
  length (xs ++ ys) = length xs + length ys :=
by sorry

1. Proof in natural language

By induction on xs.

Base case: Suppose that xs = []. Then,

length (xs ++ ys) = length ([] ++ ys)
                  = length ys
                  = 0 + length ys
                  = length [] + length ys
                  = length xs + length ys

Induction step: Suppose that xs = a :: as and that the induction hypothesis (IH) holds

length (as ++ ys) = length as + length ys                     (IH)

Then,

length (xs ++ ys) = length ((a :: as) ++ ys)
                  = length (a :: (as ++ ys))
                  = length (as ++ ys) + 1
                  = (length as + length ys) + 1      [por IH]
                  = (length as + 1) + length ys
                  = length (a :: as) + length ys
                  = length xs + length ys

2. Proofs with Lean4

import Mathlib.Tactic

open List

variable {α : Type}
variable (xs ys : List α)

-- Proof 1
-- =======

example :
  length (xs ++ ys) = length xs + length ys :=
by
  induction' xs with a as IH
  . calc length ([] ++ ys)
         = length ys
           := congr_arg length (nil_append ys)
       _ = 0 + length ys
           := (zero_add (length ys)).symm
       _ = length [] + length ys
           := congrArg (. + length ys) length_nil.symm
  . calc length ((a :: as) ++ ys)
         = length (a :: (as ++ ys))
           := congr_arg length (cons_append a as ys)
       _ = length (as ++ ys) + 1
           := length_cons a (as ++ ys)
       _ = (length as + length ys) + 1
           := congrArg (. + 1) IH
       _ = (length as + 1) + length ys
           := (Nat.succ_add (length as) (length ys)).symm
       _ = length (a :: as) + length ys
           := congrArg (. + length ys) (length_cons a as).symm

-- Proof 2
-- =======

example :
  length (xs ++ ys) = length xs + length ys :=
by
  induction' xs with a as IH
  . calc length ([] ++ ys)
         = length ys
           := by rw [nil_append]
       _ = 0 + length ys
           := (zero_add (length ys)).symm
       _ = length [] + length ys
           := by rw [length_nil]
  . calc length ((a :: as) ++ ys)
         = length (a :: (as ++ ys))
           := by rw [cons_append]
       _ = length (as ++ ys) + 1
           := by rw [length_cons]
       _ = (length as + length ys) + 1
           := by rw [IH]
       _ = (length as + 1) + length ys
           := (Nat.succ_add (length as) (length ys)).symm
       _ = length (a :: as) + length ys
           := congrArg (. + length ys) (length_cons a as).symm

-- Proof 3
-- =======

example :
  length (xs ++ ys) = length xs + length ys :=
by
  induction' xs with _ as IH
  . simp only [nil_append, zero_add, length_nil]
  . simp only [cons_append, length_cons, IH, Nat.succ_add]

-- Proof 4
-- =======

example :
  length (xs ++ ys) = length xs + length ys :=
by
  induction' xs with _ as IH
  . simp
  . simp [IH, Nat.succ_add]

-- Proof 5
-- =======

example :
  length (xs ++ ys) = length xs + length ys :=
by
  induction' xs with a as IH
  . simp
  . simp [IH] ; linarith

-- Proof 6
-- =======

lemma length_conc_1 (xs ys : List α):
  length (xs ++ ys) = length xs + length ys :=
by
  induction xs with
  | nil => calc
    length ([] ++ ys)
        = length ys
          := by rw [nil_append]
      _ = 0 + length ys
          := by rw [zero_add]
      _ = length [] + length ys
          := by rw [length_nil]
  | cons a as IH => calc
    length ((a :: as) ++ ys)
        = length (a :: (as ++ ys))
          := by rw [cons_append]
      _ = length (as ++ ys) + 1
          := by rw [length_cons]
      _ = (length as + length ys) + 1
          := by rw [IH]
      _ = (length as + 1) + length ys
          := (Nat.succ_add (length as) (length ys)).symm
      _ = length (a :: as) + length ys
          := by rw [length_cons]

-- Proof 7
-- =======

lemma length_conc_2 (xs ys : List α):
  length (xs ++ ys) = length xs + length ys :=
by
  induction xs with
  | nil          => simp
  | cons _ as IH => simp [IH, Nat.succ_add]

-- Proof 8
-- =======

example :
  length (xs ++ ys) = length xs + length ys :=
by
  induction' xs with a as IH
  . -- ⊢ length ([] ++ ys) = length [] + length ys
    rw [nil_append]
    -- ⊢ length ys = length [] + length ys
    rw [length_nil]
    -- ⊢ length ys = 0 + length ys
    rw [zero_add]
  . -- a : α
    -- as : List α
    -- IH : length (as ++ ys) = length as + length ys
    -- ⊢ length (a :: as ++ ys) = length (a :: as) + length ys
    rw [cons_append]
    -- ⊢ length (a :: (as ++ ys)) = length (a :: as) + length ys
    rw [length_cons]
    -- ⊢ Nat.succ (length (as ++ ys)) = length (a :: as) + length ys
    rw [IH]
    -- ⊢ Nat.succ (length as + length ys) = length (a :: as) + length ys
    rw [length_cons]
    -- ⊢ Nat.succ (length as + length ys) = Nat.succ (length as) + length ys
    rw [Nat.succ_add]

-- Proof 9
-- =======

example :
  length (xs ++ ys) = length xs + length ys :=
by
  induction' xs with a as IH
  . -- ⊢ length ([] ++ ys) = length [] + length ys
    rw [nil_append]
    -- ⊢ length ys = length [] + length ys
    rw [length_nil]
    -- ⊢ length ys = 0 + length ys
    rw [zero_add]
  . -- a : α
    -- as : List α
    -- IH : length (as ++ ys) = length as + length ys
    -- ⊢ length (a :: as ++ ys) = length (a :: as) + length ys
    rw [cons_append]
    -- ⊢ length (a :: (as ++ ys)) = length (a :: as) + length ys
    rw [length_cons]
    -- ⊢ Nat.succ (length (as ++ ys)) = length (a :: as) + length ys
    rw [IH]
    -- ⊢ Nat.succ (length as + length ys) = length (a :: as) + length ys
    rw [length_cons]
    -- ⊢ Nat.succ (length as + length ys) = length (a :: as) + length ys
    rw [Nat.succ_add]

-- Proof 10
-- ========

example :
  length (xs ++ ys) = length xs + length ys :=
by
  induction' xs with a as IH
  . -- ⊢ length ([] ++ ys) = length [] + length ys
    rw [nil_append]
    -- ⊢ length ys = length [] + length ys
    rw [length_nil]
    -- ⊢ length ys = 0 + length ys
    rw [zero_add]
  . -- a : α
    -- as : List α
    -- IH : length (as ++ ys) = length as + length ys
    -- ⊢ length (a :: as ++ ys) = length (a :: as) + length ys
    rw [cons_append]
    -- ⊢ length (a :: (as ++ ys)) = length (a :: as) + length ys
    rw [length_cons]
    -- ⊢ Nat.succ (length (as ++ ys)) = length (a :: as) + length ys
    rw [IH]
    -- ⊢ Nat.succ (length as + length ys) = length (a :: as) + length ys
    rw [length_cons]
    -- ⊢ Nat.succ (length as + length ys) = Nat.succ (length as) + length ys
    linarith

-- Proof 11
-- ========

example :
  length (xs ++ ys) = length xs + length ys :=
length_append xs ys

-- Proof 12
-- ========

example :
  length (xs ++ ys) = length xs + length ys :=
by simp

-- Used lemmas
-- ===========

-- variable (m n p : ℕ)
-- variable (x : α)
-- #check (Nat.succ_add n m : Nat.succ n + m = Nat.succ (n + m))
-- #check (cons_append x xs ys : (x :: xs) ++ ys = x :: (xs ++ ys))
-- #check (length_append xs ys : length (xs ++ ys) = length xs + length ys)
-- #check (length_cons x xs : length (x :: xs) = length xs + 1)
-- #check (length_nil : length [] = 0)
-- #check (nil_append xs : [] ++ xs = xs)
-- #check (zero_add n : 0 + n = n)

You can interact with the previous proofs at Lean 4 Web.

3. Proofs with Isabelle/HOL

theory "Proofs_of_the_equality_length(xs++ys)_Eq_length(xs)+length(ys)"
imports Main
begin

(* Proof 1 *)

lemma "length (xs @ ys) = length xs + length ys"
proof (induct xs)
  have "length ([] @ ys) = length ys"
    by (simp only: append_Nil)
  also have "\<dots> = 0 + length ys"
    by (rule add_0 [symmetric])
  also have "\<dots> = length [] + length ys"
    by (simp only: list.size(3))
  finally show "length ([] @ ys) = length [] + length ys"
    by this
next
  fix x xs
  assume HI : "length (xs @ ys) = length xs + length ys"
  have "length ((x # xs) @ ys) = length (x # (xs @ ys))"
    by (simp only: append_Cons)
  also have "\<dots> = length (xs @ ys) + 1"
    by (simp only: list.size(4))
  also have "\<dots> = (length xs + length ys) + 1"
    by (simp only: HI)
  also have "\<dots> = (length xs + 1) + length ys"
    by (simp only: add.assoc add.commute)
  also have "\<dots> = length (x # xs) + length ys"
    by (simp only: list.size(4))
  then show "length ((x # xs) @ ys) = length (x # xs) + length ys"
    by simp
qed

(* Proof 2 *)

lemma "length (xs @ ys) = length xs + length ys"
proof (induct xs)
  show "length ([] @ ys) = length [] + length ys"
    by simp
next
  fix x xs
  assume "length (xs @ ys) = length xs + length ys"
  then show "length ((x # xs) @ ys) = length (x # xs) + length ys"
    by simp
qed

(* Proof 3 *)

lemma "length (xs @ ys) = length xs + length ys"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by simp
qed

(* Proof 4 *)

lemma "length (xs @ ys) = length xs + length ys"
by (induct xs) simp_all

(* Proof 5 *)

lemma "length (xs @ ys) = length xs + length ys"
by (fact length_append)

(* Note: Auto_solve suggests the previous proof. *)

end

Note: The code for the previous proofs can be found in the Calculemus repository on GitHub.