Coq adding a new variable instead of using the correct one

Question

I'm working on my own implementation of vectors in Coq, and I'm running into a bizarre problem.

Here is my code thus far:

Inductive Fin : nat -> Type :=
  |FZ : forall n, Fin (S n)
  |FS : forall n, Fin n -> Fin (S n).

Definition emptyf(A : Type) : Fin 0 -> A.
  intro e; inversion e.
Defined.

Inductive Vec(A : Type) : nat -> Type :=
  |Nil  : Vec A 0
  |Cons : forall n, A -> Vec A n -> Vec A (S n).

Definition head(A : Type)(n : nat)(v : Vec A (S n)) : A :=
  match v with
  |Cons a _ => a
  end.

Definition tail(A : Type)(n : nat)(v : Vec A (S n)) : Vec A n :=
  match v with
  |Cons _ w => w
  end.

Fixpoint index(A : Type)(n : nat) : Vec A n -> Fin n -> A :=
  match n as n return Vec A n -> Fin n -> A with
  |0   => fun _ i => emptyf _ i
  |S m => fun v i => match i with
                     |FZ _ => head v
                     |FS j => index (tail v) j
                     end
  end.

Everything up to tail compiles fine, but when I try to compile index, I receive the following error:

Error:
In environment
index : forall (A : Type) (n : nat), Vec A n -> Fin n -> A
A : Type
n : nat
m : nat
v : Vec A (S m)
i : Fin (S m)
n0 : nat
j : Fin n0
The term "j" has type "Fin n0" while it is expected to have type "Fin m".

Clearly, the culprit is that Coq introduces the new variable n0 instead of assigning j the type Fin m, even though this is the only possible type for j which would result in i being built from j. Any idea why this would happen, and how I might be able to resolve this issue?

Answer 1

I find Vec and Fin very hard to use in general, so I these days I use 'I_n and n.-tuples T from math-comp, which are just naturals and lists with an irrelevant proof attached. However, if you want to continue the fun of complex pattern matches, you could try to define a stronger pattern matching principle:

Definition fin_case T m (i : Fin m) : T -> (Fin (pred m) -> T) -> T :=
  match i with
  | FZ _   => fun fn fz => fn
  | FS _ j => fun fn fz => fz j
  end.

Once you have fin_case, you function definition works:

Fixpoint index (A : Type) (n : nat) : Vec A n -> Fin n -> A :=
  match n as n return Vec A n -> Fin n -> A with
  | 0   => fun _ i => emptyf _ i
  | S m => fun v i => fin_case i (head v) (index (tail v))
  end.