The Coq mailing list

[Matěj Grabovský <matej.grabovsky AT gmail.com>]

Hello.

I'm trying to prove the following, apparently simple statement about
the Vector.replace function from the standard library (the full code
is at http://lpaste.net/360859):

    forall {A n} (xs : Vector.t A n) i x, (Vector.replace xs i x)[@i] = x

Although I can prove this just fine using Program, I'd also like to
perform the proof without it, without assuming additional axioms.
However, I can't quite wrap my head around what's going on with all
the type dependencies.

I can destruct the with an intricate matching trick, but I'm unable to
proceed in the latter branch as I need more information for the proof
to progress.

What is the Coq canonical/recommended approach to dependent induction
without on inductives indexed by types with decidable equality? Is
there a general approach to this? If not, how would I go about this in
the Vector case?

Note that I'm not looking for alternatives to stdlib Vector or
specialised libraries as of now. I'd very much like to understand the
concept in vanilla Coq first.

Best regards,

Matěj