The Coq mailing list

[John Wiegley <johnw AT newartisans.com>]

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

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

I was able to complete the proof today, after sleeping on it:

    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.
    Proof.
      move=> n v k j z.
      elim/vec_ind: v => // [x|sz x xs IHxs] in k j *.
        by move: (fin1_eq k j) => /eqP ? /eqP ?.
      elim/@fin_ind: k; elim/@fin_ind: j;
        try by elim: sz => // in xs IHxs *.
      move=> ? ? _ ? ? _ Hneg.
      rewrite replace_consn !vnth_consn IHxs; first by [].
      exact: Hneg.
    Qed.

Thanks for all your help, this is a much nicer direction to move in than the
previous vector representation.

John