Library Coq.NArith.Ndigits
Operation over bits of a N number.
xor
Fixpoint Pxor (
p1 p2:positive) {
struct p1} :
N :=
match p1,
p2 with
|
xH,
xH =>
N0
|
xH,
xO p2 =>
Npos (
xI p2)
|
xH,
xI p2 =>
Npos (
xO p2)
|
xO p1,
xH =>
Npos (
xI p1)
|
xO p1,
xO p2 =>
Ndouble (
Pxor p1 p2)
|
xO p1,
xI p2 =>
Ndouble_plus_one (
Pxor p1 p2)
|
xI p1,
xH =>
Npos (
xO p1)
|
xI p1,
xO p2 =>
Ndouble_plus_one (
Pxor p1 p2)
|
xI p1,
xI p2 =>
Ndouble (
Pxor p1 p2)
end.
Definition Nxor (
n n':N) :=
match n,
n' with
|
N0,
_ =>
n'
|
_,
N0 =>
n
|
Npos p,
Npos p' =>
Pxor p p'
end.
Lemma Nxor_neutral_left :
forall n:N,
Nxor N0 n =
n.
Lemma Nxor_neutral_right :
forall n:N,
Nxor n N0 =
n.
Lemma Nxor_comm :
forall n n':N,
Nxor n n' =
Nxor n' n.
Lemma Nxor_nilpotent :
forall n:N,
Nxor n n =
N0.
Checking whether a particular bit is set on not
Fixpoint Pbit (
p:positive) :
nat ->
bool :=
match p with
|
xH =>
fun n:nat =>
match n with
|
O =>
true
|
S _ =>
false
end
|
xO p =>
fun n:nat =>
match n with
|
O =>
false
|
S n' =>
Pbit p n'
end
|
xI p =>
fun n:nat =>
match n with
|
O =>
true
|
S n' =>
Pbit p n'
end
end.
Definition Nbit (
a:N) :=
match a with
|
N0 =>
fun _ =>
false
|
Npos p =>
Pbit p
end.
Auxiliary results about streams of bits
End of auxilliary results
This part is aimed at proving that if two numbers produce
the same stream of bits, then they are equal.
We now describe the semantics of Nxor in terms of bit streams.
Consequences:
- only equal numbers lead to a null xor
- xor is associative
Checking whether a number is odd, i.e.
if its lower bit is set.
Definition Nbit0 (
n:N) :=
match n with
|
N0 =>
false
|
Npos (
xO _) =>
false
|
_ =>
true
end.
Definition Nodd (
n:N) :=
Nbit0 n =
true.
Definition Neven (
n:N) :=
Nbit0 n =
false.
Lemma Nbit0_correct :
forall n:N,
Nbit n 0 =
Nbit0 n.
Lemma Ndouble_bit0 :
forall n:N,
Nbit0 (
Ndouble n) =
false.
Lemma Ndouble_plus_one_bit0 :
forall n:N,
Nbit0 (
Ndouble_plus_one n) =
true.
Lemma Ndiv2_double :
forall n:N,
Neven n ->
Ndouble (
Ndiv2 n) =
n.
Lemma Ndiv2_double_plus_one :
forall n:N,
Nodd n ->
Ndouble_plus_one (
Ndiv2 n) =
n.
Lemma Ndiv2_correct :
forall (
a:N) (
n:nat),
Nbit (
Ndiv2 a)
n =
Nbit a (
S n).
Lemma Nxor_bit0 :
forall a a':N,
Nbit0 (
Nxor a a') =
xorb (
Nbit0 a) (
Nbit0 a').
Lemma Nxor_div2 :
forall a a':N,
Ndiv2 (
Nxor a a') =
Nxor (
Ndiv2 a) (
Ndiv2 a').
Lemma Nneg_bit0 :
forall a a':N,
Nbit0 (
Nxor a a') =
true ->
Nbit0 a =
negb (
Nbit0 a').
Lemma Nneg_bit0_1 :
forall a a':N,
Nxor a a' =
Npos 1 ->
Nbit0 a =
negb (
Nbit0 a').
Lemma Nneg_bit0_2 :
forall (
a a':N) (
p:positive),
Nxor a a' =
Npos (
xI p) ->
Nbit0 a =
negb (
Nbit0 a').
Lemma Nsame_bit0 :
forall (
a a':N) (
p:positive),
Nxor a a' =
Npos (
xO p) ->
Nbit0 a =
Nbit0 a'.
a lexicographic order on bits, starting from the lowest bit
Fixpoint Nless_aux (
a a':N) (
p:positive) {
struct p} :
bool :=
match p with
|
xO p' =>
Nless_aux (
Ndiv2 a) (
Ndiv2 a')
p'
|
_ =>
andb (
negb (
Nbit0 a)) (
Nbit0 a')
end.
Definition Nless (
a a':N) :=
match Nxor a a' with
|
N0 =>
false
|
Npos p =>
Nless_aux a a' p
end.
Lemma Nbit0_less :
forall a a',
Nbit0 a =
false ->
Nbit0 a' =
true ->
Nless a a' =
true.
Lemma Nbit0_gt :
forall a a',
Nbit0 a =
true ->
Nbit0 a' =
false ->
Nless a a' =
false.
Lemma Nless_not_refl :
forall a,
Nless a a =
false.
Lemma Nless_def_1 :
forall a a',
Nless (
Ndouble a) (
Ndouble a') =
Nless a a'.
Lemma Nless_def_2 :
forall a a',
Nless (
Ndouble_plus_one a) (
Ndouble_plus_one a') =
Nless a a'.
Lemma Nless_def_3 :
forall a a',
Nless (
Ndouble a) (
Ndouble_plus_one a') =
true.
Lemma Nless_def_4 :
forall a a',
Nless (
Ndouble_plus_one a) (
Ndouble 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.
Xor is the same in the two worlds.