Proving Length Preservation by List Map Example

Assume the following type 'a list is inductive. Prove that length (map f l) = length l for all lists l : 'a list and all total functions f : 'a -> 'b.

ocaml

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

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

let rec map : ('a -> 'b) -> 'a list -> 'b list =
  fun f l ->
    match l with
    | [] -> []
    | x :: xs ->
        let y = f x in
        let ys = map f xs in
        y :: ys

Solution

Let l : 'a list and f : 'a -> 'b be total.

We proceed by structural induction on the list l.

Case l = []:
By definition of map:
ocaml
```
length (map f [])
= length []
```
Case l = x :: xs:
Our induction hypothesis is that length (map f xs) = length xs.
By definition of map and length, as well as the induction hypothesis:
ocaml
```
length (map f (x :: xs))
= length (f x :: map f xs)
= 1 + length (map f xs)
= 1 + length xs
```
Likewise:
ocaml
```
length (x :: xs)
= 1 + length xs
```

Therefore, length (map f l) = length l holds for all lists l : 'a list and all total functions f : 'a -> 'b.