The Coq mailing list

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

Hello John,

John Wiegley 
<johnw AT newartisans.com>
 writes:

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

I'm sure you already know about it, but given that you are using
ordinals, moving to ssreflect tuples could also work well for this case.

I have tried different Vector approaches, so far the n.-tuple one works best
for me.

A definition of replace (set_tnth) and the lemma using tuples could be:

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype 
tuple.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section SetNthTuple.

  Variables (n : nat) (T : Type).

  Implicit Types (i : 'I_n) (t : n.-tuple T) (x : T).

  Lemma set_nth_tupleP t i x :
    size (set_nth (tnth_default t i) t i x) == n.
  Proof. by rewrite size_set_nth size_tuple maxnE addnC subnK. Qed.

  Canonical set_nth_tuple t i x := Tuple (set_nth_tupleP t i x).

  Definition set_tnth t i x :=
    [tuple of set_nth (tnth_default t i) t i x].

  Lemma set_tnth_nth t i x :
    set_tnth t i x = set_nth (tnth_default t i) t i x :> seq T.
  Proof. by []. Qed.

End SetNthTuple.

Lemma vnth_replace_neq
      (T : eqType) n
      (t : n.-tuple T)
      (k j : 'I_n)
      (z : T) :
  j != k ->
  tnth (set_tnth t k z) j = tnth t j.
Proof.
  rewrite -val_eqE /= => /negbTE Hidx.
  rewrite (tnth_nth (tnth_default t k))
          (tnth_nth (tnth_default t j)).
  by rewrite set_tnth_nth nth_set_nth /= Hidx -!tnth_nth.
Qed.

Best regards,
Emilio