The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

In my opinion, it is a very handy feature to make out-of-the-box vectors 
difficult to work with, since almost no one should be using dependently 
typed vectors for anything.

On 12/17/2017 10:39 AM, Emilio Jesús Gallego Arias wrote:
> Hi all,
>
> I don't mean to start any kind of controversial discussion but I can't
> stop wondering about:
>
> a) whether "Vector" and "Fin" are really usable libraries
>
> b) if it is OK that Coq proposes it as the standard solution for sized
>     lists and bounded integers to newcomers
>
> IMHO, having to learn ultra-advanced pattern matching patterns in order
> to manipulate vectors and ordinals seems a bit of a too step learning
> curve, specially for such pervasive structures.
>
> An even so, learning all that may not be enough, for example, try to
> prove the following lemma:
>
>   `∀ x, Vector.rev (Vector.rev x) = x`.
>
> Unless I am missing something, it seems like a fun proof to.
>
> I wonder, what do others think?
>
> Best,
> E.