The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

I'm stuck again in trying to write some dependent code. I want to index a
vector:

  Section vectors.
  
  Variable (A : Set).
  
  Inductive vec : nat -> Set :=
    | vnil : vec 0
    | vcons : forall n, A -> vec n -> vec (S n).
  
  Inductive fin : nat -> Set :=
    | finz : fin 1
    | fins : forall n, fin n -> fin (S n). 
  
  Fixpoint vind n (i : fin n) {struct i} : vec n -> A :=
    match i in fin n return vec n -> A with
    | finz => fun v => 
        match v in vec m return (match m with 0 => True | S _ => A end) with
        | vnil => I
        | vcons _ x _ => x
        end
    | fins m j => fun v =>
        match v in vec m return (match m with 0 => True | S _ => A end) with
        | vnil => I
        | vcons m' _ xs => vind m j xs (* wrong *)
        end
    end.

Unfortunately, this code does not typecheck; the line marked as (* wrong *)
gives

  Error:
  In environment
  A : Set
  vind : forall n : nat, fin n -> vec n -> A
  n : nat
  i : fin n
  m : nat
  j : fin m
  v : vec (S m)
  m' : nat
  a : A
  xs : vec m'
  The term "xs" has type "vec m'" while it is expected to have type "vec m"

It seems clear to me (but apparently not to the Coq typechecker) that m and m'
must be the same. Obviously, I can rewrite this code using inversion, but that
yields a large term which, moreover, includes an equality proof of m and m' --
which makes proofs more difficult because equality proofs are not transparent.
Is there another way?

Thanks,

Edsko