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

Question

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?

Answer 1

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

Answer 2

Transport (cf. Théo's answer) is indeed a common solution. A less common one is to use a more direct form of heterogeneous equality. Instead of the homogeneous eq, use eq_dep, imported from Coq.Logic.Eqdep.

To state the equation between to_d (from_d l) : dlist a (len (from_d l)) and l : dlist a n:

1. Find the difference between the two types, in this case len (from_d l) vs n, which are of type nat;

2. Find the common context around those differences: dlist a (or fun n => dlist a n), i.e., the function that maps the previous terms to the respective types of the two sides of the desired equation.

3. The first argument of eq_dep is the type of the differences (nat); the second argument is the common context (dlist a); the third argument is the term to pass that context to get the type of the left hand side (one might call it the "type index" of the LHS, len (from_d l)); the fourth argument is the left hand side of the equation; fifth and sixth similarly describe the right hand side.

The resulting theorem is stronger than the transport version: it states equality of both terms and both their type indices at the same time, whereas transport requires the proof of equality of type indices (n = len (from_d l)) to be made separately. Furthermore, with transport, that equality proof would explicitly appear as a term of the final equality theorem, whereas heterogeneous equality does not expose such superfluous data.

The proof has a straightforward structure (in fact, the exact same script works for the similar theorem for simple lists), but also hides a lot of complexity that one nevertheless needs to be aware of when carrying out such proofs. Familiarity with dependent pattern-matching and some idea of the proof terms that tactics generate is warmly recommended.

Require Import Coq.Logic.Eqdep.

(* "to_d (from_d l) = l" *)
Theorem d_round : forall (a : Set) (n : nat) (l : dlist a n),
    eq_dep _ (dlist a) _ (to_d (from_d l)) _ l.
(* In full: eq_dep nat (dlist a) (len (from_d l)) (to_d (from_d l)) n l *)
Proof.
  intros.
  induction l.
  - simpl.
    reflexivity.
  - simpl.
    rewrite IHl.
    reflexivity.
Qed.