Library Stdlib.Numbers.Natural.Abstract.NBits
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'.
Global 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.
#[global]
Instance b2n_proper : Proper (Logic.eq ==> eq) b2n.
Lemma b2n_le_1 (b : bool) : b <= 1.
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.
Specification without useless condition on the bit number
Lemma testbit_odd_succ' a n : testbit (2*a+1) (S n) = testbit a n.
Lemma testbit_even_succ' a n : testbit (2*a) (S n) = testbit a n.
Lemma testbit_even_succ' a n : testbit (2*a) (S n) = testbit a n.
Alternative characterisations 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
This characterisation 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 characterisation
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
All bits of number 0 are 0
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
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 testbit_div2 : forall a n, (div2 a).[n] = a.[S n].
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.
#[global]
Instance eqf_equiv : Equivalence eqf.
Local Infix "===" := eqf (at level 70, no associativity).
#[global]
Instance testbit_eqf : Proper (eq==>eqf) testbit.
Only zero corresponds to the always-false stream.
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.
Global Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise.
Tactic Notation "bitwise" "as" simple_intropattern(m)
:= apply bits_inj; intros m; autorewrite with bitwise.
Ltac bitwise := bitwise as ?m.
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].
#[global]
Instance shiftr_wd : Proper (eq==>eq==>eq) shiftr.
#[global]
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.
Lemma div2_0 : div2 0 == 0.
Lemma div2_1 : div2 1 == 0.
Lemma div2_le_mono : forall a b, a <= b -> div2 a <= div2 b.
#[global]
Instance div2_wd : Proper (eq==>eq) div2.
Lemma div2_odd : forall a, a == 2*(div2 a) + odd a.
Lemma div2_even : forall a, div2 (2 * a) == a.
Lemma div2_odd' : forall a, div2 (2 * a + 1) == a.
Lemma le_div2_diag_l a : div2 a <= a.
Lemma div2_le_upper_bound a q : a <= 2 * q -> div2 a <= q.
Lemma div2_le_lower_bound a q : 2 * q <= a -> q <= div2 a.
Lemma lt_div2_diag_l a : a ~= 0 -> div2 a < a.
Lemma le_div2 n : div2 (S n) <= n.
Lemma lt_div2 n : 0 < n -> div2 n < n.
Lemma div2_decr a n : a <= S n -> div2 a <= n.
Properties of lxor and others, directly deduced
from properties of xorb and others.
#[global]
Instance lxor_wd : Proper (eq ==> eq ==> eq) lxor.
#[global]
Instance land_wd : Proper (eq ==> eq ==> eq) land.
#[global]
Instance lor_wd : Proper (eq ==> eq ==> eq) lor.
#[global]
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 land_even_l :
forall a b, land (2 * a) b == 2 * (land a (div2 b)).
Lemma land_even_r :
forall a b, land a (2 * b) == 2 * (land (div2 a) b).
Lemma land_odd_l :
forall a b, land (2 * a + 1) b == 2 * (land a (div2 b)) + odd b.
Lemma land_odd_r :
forall a b, land a (2 * b + 1) == 2 * (land (div2 a) b) + odd a.
Lemma land_even_even : forall a b, land (2 * a) (2 * b) == 2 * land a b.
Lemma land_odd_even : forall a b, land (2 * a + 1) (2 * b) == 2 * land a b.
Lemma land_even_odd : forall a b, land (2 * a) (2 * b + 1) == 2 * land a b.
Lemma land_odd_odd :
forall a b, land (2 * a + 1) (2 * b + 1) == 2 * (land a b) + 1.
Lemma land_le_l :
forall a b, land a b <= a.
Lemma land_le_r :
forall a b, land a b <= b.
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 ldiff_even_l : forall a b, ldiff (2 * a) b == 2 * ldiff a (div2 b).
Lemma ldiff_odd_l :
forall a b, ldiff (2 * a + 1) b == 2 * ldiff a (div2 b) + even b.
Lemma ldiff_even_r :
forall a b, ldiff a (2 * b) == 2 * ldiff (div2 a) b + odd a.
Lemma ldiff_odd_r :
forall a b, ldiff a (2 * b + 1) == 2 * ldiff (div2 a) b.
Lemma ldiff_even_even : forall a b, ldiff (2 * a) (2 * b) == 2 * ldiff a b.
Lemma ldiff_odd_even :
forall a b, ldiff (2 * a + 1) (2 * b) == 2 * (ldiff a b) + 1.
Lemma ldiff_even_odd : forall a b, ldiff (2 * a) (2 * b + 1) == 2 * ldiff a b.
Lemma ldiff_odd_odd :
forall a b, ldiff (2 * a + 1) (2 * b + 1) == 2 * ldiff a b.
Lemma ldiff_le_l :
forall a b, ldiff a b <= a.
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).
#[global]
Instance setbit_wd : Proper (eq==>eq==>eq) setbit.
#[global]
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).
Shifts and order
Lemma shiftl_lower_bound : forall a n, a <= a << n.
Lemma shiftr_upper_bound : forall a n, a >> n <= a.
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).
#[global]
Instance ones_wd : Proper (eq==>eq) ones.
#[global]
Instance lnot_wd : Proper (eq==>eq==>eq) lnot.
Lemma ones_equiv : forall n, ones n == P (2^n).
Lemma ones_0 : ones 0 == 0.
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.
Lemma ones_succ : forall n, ones (S n) == 2 * (ones n) + 1.
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
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
A null ldiff implies being smaller
Subtraction can be a ldiff when the opposite ldiff is null.
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