The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

Hi,

The theorem 

> append (n & MASK27) (n >> 27) == n

looks similar to one we have in our bitvector library [1]:

> Theorem combine_split : forall sz1 sz2 (w : word (sz1 + sz2)),
>   combine (split1 sz1 sz2 w) (split2 sz1 sz2 w) = w.

"combine" is "append", and "split1"/"split2" take the lower and
upper bits of a bit vector, respectively.

But before you start using it I'd like to warn you about the dependent
types, they're not easy to use and require a lot of eq_rect stuff.
Maybe you'll be better off just using Z.

Best,

Sam


[1] https://github.com/mit-plv/bbv/blob/4dcd180f06/Word.v#L587



On Fri, 2018-03-02 at 13:18 +0100, Vincent Siles wrote:
> 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
> 
>