diff options
Diffstat (limited to 'theories/PArith')
| -rw-r--r-- | theories/PArith/BinPos.v | 82 | ||||
| -rw-r--r-- | theories/PArith/BinPosDef.v | 13 |
2 files changed, 52 insertions, 43 deletions
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 000d895e..01ecdd71 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1871,6 +1871,8 @@ Bind Scope positive_scope with Pos.t positive. (** Exportation of notations *) +Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. + Infix "+" := Pos.add : positive_scope. Infix "-" := Pos.sub : positive_scope. Infix "*" := Pos.mul : positive_scope. @@ -1905,12 +1907,12 @@ Notation IsNul := Pos.IsNul (only parsing). Notation IsPos := Pos.IsPos (only parsing). Notation IsNeg := Pos.IsNeg (only parsing). -Notation Psucc := Pos.succ (compat "8.6"). +Notation Psucc := Pos.succ (compat "8.7"). Notation Pplus := Pos.add (only parsing). Notation Pplus_carry := Pos.add_carry (only parsing). -Notation Ppred := Pos.pred (compat "8.6"). -Notation Piter_op := Pos.iter_op (compat "8.6"). -Notation Piter_op_succ := Pos.iter_op_succ (compat "8.6"). +Notation Ppred := Pos.pred (compat "8.7"). +Notation Piter_op := Pos.iter_op (compat "8.7"). +Notation Piter_op_succ := Pos.iter_op_succ (compat "8.7"). Notation Pmult_nat := (Pos.iter_op plus) (only parsing). Notation nat_of_P := Pos.to_nat (only parsing). Notation P_of_succ_nat := Pos.of_succ_nat (only parsing). @@ -1920,29 +1922,29 @@ Notation positive_mask_rect := Pos.mask_rect (only parsing). Notation positive_mask_ind := Pos.mask_ind (only parsing). Notation positive_mask_rec := Pos.mask_rec (only parsing). Notation Pdouble_plus_one_mask := Pos.succ_double_mask (only parsing). -Notation Pdouble_mask := Pos.double_mask (compat "8.6"). +Notation Pdouble_mask := Pos.double_mask (compat "8.7"). Notation Pdouble_minus_two := Pos.double_pred_mask (only parsing). Notation Pminus_mask := Pos.sub_mask (only parsing). Notation Pminus_mask_carry := Pos.sub_mask_carry (only parsing). Notation Pminus := Pos.sub (only parsing). Notation Pmult := Pos.mul (only parsing). Notation iter_pos := @Pos.iter (only parsing). -Notation Ppow := Pos.pow (compat "8.6"). -Notation Pdiv2 := Pos.div2 (compat "8.6"). -Notation Pdiv2_up := Pos.div2_up (compat "8.6"). +Notation Ppow := Pos.pow (compat "8.7"). +Notation Pdiv2 := Pos.div2 (compat "8.7"). +Notation Pdiv2_up := Pos.div2_up (compat "8.7"). Notation Psize := Pos.size_nat (only parsing). Notation Psize_pos := Pos.size (only parsing). Notation Pcompare x y m := (Pos.compare_cont m x y) (only parsing). -Notation Plt := Pos.lt (compat "8.6"). -Notation Pgt := Pos.gt (compat "8.6"). -Notation Ple := Pos.le (compat "8.6"). -Notation Pge := Pos.ge (compat "8.6"). -Notation Pmin := Pos.min (compat "8.6"). -Notation Pmax := Pos.max (compat "8.6"). -Notation Peqb := Pos.eqb (compat "8.6"). +Notation Plt := Pos.lt (compat "8.7"). +Notation Pgt := Pos.gt (compat "8.7"). +Notation Ple := Pos.le (compat "8.7"). +Notation Pge := Pos.ge (compat "8.7"). +Notation Pmin := Pos.min (compat "8.7"). +Notation Pmax := Pos.max (compat "8.7"). +Notation Peqb := Pos.eqb (compat "8.7"). Notation positive_eq_dec := Pos.eq_dec (only parsing). Notation xI_succ_xO := Pos.xI_succ_xO (only parsing). -Notation Psucc_discr := Pos.succ_discr (compat "8.6"). +Notation Psucc_discr := Pos.succ_discr (compat "8.7"). Notation Psucc_o_double_minus_one_eq_xO := Pos.succ_pred_double (only parsing). Notation Pdouble_minus_one_o_succ_eq_xI := @@ -1951,9 +1953,9 @@ Notation xO_succ_permute := Pos.double_succ (only parsing). Notation double_moins_un_xO_discr := Pos.pred_double_xO_discr (only parsing). Notation Psucc_not_one := Pos.succ_not_1 (only parsing). -Notation Ppred_succ := Pos.pred_succ (compat "8.6"). +Notation Ppred_succ := Pos.pred_succ (compat "8.7"). Notation Psucc_pred := Pos.succ_pred_or (only parsing). -Notation Psucc_inj := Pos.succ_inj (compat "8.6"). +Notation Psucc_inj := Pos.succ_inj (compat "8.7"). Notation Pplus_carry_spec := Pos.add_carry_spec (only parsing). Notation Pplus_comm := Pos.add_comm (only parsing). Notation Pplus_succ_permute_r := Pos.add_succ_r (only parsing). @@ -2000,17 +2002,17 @@ Notation Pmult_xO_discr := Pos.mul_xO_discr (only parsing). Notation Pmult_reg_r := Pos.mul_reg_r (only parsing). Notation Pmult_reg_l := Pos.mul_reg_l (only parsing). Notation Pmult_1_inversion_l := Pos.mul_eq_1_l (only parsing). -Notation Psquare_xO := Pos.square_xO (compat "8.6"). -Notation Psquare_xI := Pos.square_xI (compat "8.6"). +Notation Psquare_xO := Pos.square_xO (compat "8.7"). +Notation Psquare_xI := Pos.square_xI (compat "8.7"). Notation iter_pos_swap_gen := Pos.iter_swap_gen (only parsing). Notation iter_pos_swap := Pos.iter_swap (only parsing). Notation iter_pos_succ := Pos.iter_succ (only parsing). Notation iter_pos_plus := Pos.iter_add (only parsing). Notation iter_pos_invariant := Pos.iter_invariant (only parsing). -Notation Ppow_1_r := Pos.pow_1_r (compat "8.6"). -Notation Ppow_succ_r := Pos.pow_succ_r (compat "8.6"). -Notation Peqb_refl := Pos.eqb_refl (compat "8.6"). -Notation Peqb_eq := Pos.eqb_eq (compat "8.6"). +Notation Ppow_1_r := Pos.pow_1_r (compat "8.7"). +Notation Ppow_succ_r := Pos.pow_succ_r (compat "8.7"). +Notation Peqb_refl := Pos.eqb_refl (compat "8.7"). +Notation Peqb_eq := Pos.eqb_eq (compat "8.7"). Notation Pcompare_refl_id := Pos.compare_cont_refl (only parsing). Notation Pcompare_eq_iff := Pos.compare_eq_iff (only parsing). Notation Pcompare_Gt_Lt := Pos.compare_cont_Gt_Lt (only parsing). @@ -2020,23 +2022,23 @@ Notation Pcompare_Lt_Gt := Pos.compare_cont_Lt_Gt (only parsing). Notation Pcompare_antisym := Pos.compare_cont_antisym (only parsing). Notation ZC1 := Pos.gt_lt (only parsing). Notation ZC2 := Pos.lt_gt (only parsing). -Notation Pcompare_spec := Pos.compare_spec (compat "8.6"). +Notation Pcompare_spec := Pos.compare_spec (compat "8.7"). Notation Pcompare_p_Sp := Pos.lt_succ_diag_r (only parsing). -Notation Pcompare_succ_succ := Pos.compare_succ_succ (compat "8.6"). +Notation Pcompare_succ_succ := Pos.compare_succ_succ (compat "8.7"). Notation Pcompare_1 := Pos.nlt_1_r (only parsing). Notation Plt_1 := Pos.nlt_1_r (only parsing). -Notation Plt_1_succ := Pos.lt_1_succ (compat "8.6"). -Notation Plt_lt_succ := Pos.lt_lt_succ (compat "8.6"). -Notation Plt_irrefl := Pos.lt_irrefl (compat "8.6"). -Notation Plt_trans := Pos.lt_trans (compat "8.6"). -Notation Plt_ind := Pos.lt_ind (compat "8.6"). -Notation Ple_lteq := Pos.le_lteq (compat "8.6"). -Notation Ple_refl := Pos.le_refl (compat "8.6"). -Notation Ple_lt_trans := Pos.le_lt_trans (compat "8.6"). -Notation Plt_le_trans := Pos.lt_le_trans (compat "8.6"). -Notation Ple_trans := Pos.le_trans (compat "8.6"). -Notation Plt_succ_r := Pos.lt_succ_r (compat "8.6"). -Notation Ple_succ_l := Pos.le_succ_l (compat "8.6"). +Notation Plt_1_succ := Pos.lt_1_succ (compat "8.7"). +Notation Plt_lt_succ := Pos.lt_lt_succ (compat "8.7"). +Notation Plt_irrefl := Pos.lt_irrefl (compat "8.7"). +Notation Plt_trans := Pos.lt_trans (compat "8.7"). +Notation Plt_ind := Pos.lt_ind (compat "8.7"). +Notation Ple_lteq := Pos.le_lteq (compat "8.7"). +Notation Ple_refl := Pos.le_refl (compat "8.7"). +Notation Ple_lt_trans := Pos.le_lt_trans (compat "8.7"). +Notation Plt_le_trans := Pos.lt_le_trans (compat "8.7"). +Notation Ple_trans := Pos.le_trans (compat "8.7"). +Notation Plt_succ_r := Pos.lt_succ_r (compat "8.7"). +Notation Ple_succ_l := Pos.le_succ_l (compat "8.7"). Notation Pplus_compare_mono_l := Pos.add_compare_mono_l (only parsing). Notation Pplus_compare_mono_r := Pos.add_compare_mono_r (only parsing). Notation Pplus_lt_mono_l := Pos.add_lt_mono_l (only parsing). @@ -2055,8 +2057,8 @@ Notation Pmult_le_mono_r := Pos.mul_le_mono_r (only parsing). Notation Pmult_le_mono := Pos.mul_le_mono (only parsing). Notation Plt_plus_r := Pos.lt_add_r (only parsing). Notation Plt_not_plus_l := Pos.lt_not_add_l (only parsing). -Notation Ppow_gt_1 := Pos.pow_gt_1 (compat "8.6"). -Notation Ppred_mask := Pos.pred_mask (compat "8.6"). +Notation Ppow_gt_1 := Pos.pow_gt_1 (compat "8.7"). +Notation Ppred_mask := Pos.pred_mask (compat "8.7"). Notation Pminus_mask_succ_r := Pos.sub_mask_succ_r (only parsing). Notation Pminus_mask_carry_spec := Pos.sub_mask_carry_spec (only parsing). Notation Pminus_succ_r := Pos.sub_succ_r (only parsing). diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 07031474..7f307335 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -26,6 +26,8 @@ Require Export BinNums. for the number 6 (which is 110 in binary notation). *) +Local Notation "1" := xH. + Notation "p ~ 1" := (xI p) (at level 7, left associativity, format "p '~' '1'") : positive_scope. Notation "p ~ 0" := (xO p) @@ -325,14 +327,14 @@ Definition sqrtrem_step (f g:positive->positive) p := let r' := g (f r) in if s' <=? r' then (s~1, sub_mask r' s') else (s~0, IsPos r') - | (s,_) => (s~0, sub_mask (g (f 1)) 4) + | (s,_) => (s~0, sub_mask (g (f 1)) 1~0~0) end. Fixpoint sqrtrem p : positive * mask := match p with | 1 => (1,IsNul) - | 2 => (1,IsPos 1) - | 3 => (1,IsPos 2) + | 1~0 => (1,IsPos 1) + | 1~1 => (1,IsPos 1~0) | p~0~0 => sqrtrem_step xO xO (sqrtrem p) | p~0~1 => sqrtrem_step xO xI (sqrtrem p) | p~1~0 => sqrtrem_step xI xO (sqrtrem p) @@ -614,4 +616,9 @@ Definition to_uint p := Decimal.rev (to_little_uint p). Definition to_int n := Decimal.Pos (to_uint n). +Numeral Notation positive of_int to_uint : positive_scope. + End Pos. + +(** Re-export the notation for those who just [Import BinPosDef] *) +Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. |