The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

>>>>> Cedric Auger 
>>>>> <sedrikov AT gmail.com>
>>>>>  writes:

> This way dependant types will be less annoying to deal with.

Hi Cedric,

I've moved to the following dependent type:

    Definition Vec : nat -> Type :=
      fix vec n := match n return Type with
                   | O   => Void
                   | S O => A
                   | S n => prod A (vec n)
                   end.

In general, this has worked out quite well.  However, I'm still having
difficulty with one lemma in particular (where fin n is "ordinal n" from
ssreflect):

  Lemma vnth_replace_neq : forall n (v : Vec n) (k j : fin n) (z : A),
    k != j -> vnth (replace v k z) j = vnth v j.

The problem seems to be that I need to relate three different things in
lock-step: v, k and j.  I've tried induction on all three, and also n, but
each direction leaves me with a branch where it asks to prove something that
doesn't make sense.

You can see the code I have so far here, if interested:

    https://github.com/jwiegley/linearscan/blob/master/Vector2.v#L209

I also tried building a recursion principle that would walk over the vector at
the same time as its indices, but I'm not sure if this is a worthwhile avenue
to continue pursuing.

Thanks, John