Structural induction haskell

I would like to know how I can show in structural induction that list xs , or how the induction work in this:

map f (map g xs) = map (\x -> f(g x)) xs

with this function definition

  map :: ( a -> b ) -> [ a ] -> [ b ]

  map _ [] = []

  map f ( x : xs ) = f x : map f xs

Is it like the math induction or not ?

Thanks in advance

Solution

Structural induction is a generalization of the mathematical notion of induction. Mathematical induction works specifically over natural numbers and splits the situation into two cases: the case where the number is zero, and the case where it's one bigger than any other number. Specifically, this corresponds to the Peano definition of natural numbers, which can be written in Haskell as follows.

data Nat = Zero | Succ Nat

So an inductive proof over this data type splits into two cases, one for each type constructor. The first says "assume we have a Zero; prove it". The second says "assume we have a Succ n where the work is already done for n; now prove it".

Now you want to prove something inductively over lists. The list type can be written (modulo syntax sugar) as

data [a] = [] | a : [a]

to be perfectly precise, this corresponds to the following (magic-free) definition

data List a = Nil | Cons a (List a)

though I'll use the first one, since it's a little cleaner to work with in Haskell. A structural induction proof over [a] shall be split into two cases:

Assume the list is empty. Prove the statement.
Assume the list is non-empty and whatever we wanted to prove is true for the tail. Prove the statement for the whole list.

So let's apply that to map. Here's your map function.

map :: (a -> b) -> [a] -> [b]
map _ [] = []
map f (x : xs) = f x : map f xs

and the thing we want to prove is, written precisely:

Let f :: b -> c and g :: a -> b be arbitrary functions. Then prove that, for any list xs :: [a], we have
map f (map g xs) = map (\y -> f (g y)) xs 

Let's begin. There are two cases. First, assume xs is empty, i.e. xs == []. Then, straight from the function definition above, we know map g xs == map g [] == [] and the same for f, so we have the following equivalences

map f (map g [])
map f []
[]
map (\y -> f (g y)) []

Each of these deductions follows from the definition of map, since we have a complete understanding of what map does to the empty list (namely, it doesn't do anything, and the function makes no difference). So the first case is complete.

Now, the inductive step. Assume we have a list (x : xs), and assume the statement is true for xs. So we're assuming

map f (map g xs) == map (\y -> f (g y)) xs

and we want to prove

map f (map g (x : xs)) == map (\y -> f (g y)) (x : xs)

So let's proceed step-by-step.

map f (map g (x : xs))
map f (g x : map g xs)           -- By the function definition
f (g x) : map f (map g xs)       -- By the function definition
f (g x) : map (\y -> f (g y)) xs -- By induction hypothesis
map (\y -> f (g y)) (x : xs)     -- By the function definition

Hence, the statement holds.

By structural induction, the statement holds for [] and, assuming the statement holds for xs, it holds for x : xs as well. Hence, we can conclude that it holds for all finite lists.

Structural induction is not powerful enough to prove that it holds for infinite lists. Haskell's [a] type (and indeed Haskell in general) is a weird mix of induction and coinduction that makes a formal mathematical proof of this a bit awkward. Going strictly by the inductive definition, the type [a] should not have any infinite cases, so we shan't worry about them for the purposes of this proof.