Unfold a type-function in a match (like destruct)

Question

TL;DR

I want to write a fixpoint definition that matches over a value inside a dependent type without proof-mode. The essential issue is that Coq won't use the match to notice that the types are equivalent in a dependent type; I can force it in proof-mode, but I wonder if it's possible to do so without it.

---

I'm working on a project that involves lots of matrix operations. The matrices can be arbitrarily many dimensions (each of which is rectangular), so I wrote a definition to compute the type of the matrix:

Require Import Coq.Unicode.Utf8.
Require Export Vector.
Import VectorNotations.
Require Import List.
Import ListNotations.

Fixpoint matrix (A: Type) (dims: list nat) :=
  match dims with
  | [] => A
  | head::tail => Vector.t (matrix A tail) head
  end.

For "reasons" I need to linearize the elements in order to select the nth element of a linearized matrix. My first attempt was to try to return a single-dimensional matrix, but I ran into a wall with List's fold_left (advice on proceeding would be appreciated):

Definition product (dims: list nat) := List.fold_left Nat.mul dims 1.

Definition linearize {A: Type} {dims: list nat} (m: matrix A dims): matrix A [product dims].
Proof.
  generalize dependent m.
  induction dims.
  - intros.
    assert (product [] = 1) by reflexivity. rewrite H; clear H.
    exact (Vector.cons A m 0 (Vector.nil A)).
  - intros.
    (* why so hard? *)
    assert (product (a::dims) = a * product dims).
    { unfold product.
      assert (a::dims = [a] ++ dims) by reflexivity. rewrite H; clear H.
      rewrite List.fold_left_app.
      assert (List.fold_left Nat.mul [a] 1 = a). admit. }
Abort.

I decided it might be easier to convert to a list, so:

Fixpoint linearize' {A: Type} {dims: list nat} (m: matrix A dims): list A :=
  match dims with
  | [] => []
  | h::t => Vector.fold_left
            (@app A)
            []
            (Vector.map linearize' (m: Vector.t (matrix (list A) t) h))
  end.

but Coq complains:

In environment
linearize' : ∀ (A : Type) (dims : list nat), matrix A dims → list A
A : Type
dims : list nat
m : matrix A dims
h : nat
t : list nat
The term "m" has type "matrix A dims" while it is expected to have type
 "Vector.t (matrix (list A) t) h".

I am able to write the definition using a "proof style," but I am flummoxed that I cannot get Coq to accept the fixpoint that is essentially the same!

Definition linearize {A: Type} {dims: list nat} (m: matrix A dims): list A.
Proof.
  induction dims.
  - (* unfold matrix in m. *) (* exact [m]. *) apply [m].
  - simpl in m.
    (* exact (Vector.fold_left (@List.app A) [] (Vector.map IHdims m)). *)
    apply (Vector.map IHdims) in m.
    apply (Vector.fold_left (@List.app A) [] m).
Defined.

It seems like if I could get Coq to destruct the type of m along with dims, like what happens in induction, I would be good to go… here's Print linearize.

linearize = 
λ (A : Type) (dims : list nat) (m : matrix A dims),
  list_rect (λ dims0 : list nat, matrix A dims0 → list A)
    (λ m0 : matrix A [], [m0])
    (λ (a : nat) (dims0 : list nat) (IHdims : matrix A dims0 → list A) 
       (m0 : matrix A (a :: dims0)),
       let m1 := Vector.map IHdims m0 in Vector.fold_left (app (A:=A)) [] m1)
    dims m
     : ∀ (A : Type) (dims : list nat), matrix A dims → list A

Arguments linearize {A}%type_scope {dims}%list_scope _

Answer 1

My first reaction was "List.fold_left, he's going to have a bad time."

Here's a solution using List.fold_right instead.

Definition product (dims: list nat) := List.fold_right Nat.mul 1 dims.

Fixpoint concat {A} {n m : nat} (v : Vector.t (Vector.t A m) n) : Vector.t A (n * m) :=
  match v with
  | []%vector => []%vector
  | (x :: xs)%vector => append x (concat xs)
  end. 

Fixpoint linearize {A: Type} {dims: list nat} : matrix A dims -> matrix A [product dims] :=
  match dims with
  | [] => fun a => (a :: [])%vector
  | head :: tail => fun a => concat (Vector.map (linearize (dims := tail)) a)
  end.

The problem with fold_left is that, in the non-empty case, it unfolds to an immediate recursive call, which keeps too much information hidden for dependently typed programming. One use case might be to define tail-recursive functions, but this is not applicable here.

With fold_right, whenever you pattern-match on dims, the cons case exposes one Nat.mul which permits one use of concat : Vector.t (Vector.t A m) n -> Vector.t A (n * m).

Answer 2

This is one of the major headaches of using dependent types in Coq. The solution is to rewrite linearize so that it returns a function after matching:

Require Import Coq.Unicode.Utf8.
Require Export Vector.
Import VectorNotations.
Require Import List.
Import ListNotations.

Fixpoint matrix (A: Type) (dims: list nat) :=
  match dims with
  | [] => A
  | head::tail => Vector.t (matrix A tail) head
  end.

Fixpoint linearize {A: Type} {dims: list nat} : matrix A dims -> list A :=
  match dims with
  | [] => fun _ => []
  | dim :: dims => fun mat =>
    let res := Vector.map (@linearize _ dims) mat in
    Vector.fold_left (@app _) [] res
  end.

This trick is known as the convoy pattern; you can find more about it here: http://adam.chlipala.net/cpdt/html/MoreDep.html .