The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

I see. Clever use of rev, I'll try to make it work for my case !

2018-02-21 14:59 GMT+01:00 Lars Rasmusson <lars.rasmusson AT ri.se>:

If by "shift" you mean "rotate", perhaps you can build on 'rot1', which puts the last element first...

Require Import Vector.

Definition last_n {T m} (v:Vector.t T m) n (H:n<=m) := rev ((take n H (rev v))).

Definition rot1 {T n} (v:Vector.t T (S n)) := append (last_n v 1 (le_n_S _ _ (le_0_n _))) (take n (le_S _ _ (le_n _)) v).

On 20 Feb 2018, at 10:25 , Vincent <vincent.siles AT gmail.com> wrote:

Hi !

I'm trying to write some properties about N bit integers in Coq (N = 54 and 27), and I am considering the 'mask' and 'left/right shifts'.

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'. My first goal is to prove something like:

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

Did I miss something in the lib or am I looking at the from library ?

Best,
V.

[1] https://coq.inria.fr/library/Coq.Vectors.VectorDef.html#