The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi Vincent. You can perhaps find some useful functions on vectors in http://color.inria.fr/ available on opam and github. See the section on vectors on http://color.inria.fr/doc/main.html . Best regards, Frédéric.

Le 02/03/2018 à 13:18, Vincent Siles a écrit :

Hi !

Yes, I remember that `rev (rev v) = v` is kind of a Kraken for dependent types :)

I already had a look at the CompCert library, but I won't be able to use for my current project because of the license.

Thank you for the last link, I'll have a look !

Best,

V.

2018-03-02 9:01 GMT+01:00 Pierre-Evariste Dagand <pedagand AT gmail.com>:
Hi Vincent,

> From the library [1], I see that I can use 'trunc' to implement my 'mask'
> operation, but I don't see anything I could use to implement 'right shift'.
> [...]
> [1] https://coq.inria.fr/library/Coq.Vectors.VectorDef.html#

AFAIK, Coq.Vectors is a proof-of-concept but it is not actually
"usable" in today's Coq. Emilio has this "do or dare" game where he
asks you to prove that "rev (rev v) = v", which often results in
someone badmouthing dependent types.

For a usable model of bitvectors, there is the tried-and-trusted

    https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v

and some more experimental/unfinished business:

    https://github.com/ejgallego/ssrbit/


Hope this helps,

--
Pierre