The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Dear Mukesh,

I have been working with Vector.t/Fin.t for quite a while.
In fact, long enough from a time where the standard library
was not as complete as it is now and so I did develop my
own library which is fully compatible with the standard
lib. The stdlib still has pitfalls IMHO, see below.

I used to denote vectors and positions by 

vec : Type -> nat -> Type
pos : nat -> Type

Indeed Fin meaning "finite" is too general a qualifier (it
can mean many other things in the devels I was/am involved
with) so I did call it pos(ition) but that itself clashes
with pos(itive) which I do not use though. Recently, I did 
switch to idx (for index) instead of pos but that is not 
published for the moment, hopefully soon.

I did program with vectors in the context of dependent trees

Inductive dtree (X : nat -> Type) : Type :=
  | dtree_cons k : X k -> vec (dtree X) k -> dtree X.

These can be quite tricky until you find the right tools. 
The thing I learned along is that there are ways to program 
more or less smoothly with dependent types, but much lesser 
that with non-dependent types (eg lists). And all the other 
ways lead you to (setoid) hell.

In particular, it took me quite some type to program

vec_pos {X n} : vec X n -> pos n -> X

so that vec_pos v p can be recognised as a sub-term of v
by Coq, which is quite handy for dtree. In particular,
you need a carefully designed inversion lemma:

pos_inv {n} : pos (S n) -> option (pos n)

In general, you need to master dependent pattern matching 
and program small inversions by hand if you want Fixpoints
to guard-check.

As said, this development is still unpublished also but you 
can find something close (mu-recursive algorithms) here:

https://github.com/DmxLarchey/Coq-is-total

In particular, you can look at the recalg_rect recursor
in recalg.v and vec_pos in vec.v.

Vectors are also used at least for Minsky machines and 
FOL/Trakhtenbrot in the Coq library undecidability:

https://github.com/uds-psl/coq-library-undecidability

see Shared/Libs/DLW/Vec/

where they are interfaced with Vector.t, using the
same underlying inductive type Vector.t/vec and Fin.t/pos.

Good luck,

Dominique


----- Mail original -----
> De: "mukesh tiwari" <mukeshtiwari.iiitm AT gmail.com>
> À: "coq-club" <coq-club AT inria.fr>
> Envoyé: Dimanche 15 Mai 2022 20:40:58
> Objet: [Coq-Club] Experience with formalising projects with length indexed 
> vector (Vector.t) and finite type (Fin.t)

> 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?
> 
> Best,
> Mukesh
> 
> [1] https://coq.inria.fr/library/Coq.Vectors.VectorDef.html