The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

In case anyone, now or in the future, is wanting to do this, I managed to do this with some help from Andres, and the bulk of the code is https://github.com/mit-plv/fiat-crypto/blob/4d334608f7f8f5be98276c5f1904d7955e1b6f53/src/Util/ZUtil/Stabilization.v, with the actual bounds lemmas in the forms that I use them here: https://github.com/mit-plv/fiat-crypto/blob/4d334608f7f8f5be98276c5f1904d7955e1b6f53/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v#L152-L171 

On Sat, Apr 8, 2017 at 3:36 PM Jason Gross <jasongross9 AT gmail.com> wrote:

Hi,

I'm trying to establish bounds on Z.lor and Z.land, in particular for negative arguments.  The standard library seems fairly impoverished on lemmas about N.ldiff (which is used in the definition of Z.lor and Z.land).  Can anyone help me prove the following two lemmas?

Lemma land_abs_bounds a b

  : a < 0 \/ b < 0

    -> -(2^(Z.log2_up (Z.max (Z.abs a) (Z.abs b))))

       <= Z.land a b

       <= Z.max a b.

Lemma lor_abs_bounds a b

  : a < 0 \/ b < 0

    -> Z.min a b

       <= Z.lor a b

       <= 2^(Z.log2_up (Z.max (Z.abs a) (Z.abs b) + 1)) - 1.

(It doesn't matter much to me what the bounds are, as long as they don't use Z.lor/Z.land.  These bounds also hold when both inputs are non-negative; I've already proven those cases)

Thanks,

Jason