The Coq mailing list

[jtm <me AT jtm.cx>]

On Sun, 2022-05-15 at 19:40 +0100, mukesh tiwari wrote:
> Hi everyone,
> 
> Have you formalised some non-trivial project  using vectors, and
> finite type [1]? If yes, then what was your experience? What did you
> like and what did you not like about it? Also, could you point me
> towards your project?

I don't have much experience working with [1], but in the couple
instances where I have, I found it very difficult to do dependent
pattern matching (i.e. `match x return y ...`). I found the following
definition to be much easier to work with:

    Definition vector a n :=
      { xs : list a | length xs = n }.

I prefer this definition for a couple reasons, First, you can write
functions in terms of plain old lists, and then prove things about
their lengths later. Second, a lot of proofs regarding length can
be solved using `lia`. A big disadvantage is that some functions
regarding vectors need to be defined inside proof blocks to deal
with propositions regarding vector length.

An example of defining vector concatenation:

    Definition vector_append : forall a m n,
      vector a m -> vector a n -> vector a (m + n).
    Proof.
      intros a m n [xs P] [ys Q].
      exists (xs ++ ys).
      rewrite List.app_length.
      subst. reflexivity.
    Defined.

Best,
jtm

> [1] https://coq.inria.fr/library/Coq.Vectors.VectorDef.html