Library Coq.Numbers.Natural.Abstract.NBits

Require Import Bool NAxioms NSub NPow NDiv NParity NLog.

Derived properties of bitwise operations

Module Type NBitsProp
(Import A : NAxiomsSig´)
(Import B : NSubProp A)
(Import C : NParityProp A B)
(Import D : NPowProp A B C)
(Import E : NDivProp A B)
(Import F : NLog2Prop A B C D).

Include BoolEqualityFacts A.

Ltac order_nz := try apply pow_nonzero; order´.
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 -> c <=b -> a ^(b -c ) == a ^b / a ^c.

Lemma pow_div_l : forall a b c, b ~=0 -> 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 b2n (b:bool) := if b then 1 else 0.
Local Coercion b2n : bool >-> t.

Instance b2n_proper : Proper (Logic.eq ==> eq) b2n.

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 :
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 : 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 :
exists l h, 0<=l <2^n /\ a == l + (a .[n ] + 2*h )*2^n.

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

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

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

Results about the injection b2n

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

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

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

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

Lemma b2n_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,
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.

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

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

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

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

Testing bits after division or multiplication by a power of two

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

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

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

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

Lemma mul_pow2_bits_high : forall a n m, n <=m -> (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, 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.

Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise.

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

The streams of bits that correspond to a natural numbers are exactly the ones that are always 0 after some point

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

Properties of shifts

Lemma shiftr_spec´ : forall a n m, (a >> n ).[m ] = a .[m +n ].

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

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

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

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

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

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

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

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

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

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

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, 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, 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, (2^n ).[n ] = true.

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

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

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

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

Lemma setbit_eq : forall a n, (setbit a n ).[n ] = true.

Lemma setbit_neq : forall a n m, 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).

We cannot have a function complementing all bits of a number, otherwise it would have an infinity of bit 1. Nonetheless, we can design a bounded complement

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

Definition lnot a n := lxor a (ones n).

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

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

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

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

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

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

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

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

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

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

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

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

Lemma lnot_0_l : forall n, lnot 0 n == ones n.

Lemma lnot_ones : forall n, lnot (ones n) n == 0.

Bounded complement and other operations

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

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

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

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

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

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

Lemma lor_lnot_diag : forall a n,
lor a (lnot a n) == lor a (ones n).

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

Lemma land_lnot_diag : forall a n,
land a (lnot a n) == ldiff a (ones n).

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

Lemma lnot_lor_low : forall a b n, log2 a < n -> log2 b < n ->
lnot (lor a b) n == land (lnot a n) (lnot b n).

Lemma lnot_land_low : forall a b n, log2 a < n -> log2 b < n ->
lnot (land a b) n == lor (lnot a n) (lnot b n).

Lemma ldiff_land_low : forall a b n, log2 a < n ->
ldiff a b == land a (lnot b n).

Lemma lnot_ldiff_low : forall a b n, log2 a < n -> log2 b < n ->
lnot (ldiff a b) n == lor (lnot a n) b.

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

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

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

Lemma lxor_lor : forall a b, land a b == 0 ->
lxor a b == lor a 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, log2 (a >> n) == log2 a - n.

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

Lemma log2_lor : forall a b,
log2 (lor a b) == max (log2 a) (log2 b).

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

Lemma log2_lxor : forall a 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 : 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, ldiff a b == 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.

We can express lnot in term of subtraction

Lemma add_lnot_diag_low : forall a n, log2 a < n ->
a + lnot a n == ones n.

Lemma lnot_sub_low : forall a n, log2 a < n ->
lnot a n == ones n - a.

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, land a b == 0 ->
a mod 2^n + b mod 2^n < 2^n.

End NBitsProp.