Library Coq.NArith.Ndigits
Require Import Bool Morphisms Setoid Bvector BinPos BinNat Wf_nat
Pnat Nnat Compare_dec Lt Minus.
Local Open Scope N_scope.
This file is mostly obsolete, see directly BinNat now.
Compatibility names for some bitwise operations
Notation Pxor := Pos.lxor (only parsing).
Notation Nxor := N.lxor (only parsing).
Notation Pbit := Pos.testbit_nat (only parsing).
Notation Nbit := N.testbit_nat (only parsing).
Notation Nxor_eq := N.lxor_eq (only parsing).
Notation Nxor_comm := N.lxor_comm (only parsing).
Notation Nxor_assoc := N.lxor_assoc (only parsing).
Notation Nxor_neutral_left := N.lxor_0_l (only parsing).
Notation Nxor_neutral_right := N.lxor_0_r (only parsing).
Notation Nxor_nilpotent := N.lxor_nilpotent (only parsing).
Equivalence of bit-testing functions,
either with index in N or in nat.
Lemma Ptestbit_Pbit :
forall p n, Pos.testbit p (N.of_nat n) = Pbit p n.
Lemma Ntestbit_Nbit : forall a n, N.testbit a (N.of_nat n) = Nbit a n.
Lemma Pbit_Ptestbit :
forall p n, Pbit p (N.to_nat n) = Pos.testbit p n.
Lemma Nbit_Ntestbit :
forall a n, Nbit a (N.to_nat n) = N.testbit a n.
Equivalence of shifts, index in N or nat
Lemma Nshiftr_nat_S : forall a n,
N.shiftr_nat a (S n) = N.div2 (N.shiftr_nat a n).
Lemma Nshiftl_nat_S : forall a n,
N.shiftl_nat a (S n) = N.double (N.shiftl_nat a n).
Lemma Nshiftr_nat_equiv :
forall a n, N.shiftr_nat a (N.to_nat n) = N.shiftr a n.
Lemma Nshiftr_equiv_nat :
forall a n, N.shiftr a (N.of_nat n) = N.shiftr_nat a n.
Lemma Nshiftl_nat_equiv :
forall a n, N.shiftl_nat a (N.to_nat n) = N.shiftl a n.
Lemma Nshiftl_equiv_nat :
forall a n, N.shiftl a (N.of_nat n) = N.shiftl_nat a n.
Correctness proofs for shifts, nat version
Lemma Nshiftr_nat_spec : forall a n m,
Nbit (N.shiftr_nat a n) m = Nbit a (m+n).
Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat ->
Nbit (N.shiftl_nat a n) m = Nbit a (m-n).
Lemma Nshiftl_nat_spec_low : forall a n m, (m<n)%nat ->
Nbit (N.shiftl_nat a n) m = false.
A left shift for positive numbers (used in BigN)
Lemma Pshiftl_nat_0 : forall p, Pos.shiftl_nat p 0 = p.
Lemma Pshiftl_nat_S :
forall p n, Pos.shiftl_nat p (S n) = xO (Pos.shiftl_nat p n).
Lemma Pshiftl_nat_N :
forall p n, Npos (Pos.shiftl_nat p n) = N.shiftl_nat (Npos p) n.
Lemma Pshiftl_nat_plus : forall n m p,
Pos.shiftl_nat p (m + n) = Pos.shiftl_nat (Pos.shiftl_nat p n) m.
Semantics of bitwise operations with respect to Nbit
Lemma Pxor_semantics p p' n :
Nbit (Pos.lxor p p') n = xorb (Pbit p n) (Pbit p' n).
Lemma Nxor_semantics a a' n :
Nbit (N.lxor a a') n = xorb (Nbit a n) (Nbit a' n).
Lemma Por_semantics p p' n :
Pbit (Pos.lor p p') n = (Pbit p n) || (Pbit p' n).
Lemma Nor_semantics a a' n :
Nbit (N.lor a a') n = (Nbit a n) || (Nbit a' n).
Lemma Pand_semantics p p' n :
Nbit (Pos.land p p') n = (Pbit p n) && (Pbit p' n).
Lemma Nand_semantics a a' n :
Nbit (N.land a a') n = (Nbit a n) && (Nbit a' n).
Lemma Pdiff_semantics p p' n :
Nbit (Pos.ldiff p p') n = (Pbit p n) && negb (Pbit p' n).
Lemma Ndiff_semantics a a' n :
Nbit (N.ldiff a a') n = (Nbit a n) && negb (Nbit a' n).
Equality over functional streams of bits
Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n.
Program Instance eqf_equiv : Equivalence eqf.
Local Infix "==" := eqf (at level 70, no associativity).
If two numbers produce the same stream of bits, they are equal.
Local Notation Step H := (fun n => H (S n)).
Lemma Pbit_faithful_0 : forall p, ~(Pbit p == (fun _ => false)).
Lemma Pbit_faithful : forall p p', Pbit p == Pbit p' -> p = p'.
Lemma Nbit_faithful : forall n n', Nbit n == Nbit n' -> n = n'.
Lemma Nbit_faithful_iff : forall n n', Nbit n == Nbit n' <-> n = n'.
Local Close Scope N_scope.
Checking whether a number is odd, i.e.
if its lower bit is set.
Notation Nbit0 := N.odd (only parsing).
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) : 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.
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) : N :=
match bv with
| Vector.nil => N0
| Vector.cons false n bv => Ndouble (Bv2N n bv)
| Vector.cons 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:
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 :
Fixpoint N2Bv_gen (n:nat)(a: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
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 = Vector.append (N2Bv a) (Bvect_false k).
Here comes now the second composition result.
accessing some precise bits.
Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)),
Nbit0 (Bv2N _ bv) = Blow _ bv.
Notation Bnth := (@Vector.nth_order bool).
Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n),
Bnth bv 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) H.
Binary bitwise operations are the same in the two worlds.