From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- theories/NArith/BinNat.v | 80 +++++++++++++++++++++++---------------------- theories/NArith/BinNatDef.v | 9 +++++ theories/NArith/Ndec.v | 4 +-- theories/NArith/Ndigits.v | 43 ++++++++++++++++++++++++ theories/NArith/Ndiv_def.v | 6 ++-- theories/NArith/Nsqrt_def.v | 8 ++--- 6 files changed, 102 insertions(+), 48 deletions(-) (limited to 'theories/NArith') 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"). -- cgit v1.2.3