# Library Coq.NArith.Ndigits

Require Import Bool.
Require Import Bvector.
Require Import BinPos.
Require Import BinNat.

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

Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n.

Lemma eqf_sym : forall f f':nat -> bool, eqf f f' -> eqf f' f.

Lemma eqf_refl : forall f:nat -> bool, eqf f f.

Lemma eqf_trans :
forall f f' f'':nat -> bool, eqf f f' -> eqf f' f'' -> eqf f f''.

Definition xorf (f g:nat -> bool) (n:nat) := xorb (f n) (g n).

Lemma xorf_eq :
forall f f', eqf (xorf f f') (fun n => false) -> eqf f f'.

Lemma xorf_assoc :
forall f f' f'',
eqf (xorf (xorf f f') f'') (xorf f (xorf f' f'')).

Lemma eqf_xorf :
forall f f' f'' f''',
eqf f f' -> eqf f'' f''' -> eqf (xorf f f'') (xorf f' f''').

End of auxilliary results

This part is aimed at proving that if two numbers produce the same stream of bits, then they are equal.

Lemma Nbit_faithful_1 : forall a:N, eqf (Nbit N0) (Nbit a) -> N0 = a.

Lemma Nbit_faithful_2 :
forall a:N, eqf (Nbit (Npos 1)) (Nbit a) -> Npos 1 = a.

Lemma Nbit_faithful_3 :
forall (a:N) (p:positive),
(forall p':positive, eqf (Nbit (Npos p)) (Nbit (Npos p')) -> p = p') ->
eqf (Nbit (Npos (xO p))) (Nbit a) -> Npos (xO p) = a.

Lemma Nbit_faithful_4 :
forall (a:N) (p:positive),
(forall p':positive, eqf (Nbit (Npos p)) (Nbit (Npos p')) -> p = p') ->
eqf (Nbit (Npos (xI p))) (Nbit a) -> Npos (xI p) = a.

Lemma Nbit_faithful : forall a a':N, eqf (Nbit a) (Nbit a') -> a = a'.

We now describe the semantics of Nxor in terms of bit streams.

Lemma Nxor_sem_1 : forall a':N, Nbit (Nxor N0 a') 0 = Nbit a' 0.

Lemma Nxor_sem_2 :
forall a':N, Nbit (Nxor (Npos 1) a') 0 = negb (Nbit a' 0).

Lemma Nxor_sem_3 :
forall (p:positive) (a':N),
Nbit (Nxor (Npos (xO p)) a') 0 = Nbit a' 0.

Lemma Nxor_sem_4 :
forall (p:positive) (a':N),
Nbit (Nxor (Npos (xI p)) a') 0 = negb (Nbit a' 0).

Lemma Nxor_sem_5 :
forall a a':N, Nbit (Nxor a a') 0 = xorf (Nbit a) (Nbit a') 0.

Lemma Nxor_sem_6 :
forall n:nat,
(forall a a':N, Nbit (Nxor a a') n = xorf (Nbit a) (Nbit a') n) ->
forall a a':N,
Nbit (Nxor a a') (S n) = xorf (Nbit a) (Nbit a') (S n).

Lemma Nxor_semantics :
forall a a':N, eqf (Nbit (Nxor a a')) (xorf (Nbit a) (Nbit a')).

Consequences:
• only equal numbers lead to a null xor
• xor is associative

Lemma Nxor_eq : forall a a':N, Nxor a a' = N0 -> a = a'.

Lemma Nxor_assoc :
forall a a' a'':N, Nxor (Nxor a a') a'' = Nxor a (Nxor a' a'').

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

Definition Nsize (n:N) : nat := match n with
| N0 => 0%nat
| Npos p => Psize p
end.

conversions between N and bit vectors.

Fixpoint P2Bv (p:positive) : Bvector (Psize p) :=
match p return Bvector (Psize p) with
| xH => Bvect_true 1%nat
| xO p => Bcons false (Psize p) (P2Bv p)
| xI p => Bcons true (Psize p) (P2Bv p)
end.

Definition N2Bv (n:N) : Bvector (Nsize n) :=
match n as n0 return Bvector (Nsize n0) with
| N0 => Bnil
| Npos p => P2Bv p
end.

Fixpoint Bv2N (n:nat)(bv:Bvector n) {struct bv} : N :=
match bv with
| Vnil => N0
| Vcons false n bv => Ndouble (Bv2N n bv)
| Vcons true n bv => Ndouble_plus_one (Bv2N n bv)
end.

Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n.

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:

Lemma Bv2N_Nsize : forall n (bv:Bvector n), Nsize (Bv2N n bv) <= n.

In the previous lemma, we can only replace the inequality by an equality whenever the highest bit is non-null.

Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)),
Bsign _ bv = true <->
Nsize (Bv2N _ bv) = (S n).

To state nonetheless a second result about composition of conversions, we define a conversion on a given number of bits :

Fixpoint N2Bv_gen (n:nat)(a:N) { struct n } : Bvector n :=
match n return Bvector n with
| 0 => Bnil
| S n => match a with
| N0 => Bvect_false (S n)
| Npos xH => Bcons true _ (Bvect_false n)
| Npos (xO p) => Bcons false _ (N2Bv_gen n (Npos p))
| Npos (xI p) => Bcons true _ (N2Bv_gen n (Npos p))
end
end.

The first N2Bv is then a special case of N2Bv_gen

Lemma N2Bv_N2Bv_gen : forall (a:N), N2Bv a = N2Bv_gen (Nsize a) a.

In fact, if k is large enough, N2Bv_gen k a contains all digits of a plus some zeros.

Lemma N2Bv_N2Bv_gen_above : forall (a:N)(k:nat),
N2Bv_gen (Nsize a + k) a = Vextend _ _ _ (N2Bv a) (Bvect_false k).

Here comes now the second composition result.

Lemma N2Bv_Bv2N : forall n (bv:Bvector n),
N2Bv_gen n (Bv2N n bv) = bv.

accessing some precise bits.

Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)),
Nbit0 (Bv2N _ bv) = Blow _ bv.

Definition Bnth (n:nat)(bv:Bvector n)(p:nat) : p<n -> bool.

Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n),
Bnth _ bv p H = Nbit (Bv2N _ bv) p.

Lemma Nbit_Nsize : forall n p, Nsize n <= p -> Nbit n p = false.

Lemma Nbit_Bth: forall n p (H:p < Nsize n), Nbit n p = Bnth _ (N2Bv n) p H.

Xor is the same in the two worlds.

Lemma Nxor_BVxor : forall n (bv bv' : Bvector n),
Bv2N _ (BVxor _ bv bv') = Nxor (Bv2N _ bv) (Bv2N _ bv').