Library Coq.Vectors.Vector

N.B.: Lists inductively defined with a dependency on their length, here called vectors, are popular in dependent type programming: programs embed their specification and only programs are manipulated. However, this currently requires mastering advanced dependent type programming to simultaneously handle the list manipulation and the specification of its length. We recommend using lists bundled with, when needed, a proof about their length rather than vectors. (Thanks to the proof irrelevance of equality on nat, any two bundlings of a same list are provably equal.) This decouples the two aspects above, making it easy to write code in Gallina and develop proofs with tactics. Such an implementation can be found for instance in https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/tuple.v One can read more about this tuple type in section 7.1 of this book: https://doi.org/10.5281/zenodo.4282710 . In particular, this implementation comes with coercion and canonical structures so that lists and tuples can be transparently mixed most of the time. For instance, after From mathcomp Require Import seq tuple., in Context n1 n2 T (v1 : n1.-tuple T) (v2 : n2.-tuple T) (foo : (n1 + n2).-tuple T -> bool). one can write Check foo (v1 ++ v2)., where ++ is the list concatenation, and Coq will automatically elaborate it, as Set Printing All. would show, to foo (cat_tuple v1 v2) where cat_tuple is the lifting of ++ on tuples. Another representation can be found in https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Datatypes/HList.v where tuples can be manipulated through the of_list and to_list functions. This has to be done manually though as the library doesn't automate it. To give an example of the difficulties faced with Vector.t, writing VectorDef.rev constitutes a good exercise. This proves fairly tricky and requires reimplementing dependent type versions of functions already written on lists (typing Vector.rev even relies on a tail-recursive version of the addition on natural numbers whose computational content structurally follows the one of the auxiliary function Vector.rev_append from which Vector.rev is defined; additionally, the computational content is intertwined with some rewriting steps). In contrast, the dependent pair encoding reuses functions and lemmas already written on lists and the definition (called rev_tuple in mathcomp's tuple.v) only needs the property that rev preserves the length:
Require Import List.

Record tuple_of (n : nat) T := Tuple
  { tval :> list T; tsize : length tval = n }.

Lemma rev_tupleP [T n] (t : tuple_of n T) : length (rev t) = n.
Proof. now rewrite length_rev, tsize. Qed.
Canonical rev_tuple T n (t : tuple_of n T) := Tuple n T (rev t) (rev_tupleP t).


Section TestRevTuple.
Variables (T : Type) (n : nat) (t : tuple_of n T).
Check rev t : tuple_of n T.

Thus lemmas about lists are enough in most cases.

Vectors. Initial Author: Pierre Boutillier Institution: PPS, INRIA 12/2010 Originally from the contribution bit vector by Jean Duprat (ENS Lyon). Based on contents from Util/VecUtil of the CoLoR contribution