Library Coq.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'.
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.
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 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 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.
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.
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].
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
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