Coq: type mismatch on dependent lists which could be solved by a proof

During my last play with lists in coq I have encountered a type problem. But first, the definitions;

Casual list:

Inductive list (a : Set) : Set :=
| nil : list a
| cons : a -> list a -> list a
.

Fixpoint len {a : Set} (l : list a) : nat :=
  match l with
  | nil _ => 0
  | cons _ _ t => 1 + (len t)
  end.

Dependent list:

Inductive dlist (a : Set) : nat -> Set :=
| dnil : dlist a 0
| dcons : a -> forall n, dlist a n -> dlist a (S n)
.

Conversions:

Fixpoint from_d {a : Set} {n : nat} (l : dlist a n) : list a :=
  match l with
  | dnil _ => nil _
  | dcons _ h _ t => cons _ h (from_d t)
  end.

Fixpoint to_d {a : Set} (l : list a) : dlist a (len l) :=
  match l with
  | nil _ => dnil _
  | cons _ h t => dcons _ h _ (to_d t)
  end.

I wanted to prove the conversion roundabout, strictly speaking

Theorem d_round : forall (a : Set) (n : nat) (l : dlist a n),
    to_d (from_d l) = l.

But I get the following error:

The term "l" has type "dlist a n" while it is expected to have type
 "dlist a (len (from_d l))".

It is quite easy to understand, but I have completely no clue how to workaround it. I can easily prove that

forall (a : Set) (n : nat) (l : dlist a n), n = len (from_d l).

but I see no way to use this theorem to convince Coq that the length of the list remains the same. How to do it?

Solution

What you're trying to prove is a heterogenous equality, l and to_d (from_d l) have different types and therefore cannot be compared with the homogenous equality type (=).

Were the theory extensional it would be a different matter (equal types would be convertible), however you have to deal with this discrepancy manually. One way to do this is to define some transport which corresponds to the Leibniz principle: from x = y you derive P x -> P y for any P.

Definition transport {A} {x y : A} (e : x = y) {P : A -> Type} (t : P x) : P y :=
  match e with
  | eq_refl => t
  end.

In your case it would be n = m -> dlist A n -> dlist A m so you could even use a specialised version.

The theorem can then be stated as:

Axiom e : forall (a : Set) (n : nat) (l : dlist a n), n = len (from_d l).

Theorem d_round : 
  forall (A : Set) (n : nat) (l : dlist A n),
    to_d (from_d l) = transport (e _ _ _) l.

Now you have to deal with the equality that gets in your way, but equality on natural numbers is decidable and thus a proposition (any two proofs of n = m are always equal, in particular any proof of n = n is equal to eq_refl; a fact well-combined with transport eq_refl t = t).