The Coq mailing list

[Fritjof Bornebusch <fritjof AT uni-bremen.de>]

On Wed, May 20, 2020 at 10:36:29AM -0700, Talia Ringer 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?
> 
>    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 [1]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:
>    [2]https://www.reddit.com/r/dependent_types/comments/g8v59q/coq_applyin
>    g_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 [3]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.
> 

Sounds interessting, I will take a look into it.
Thank you for the hint.

>    On Wed, May 20, 2020 at 9:16 AM Fritjof Bornebusch
>    <[4]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" <[5]fritjof AT uni-bremen.de>
>      > > À: "coq-club" <[6]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 -
>      > > [7]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.
> 
> References
> 
>    1. https://github.com/uwplse/ornamental-search
>    2. 
> https://www.reddit.com/r/dependent_types/comments/g8v59q/coq_applying_a_proof_on_lists_to_a_proof_on/fov7w1t/?context=3
>    3. 
> https://github.com/uwplse/ornamental-search/blob/master/plugin/coq/examples/Example.v
>    4. mailto:fritjof AT uni-bremen.de
>    5. mailto:fritjof AT uni-bremen.de
>    6. mailto:coq-club AT inria.fr
>    7. https://coq.inria.fr/library/Coq.Vectors.Vector.html