The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

On Wed, May 20, 2020 at 05:29:19PM +0200, Dominique Larchey-Wendling wrote:
> Quick fix ... project your vector into a list ;-)
>

Interessting, do you know any function that does that for me?

You can get between list T and sigT (vector T) freely, or otherwise between { l : list T & length l = n } and vector T n. I have a tool called DEVOID that ports proofs between types like these including lists and vectors. It can probably just spit out the thing you want for you if you want to use it directly. But if that feels too heavy-weight for you, you can just use the conversion functions it generates automatically:

https://www.reddit.com/r/dependent_types/comments/g8v59q/coq_applying_a_proof_on_lists_to_a_proof_on/fov7w1t/?context=3

If you want a particular function or proof over vectors from one over lists I can generate it, but I'm a bit busy so it won't be immediate. I'm hoping to port the entire list library at some point. The process looks like this. Note how to get functions and proofs over vectors of a particular length, rather than over sigT (vector T), you need not only a list function but also its length.

On Wed, May 20, 2020 at 9:16 AM Fritjof Bornebusch <fritjof AT uni-bremen.de> wrote:

On Wed, May 20, 2020 at 05:29:19PM +0200, Dominique Larchey-Wendling wrote:
> Quick fix ... project your vector into a list ;-)
>

Interessting, do you know any function that does that for me?

>
> ----- Mail original -----
> > De: "Fritjof Bornebusch" <fritjof AT uni-bremen.de>
> > À: "coq-club" <coq-club AT inria.fr>
> > Envoyé: Mercredi 20 Mai 2020 17:15:33
> > Objet: [Coq-Club] nth element of a vector
>
> > Hi there,
> >
> > I'm looking for a function that iterates over a vector -
> > https://coq.inria.fr/library/Coq.Vectors.Vector.html - and returns
> > the Zth element, like the nth element of a list.
> >
> > The library function only dealy with the Fin.t type, but I need Z.
> > Does anyone has a suggestion or hint?
> >
> > Best Regards,
> > --f.