Prouver la conservation de longueur de liste par « map » Exemple

Suppose que le type 'a list est inductif. Prouve que length (map f l) = length l pour toutes listes l : 'a list et toutes fonctions totales 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

Soient l : 'a list une liste et f : 'a -> 'b une fonction totale.

Nous procédons par le principe d'induction structurelle sur la liste l.

Cas l = []:
Par définition de map:
ocaml
```
length (map f [])
= length []
```
Cas l = x :: xs:
Notre hypothèse d'induction est que length (map f xs) = length xs.
Par définition de map et length, et grâce à l'hypothèse d'induction:
ocaml
```
length (map f (x :: xs))
= length (f x :: map f xs)
= 1 + length (map f xs)
= 1 + length xs
```
Similairement:
ocaml
```
length (x :: xs)
= 1 + length xs
```

Par conséquent, length (map f l) = length l est vraie pour toutes listes l : 'a list et fonctions totales f : 'a -> 'b.