The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-11-10 10:49 GMT+01:00 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.

​I am sorry to have mentionned Empty_set for the base case. I meant "unit" (and you do not require the "S O" case, as "prod A unit" is isomorphic to "A").​

 

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.

​If you use my definition, you should as well use "vector unit n" instead of "fin n", for same reasons as why to change from previous vector type. Then recursion over "n" should be enough.​

 

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

--

.../Sedrikov\...