diff options
Diffstat (limited to 'theories/NArith/BinNat.v')
| -rw-r--r-- | theories/NArith/BinNat.v | 175 |
1 files changed, 88 insertions, 87 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 4c398573..5d3ec5ab 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Export BinNums. @@ -956,95 +958,94 @@ Notation "( p | q )" := (N.divide p q) (at level 0) : N_scope. (** Compatibility notations *) -(*Notation N := N (compat "8.3").*) (*hidden by module N above *) Notation N_rect := N_rect (only parsing). Notation N_rec := N_rec (only parsing). Notation N_ind := N_ind (only parsing). Notation N0 := N0 (only parsing). Notation Npos := N.pos (only parsing). -Notation Ndiscr := N.discr (compat "8.3"). -Notation Ndouble_plus_one := N.succ_double (compat "8.3"). -Notation Ndouble := N.double (compat "8.3"). -Notation Nsucc := N.succ (compat "8.3"). -Notation Npred := N.pred (compat "8.3"). -Notation Nsucc_pos := N.succ_pos (compat "8.3"). -Notation Ppred_N := Pos.pred_N (compat "8.3"). -Notation Nplus := N.add (compat "8.3"). -Notation Nminus := N.sub (compat "8.3"). -Notation Nmult := N.mul (compat "8.3"). -Notation Neqb := N.eqb (compat "8.3"). -Notation Ncompare := N.compare (compat "8.3"). -Notation Nlt := N.lt (compat "8.3"). -Notation Ngt := N.gt (compat "8.3"). -Notation Nle := N.le (compat "8.3"). -Notation Nge := N.ge (compat "8.3"). -Notation Nmin := N.min (compat "8.3"). -Notation Nmax := N.max (compat "8.3"). -Notation Ndiv2 := N.div2 (compat "8.3"). -Notation Neven := N.even (compat "8.3"). -Notation Nodd := N.odd (compat "8.3"). -Notation Npow := N.pow (compat "8.3"). -Notation Nlog2 := N.log2 (compat "8.3"). - -Notation nat_of_N := N.to_nat (compat "8.3"). -Notation N_of_nat := N.of_nat (compat "8.3"). -Notation N_eq_dec := N.eq_dec (compat "8.3"). -Notation Nrect := N.peano_rect (compat "8.3"). -Notation Nrect_base := N.peano_rect_base (compat "8.3"). -Notation Nrect_step := N.peano_rect_succ (compat "8.3"). -Notation Nind := N.peano_ind (compat "8.3"). -Notation Nrec := N.peano_rec (compat "8.3"). -Notation Nrec_base := N.peano_rec_base (compat "8.3"). -Notation Nrec_succ := N.peano_rec_succ (compat "8.3"). - -Notation Npred_succ := N.pred_succ (compat "8.3"). -Notation Npred_minus := N.pred_sub (compat "8.3"). -Notation Nsucc_pred := N.succ_pred (compat "8.3"). -Notation Ppred_N_spec := N.pos_pred_spec (compat "8.3"). -Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.3"). -Notation Ppred_Nsucc := N.pos_pred_succ (compat "8.3"). -Notation Nplus_0_l := N.add_0_l (compat "8.3"). -Notation Nplus_0_r := N.add_0_r (compat "8.3"). -Notation Nplus_comm := N.add_comm (compat "8.3"). -Notation Nplus_assoc := N.add_assoc (compat "8.3"). -Notation Nplus_succ := N.add_succ_l (compat "8.3"). -Notation Nsucc_0 := N.succ_0_discr (compat "8.3"). -Notation Nsucc_inj := N.succ_inj (compat "8.3"). -Notation Nminus_N0_Nle := N.sub_0_le (compat "8.3"). -Notation Nminus_0_r := N.sub_0_r (compat "8.3"). -Notation Nminus_succ_r:= N.sub_succ_r (compat "8.3"). -Notation Nmult_0_l := N.mul_0_l (compat "8.3"). -Notation Nmult_1_l := N.mul_1_l (compat "8.3"). -Notation Nmult_1_r := N.mul_1_r (compat "8.3"). -Notation Nmult_comm := N.mul_comm (compat "8.3"). -Notation Nmult_assoc := N.mul_assoc (compat "8.3"). -Notation Nmult_plus_distr_r := N.mul_add_distr_r (compat "8.3"). -Notation Neqb_eq := N.eqb_eq (compat "8.3"). -Notation Nle_0 := N.le_0_l (compat "8.3"). -Notation Ncompare_refl := N.compare_refl (compat "8.3"). -Notation Ncompare_Eq_eq := N.compare_eq (compat "8.3"). -Notation Ncompare_eq_correct := N.compare_eq_iff (compat "8.3"). -Notation Nlt_irrefl := N.lt_irrefl (compat "8.3"). -Notation Nlt_trans := N.lt_trans (compat "8.3"). -Notation Nle_lteq := N.lt_eq_cases (compat "8.3"). -Notation Nlt_succ_r := N.lt_succ_r (compat "8.3"). -Notation Nle_trans := N.le_trans (compat "8.3"). -Notation Nle_succ_l := N.le_succ_l (compat "8.3"). -Notation Ncompare_spec := N.compare_spec (compat "8.3"). -Notation Ncompare_0 := N.compare_0_r (compat "8.3"). -Notation Ndouble_div2 := N.div2_double (compat "8.3"). -Notation Ndouble_plus_one_div2 := N.div2_succ_double (compat "8.3"). -Notation Ndouble_inj := N.double_inj (compat "8.3"). -Notation Ndouble_plus_one_inj := N.succ_double_inj (compat "8.3"). -Notation Npow_0_r := N.pow_0_r (compat "8.3"). -Notation Npow_succ_r := N.pow_succ_r (compat "8.3"). -Notation Nlog2_spec := N.log2_spec (compat "8.3"). -Notation Nlog2_nonpos := N.log2_nonpos (compat "8.3"). -Notation Neven_spec := N.even_spec (compat "8.3"). -Notation Nodd_spec := N.odd_spec (compat "8.3"). -Notation Nlt_not_eq := N.lt_neq (compat "8.3"). -Notation Ngt_Nlt := N.gt_lt (compat "8.3"). +Notation Ndiscr := N.discr (compat "8.6"). +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 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 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 Nrect := N.peano_rect (only parsing). +Notation Nrect_base := N.peano_rect_base (only parsing). +Notation Nrect_step := N.peano_rect_succ (only parsing). +Notation Nind := N.peano_ind (only parsing). +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_minus := N.pred_sub (only parsing). +Notation Nsucc_pred := N.succ_pred (compat "8.6"). +Notation Ppred_N_spec := N.pos_pred_spec (only parsing). +Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.6"). +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). +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 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). +Notation Nmult_0_l := N.mul_0_l (only parsing). +Notation Nmult_1_l := N.mul_1_l (only parsing). +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 Nle_0 := N.le_0_l (only parsing). +Notation Ncompare_refl := N.compare_refl (compat "8.6"). +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 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 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_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 Nlt_not_eq := N.lt_neq (only parsing). +Notation Ngt_Nlt := N.gt_lt (only parsing). (** More complex compatibility facts, expressed as lemmas (to preserve scopes for instance) *) |