Every List

Part 2 of What a Proof Covers.

The previous post checked reverse (reverse xs) = xs for one list and then for a thousand generated ones. This post proves it for every finite list, in Lean. I assume no Lean; each piece of notation is explained where it first appears.

A list has two cases

[]                 -- Empty.
head :: tail       -- An element followed by a list.

[10, 20, 30] = 10 :: [20, 30]
             = 10 :: 20 :: 30 :: []

head is an element, tail is another list, and :: builds a list from the two. There is no third case. Everything below follows from that: a function on lists has to say what it does with [] and with head :: tail, and a proof about lists has to cover the same two.

Reverse, defined on those cases

def rev {α : Type} : List α → List α
  | []           => []
  | head :: tail => rev tail ++ [head]

α is the element type, ++ joins two lists, and [head] is the list holding only head. For a non-empty list: reverse the tail, then put the head at the end. The recursive call gets a shorter list, so it reaches [] and stops.

Expanding the definition on a small list shows the mechanism:

rev [10, 20, 30]
= rev [20, 30] ++ [10]
= (rev [30] ++ [20]) ++ [10]
= ((rev [] ++ [30]) ++ [20]) ++ [10]
= (([] ++ [30]) ++ [20]) ++ [10]
= [30, 20, 10]

The proof has the same two cases

theorem rev_twice {α : Type} (xs : List α) :
    rev (rev xs) = xs := by
  induction xs with
  | nil => ...
  | cons head tail ih => ...

nil asks for the claim on []. cons asks for it on head :: tail and hands over ih, the induction hypothesis: rev (rev tail) = tail.

Being allowed to assume the claim for the tail can look like cheating. It is not. Establish the rule for the empty list. Then show that whenever it holds for a tail, it still holds after adding a head. That covers length 0, then 1, then 2, and so on. It is one argument for all lengths, not a loop that tries them.

The empty case

  | nil => rfl

rev [] is [] by definition, so rev (rev []) reduces to [] and the goal becomes [] = []. rfl closes an equality whose two sides reduce to the same thing.

The non-empty case needs a helper

Unfolding the definition once gives:

rev (rev (head :: tail))
= rev (rev tail ++ [head])

Now rev is applied to two joined lists, and the definition does not say what that is. It takes a separate fact: reversing joined lists reverses each part and swaps their order.

theorem rev_append {α : Type} (xs ys : List α) :
    rev (xs ++ ys) = rev ys ++ rev xs := by
  induction xs with
  | nil => simp [rev]
  | cons head tail ih =>
      simp [rev, ih, List.append_assoc]

A proved fact used inside another proof is called a lemma. This one is again by induction on the two cases. simp unfolds rev and rewrites with the hypothesis for the tail; List.append_assoc says that the grouping of joined lists does not matter.

With the lemma, the non-empty case is four steps:

rev (rev (head :: tail))
= rev (rev tail ++ [head])
= rev [head] ++ rev (rev tail)     -- By rev_append.
= [head] ++ tail                   -- By the definition and ih.
= head :: tail

The head returns to the front, and the tail is restored by the induction hypothesis. At no point was a length or an element value chosen.

The complete proof

theorem rev_twice {α : Type} (xs : List α) :
    rev (rev xs) = xs := by
  induction xs with
  | nil => rfl
  | cons head tail ih =>
      calc
        rev (rev (head :: tail))
            = rev (rev tail ++ [head]) := rfl
        _ = rev [head] ++ rev (rev tail) := rev_append _ _
        _ = [head] ++ tail := by rw [ih]; rfl
        _ = head :: tail := rfl

Lean checks every step. If one did not follow, the file would not compile.

What was established

This is the gap the previous post ended on, closed. No generator bounds, no sample count, no luck.

One sentence above carries more weight than it seems to: the proof is about rev, the three-line Lean definition. It says that this definition, composed with itself, is the identity. It does not mention the C# method or the Go function from the previous post, and it does not say that rev reverses anything.

Next: The Theorem Holds for the Wrong Function