6 files changed, 102 insertions, 48 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 5d3ec5ab..92c124ec 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -930,6 +930,8 @@ Bind Scope N_scope with N.t N.
 
 (** Exportation of notations *)
 
+Numeral Notation N N.of_uint N.to_uint : N_scope.
+
 Infix "+" := N.add : N_scope.
 Infix "-" := N.sub : N_scope.
 Infix "*" := N.mul : N_scope.
@@ -964,33 +966,33 @@ Notation N_ind := N_ind (only parsing).
 Notation N0 := N0 (only parsing).
 Notation Npos := N.pos (only parsing).
 
-Notation Ndiscr := N.discr (compat "8.6").
+Notation Ndiscr := N.discr (compat "8.7").
 Notation Ndouble_plus_one := N.succ_double (only parsing).
-Notation Ndouble := N.double (compat "8.6").
-Notation Nsucc := N.succ (compat "8.6").
-Notation Npred := N.pred (compat "8.6").
-Notation Nsucc_pos := N.succ_pos (compat "8.6").
-Notation Ppred_N := Pos.pred_N (compat "8.6").
+Notation Ndouble := N.double (compat "8.7").
+Notation Nsucc := N.succ (compat "8.7").
+Notation Npred := N.pred (compat "8.7").
+Notation Nsucc_pos := N.succ_pos (compat "8.7").
+Notation Ppred_N := Pos.pred_N (compat "8.7").
 Notation Nplus := N.add (only parsing).
 Notation Nminus := N.sub (only parsing).
 Notation Nmult := N.mul (only parsing).
-Notation Neqb := N.eqb (compat "8.6").
-Notation Ncompare := N.compare (compat "8.6").
-Notation Nlt := N.lt (compat "8.6").
-Notation Ngt := N.gt (compat "8.6").
-Notation Nle := N.le (compat "8.6").
-Notation Nge := N.ge (compat "8.6").
-Notation Nmin := N.min (compat "8.6").
-Notation Nmax := N.max (compat "8.6").
-Notation Ndiv2 := N.div2 (compat "8.6").
-Notation Neven := N.even (compat "8.6").
-Notation Nodd := N.odd (compat "8.6").
-Notation Npow := N.pow (compat "8.6").
-Notation Nlog2 := N.log2 (compat "8.6").
+Notation Neqb := N.eqb (compat "8.7").
+Notation Ncompare := N.compare (compat "8.7").
+Notation Nlt := N.lt (compat "8.7").
+Notation Ngt := N.gt (compat "8.7").
+Notation Nle := N.le (compat "8.7").
+Notation Nge := N.ge (compat "8.7").
+Notation Nmin := N.min (compat "8.7").
+Notation Nmax := N.max (compat "8.7").
+Notation Ndiv2 := N.div2 (compat "8.7").
+Notation Neven := N.even (compat "8.7").
+Notation Nodd := N.odd (compat "8.7").
+Notation Npow := N.pow (compat "8.7").
+Notation Nlog2 := N.log2 (compat "8.7").
 
 Notation nat_of_N := N.to_nat (only parsing).
 Notation N_of_nat := N.of_nat (only parsing).
-Notation N_eq_dec := N.eq_dec (compat "8.6").
+Notation N_eq_dec := N.eq_dec (compat "8.7").
 Notation Nrect := N.peano_rect (only parsing).
 Notation Nrect_base := N.peano_rect_base (only parsing).
 Notation Nrect_step := N.peano_rect_succ (only parsing).
@@ -999,11 +1001,11 @@ Notation Nrec := N.peano_rec (only parsing).
 Notation Nrec_base := N.peano_rec_base (only parsing).
 Notation Nrec_succ := N.peano_rec_succ (only parsing).
 
-Notation Npred_succ := N.pred_succ (compat "8.6").
+Notation Npred_succ := N.pred_succ (compat "8.7").
 Notation Npred_minus := N.pred_sub (only parsing).
-Notation Nsucc_pred := N.succ_pred (compat "8.6").
+Notation Nsucc_pred := N.succ_pred (compat "8.7").
 Notation Ppred_N_spec := N.pos_pred_spec (only parsing).
-Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.6").
+Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.7").
 Notation Ppred_Nsucc := N.pos_pred_succ (only parsing).
 Notation Nplus_0_l := N.add_0_l (only parsing).
 Notation Nplus_0_r := N.add_0_r (only parsing).
@@ -1011,7 +1013,7 @@ Notation Nplus_comm := N.add_comm (only parsing).
 Notation Nplus_assoc := N.add_assoc (only parsing).
 Notation Nplus_succ := N.add_succ_l (only parsing).
 Notation Nsucc_0 := N.succ_0_discr (only parsing).
-Notation Nsucc_inj := N.succ_inj (compat "8.6").
+Notation Nsucc_inj := N.succ_inj (compat "8.7").
 Notation Nminus_N0_Nle := N.sub_0_le (only parsing).
 Notation Nminus_0_r := N.sub_0_r (only parsing).
 Notation Nminus_succ_r:= N.sub_succ_r (only parsing).
@@ -1021,29 +1023,29 @@ Notation Nmult_1_r := N.mul_1_r (only parsing).
 Notation Nmult_comm := N.mul_comm (only parsing).
 Notation Nmult_assoc := N.mul_assoc (only parsing).
 Notation Nmult_plus_distr_r := N.mul_add_distr_r (only parsing).
-Notation Neqb_eq := N.eqb_eq (compat "8.6").
+Notation Neqb_eq := N.eqb_eq (compat "8.7").
 Notation Nle_0 := N.le_0_l (only parsing).
-Notation Ncompare_refl := N.compare_refl (compat "8.6").
+Notation Ncompare_refl := N.compare_refl (compat "8.7").
 Notation Ncompare_Eq_eq := N.compare_eq (only parsing).
 Notation Ncompare_eq_correct := N.compare_eq_iff (only parsing).
-Notation Nlt_irrefl := N.lt_irrefl (compat "8.6").
-Notation Nlt_trans := N.lt_trans (compat "8.6").
+Notation Nlt_irrefl := N.lt_irrefl (compat "8.7").
+Notation Nlt_trans := N.lt_trans (compat "8.7").
 Notation Nle_lteq := N.lt_eq_cases (only parsing).
-Notation Nlt_succ_r := N.lt_succ_r (compat "8.6").
-Notation Nle_trans := N.le_trans (compat "8.6").
-Notation Nle_succ_l := N.le_succ_l (compat "8.6").
-Notation Ncompare_spec := N.compare_spec (compat "8.6").
+Notation Nlt_succ_r := N.lt_succ_r (compat "8.7").
+Notation Nle_trans := N.le_trans (compat "8.7").
+Notation Nle_succ_l := N.le_succ_l (compat "8.7").
+Notation Ncompare_spec := N.compare_spec (compat "8.7").
 Notation Ncompare_0 := N.compare_0_r (only parsing).
 Notation Ndouble_div2 := N.div2_double (only parsing).
 Notation Ndouble_plus_one_div2 := N.div2_succ_double (only parsing).
-Notation Ndouble_inj := N.double_inj (compat "8.6").
+Notation Ndouble_inj := N.double_inj (compat "8.7").
 Notation Ndouble_plus_one_inj := N.succ_double_inj (only parsing).
-Notation Npow_0_r := N.pow_0_r (compat "8.6").
-Notation Npow_succ_r := N.pow_succ_r (compat "8.6").
-Notation Nlog2_spec := N.log2_spec (compat "8.6").
-Notation Nlog2_nonpos := N.log2_nonpos (compat "8.6").
-Notation Neven_spec := N.even_spec (compat "8.6").
-Notation Nodd_spec := N.odd_spec (compat "8.6").
+Notation Npow_0_r := N.pow_0_r (compat "8.7").
+Notation Npow_succ_r := N.pow_succ_r (compat "8.7").
+Notation Nlog2_spec := N.log2_spec (compat "8.7").
+Notation Nlog2_nonpos := N.log2_nonpos (compat "8.7").
+Notation Neven_spec := N.even_spec (compat "8.7").
+Notation Nodd_spec := N.odd_spec (compat "8.7").
 Notation Nlt_not_eq := N.lt_neq (only parsing).
 Notation Ngt_Nlt := N.gt_lt (only parsing).
 
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 5de75537..be12fffa 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -13,6 +13,10 @@ Require Import BinPos.
 
 Local Open Scope N_scope.
 
+Local Notation "0" := N0.
+Local Notation "1" := (Npos 1).
+Local Notation "2" := (Npos 2).
+
 (**********************************************************************)
 (** * Binary natural numbers, definitions of operations *)
 (**********************************************************************)
@@ -398,4 +402,9 @@ Definition to_uint n :=
 
 Definition to_int n := Decimal.Pos (to_uint n).
 
+Numeral Notation N of_uint to_uint : N_scope.
+
 End N.
+
+(** Re-export the notation for those who just [Import NatIntDef] *)
+Numeral Notation N N.of_uint N.to_uint : N_scope.
diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v
index 67c30f22..e2b2b490 100644
--- a/theories/NArith/Ndec.v
+++ b/theories/NArith/Ndec.v
@@ -22,8 +22,8 @@ Local Open Scope N_scope.
 (** Obsolete results about boolean comparisons over [N],
     kept for compatibility with IntMap and SMC. *)
 
-Notation Peqb := Pos.eqb (compat "8.6").
-Notation Neqb := N.eqb (compat "8.6").
+Notation Peqb := Pos.eqb (compat "8.7").
+Notation Neqb := N.eqb (compat "8.7").
 Notation Peqb_correct := Pos.eqb_refl (only parsing).
 Notation Neqb_correct := N.eqb_refl (only parsing).
 Notation Neqb_comm := N.eqb_sym (only parsing).
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 3ccaa721..a2a2430e 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -517,6 +517,23 @@ Definition N2Bv (n:N) : Bvector (N.size_nat n) :=
     | Npos p => P2Bv p
   end.
 
+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.
+
+Definition N2Bv_sized (m : nat) (n : N) : Bvector m :=
+  match n with
+  | N0     => Bvect_false m
+  | Npos p => P2Bv_sized  m p
+  end.
+
 Fixpoint Bv2N (n:nat)(bv:Bvector n) : N :=
   match bv with
     | Vector.nil _ => N0
@@ -561,6 +578,7 @@ Qed.
 (** To state nonetheless a second result about composition of
  conversions, we define a conversion on a given number of bits : *)
 
+#[deprecated(since = "8.9.0", note = "Use N2Bv_sized instead.")]
 Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n :=
  match n return Bvector n with
    | 0 => Bnil
@@ -670,3 +688,28 @@ rewrite H.
 destruct a, b, (Bv2N n v1), (Bv2N n v2);
  simpl; auto.
 Qed.
+
+Lemma N2Bv_sized_Nsize (n : N) :
+  N2Bv_sized (N.size_nat n) n = N2Bv n.
+Proof with simpl; auto.
+  destruct n...
+  induction p...
+  all: rewrite IHp...
+Qed.
+
+Lemma N2Bv_sized_Bv2N (n : nat) (v : Bvector n) :
+  N2Bv_sized n (Bv2N n v) = v.
+Proof with simpl; auto.
+  induction v...
+  destruct h;
+  unfold N2Bv_sized;
+  destruct (Bv2N n v) as [|[]];
+  rewrite <- IHv...
+Qed.
+
+Lemma N2Bv_N2Bv_sized_above (a : N) (k : nat) :
+  N2Bv_sized (N.size_nat a + k) a = N2Bv a ++ Bvect_false k.
+Proof with auto.
+  destruct a...
+  induction p; simpl; f_equal...
+Qed.
diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v
index 7c9fd869..885c0d48 100644
--- a/theories/NArith/Ndiv_def.v
+++ b/theories/NArith/Ndiv_def.v
@@ -24,10 +24,10 @@ Lemma Pdiv_eucl_remainder a b :
   snd (Pdiv_eucl a b) < Npos b.
 Proof. now apply (N.pos_div_eucl_remainder a (Npos b)). Qed.
 
-Notation Ndiv_eucl := N.div_eucl (compat "8.6").
-Notation Ndiv := N.div (compat "8.6").
+Notation Ndiv_eucl := N.div_eucl (compat "8.7").
+Notation Ndiv := N.div (compat "8.7").
 Notation Nmod := N.modulo (only parsing).
 
 Notation Ndiv_eucl_correct := N.div_eucl_spec (only parsing).
 Notation Ndiv_mod_eq := N.div_mod' (only parsing).
-Notation Nmod_lt := N.mod_lt (compat "8.6").
+Notation Nmod_lt := N.mod_lt (compat "8.7").
diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v
index e771fe91..f0433283 100644
--- a/theories/NArith/Nsqrt_def.v
+++ b/theories/NArith/Nsqrt_def.v
@@ -13,8 +13,8 @@ Require Import BinNat.
 (** Obsolete file, see [BinNat] now,
     only compatibility notations remain here. *)
 
-Notation Nsqrtrem := N.sqrtrem (compat "8.6").
-Notation Nsqrt := N.sqrt (compat "8.6").
-Notation Nsqrtrem_spec := N.sqrtrem_spec (compat "8.6").
+Notation Nsqrtrem := N.sqrtrem (compat "8.7").
+Notation Nsqrt := N.sqrt (compat "8.7").
+Notation Nsqrtrem_spec := N.sqrtrem_spec (compat "8.7").
 Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (only parsing).
-Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (compat "8.6").
+Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (compat "8.7").