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

Using Rocq
1

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!

2

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

3

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.
4

Here is my hd function:

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

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

6

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

Gaëtan Gilbert

7

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

8

Ah ok. So where have I gone wrong?

9

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.
Proving matrix transpose function
10

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

1 Like