Proving Structural Equivalence of List Length Computations Example

Assume the following type 'a list is inductive. Prove that length l = length_tl l 0 for all lists l.

ocaml

type 'a list =
  | []
  | (::) of 'a * 'a list

let rec length : 'a list -> int =
  function
  | [] -> 0
  | _x :: xs -> 1 + length xs

let rec length_tl : 'a list -> int -> int =
  fun l acc ->
    match l with
    | [] -> acc
    | _x :: xs -> length_tl xs (1 + acc)

Solution

If we attempt to prove the initial proposition by structural induction, we'll end up with the issue that the induction hypothesis length xs = length_tl xs 0 won't be useful to prove length (x :: xs) = length_tl (x :: xs) 0. We'll first prove a more general proposition, and use that to show the initial proposition.

We need to show that length l + acc = length_tl l acc for all lists l and all integer acc. We proceed by structural induction on l.

Case l = []:
By definition of length:
ocaml
```
length [] + acc
= 0 + acc
= acc
```
By definition of length_tl:
ocaml
```
length_tl [] acc
= acc
```
Case l = x :: xs:
Our induction hypothesis is that length xs + a = length_tl xs a for all a.
By definition of length and the induction hypothesis:
ocaml
```
length (x :: xs) + acc
= 1 + length xs + acc
= length xs + (1 + acc)
= length_tl xs (1 + acc)
```
By definition of length_tl:
ocaml
```
length_tl (x :: xs) acc
= length_tl xs (1 + acc)
```

Since the more general proposition length l + acc = length_tl l acc holds for all lists l and all integer acc, then letting acc = 0 demonstrates that length l = length_tl l 0 for all lists l.