Library Coq.NArith.Ndigits
This file is mostly obsolete, see directly
BinNat now.
Compatibility names for some bitwise operations
Equivalence of bit-testing functions,
either with index in N or in nat.
Equivalence of shifts, index in N or nat
Correctness proofs for shifts, nat version
A left shift for positive numbers (used in BigN)
Semantics of bitwise operations with respect to N.testbit_nat
Equality over functional streams of bits
If two numbers produce the same stream of bits, they are equal.
Checking whether a number is odd, i.e.
if its lower bit is set.
Notation Nbit0 :=
N.odd (
compat "8.3").
Definition Nodd (
n:
N) :=
N.odd n = true.
Definition Neven (
n:
N) :=
N.odd n = false.
Lemma Nbit0_correct :
forall n:
N,
N.testbit_nat n 0
= N.odd n.
Lemma Ndouble_bit0 :
forall n:
N,
N.odd (
N.double n)
= false.
Lemma Ndouble_plus_one_bit0 :
forall n:
N,
N.odd (
N.succ_double n)
= true.
Lemma Ndiv2_double :
forall n:
N,
Neven n ->
N.double (
N.div2 n)
= n.
Lemma Ndiv2_double_plus_one :
forall n:
N,
Nodd n ->
N.succ_double (
N.div2 n)
= n.
Lemma Ndiv2_correct :
forall (
a:
N) (
n:
nat),
N.testbit_nat (
N.div2 a)
n = N.testbit_nat a (
S n).
Lemma Nxor_bit0 :
forall a a´:
N,
N.odd (
N.lxor a a´)
= xorb (
N.odd a) (
N.odd a´).
Lemma Nxor_div2 :
forall a a´:
N,
N.div2 (
N.lxor a a´)
= N.lxor (
N.div2 a) (
N.div2 a´).
Lemma Nneg_bit0 :
forall a a´:
N,
N.odd (
N.lxor a a´)
= true ->
N.odd a = negb (
N.odd a´).
Lemma Nneg_bit0_1 :
forall a a´:
N,
N.lxor a a´ = Npos 1 ->
N.odd a = negb (
N.odd a´).
Lemma Nneg_bit0_2 :
forall (
a a´:
N) (
p:
positive),
N.lxor a a´ = Npos (
xI p) ->
N.odd a = negb (
N.odd a´).
Lemma Nsame_bit0 :
forall (
a a´:
N) (
p:
positive),
N.lxor a a´ = Npos (
xO p) ->
N.odd a = N.odd a´.
a lexicographic order on bits, starting from the lowest bit
Fixpoint Nless_aux (
a a´:
N) (
p:
positive) :
bool :=
match p with
|
xO p´ =>
Nless_aux (
N.div2 a) (
N.div2 a´)
p´
|
_ =>
andb (
negb (
N.odd a)) (
N.odd a´)
end.
Definition Nless (
a a´:
N) :=
match N.lxor a a´ with
|
N0 =>
false
|
Npos p =>
Nless_aux a a´ p
end.
Lemma Nbit0_less :
forall a a´,
N.odd a = false ->
N.odd a´ = true ->
Nless a a´ = true.
Lemma Nbit0_gt :
forall a a´,
N.odd a = true ->
N.odd a´ = false ->
Nless a a´ = false.
Lemma Nless_not_refl :
forall a,
Nless a a = false.
Lemma Nless_def_1 :
forall a a´,
Nless (
N.double a) (
N.double a´)
= Nless a a´.
Lemma Nless_def_2 :
forall a a´,
Nless (
N.succ_double a) (
N.succ_double a´)
= Nless a a´.
Lemma Nless_def_3 :
forall a a´,
Nless (
N.double a) (
N.succ_double a´)
= true.
Lemma Nless_def_4 :
forall a a´,
Nless (
N.succ_double a) (
N.double a´)
= false.
Lemma Nless_z :
forall a,
Nless a N0 = false.
Lemma N0_less_1 :
forall a,
Nless N0 a = true ->
{p : positive | a = Npos p}.
Lemma N0_less_2 :
forall a,
Nless N0 a = false ->
a = N0.
Lemma Nless_trans :
forall a a´ a´´,
Nless a a´ = true ->
Nless a´ a´´ = true ->
Nless a a´´ = true.
Lemma Nless_total :
forall a a´,
{Nless a a´ = true} + {Nless a´ a = true} + {a = a´}.
Number of digits in a number
conversions between N and bit vectors.
The opposite composition is not so simple: if the considered
bit vector has some zeros on its right, they will disappear during
the return Bv2N translation:
In the previous lemma, we can only replace the inequality by
an equality whenever the highest bit is non-null.
To state nonetheless a second result about composition of
conversions, we define a conversion on a given number of bits :
The first N2Bv is then a special case of N2Bv_gen
In fact, if k is large enough, N2Bv_gen k a contains all digits of
a plus some zeros.
Here comes now the second composition result.
accessing some precise bits.
Binary bitwise operations are the same in the two worlds.