The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi. You can have a look at the lemma Vnth_replace in the file 
Util/Vector/VecUtil.v of the CoLoR library (http://color.inria.fr). Best 
regards, Frédéric.

Le 09/11/2014 11:33, John Wiegley a écrit :
> Hello,
>
> I'm having difficulty proving the following, using Coq.Vectors.Vector:
>
>      Lemma nth_replace {A : Type} : forall n (v : t A n) k x,
>        nth (replace v k x) k = x.
>
> The induction principle is unable to accept an argument of type t A n.+1.  Is
> this a case where a custom principle is needed?  What form would that take?
> I've tried a few, but nothing so far has allowed me to progress.
>
> Any help is greatly appreciated,
>    John