Library Coq.Numbers.Integer.Abstract.ZBits

Require Import
Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog.

Derived properties of bitwise operations

Module Type ZBitsProp
(Import A : ZAxiomsSig´)
(Import B : ZMulOrderProp A)
(Import C : ZParityProp A B)
(Import D : ZSgnAbsProp A B)
(Import E : ZPowProp A B C D)
(Import F : ZDivProp A B D)
(Import G : NZLog2Prop A A A B E).

Include BoolEqualityFacts A.

Ltac order_nz := try apply pow_nonzero; order´.
Ltac order_pos´ := try apply abs_nonneg; order_pos.
Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz.

Some properties of power and division

Lemma pow_sub_r : forall a b c, a ~=0 -> 0<=c <=b -> a ^(b -c ) == a ^b / a ^c.

Lemma pow_div_l : forall a b c, b ~=0 -> 0<=c -> a mod b == 0 ->
(a /b )^c == a ^c / b ^c.

An injection from bits true and false to numbers 1 and 0. We declare it as a (local) coercion for shorter statements.

Definition b2z (b:bool) := if b then 1 else 0.
Local Coercion b2z : bool >-> t.

Instance b2z_wd : Proper (Logic.eq ==> eq) b2z := _.

Lemma exists_div2 a : exists a´ (b:bool ), a == 2*a´ + b.

We can compact testbit_odd_0 testbit_even_0 testbit_even_succ testbit_odd_succ in only two lemmas.

Lemma testbit_0_r a (b:bool) : testbit (2*a +b) 0 = b.

Lemma testbit_succ_r a (b:bool) n : 0<=n ->
testbit (2*a +b) (succ n) = testbit a n.

Alternative caracterisations of testbit

This concise equation could have been taken as specification for testbit in the interface, but it would have been hard to implement with little initial knowledge about div and mod

Lemma testbit_spec´ a n : 0<=n -> a .[n ] == (a / 2^n ) mod 2.

This caracterisation that uses only basic operations and power was initially taken as specification for testbit. We describe a as having a low part and a high part, with the corresponding bit in the middle. This caracterisation is moderatly complex to implement, but also moderately usable...

Lemma testbit_spec a n : 0<=n ->
exists l h, 0<=l <2^n /\ a == l + (a .[n ] + 2*h )*2^n.

Lemma testbit_true : forall a n, 0<=n ->
(a .[n ] = true <-> (a / 2^n ) mod 2 == 1).

Lemma testbit_false : forall a n, 0<=n ->
(a .[n ] = false <-> (a / 2^n ) mod 2 == 0).

Lemma testbit_eqb : forall a n, 0<=n ->
a .[n ] = eqb ((a / 2^n ) mod 2) 1.

Results about the injection b2z

Lemma b2z_inj : forall (a0 b0:bool), a0 == b0 -> a0 = b0.

Lemma add_b2z_double_div2 : forall (a0:bool) a, (a0 +2*a )/2 == a.

Lemma add_b2z_double_bit0 : forall (a0:bool) a, (a0 +2*a ).[0] = a0.

Lemma b2z_div2 : forall (a0:bool), a0 /2 == 0.

Lemma b2z_bit0 : forall (a0:bool), a0 .[0] = a0.

The specification of testbit by low and high parts is complete

Lemma testbit_unique : forall a n (a0:bool) l h,
0<=l <2^n -> a == l + (a0 + 2*h )*2^n -> a .[n ] = a0.

All bits of number 0 are 0

Lemma bits_0 : forall n, 0.[n ] = false.

For negative numbers, we are actually doing two's complement

Lemma bits_opp : forall a n, 0<=n -> (-a ).[n ] = negb (P a ).[n ].

All bits of number (-1) are 1

Lemma bits_m1 : forall n, 0<=n -> (-1).[n ] = true.

Various ways to refer to the lowest bit of a number

Lemma bit0_odd : forall a, a .[0] = odd a.

Lemma bit0_eqb : forall a, a .[0] = eqb (a mod 2) 1.

Lemma bit0_mod : forall a, a .[0] == a mod 2.

Hence testing a bit is equivalent to shifting and testing parity

Lemma testbit_odd : forall a n, a .[n ] = odd (a >>n).

log2 gives the highest nonzero bit of positive numbers

Lemma bit_log2 : forall a, 0<a -> a .[log2 a ] = true.

Lemma bits_above_log2 : forall a n, 0<=a -> log2 a < n ->
a .[n ] = false.

Hence the number of bits of a is 1+log2 a (see Pos.size_nat and Pos.size).

For negative numbers, things are the other ways around: log2 gives the highest zero bit (for numbers below -1).

Lemma bit_log2_neg : forall a, a < -1 -> a .[log2 (P (-a))] = false.

Lemma bits_above_log2_neg : forall a n, a < 0 -> log2 (P (-a)) < n ->
a .[n ] = true.

Accesing a high enough bit of a number gives its sign

Lemma bits_iff_nonneg : forall a n, log2 (abs a) < n ->
(0<=a <-> a .[n ] = false).

Lemma bits_iff_nonneg´ : forall a,
0<=a <-> a .[S (log2 (abs a))] = false.

Lemma bits_iff_nonneg_ex : forall a,
0<=a <-> (exists k, forall m, k <m -> a .[m ] = false ).

Lemma bits_iff_neg : forall a n, log2 (abs a) < n ->
(a <0 <-> a .[n ] = true).

Lemma bits_iff_neg´ : forall a, a <0 <-> a .[S (log2 (abs a))] = true.

Lemma bits_iff_neg_ex : forall a,
a <0 <-> (exists k, forall m, k <m -> a .[m ] = true ).

Testing bits after division or multiplication by a power of two

Lemma div2_bits : forall a n, 0<=n -> (a /2).[n ] = a .[S n ].

Lemma div_pow2_bits : forall a n m, 0<=n -> 0<=m -> (a /2^n ).[m ] = a .[m +n ].

Lemma double_bits_succ : forall a n, (2*a ).[S n ] = a .[n ].

Lemma double_bits : forall a n, (2*a ).[n ] = a .[P n ].

Lemma mul_pow2_bits_add : forall a n m, 0<=n -> (a *2^n ).[n +m ] = a .[m ].

Lemma mul_pow2_bits : forall a n m, 0<=n -> (a *2^n ).[m ] = a .[m -n ].

Lemma mul_pow2_bits_low : forall a n m, m <n -> (a *2^n ).[m ] = false.

Selecting the low part of a number can be done by a modulo

Lemma mod_pow2_bits_high : forall a n m, 0<=n <=m ->
(a mod 2^n ).[m ] = false.

Lemma mod_pow2_bits_low : forall a n m, m <n ->
(a mod 2^n ).[m ] = a .[m ].

We now prove that having the same bits implies equality. For that we use a notion of equality over functional streams of bits.

Definition eqf (f g:t -> bool) := forall n:t, f n = g n.

Instance eqf_equiv : Equivalence eqf.

Local Infix "===" := eqf (at level 70, no associativity).

Instance testbit_eqf : Proper (eq ==>eqf) testbit.

Only zero corresponds to the always-false stream.

Lemma bits_inj_0 :
forall a, (forall n, a .[n ] = false) -> a == 0.

If two numbers produce the same stream of bits, they are equal.

Lemma bits_inj : forall a b, testbit a === testbit b -> a == b.

Lemma bits_inj_iff : forall a b, testbit a === testbit b <-> a == b.

In fact, checking the bits at positive indexes is enough.

Lemma bits_inj´ : forall a b,
(forall n, 0<=n -> a .[n ] = b .[n ]) -> a == b.

Lemma bits_inj_iff´ : forall a b, (forall n, 0<=n -> a .[n ] = b .[n ]) <-> a == b.

Ltac bitwise := apply bits_inj´; intros ?m ?Hm; autorewrite with bitwise.

Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise.

The streams of bits that correspond to a numbers are exactly the ones which are stationary after some point.

Lemma are_bits : forall (f:t->bool), Proper (eq ==>Logic.eq) f ->
((exists n, forall m, 0<=m -> f m = n .[m ]) <->
(exists k, forall m, k <=m -> f m = f k )).

Properties of shifts

First, a unified specification for shiftl : the shiftl_spec below (combined with testbit_neg_r) is equivalent to shiftl_spec_low and shiftl_spec_high.

Lemma shiftl_spec : forall a n m, 0<=m -> (a << n ).[m ] = a .[m -n ].

A shiftl by a negative number is a shiftr, and vice-versa

Lemma shiftr_opp_r : forall a n, a >> (-n ) == a << n.

Lemma shiftl_opp_r : forall a n, a << (-n ) == a >> n.

Shifts correspond to multiplication or division by a power of two

Lemma shiftr_div_pow2 : forall a n, 0<=n -> a >> n == a / 2^n.

Lemma shiftr_mul_pow2 : forall a n, n <=0 -> a >> n == a * 2^(-n ).

Lemma shiftl_mul_pow2 : forall a n, 0<=n -> a << n == a * 2^n.

Lemma shiftl_div_pow2 : forall a n, n <=0 -> a << n == a / 2^(-n ).

Shifts are morphisms

Instance shiftr_wd : Proper (eq ==>eq ==>eq) shiftr.

Instance shiftl_wd : Proper (eq ==>eq ==>eq) shiftl.

We could also have specified shiftl with an addition on the left.

Lemma shiftl_spec_alt : forall a n m, 0<=n -> (a << n ).[m +n ] = a .[m ].

Chaining several shifts. The only case for which there isn't any simple expression is a true shiftr followed by a true shiftl.

Lemma shiftl_shiftl : forall a n m, 0<=n ->
(a << n ) << m == a << (n +m ).

Lemma shiftr_shiftl_l : forall a n m, 0<=n ->
(a << n ) >> m == a << (n -m ).

Lemma shiftr_shiftl_r : forall a n m, 0<=n ->
(a << n ) >> m == a >> (m -n ).

Lemma shiftr_shiftr : forall a n m, 0<=m ->
(a >> n ) >> m == a >> (n +m ).

shifts and constants

Lemma shiftl_1_l : forall n, 1 << n == 2^n.

Lemma shiftl_0_r : forall a, a << 0 == a.

Lemma shiftr_0_r : forall a, a >> 0 == a.

Lemma shiftl_0_l : forall n, 0 << n == 0.

Lemma shiftr_0_l : forall n, 0 >> n == 0.

Lemma shiftl_eq_0_iff : forall a n, 0<=n -> (a << n == 0 <-> a == 0).

Lemma shiftr_eq_0_iff : forall a n,
a >> n == 0 <-> a ==0 \/ (0<a /\ log2 a < n ).

Lemma shiftr_eq_0 : forall a n, 0<=a -> log2 a < n -> a >> n == 0.

Properties of div2.

Lemma div2_div : forall a, div2 a == a /2.

Instance div2_wd : Proper (eq ==>eq) div2.

Lemma div2_odd : forall a, a == 2*(div2 a ) + odd a.

Properties of lxor and others, directly deduced from properties of xorb and others.

Instance lxor_wd : Proper (eq ==> eq ==> eq) lxor.

Instance land_wd : Proper (eq ==> eq ==> eq) land.

Instance lor_wd : Proper (eq ==> eq ==> eq) lor.

Instance ldiff_wd : Proper (eq ==> eq ==> eq) ldiff.

Lemma lxor_eq : forall a a´, lxor a a´ == 0 -> a == a´.

Lemma lxor_nilpotent : forall a, lxor a a == 0.

Lemma lxor_eq_0_iff : forall a a´, lxor a a´ == 0 <-> a == a´.

Lemma lxor_0_l : forall a, lxor 0 a == a.

Lemma lxor_0_r : forall a, lxor a 0 == a.

Lemma lxor_comm : forall a b, lxor a b == lxor b a.

Lemma lxor_assoc :
forall a b c, lxor (lxor a b) c == lxor a (lxor b c).

Lemma lor_0_l : forall a, lor 0 a == a.

Lemma lor_0_r : forall a, lor a 0 == a.

Lemma lor_comm : forall a b, lor a b == lor b a.

Lemma lor_assoc :
forall a b c, lor a (lor b c) == lor (lor a b) c.

Lemma lor_diag : forall a, lor a a == a.

Lemma lor_eq_0_l : forall a b, lor a b == 0 -> a == 0.

Lemma lor_eq_0_iff : forall a b, lor a b == 0 <-> a == 0 /\ b == 0.

Lemma land_0_l : forall a, land 0 a == 0.

Lemma land_0_r : forall a, land a 0 == 0.

Lemma land_comm : forall a b, land a b == land b a.

Lemma land_assoc :
forall a b c, land a (land b c) == land (land a b) c.

Lemma land_diag : forall a, land a a == a.

Lemma ldiff_0_l : forall a, ldiff 0 a == 0.

Lemma ldiff_0_r : forall a, ldiff a 0 == a.

Lemma ldiff_diag : forall a, ldiff a a == 0.

Lemma lor_land_distr_l : forall a b c,
lor (land a b) c == land (lor a c) (lor b c).

Lemma lor_land_distr_r : forall a b c,
lor a (land b c) == land (lor a b) (lor a c).

Lemma land_lor_distr_l : forall a b c,
land (lor a b) c == lor (land a c) (land b c).

Lemma land_lor_distr_r : forall a b c,
land a (lor b c) == lor (land a b) (land a c).

Lemma ldiff_ldiff_l : forall a b c,
ldiff (ldiff a b) c == ldiff a (lor b c).

Lemma lor_ldiff_and : forall a b,
lor (ldiff a b) (land a b) == a.

Lemma land_ldiff : forall a b,
land (ldiff a b) b == 0.

Properties of setbit and clearbit

Definition setbit a n := lor a (1 << n).
Definition clearbit a n := ldiff a (1 << n).

Lemma setbit_spec´ : forall a n, setbit a n == lor a (2^n).

Lemma clearbit_spec´ : forall a n, clearbit a n == ldiff a (2^n).

Instance setbit_wd : Proper (eq ==>eq ==>eq) setbit.

Instance clearbit_wd : Proper (eq ==>eq ==>eq) clearbit.

Lemma pow2_bits_true : forall n, 0<=n -> (2^n ).[n ] = true.

Lemma pow2_bits_false : forall n m, n ~=m -> (2^n ).[m ] = false.

Lemma pow2_bits_eqb : forall n m, 0<=n -> (2^n ).[m ] = eqb n m.

Lemma setbit_eqb : forall a n m, 0<=n ->
(setbit a n ).[m ] = eqb n m || a .[m ].

Lemma setbit_iff : forall a n m, 0<=n ->
((setbit a n ).[m ] = true <-> n ==m \/ a .[m ] = true).

Lemma setbit_eq : forall a n, 0<=n -> (setbit a n ).[n ] = true.

Lemma setbit_neq : forall a n m, 0<=n -> n ~=m ->
(setbit a n ).[m ] = a .[m ].

Lemma clearbit_eqb : forall a n m,
(clearbit a n ).[m ] = a .[m ] && negb (eqb n m).

Lemma clearbit_iff : forall a n m,
(clearbit a n ).[m ] = true <-> a .[m ] = true /\ n ~=m.

Lemma clearbit_eq : forall a n, (clearbit a n ).[n ] = false.

Lemma clearbit_neq : forall a n m, n ~=m ->
(clearbit a n ).[m ] = a .[m ].

Shifts of bitwise operations

Lemma shiftl_lxor : forall a b n,
(lxor a b ) << n == lxor (a << n) (b << n).

Lemma shiftr_lxor : forall a b n,
(lxor a b ) >> n == lxor (a >> n) (b >> n).

Lemma shiftl_land : forall a b n,
(land a b ) << n == land (a << n) (b << n).

Lemma shiftr_land : forall a b n,
(land a b ) >> n == land (a >> n) (b >> n).

Lemma shiftl_lor : forall a b n,
(lor a b ) << n == lor (a << n) (b << n).

Lemma shiftr_lor : forall a b n,
(lor a b ) >> n == lor (a >> n) (b >> n).

Lemma shiftl_ldiff : forall a b n,
(ldiff a b ) << n == ldiff (a << n) (b << n).

Lemma shiftr_ldiff : forall a b n,
(ldiff a b ) >> n == ldiff (a >> n) (b >> n).

For integers, we do have a binary complement function

Definition lnot a := P (-a).

Instance lnot_wd : Proper (eq ==>eq) lnot.

Lemma lnot_spec : forall a n, 0<=n -> (lnot a ).[n ] = negb a .[n ].

Lemma lnot_involutive : forall a, lnot (lnot a) == a.

Lemma lnot_0 : lnot 0 == -1.

Lemma lnot_m1 : lnot (-1) == 0.

Complement and other operations

Lemma lor_m1_r : forall a, lor a (-1) == -1.

Lemma lor_m1_l : forall a, lor (-1) a == -1.

Lemma land_m1_r : forall a, land a (-1) == a.

Lemma land_m1_l : forall a, land (-1) a == a.

Lemma ldiff_m1_r : forall a, ldiff a (-1) == 0.

Lemma ldiff_m1_l : forall a, ldiff (-1) a == lnot a.

Lemma lor_lnot_diag : forall a, lor a (lnot a) == -1.

Lemma add_lnot_diag : forall a, a + lnot a == -1.

Lemma ldiff_land : forall a b, ldiff a b == land a (lnot b).

Lemma land_lnot_diag : forall a, land a (lnot a) == 0.

Lemma lnot_lor : forall a b, lnot (lor a b) == land (lnot a) (lnot b).

Lemma lnot_land : forall a b, lnot (land a b) == lor (lnot a) (lnot b).

Lemma lnot_ldiff : forall a b, lnot (ldiff a b) == lor (lnot a) b.

Lemma lxor_lnot_lnot : forall a b, lxor (lnot a) (lnot b) == lxor a b.

Lemma lnot_lxor_l : forall a b, lnot (lxor a b) == lxor (lnot a) b.

Lemma lnot_lxor_r : forall a b, lnot (lxor a b) == lxor a (lnot b).

Lemma lxor_m1_r : forall a, lxor a (-1) == lnot a.

Lemma lxor_m1_l : forall a, lxor (-1) a == lnot a.

Lemma lxor_lor : forall a b, land a b == 0 ->
lxor a b == lor a b.

Lemma lnot_shiftr : forall a n, 0<=n -> lnot (a >> n) == (lnot a ) >> n.

(ones n) is 2^n-1, the number with n digits 1

Definition ones n := P (1<<n).

Instance ones_wd : Proper (eq ==>eq) ones.

Lemma ones_equiv : forall n, ones n == P (2^n).

Lemma ones_add : forall n m, 0<=n -> 0<=m ->
ones (m +n) == 2^m * ones n + ones m.

Lemma ones_div_pow2 : forall n m, 0<=m <=n -> ones n / 2^m == ones (n -m).

Lemma ones_mod_pow2 : forall n m, 0<=m <=n -> (ones n ) mod (2^m ) == ones m.

Lemma ones_spec_low : forall n m, 0<=m <n -> (ones n ).[m ] = true.

Lemma ones_spec_high : forall n m, 0<=n <=m -> (ones n ).[m ] = false.

Lemma ones_spec_iff : forall n m, 0<=n ->
((ones n ).[m ] = true <-> 0<=m <n).

Lemma lor_ones_low : forall a n, 0<=a -> log2 a < n ->
lor a (ones n) == ones n.

Lemma land_ones : forall a n, 0<=n -> land a (ones n) == a mod 2^n.

Lemma land_ones_low : forall a n, 0<=a -> log2 a < n ->
land a (ones n) == a.

Lemma ldiff_ones_r : forall a n, 0<=n ->
ldiff a (ones n) == (a >> n ) << n.

Lemma ldiff_ones_r_low : forall a n, 0<=a -> log2 a < n ->
ldiff a (ones n) == 0.

Lemma ldiff_ones_l_low : forall a n, 0<=a -> log2 a < n ->
ldiff (ones n) a == lxor a (ones n).

Bitwise operations and sign

Lemma shiftl_nonneg : forall a n, 0 <= (a << n ) <-> 0 <= a.

Lemma shiftl_neg : forall a n, (a << n ) < 0 <-> a < 0.

Lemma shiftr_nonneg : forall a n, 0 <= (a >> n ) <-> 0 <= a.

Lemma shiftr_neg : forall a n, (a >> n ) < 0 <-> a < 0.

Lemma div2_nonneg : forall a, 0 <= div2 a <-> 0 <= a.

Lemma div2_neg : forall a, div2 a < 0 <-> a < 0.

Lemma lor_nonneg : forall a b, 0 <= lor a b <-> 0<=a /\ 0<=b.

Lemma lor_neg : forall a b, lor a b < 0 <-> a < 0 \/ b < 0.

Lemma lnot_nonneg : forall a, 0 <= lnot a <-> a < 0.

Lemma lnot_neg : forall a, lnot a < 0 <-> 0 <= a.

Lemma land_nonneg : forall a b, 0 <= land a b <-> 0<=a \/ 0<=b.

Lemma land_neg : forall a b, land a b < 0 <-> a < 0 /\ b < 0.

Lemma ldiff_nonneg : forall a b, 0 <= ldiff a b <-> 0<=a \/ b <0.

Lemma ldiff_neg : forall a b, ldiff a b < 0 <-> a <0 /\ 0<=b.

Lemma lxor_nonneg : forall a b, 0 <= lxor a b <-> (0<=a <-> 0<=b ).

Bitwise operations and log2

Lemma log2_bits_unique : forall a n,
a .[n ] = true ->
(forall m, n <m -> a .[m ] = false) ->
log2 a == n.

Lemma log2_shiftr : forall a n, 0<a -> log2 (a >> n) == max 0 (log2 a - n).

Lemma log2_shiftl : forall a n, 0<a -> 0<=n -> log2 (a << n) == log2 a + n.

Lemma log2_shiftl´ : forall a n, 0<a -> log2 (a << n) == max 0 (log2 a + n).

Lemma log2_lor : forall a b, 0<=a -> 0<=b ->
log2 (lor a b) == max (log2 a) (log2 b).

Lemma log2_land : forall a b, 0<=a -> 0<=b ->
log2 (land a b) <= min (log2 a) (log2 b).

Lemma log2_lxor : forall a b, 0<=a -> 0<=b ->
log2 (lxor a b) <= max (log2 a) (log2 b).

Bitwise operations and arithmetical operations

Local Notation xor3 a b c := (xorb (xorb a b) c).
Local Notation lxor3 a b c := (lxor (lxor a b) c).
Local Notation nextcarry a b c := ((a&&b) || (c && (a||b))).
Local Notation lnextcarry a b c := (lor (land a b) (land c (lor a b))).

Lemma add_bit0 : forall a b, (a +b ).[0] = xorb a .[0] b .[0].

Lemma add3_bit0 : forall a b c,
(a +b +c ).[0] = xor3 a .[0] b .[0] c .[0].

Lemma add3_bits_div2 : forall (a0 b0 c0 : bool),
(a0 + b0 + c0 )/2 == nextcarry a0 b0 c0.

Lemma add_carry_div2 : forall a b (c0:bool),
(a + b + c0 )/2 == a /2 + b /2 + nextcarry a .[0] b .[0] c0.

The main result concerning addition: we express the bits of the sum in term of bits of a and b and of some carry stream which is also recursively determined by another equation.

Lemma add_carry_bits_aux : forall n, 0<=n ->
forall a b (c0:bool), -(2^n ) <= a < 2^n -> -(2^n ) <= b < 2^n ->
exists c,
a +b +c0 == lxor3 a b c /\ c /2 == lnextcarry a b c /\ c .[0] = c0.

Lemma add_carry_bits : forall a b (c0:bool), exists c,
a +b +c0 == lxor3 a b c /\ c /2 == lnextcarry a b c /\ c .[0] = c0.

Particular case : the second bit of an addition

Lemma add_bit1 : forall a b,
(a +b ).[1] = xor3 a .[1] b .[1] (a .[0] && b .[0]).

In an addition, there will be no carries iff there is no common bits in the numbers to add

Lemma nocarry_equiv : forall a b c,
c /2 == lnextcarry a b c -> c .[0] = false ->
(c == 0 <-> land a b == 0).

When there is no common bits, the addition is just a xor

Lemma add_nocarry_lxor : forall a b, land a b == 0 ->
a +b == lxor a b.

A null ldiff implies being smaller

Lemma ldiff_le : forall a b, 0<=b -> ldiff a b == 0 -> 0 <= a <= b.

Subtraction can be a ldiff when the opposite ldiff is null.

Lemma sub_nocarry_ldiff : forall a b, ldiff b a == 0 ->
a -b == ldiff a b.

Adding numbers with no common bits cannot lead to a much bigger number

Lemma add_nocarry_lt_pow2 : forall a b n, land a b == 0 ->
a < 2^n -> b < 2^n -> a +b < 2^n.

Lemma add_nocarry_mod_lt_pow2 : forall a b n, 0<=n -> land a b == 0 ->
a mod 2^n + b mod 2^n < 2^n.

End ZBitsProp.