The Coq mailing list

[gallego AT cri.ensmp.fr (Emilio Jesús Gallego Arias)]

Hello John,

"John Wiegley" 
<johnw AT newartisans.com>
 writes:

> 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.

I don't know how to prove it without using a destruction or
elimination principle specific for an n.+1 index.

The simplest proof may be to elim the vector, then destroy the (k : Fin
n.+1) using the Fin.caseS method:

,----
| Lemma nth_replace {A : Type} : forall n (v : t A n) k x,
|       nth (replace v k x) k = x.
| Proof.
|   move=>n.
|   elim:n/ =>[H|x n v IH i].
|   - inversion H.
|   - move: n i v IH.
|     by apply: Fin.caseS=>/=.
| Qed.
`----

Best regards,
Emilio