Trying to define a "rect2"-like function on heterogeneous vectors

I have the following (hopefully non-controversial!) definition of heterogeneous vectors:

Require Vectors.Vector.
Import Vector.VectorNotations.

Section hvec.
  Variable A : Type.
  Variable B : A -> Type.

  Inductive t : forall k : nat, Vector.t A k -> Type :=
  | nil : t 0 []
  | cons :
      forall (a : A) (b : B a) (k : nat) (v : Vector.t A k), t k v -> t (S k) (a :: v).

  Local Notation "[! ]" := nil (format "[! ]").
  Local Notation "h :! t" := (cons _ h _ _ t) (at level 60, right associativity).
  Local Notation "[! x ]" := (x :! [! ]).

I'd like to define an eqb function (assuming there's one for the component types). To define one, I think I need something like a rect2. Following on from the Vectors library by analogy, I think its type should be something like this:

  Fixpoint rect2
             (P : forall {k : nat} {v : Vector.t A k} (hv0 hv1 : t k v), Type)
             (bas : P nil nil)
             (rect : forall {k : nat} {v : Vector.t A k} {hv0 hv1 : t k v},
                 P hv0 hv1 ->
                 forall (a : A) (b0 b1 : B a), P (b0 :! hv0) (b1 :! hv1))
             {k : nat}
    : forall (v : Vector.t A k) (hv0 hv1 : t k v), P hv0 hv1.

The problem is that I can't work out how to get all the dependent types to go through properly. Matching on k, then v then hv0 (which seemed like the obvious approach to me) doesn't seem to work. The problem is that you get this far:

refine (
    match k with
    | 0 =>
      fun v =>
        match v with
        | [] =>
          fun hv0 hv1 => _
        | _ => tt
        end
    | S k' => _
    end
).

but then can't match on hv0 sensibly. With no return annotation (match hv0 with ...), the types look like this:

  ...
  v : Vector.t A 0
  hv0, hv1 : t 0 []
  ============================
  P 0 [] hv0 hv1

(note the hv0 in the obligation, not a nil). Trying to write return annotations like match hv0 as hv0' return P 0 [] hv0' hv1 with ... doesn't help because now the type of hv0' has lost the fact that k was zero.

I assume there's a clever trick / correct order to write this sort of thing. Could someone help?

Solution

You can do the inversion with an involved dependent pattern match as follows:

 Fixpoint rect2
             (P : forall {k : nat} {v : Vector.t A k} (hv0 hv1 : t k v), Type)
             (bas : P nil nil)
             (rect : forall {k : nat} {v : Vector.t A k} {hv0 hv1 : t k v},
                 P hv0 hv1 ->
                 forall (a : A) (b0 b1 : B a), P (b0 :! hv0) (b1 :! hv1))
             {k : nat}
    : forall (v : Vector.t A k) (hv0 hv1 : t k v), P hv0 hv1.
 Proof.
   intro v.
   induction v using Vector.t_rect.
   - intros hv0.
     refine (
            (* match on hv0, retaining info on its indices *)
             match hv0 as z in t k l return forall (hv1 : t k l),
                 (* match on the abstracted index l : Vector.t A k *)
                 match l as l' in Vector.t _ k'
                               return forall (hv0 hv1 : t k' l'), Type
                 with
                 (* when l = [] we have our goal *)
                 | [] => P 0 []
                 (* otherwise we create a dummy goal that we can fulfill *)
                 | _ => fun _ _ => unit
                 end z hv1
             with
             | [!] => _ (* Actual goal with hv0 replaced by [!] *)
             | _ => fun _ => tt  (* Dummy goal of type unit *)
             end).

Playing a bit with these kinds of pattern matches can teach you how dependent types work (or not) but it quickly becomes tedious. To go further, the Equations library provides some utilities to handle type dependency and in particular to help with this kind of dependent inversions. Here is a complete solution using Equations:

Require Vectors.Vector.
Import Vector.VectorNotations.

From Equations Require Import Equations.

Module VectorInd.
  (* Provided by Equations *)
  Derive Signature NoConfusionHom for Vector.t.
End VectorInd.

Import VectorInd.

Section hvec.
  Variable A : Type.
  Variable B : A -> Type.

  Inductive t : forall k : nat, Vector.t A k -> Type :=
  | nil : t 0 []
  | cons :
      forall (a : A) (b : B a) (k : nat) (v : Vector.t A k), t k v -> t (S k) (a :: v).

  Local Notation "[! ]" := nil (format "[! ]").
  Local Notation "h :! t" := (cons _ h _ _ t) (at level 60, right associativity).
  Local Notation "[! x ]" := (x :! [! ]).

  (* Provided by Equations *)
  Derive Signature NoConfusionHom for t.

 Fixpoint rect2
             (P : forall {k : nat} {v : Vector.t A k} (hv0 hv1 : t k v), Type)
             (bas : P nil nil)
             (rect : forall {k : nat} {v : Vector.t A k} {hv0 hv1 : t k v},
                 P hv0 hv1 ->
                 forall (a : A) (b0 b1 : B a), P (b0 :! hv0) (b1 :! hv1))
             {k : nat}
    : forall (v : Vector.t A k) (hv0 hv1 : t k v), P hv0 hv1.
 Proof.
   intro v.
   induction v using Vector.t_rect.
   all: intros hv0 hv1; depelim hv0; depelim hv1.
   - apply bas.
   - now apply rect, IHv.
 Defined.