# Writing a function to find the head of each item in list of lists

Hi! I am very new to Coq and I’m trying to prove a simple matrix transpose function. As part of my matrix transpose, I have a function called `maphd`, which takes the head of each item in a list of lists, and returns the result as a new list.

I have:

``````    Fixpoint maphd (l: list (list A)): (list A):=
match l with
| nil => nil
| a :: t  => (hd a):: (maphd t)
end.
``````

However, this fails with the error:

``````In environment
A : Type
maphd : list (list A) -> list A
l : list (list A)
a : list A
t : list (list A)
The term "maphd t" has type "list A"
while it is expected to have type "list (list (list A) -> list A)".
``````

I don’t know how to put this right!

I should add, I have a separate `hd` function to get the head of a list, which compiles fine.

What is the type of your `hd` function?

The following seems to work:

``````Fixpoint maphd (hd : list A -> A) (l: list (list A)) : (list A):=
match l with
| nil => nil
| a :: t  => (hd a):: (maphd hd t)
end.
``````

Here is my `hd` function:

``````  Definition hd (default:A) (l:list A): A :=
match l with
| [] => default
| x :: _ => x
end.
``````

so `hd` needs a `default` argument.
You should probably do the same in `maphd`. What behavior are you waiting for in `maphd [ [] ]` ?

The type of “hd” is not what you think it is

Gaëtan Gilbert

So you mean if I supply an empty list of lists? I would expect an empty list back, I guess.

Ah ok. So where have I gone wrong?

First you cannot imagine have a `hd` function from `list A` to `A` for an arbitrary `A`. This is why you need a `default` argument in the definition of `hd`. This leads to `hd : A -> list A -> A`.
Then in your code for `maphd`, the term `hd a` should be `hd default a : A` for some appropriate `default` element of type `A`. So the most direct modification of your `maphd` would be:

``````Fixpoint maphd (default : A) (l: list (list A)) : (list A):=
match l with
| nil => nil
| a :: t  => (hd default a):: (maphd default t)
end.
``````

which leads to `maphd default [ [] ] = [ default ]`.

Now if you want `maphd` to throw away empty lists, you have to say so in the code:

``````Fixpoint maphd (l: list (list A)) : (list A):=
match l with
| nil => nil
| nil :: t => maphd t
| (a :: r) :: t  => (hd  a (a::r)):: (maphd t)
end.
``````

(here choosing `a` as `default` argument) but then the call to `hd` can be inlined to get:

``````Fixpoint maphd (l: list (list A)) : (list A):=
match l with
| nil => nil
| nil :: t => maphd t
| (a :: r) :: t  => a :: (maphd t)
end.
``````

Thank you so much! I’ll need to take some time to parse and understand your reply, but it looks immensely helpful.

1 Like