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 (
only parsing).
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.