The Coq mailing list

[Qinshi Wang <qinshiw AT cs.princeton.edu>]

I would like to pop up with my piece of experience. I agree with jtm that refinement type (a type with a constraint, e.g. {xs : list a | length xs = n}) is easier to use. In particular, it's nice to bind additional information like lengths as a part of types when we don't need to maintain it explicitly. For example, when we have lists of the same length and we usually only read and write to list entries without changing length. In this case, dependent type is your friend. But when you need to write functions to construct lists of different lengths, dependent type is not so friendly. For example, you need to annotate the length for each intermediate value. So refinement type provides the flexibility that one can maintain the constraint part when it's useful and drop it when it's a burden. When it's needed again, we can reconstruct the constraint by giving a proof. Program definition [2] makes this procedure easier. For example,

Require Import Coq.Program.Tactics.

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

Program Definition vector_app {A n m} (xs : vector A n) (ys : vector A m) : vector A (n+m) :=

  exist _ (app xs ys) _.

Next Obligation.

  ...

Qed.

This makes the definition more clear. And a benefit is that the definition is transparent but the proof for the constraint is opaque. 

We have an open-source tool [3] for proving list length and indexing that you might find useful. It has a nice automatic prover. It is for basic lists indexed by Z instead of nat, because Z is more intuitive for arithmetic (while the advantage for nat is induction). 

Thanks,

Qinshi

[2] https://coq.inria.fr/refman/addendum/program.html
[3] https://github.com/PrincetonUniversity/VST/tree/master/zlist

On Mon, May 16, 2022 at 11:08 AM jtm <me AT jtm.cx> wrote:

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