Library Coq.NArith.Ndigits


Require Import Bool Morphisms Setoid Bvector BinPos BinNat PeanoNat Pnat Nnat
        Basics ByteVector.

Local Open Scope N_scope.
Local Open Scope program_scope.

This file is mostly obsolete, see directly BinNat now.

Compatibility names for some bitwise operations

#[deprecated(since="8.19", note="Use Pos.lxor.")]
Notation Pxor := Pos.lxor (only parsing).
#[deprecated(since="8.19", note="Use N.lxor.")]
Notation Nxor := N.lxor (only parsing).
#[deprecated(since="8.19", note="Use Pos.testbit_nat.")]
Notation Pbit := Pos.testbit_nat (only parsing).
#[deprecated(since="8.19", note="Use N.testbit_nat.")]
Notation Nbit := N.testbit_nat (only parsing).

#[deprecated(since="8.19", note="Use N.lxor_eq.")]
Notation Nxor_eq := N.lxor_eq (only parsing).
#[deprecated(since="8.19", note="Use N.lxor_comm.")]
Notation Nxor_comm := N.lxor_comm (only parsing).
#[deprecated(since="8.19", note="Use N.lxor_assoc.")]
Notation Nxor_assoc := N.lxor_assoc (only parsing).
#[deprecated(since="8.19", note="Use N.lxor_0_l.")]
Notation Nxor_neutral_left := N.lxor_0_l (only parsing).
#[deprecated(since="8.19", note="Use N.lxor_0_r.")]
Notation Nxor_neutral_right := N.lxor_0_r (only parsing).
#[deprecated(since="8.19", note="Use N.lxor_nilpotent.")]
Notation Nxor_nilpotent := N.lxor_nilpotent (only parsing).

Equivalence of bit-testing functions, either with index in N or in nat.

#[deprecated(since="8.19", note="Consider BinPos instead.")]
Lemma Ptestbit_Pbit :
 forall p n, Pos.testbit p (N.of_nat n) = Pos.testbit_nat p n.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Ntestbit_Nbit : forall a n, N.testbit a (N.of_nat n) = N.testbit_nat a n.

#[deprecated(since="8.19", note="Consider BinPos instead.")]
Lemma Pbit_Ptestbit :
 forall p n, Pos.testbit_nat p (N.to_nat n) = Pos.testbit p n.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nbit_Ntestbit :
 forall a n, N.testbit_nat a (N.to_nat n) = N.testbit a n.

Equivalence of shifts, index in N or nat

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nshiftr_nat_S : forall a n,
 N.shiftr_nat a (S n) = N.div2 (N.shiftr_nat a n).

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nshiftl_nat_S : forall a n,
 N.shiftl_nat a (S n) = N.double (N.shiftl_nat a n).

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nshiftr_nat_equiv :
 forall a n, N.shiftr_nat a (N.to_nat n) = N.shiftr a n.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nshiftr_equiv_nat :
 forall a n, N.shiftr a (N.of_nat n) = N.shiftr_nat a n.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nshiftl_nat_equiv :
 forall a n, N.shiftl_nat a (N.to_nat n) = N.shiftl a n.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
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

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nshiftr_nat_spec : forall a n m,
  N.testbit_nat (N.shiftr_nat a n) m = N.testbit_nat a (m+n).

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat ->
  N.testbit_nat (N.shiftl_nat a n) m = N.testbit_nat a (m-n).

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nshiftl_nat_spec_low : forall a n m, (m<n)%nat ->
 N.testbit_nat (N.shiftl_nat a n) m = false.

A left shift for positive numbers (used in BigN)

#[deprecated(since="8.19", note="Consider BinPos instead.")]
Lemma Pshiftl_nat_0 : forall p, Pos.shiftl_nat p 0 = p.

#[deprecated(since="8.19", note="Consider BinPos instead.")]
Lemma Pshiftl_nat_S :
 forall p n, Pos.shiftl_nat p (S n) = xO (Pos.shiftl_nat p n).

#[deprecated(since="8.19", note="Consider BinPos instead.")]
Lemma Pshiftl_nat_N :
 forall p n, Npos (Pos.shiftl_nat p n) = N.shiftl_nat (Npos p) n.

#[deprecated(since="8.19", note="Consider BinPos instead.")]
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 N.testbit_nat

#[deprecated(since="8.19", note="Consider BinPos instead.")]
Lemma Pxor_semantics p p' n :
 N.testbit_nat (Pos.lxor p p') n = xorb (Pos.testbit_nat p n) (Pos.testbit_nat p' n).

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nxor_semantics a a' n :
 N.testbit_nat (N.lxor a a') n = xorb (N.testbit_nat a n) (N.testbit_nat a' n).

#[deprecated(since="8.19", note="Consider BinPos instead.")]
Lemma Por_semantics p p' n :
 Pos.testbit_nat (Pos.lor p p') n = (Pos.testbit_nat p n) || (Pos.testbit_nat p' n).

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nor_semantics a a' n :
 N.testbit_nat (N.lor a a') n = (N.testbit_nat a n) || (N.testbit_nat a' n).

#[deprecated(since="8.19", note="Consider BinPos instead.")]
Lemma Pand_semantics p p' n :
 N.testbit_nat (Pos.land p p') n = (Pos.testbit_nat p n) && (Pos.testbit_nat p' n).

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nand_semantics a a' n :
 N.testbit_nat (N.land a a') n = (N.testbit_nat a n) && (N.testbit_nat a' n).

#[deprecated(since="8.19", note="Consider BinPos instead.")]
Lemma Pdiff_semantics p p' n :
 N.testbit_nat (Pos.ldiff p p') n = (Pos.testbit_nat p n) && negb (Pos.testbit_nat p' n).

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Ndiff_semantics a a' n :
 N.testbit_nat (N.ldiff a a') n = (N.testbit_nat a n) && negb (N.testbit_nat a' n).

Equality over functional streams of bits

#[deprecated(since="8.19", note="Use Coq.Classes.Morphisms.pointwise_relation.")]
Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n.

#[global]
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)).

#[deprecated(since="8.19", note="Consider BinPos instead.")]
Lemma Pbit_faithful_0 : forall p, ~(Pos.testbit_nat p == (fun _ => false)).

#[deprecated(since="8.19", note="Consider BinPos instead.")]
Lemma Pbit_faithful : forall p p', Pos.testbit_nat p == Pos.testbit_nat p' -> p = p'.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nbit_faithful : forall n n', N.testbit_nat n == N.testbit_nat n' -> n = n'.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nbit_faithful_iff : forall n n', N.testbit_nat n == N.testbit_nat n' <-> n = n'.

Local Close Scope N_scope.

Checking whether a number is odd, i.e. if its lower bit is set.

#[deprecated(since="8.19", note="Use N.odd.")]
Notation Nbit0 := N.odd (only parsing).

#[deprecated(since="8.19", note="Use N.odd n = true.")]
Definition Nodd (n:N) := N.odd n = true.
#[deprecated(since="8.19", note="Use N.odd n = false.")]
Definition Neven (n:N) := N.odd n = false.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nbit0_correct : forall n:N, N.testbit_nat n 0 = N.odd n.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Ndouble_bit0 : forall n:N, N.odd (N.double n) = false.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Ndouble_plus_one_bit0 :
 forall n:N, N.odd (N.succ_double n) = true.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Ndiv2_double :
 forall n:N, Neven n -> N.double (N.div2 n) = n.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Ndiv2_double_plus_one :
 forall n:N, Nodd n -> N.succ_double (N.div2 n) = n.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Ndiv2_correct :
 forall (a:N) (n:nat), N.testbit_nat (N.div2 a) n = N.testbit_nat a (S n).

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nxor_bit0 :
 forall a a':N, N.odd (N.lxor a a') = xorb (N.odd a) (N.odd a').

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nxor_div2 :
 forall a a':N, N.div2 (N.lxor a a') = N.lxor (N.div2 a) (N.div2 a').

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nneg_bit0 :
 forall a a':N,
   N.odd (N.lxor a a') = true -> N.odd a = negb (N.odd a').

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nneg_bit0_1 :
 forall a a':N, N.lxor a a' = Npos 1 -> N.odd a = negb (N.odd a').

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nneg_bit0_2 :
 forall (a a':N) (p:positive),
   N.lxor a a' = Npos (xI p) -> N.odd a = negb (N.odd a').

#[deprecated(since="8.19", note="Consider BinNat instead.")]
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

#[deprecated(since="8.19", note="Adopt the implementation if needed.")]
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.

#[deprecated(since="8.19", note="Adopt the implementation if needed.")]
Definition Nless (a a':N) :=
  match N.lxor a a' with
  | N0 => false
  | Npos p => Nless_aux a a' p
  end.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nbit0_less :
 forall a a',
   N.odd a = false -> N.odd a' = true -> Nless a a' = true.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nbit0_gt :
 forall a a',
   N.odd a = true -> N.odd a' = false -> Nless a a' = false.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nless_not_refl : forall a, Nless a a = false.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nless_def_1 :
 forall a a', Nless (N.double a) (N.double a') = Nless a a'.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nless_def_2 :
 forall a a',
   Nless (N.succ_double a) (N.succ_double a') = Nless a a'.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nless_def_3 :
 forall a a', Nless (N.double a) (N.succ_double a') = true.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nless_def_4 :
 forall a a', Nless (N.succ_double a) (N.double a') = false.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nless_z : forall a, Nless a N0 = false.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma N0_less_1 :
 forall a, Nless N0 a = true -> {p : positive | a = Npos p}.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma N0_less_2 : forall a, Nless N0 a = false -> a = N0.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nless_trans :
 forall a a' a'',
   Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nless_total :
 forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}.

Number of digits in a number

#[deprecated(since="8.19", note="Use N.size_nat.")]
Notation Nsize := N.size_nat (only parsing).

conversions between N and bit vectors.

#[deprecated(since="8.19", note="Use Pos.testbit.")]
Fixpoint P2Bv (p:positive) : Bvector (Pos.size_nat p) :=
 match p return Bvector (Pos.size_nat p) with
   | xH => Bvect_true 1%nat
   | xO p => Bcons false (Pos.size_nat p) (P2Bv p)
   | xI p => Bcons true (Pos.size_nat p) (P2Bv p)
 end.

#[deprecated(since="8.19", note="Use N.testbit.")]
Definition N2Bv (n:N) : Bvector (N.size_nat n) :=
  match n as n0 return Bvector (N.size_nat n0) with
    | N0 => Bnil
    | Npos p => P2Bv p
  end.

#[deprecated(since="8.19", note="Use Pos.testbit.")]
Fixpoint P2Bv_sized (m : nat) (p : positive) : Bvector m :=
  match m with
  | O => []
  | S m =>
    match p with
    | xI p => true :: P2Bv_sized m p
    | xO p => false :: P2Bv_sized m p
    | xH => true :: Bvect_false m
    end
  end.

#[deprecated(since="8.19", note="Use N.tesbit.")]
Definition N2Bv_sized (m : nat) (n : N) : Bvector m :=
  match n with
  | N0 => Bvect_false m
  | Npos p => P2Bv_sized m p
  end.

#[deprecated(since="8.19", note="Consider N.testbit instead.")]
Definition N2ByteV_sized (m : nat) : N -> ByteVector m :=
  of_Bvector N2Bv_sized (m * 8).

#[deprecated(since="8.19", note="Consider N.testbit instead.")]
Fixpoint Bv2N (n:nat)(bv:Bvector n) : N :=
  match bv with
    | Vector.nil _ => N0
    | Vector.cons _ false n bv => N.double (Bv2N n bv)
    | Vector.cons _ true n bv => N.succ_double (Bv2N n bv)
  end.

Arguments Bv2N {n} bv, n bv.

#[deprecated(since="8.19", note="Consider N.testbit instead.")]
Definition ByteV2N {n : nat} : ByteVector n -> N :=
  Bv2N to_Bvector.

#[deprecated(since="8.19", note="Consider N.testbit instead.")]
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:

#[deprecated(since="8.19", note="Consider N.testbit instead.")]
Lemma Bv2N_Nsize : forall n (bv:Bvector n), N.size_nat (Bv2N n bv) <= n.

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

#[deprecated(since="8.19", note="Consider N.testbit instead.")]
Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)),
  Bsign _ bv = true <->
  N.size_nat (Bv2N _ bv) = (S n).

#[deprecated(since="8.19", note="Consider N.testbit instead.")]
Lemma Bv2N_upper_bound (n : nat) (bv : Bvector n) :
    (Bv2N bv < N.shiftl_nat 1 n)%N.

#[deprecated(since="8.19", note="Consider N.testbit instead.")]
Corollary ByteV2N_upper_bound (n : nat) (v : ByteVector n) :
  (ByteV2N v < N.shiftl_nat 1 (n * 8))%N.

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

#[deprecated(since="8.19", note="Consider N.testbit instead.")]
Fixpoint N2Bv_gen_deprecated (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_deprecated n (Npos p))
       | Npos (xI p) => Bcons true _ (N2Bv_gen_deprecated n (Npos p))
      end
  end.

#[deprecated(since = "8.9.0", note = "Use N2Bv_sized instead.")]
Notation N2Bv_gen := N2Bv_gen_deprecated (only parsing).

The first N2Bv is then a special case of N2Bv_gen

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma N2Bv_N2Bv_gen (a:N) : N2Bv a = N2Bv_gen_deprecated (N.size_nat a) a.

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

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma N2Bv_N2Bv_gen_above : forall (a:N)(k:nat),
  N2Bv_gen_deprecated (N.size_nat a + k) a
  = Vector.append (N2Bv a) (Bvect_false k).

Here comes now the second composition result.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma N2Bv_Bv2N : forall n (bv:Bvector n),
  N2Bv_gen_deprecated n (Bv2N n bv) = bv.

accessing some precise bits.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)),
  N.odd (Bv2N _ bv) = Blow _ bv.

#[deprecated(since="8.19", note="Use Vector.nth_order bool.")]
Notation Bnth := (@Vector.nth_order bool).

#[deprecated(since="8.19", note="Consider N.testbit instead.")]
Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n),
  Bnth bv H = N.testbit_nat (Bv2N _ bv) p.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nbit_Nsize : forall n p, N.size_nat n <= p -> N.testbit_nat n p = false.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nbit_Bth: forall n p (H:p < N.size_nat n),
  N.testbit_nat n p = Bnth (N2Bv n) H.

Binary bitwise operations are the same in the two worlds.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nxor_BVxor : forall n (bv bv' : Bvector n),
  Bv2N _ (BVxor _ bv bv') = N.lxor (Bv2N _ bv) (Bv2N _ bv').

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma Nand_BVand : forall n (bv bv' : Bvector n),
  Bv2N _ (BVand _ bv bv') = N.land (Bv2N _ bv) (Bv2N _ bv').

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma N2Bv_sized_Nsize (n : N) :
  N2Bv_sized (N.size_nat n) n = N2Bv n.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma N2Bv_sized_Bv2N (n : nat) (v : Bvector n) :
  N2Bv_sized n (Bv2N n v) = v.

#[deprecated(since="8.19", note="Consider BinNat instead.")]
Lemma N2Bv_N2Bv_sized_above (a : N) (k : nat) :
  N2Bv_sized (N.size_nat a + k) a = N2Bv a ++ Bvect_false k.