diff options
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/BinNat.v | 220 | ||||
| -rw-r--r-- | theories/NArith/BinNatDef.v | 94 | ||||
| -rw-r--r-- | theories/NArith/NArith.v | 2 | ||||
| -rw-r--r-- | theories/NArith/Ndec.v | 443 | ||||
| -rw-r--r-- | theories/NArith/Ndigits.v | 207 | ||||
| -rw-r--r-- | theories/NArith/Ndist.v | 104 | ||||
| -rw-r--r-- | theories/NArith/Ndiv_def.v | 14 | ||||
| -rw-r--r-- | theories/NArith/Ngcd_def.v | 2 | ||||
| -rw-r--r-- | theories/NArith/Nnat.v | 56 | ||||
| -rw-r--r-- | theories/NArith/Nsqrt_def.v | 12 |
10 files changed, 510 insertions, 644 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 30e35f50..5b1e83e6 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -76,7 +76,7 @@ Defined. (** Discrimination principle *) -Definition discr n : { p:positive | n = Npos p } + { n = N0 }. +Definition discr n : { p:positive | n = pos p } + { n = 0 }. Proof. destruct n; auto. left; exists p; auto. @@ -87,12 +87,12 @@ Defined. Definition binary_rect (P:N -> Type) (f0 : P 0) (f2 : forall n, P n -> P (double n)) (fS2 : forall n, P n -> P (succ_double n)) (n : N) : P n := - let P' p := P (Npos p) in - let f2' p := f2 (Npos p) in - let fS2' p := fS2 (Npos p) in + let P' p := P (pos p) in + let f2' p := f2 (pos p) in + let fS2' p := fS2 (pos p) in match n with | 0 => f0 - | Npos p => positive_rect P' fS2' f2' (fS2 0 f0) p + | pos p => positive_rect P' fS2' f2' (fS2 0 f0) p end. Definition binary_rec (P:N -> Set) := binary_rect P. @@ -103,11 +103,11 @@ Definition binary_ind (P:N -> Prop) := binary_rect P. Definition peano_rect (P : N -> Type) (f0 : P 0) (f : forall n : N, P n -> P (succ n)) (n : N) : P n := -let P' p := P (Npos p) in -let f' p := f (Npos p) in +let P' p := P (pos p) in +let f' p := f (pos p) in match n with | 0 => f0 -| Npos p => Pos.peano_rect P' (f 0 f0) f' p +| pos p => Pos.peano_rect P' (f 0 f0) f' p end. Theorem peano_rect_base P a f : peano_rect P a f 0 = a. @@ -140,12 +140,12 @@ Qed. (** Properties of mixed successor and predecessor. *) -Lemma pos_pred_spec p : Pos.pred_N p = pred (Npos p). +Lemma pos_pred_spec p : Pos.pred_N p = pred (pos p). Proof. now destruct p. Qed. -Lemma succ_pos_spec n : Npos (succ_pos n) = succ n. +Lemma succ_pos_spec n : pos (succ_pos n) = succ n. Proof. now destruct n. Qed. @@ -155,7 +155,7 @@ Proof. destruct n. trivial. apply Pos.pred_N_succ. Qed. -Lemma succ_pos_pred p : succ (Pos.pred_N p) = Npos p. +Lemma succ_pos_pred p : succ (Pos.pred_N p) = pos p. Proof. destruct p; simpl; trivial. f_equal. apply Pos.succ_pred_double. Qed. @@ -472,7 +472,7 @@ Lemma log2_spec n : 0 < n -> 2^(log2 n) <= n < 2^(succ (log2 n)). Proof. destruct n as [|[p|p|]]; discriminate || intros _; simpl; split. - apply (size_le (Npos p)). + apply (size_le (pos p)). apply Pos.size_gt. apply Pos.size_le. apply Pos.size_gt. @@ -494,7 +494,7 @@ Proof. trivial. destruct p; simpl; split; try easy. intros (m,H). now destruct m. - now exists (Npos p). + now exists (pos p). intros (m,H). now destruct m. Qed. @@ -504,7 +504,7 @@ Proof. split. discriminate. intros (m,H). now destruct m. destruct p; simpl; split; try easy. - now exists (Npos p). + now exists (pos p). intros (m,H). now destruct m. now exists 0. Qed. @@ -512,19 +512,19 @@ Qed. (** Specification of the euclidean division *) Theorem pos_div_eucl_spec (a:positive)(b:N) : - let (q,r) := pos_div_eucl a b in Npos a = q * b + r. + let (q,r) := pos_div_eucl a b in pos a = q * b + r. Proof. induction a; cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta. (* a~1 *) destruct pos_div_eucl as (q,r). - change (Npos a~1) with (succ_double (Npos a)). + change (pos a~1) with (succ_double (pos a)). rewrite IHa, succ_double_add, double_mul. case leb_spec; intros H; trivial. rewrite succ_double_mul, <- add_assoc. f_equal. now rewrite (add_comm b), sub_add. (* a~0 *) destruct pos_div_eucl as (q,r). - change (Npos a~0) with (double (Npos a)). + change (pos a~0) with (double (pos a)). rewrite IHa, double_add, double_mul. case leb_spec; intros H; trivial. rewrite succ_double_mul, <- add_assoc. f_equal. @@ -537,7 +537,7 @@ Theorem div_eucl_spec a b : let (q,r) := div_eucl a b in a = b * q + r. Proof. destruct a as [|a], b as [|b]; unfold div_eucl; trivial. - generalize (pos_div_eucl_spec a (Npos b)). + generalize (pos_div_eucl_spec a (pos b)). destruct pos_div_eucl. now rewrite mul_comm. Qed. @@ -664,7 +664,7 @@ Proof. destruct (Pos.gcd_greatest p q r) as (u,H). exists s. now inversion Hs. exists t. now inversion Ht. - exists (Npos u). simpl; now f_equal. + exists (pos u). simpl; now f_equal. Qed. Lemma gcd_nonneg a b : 0 <= gcd a b. @@ -862,7 +862,7 @@ Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _. Theorem bi_induction : forall A : N -> Prop, Proper (Logic.eq==>iff) A -> - A N0 -> (forall n, A n <-> A (succ n)) -> forall n : N, A n. + A 0 -> (forall n, A n <-> A (succ n)) -> forall n : N, A n. Proof. intros A A_wd A0 AS. apply peano_rect. assumption. intros; now apply -> AS. Qed. @@ -893,11 +893,11 @@ Qed. (** Instantiation of generic properties of natural numbers *) -Include NProp - <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. +(** The Bind Scope prevents N to stay associated with abstract_scope. + (TODO FIX) *) -(** Otherwise N stays associated with abstract_scope : (TODO FIX) *) -Bind Scope N_scope with N. +Include NProp. Bind Scope N_scope with N. +Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. (** In generic statements, the predicates [lt] and [le] have been favored, whereas [gt] and [ge] don't even exist in the abstract @@ -1013,95 +1013,95 @@ Notation "( p | q )" := (N.divide p q) (at level 0) : N_scope. (** Compatibility notations *) -(*Notation N := N (only parsing).*) (*hidden by module N above *) +(*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 := Npos (only parsing). - -Notation Ndiscr := N.discr (only parsing). -Notation Ndouble_plus_one := N.succ_double. -Notation Ndouble := N.double (only parsing). -Notation Nsucc := N.succ (only parsing). -Notation Npred := N.pred (only parsing). -Notation Nsucc_pos := N.succ_pos (only parsing). -Notation Ppred_N := Pos.pred_N (only parsing). -Notation Nplus := N.add (only parsing). -Notation Nminus := N.sub (only parsing). -Notation Nmult := N.mul (only parsing). -Notation Neqb := N.eqb (only parsing). -Notation Ncompare := N.compare (only parsing). -Notation Nlt := N.lt (only parsing). -Notation Ngt := N.gt (only parsing). -Notation Nle := N.le (only parsing). -Notation Nge := N.ge (only parsing). -Notation Nmin := N.min (only parsing). -Notation Nmax := N.max (only parsing). -Notation Ndiv2 := N.div2 (only parsing). -Notation Neven := N.even (only parsing). -Notation Nodd := N.odd (only parsing). -Notation Npow := N.pow (only parsing). -Notation Nlog2 := N.log2 (only parsing). - -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 (only parsing). -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 (only parsing). -Notation Npred_minus := N.pred_sub (only parsing). -Notation Nsucc_pred := N.succ_pred (only parsing). -Notation Ppred_N_spec := N.pos_pred_spec (only parsing). -Notation Nsucc_pos_spec := N.succ_pos_spec (only parsing). -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 (only parsing). -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 (only parsing). -Notation Nle_0 := N.le_0_l (only parsing). -Notation Ncompare_refl := N.compare_refl (only parsing). -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 (only parsing). -Notation Nlt_trans := N.lt_trans (only parsing). -Notation Nle_lteq := N.lt_eq_cases (only parsing). -Notation Nlt_succ_r := N.lt_succ_r (only parsing). -Notation Nle_trans := N.le_trans (only parsing). -Notation Nle_succ_l := N.le_succ_l (only parsing). -Notation Ncompare_spec := N.compare_spec (only parsing). -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 (only parsing). -Notation Ndouble_plus_one_inj := N.succ_double_inj (only parsing). -Notation Npow_0_r := N.pow_0_r (only parsing). -Notation Npow_succ_r := N.pow_succ_r (only parsing). -Notation Nlog2_spec := N.log2_spec (only parsing). -Notation Nlog2_nonpos := N.log2_nonpos (only parsing). -Notation Neven_spec := N.even_spec (only parsing). -Notation Nodd_spec := N.odd_spec (only parsing). -Notation Nlt_not_eq := N.lt_neq (only parsing). -Notation Ngt_Nlt := N.gt_lt (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"). (** More complex compatibility facts, expressed as lemmas (to preserve scopes for instance) *) diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index d7660422..08e1138f 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -19,6 +19,10 @@ Module N. Definition t := N. +(** ** Nicer name [N.pos] for contructor [Npos] *) + +Notation pos := Npos. + (** ** Constants *) Definition zero := 0. @@ -30,7 +34,7 @@ Definition two := 2. Definition succ_double x := match x with | 0 => 1 - | Npos p => Npos p~1 + | pos p => pos p~1 end. (** ** Operation [x -> 2*x] *) @@ -38,7 +42,7 @@ Definition succ_double x := Definition double n := match n with | 0 => 0 - | Npos p => Npos p~0 + | pos p => pos p~0 end. (** ** Successor *) @@ -46,7 +50,7 @@ Definition double n := Definition succ n := match n with | 0 => 1 - | Npos p => Npos (Pos.succ p) + | pos p => pos (Pos.succ p) end. (** ** Predecessor *) @@ -54,15 +58,15 @@ Definition succ n := Definition pred n := match n with | 0 => 0 - | Npos p => Pos.pred_N p + | pos p => Pos.pred_N p end. (** ** The successor of a [N] can be seen as a [positive] *) Definition succ_pos (n : N) : positive := match n with - | N0 => 1%positive - | Npos p => Pos.succ p + | 0 => 1%positive + | pos p => Pos.succ p end. (** ** Addition *) @@ -71,7 +75,7 @@ Definition add n m := match n, m with | 0, _ => m | _, 0 => n - | Npos p, Npos q => Npos (p + q) + | pos p, pos q => pos (p + q) end. Infix "+" := add : N_scope. @@ -82,9 +86,9 @@ Definition sub n m := match n, m with | 0, _ => 0 | n, 0 => n -| Npos n', Npos m' => +| pos n', pos m' => match Pos.sub_mask n' m' with - | IsPos p => Npos p + | IsPos p => pos p | _ => 0 end end. @@ -97,7 +101,7 @@ Definition mul n m := match n, m with | 0, _ => 0 | _, 0 => 0 - | Npos p, Npos q => Npos (p * q) + | pos p, pos q => pos (p * q) end. Infix "*" := mul : N_scope. @@ -107,23 +111,19 @@ Infix "*" := mul : N_scope. Definition compare n m := match n, m with | 0, 0 => Eq - | 0, Npos m' => Lt - | Npos n', 0 => Gt - | Npos n', Npos m' => (n' ?= m')%positive + | 0, pos m' => Lt + | pos n', 0 => Gt + | pos n', pos m' => (n' ?= m')%positive end. Infix "?=" := compare (at level 70, no associativity) : N_scope. (** Boolean equality and comparison *) -(** Nota: this [eqb] is not convertible with the generated [N_beq], - since the underlying [Pos.eqb] differs from [positive_beq] - (cf BinIntDef). *) - Fixpoint eqb n m := match n, m with | 0, 0 => true - | Npos p, Npos q => Pos.eqb p q + | pos p, pos q => Pos.eqb p q | _, _ => false end. @@ -155,8 +155,8 @@ Definition div2 n := match n with | 0 => 0 | 1 => 0 - | Npos (p~0) => Npos p - | Npos (p~1) => Npos p + | pos (p~0) => pos p + | pos (p~1) => pos p end. (** Parity *) @@ -164,7 +164,7 @@ Definition div2 n := Definition even n := match n with | 0 => true - | Npos (xO _) => true + | pos (xO _) => true | _ => false end. @@ -176,7 +176,7 @@ Definition pow n p := match p, n with | 0, _ => 1 | _, 0 => 0 - | Npos p, Npos q => Npos (q^p) + | pos p, pos q => pos (q^p) end. Infix "^" := pow : N_scope. @@ -186,7 +186,7 @@ Infix "^" := pow : N_scope. Definition square n := match n with | 0 => 0 - | Npos p => Npos (Pos.square p) + | pos p => pos (Pos.square p) end. (** Base-2 logarithm *) @@ -195,8 +195,8 @@ Definition log2 n := match n with | 0 => 0 | 1 => 0 - | Npos (p~0) => Npos (Pos.size p) - | Npos (p~1) => Npos (Pos.size p) + | pos (p~0) => pos (Pos.size p) + | pos (p~1) => pos (Pos.size p) end. (** How many digits in a number ? @@ -206,13 +206,13 @@ Definition log2 n := Definition size n := match n with | 0 => 0 - | Npos p => Npos (Pos.size p) + | pos p => pos (Pos.size p) end. Definition size_nat n := match n with | 0 => O - | Npos p => Pos.size_nat p + | pos p => Pos.size_nat p end. (** Euclidean division *) @@ -237,7 +237,7 @@ Definition div_eucl (a b:N) : N * N := match a, b with | 0, _ => (0, 0) | _, 0 => (0, a) - | Npos na, _ => pos_div_eucl na b + | pos na, _ => pos_div_eucl na b end. Definition div a b := fst (div_eucl a b). @@ -252,7 +252,7 @@ Definition gcd a b := match a, b with | 0, _ => b | _, 0 => a - | Npos p, Npos q => Npos (Pos.gcd p q) + | pos p, pos q => pos (Pos.gcd p q) end. (** Generalized Gcd, also computing rests of [a] and [b] after @@ -262,9 +262,9 @@ Definition ggcd a b := match a, b with | 0, _ => (b,(0,1)) | _, 0 => (a,(1,0)) - | Npos p, Npos q => + | pos p, pos q => let '(g,(aa,bb)) := Pos.ggcd p q in - (Npos g, (Npos aa, Npos bb)) + (pos g, (pos aa, pos bb)) end. (** Square root *) @@ -272,17 +272,17 @@ Definition ggcd a b := Definition sqrtrem n := match n with | 0 => (0, 0) - | Npos p => + | pos p => match Pos.sqrtrem p with - | (s, IsPos r) => (Npos s, Npos r) - | (s, _) => (Npos s, 0) + | (s, IsPos r) => (pos s, pos r) + | (s, _) => (pos s, 0) end end. Definition sqrt n := match n with | 0 => 0 - | Npos p => Npos (Pos.sqrt p) + | pos p => pos (Pos.sqrt p) end. (** Operation over bits of a [N] number. *) @@ -293,7 +293,7 @@ Definition lor n m := match n, m with | 0, _ => m | _, 0 => n - | Npos p, Npos q => Npos (Pos.lor p q) + | pos p, pos q => pos (Pos.lor p q) end. (** Logical [and] *) @@ -302,7 +302,7 @@ Definition land n m := match n, m with | 0, _ => 0 | _, 0 => 0 - | Npos p, Npos q => Pos.land p q + | pos p, pos q => Pos.land p q end. (** Logical [diff] *) @@ -311,7 +311,7 @@ Fixpoint ldiff n m := match n, m with | 0, _ => 0 | _, 0 => n - | Npos p, Npos q => Pos.ldiff p q + | pos p, pos q => Pos.ldiff p q end. (** [xor] *) @@ -320,7 +320,7 @@ Definition lxor n m := match n, m with | 0, _ => m | _, 0 => n - | Npos p, Npos q => Pos.lxor p q + | pos p, pos q => Pos.lxor p q end. (** Shifts *) @@ -331,13 +331,13 @@ Definition shiftr_nat (a:N)(n:nat) := nat_iter n div2 a. Definition shiftl a n := match a with | 0 => 0 - | Npos a => Npos (Pos.shiftl a n) + | pos a => pos (Pos.shiftl a n) end. Definition shiftr a n := match n with | 0 => a - | Npos p => Pos.iter p div2 a + | pos p => Pos.iter p div2 a end. (** Checking whether a particular bit is set or not *) @@ -345,7 +345,7 @@ Definition shiftr a n := Definition testbit_nat (a:N) := match a with | 0 => fun _ => false - | Npos p => Pos.testbit_nat p + | pos p => Pos.testbit_nat p end. (** Same, but with index in N *) @@ -353,7 +353,7 @@ Definition testbit_nat (a:N) := Definition testbit a n := match a with | 0 => false - | Npos p => Pos.testbit p n + | pos p => Pos.testbit p n end. (** Translation from [N] to [nat] and back. *) @@ -361,13 +361,13 @@ Definition testbit a n := Definition to_nat (a:N) := match a with | 0 => O - | Npos p => Pos.to_nat p + | pos p => Pos.to_nat p end. Definition of_nat (n:nat) := match n with | O => 0 - | S n' => Npos (Pos.of_succ_nat n') + | S n' => pos (Pos.of_succ_nat n') end. (** Iteration of a function *) @@ -375,7 +375,7 @@ Definition of_nat (n:nat) := Definition iter (n:N) {A} (f:A->A) (x:A) : A := match n with | 0 => x - | Npos p => Pos.iter p f x + | pos p => Pos.iter p f x end. End N.
\ No newline at end of file diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v index 4a5f4ee1..d0664d37 100644 --- a/theories/NArith/NArith.v +++ b/theories/NArith/NArith.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index f2ee29cc..f8db7548 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -15,315 +15,238 @@ Require Import Pnat. Require Import Nnat. Require Import Ndigits. -(** A boolean equality over [N] *) +Local Open Scope N_scope. -Notation Peqb := Peqb (only parsing). (* Now in [BinPos] *) -Notation Neqb := Neqb (only parsing). (* Now in [BinNat] *) +(** Obsolete results about boolean comparisons over [N], + kept for compatibility with IntMap and SMC. *) -Notation Peqb_correct := Peqb_refl (only parsing). +Notation Peqb := Pos.eqb (compat "8.3"). +Notation Neqb := N.eqb (compat "8.3"). +Notation Peqb_correct := Pos.eqb_refl (compat "8.3"). +Notation Neqb_correct := N.eqb_refl (compat "8.3"). +Notation Neqb_comm := N.eqb_sym (compat "8.3"). -Lemma Peqb_complete : forall p p', Peqb p p' = true -> p = p'. -Proof. - intros. now apply (Peqb_eq p p'). -Qed. +Lemma Peqb_complete p p' : Pos.eqb p p' = true -> p = p'. +Proof. now apply Pos.eqb_eq. Qed. -Lemma Peqb_Pcompare : forall p p', Peqb p p' = true -> Pos.compare p p' = Eq. -Proof. - intros. now rewrite Pos.compare_eq_iff, <- Peqb_eq. -Qed. - -Lemma Pcompare_Peqb : forall p p', Pos.compare p p' = Eq -> Peqb p p' = true. -Proof. - intros; now rewrite Peqb_eq, <- Pos.compare_eq_iff. -Qed. +Lemma Peqb_Pcompare p p' : Pos.eqb p p' = true -> Pos.compare p p' = Eq. +Proof. now rewrite Pos.compare_eq_iff, <- Pos.eqb_eq. Qed. -Lemma Neqb_correct : forall n, Neqb n n = true. -Proof. - intros; now rewrite Neqb_eq. -Qed. +Lemma Pcompare_Peqb p p' : Pos.compare p p' = Eq -> Pos.eqb p p' = true. +Proof. now rewrite Pos.eqb_eq, <- Pos.compare_eq_iff. Qed. -Lemma Neqb_Ncompare : forall n n', Neqb n n' = true -> Ncompare n n' = Eq. -Proof. - intros; now rewrite Ncompare_eq_correct, <- Neqb_eq. -Qed. +Lemma Neqb_Ncompare n n' : N.eqb n n' = true -> N.compare n n' = Eq. +Proof. now rewrite N.compare_eq_iff, <- N.eqb_eq. Qed. -Lemma Ncompare_Neqb : forall n n', Ncompare n n' = Eq -> Neqb n n' = true. -Proof. - intros; now rewrite Neqb_eq, <- Ncompare_eq_correct. -Qed. +Lemma Ncompare_Neqb n n' : N.compare n n' = Eq -> N.eqb n n' = true. +Proof. now rewrite N.eqb_eq, <- N.compare_eq_iff. Qed. -Lemma Neqb_complete : forall a a', Neqb a a' = true -> a = a'. -Proof. - intros; now rewrite <- Neqb_eq. -Qed. +Lemma Neqb_complete n n' : N.eqb n n' = true -> n = n'. +Proof. now apply N.eqb_eq. Qed. -Lemma Neqb_comm : forall a a', Neqb a a' = Neqb a' a. +Lemma Nxor_eq_true n n' : N.lxor n n' = 0 -> N.eqb n n' = true. Proof. - intros; apply eq_true_iff_eq. rewrite 2 Neqb_eq; auto with *. + intro H. apply N.lxor_eq in H. subst. apply N.eqb_refl. Qed. -Lemma Nxor_eq_true : - forall a a', Nxor a a' = N0 -> Neqb a a' = true. -Proof. - intros. rewrite (Nxor_eq a a' H). apply Neqb_correct. -Qed. +Ltac eqb2eq := rewrite <- ?not_true_iff_false in *; rewrite ?N.eqb_eq in *. -Lemma Nxor_eq_false : - forall a a' p, Nxor a a' = Npos p -> Neqb a a' = false. +Lemma Nxor_eq_false n n' p : + N.lxor n n' = N.pos p -> N.eqb n n' = false. Proof. - intros. elim (sumbool_of_bool (Neqb a a')). intro H0. - rewrite (Neqb_complete a a' H0) in H. - rewrite (Nxor_nilpotent a') in H. discriminate H. - trivial. + intros. eqb2eq. intro. subst. now rewrite N.lxor_nilpotent in *. Qed. -Lemma Nodd_not_double : - forall a, - Nodd a -> forall a0, Neqb (Ndouble a0) a = false. +Lemma Nodd_not_double a : + Nodd a -> forall a0, N.eqb (N.double a0) a = false. Proof. - intros. elim (sumbool_of_bool (Neqb (Ndouble a0) a)). intro H0. - rewrite <- (Neqb_complete _ _ H0) in H. - unfold Nodd in H. - rewrite (Ndouble_bit0 a0) in H. discriminate H. - trivial. + intros. eqb2eq. intros <-. + unfold Nodd in *. now rewrite Ndouble_bit0 in *. Qed. -Lemma Nnot_div2_not_double : - forall a a0, - Neqb (Ndiv2 a) a0 = false -> Neqb a (Ndouble a0) = false. +Lemma Nnot_div2_not_double a a0 : + N.eqb (N.div2 a) a0 = false -> N.eqb a (N.double a0) = false. Proof. - intros. elim (sumbool_of_bool (Neqb (Ndouble a0) a)). intro H0. - rewrite <- (Neqb_complete _ _ H0) in H. rewrite (Ndouble_div2 a0) in H. - rewrite (Neqb_correct a0) in H. discriminate H. - intro. rewrite Neqb_comm. assumption. + intros H. eqb2eq. contradict H. subst. apply N.div2_double. Qed. -Lemma Neven_not_double_plus_one : - forall a, - Neven a -> forall a0, Neqb (Ndouble_plus_one a0) a = false. +Lemma Neven_not_double_plus_one a : + Neven a -> forall a0, N.eqb (N.succ_double a0) a = false. Proof. - intros. elim (sumbool_of_bool (Neqb (Ndouble_plus_one a0) a)). intro H0. - rewrite <- (Neqb_complete _ _ H0) in H. - unfold Neven in H. - rewrite (Ndouble_plus_one_bit0 a0) in H. - discriminate H. - trivial. + intros. eqb2eq. intros <-. + unfold Neven in *. now rewrite Ndouble_plus_one_bit0 in *. Qed. -Lemma Nnot_div2_not_double_plus_one : - forall a a0, - Neqb (Ndiv2 a) a0 = false -> Neqb (Ndouble_plus_one a0) a = false. +Lemma Nnot_div2_not_double_plus_one a a0 : + N.eqb (N.div2 a) a0 = false -> N.eqb (N.succ_double a0) a = false. Proof. - intros. elim (sumbool_of_bool (Neqb a (Ndouble_plus_one a0))). intro H0. - rewrite (Neqb_complete _ _ H0) in H. rewrite (Ndouble_plus_one_div2 a0) in H. - rewrite (Neqb_correct a0) in H. discriminate H. - intro H0. rewrite Neqb_comm. assumption. + intros H. eqb2eq. contradict H. subst. apply N.div2_succ_double. Qed. -Lemma Nbit0_neq : - forall a a', - Nbit0 a = false -> Nbit0 a' = true -> Neqb a a' = false. +Lemma Nbit0_neq a a' : + N.odd a = false -> N.odd a' = true -> N.eqb a a' = false. Proof. - intros. elim (sumbool_of_bool (Neqb a a')). intro H1. - rewrite (Neqb_complete _ _ H1) in H. - rewrite H in H0. discriminate H0. - trivial. + intros. eqb2eq. now intros <-. Qed. -Lemma Ndiv2_eq : - forall a a', Neqb a a' = true -> Neqb (Ndiv2 a) (Ndiv2 a') = true. +Lemma Ndiv2_eq a a' : + N.eqb a a' = true -> N.eqb (N.div2 a) (N.div2 a') = true. Proof. - intros. cut (a = a'). intros. rewrite H0. apply Neqb_correct. - apply Neqb_complete. exact H. + intros. eqb2eq. now subst. Qed. -Lemma Ndiv2_neq : - forall a a', - Neqb (Ndiv2 a) (Ndiv2 a') = false -> Neqb a a' = false. +Lemma Ndiv2_neq a a' : + N.eqb (N.div2 a) (N.div2 a') = false -> N.eqb a a' = false. Proof. - intros. elim (sumbool_of_bool (Neqb a a')). intro H0. - rewrite (Neqb_complete _ _ H0) in H. - rewrite (Neqb_correct (Ndiv2 a')) in H. discriminate H. - trivial. + intros H. eqb2eq. contradict H. now subst. Qed. -Lemma Ndiv2_bit_eq : - forall a a', - Nbit0 a = Nbit0 a' -> Ndiv2 a = Ndiv2 a' -> a = a'. +Lemma Ndiv2_bit_eq a a' : + N.odd a = N.odd a' -> N.div2 a = N.div2 a' -> a = a'. Proof. - intros. apply Nbit_faithful. unfold eqf in |- *. destruct n. - rewrite Nbit0_correct. rewrite Nbit0_correct. assumption. - rewrite <- Ndiv2_correct. rewrite <- Ndiv2_correct. - rewrite H0. reflexivity. + intros H H'; now rewrite (N.div2_odd a), (N.div2_odd a'), H, H'. Qed. -Lemma Ndiv2_bit_neq : - forall a a', - Neqb a a' = false -> - Nbit0 a = Nbit0 a' -> Neqb (Ndiv2 a) (Ndiv2 a') = false. +Lemma Ndiv2_bit_neq a a' : + N.eqb a a' = false -> + N.odd a = N.odd a' -> N.eqb (N.div2 a) (N.div2 a') = false. Proof. - intros. elim (sumbool_of_bool (Neqb (Ndiv2 a) (Ndiv2 a'))). intro H1. - rewrite (Ndiv2_bit_eq _ _ H0 (Neqb_complete _ _ H1)) in H. - rewrite (Neqb_correct a') in H. discriminate H. - trivial. + intros H H'. eqb2eq. contradict H. now apply Ndiv2_bit_eq. Qed. -Lemma Nneq_elim : - forall a a', - Neqb a a' = false -> - Nbit0 a = negb (Nbit0 a') \/ - Neqb (Ndiv2 a) (Ndiv2 a') = false. +Lemma Nneq_elim a a' : + N.eqb a a' = false -> + N.odd a = negb (N.odd a') \/ + N.eqb (N.div2 a) (N.div2 a') = false. Proof. - intros. cut (Nbit0 a = Nbit0 a' \/ Nbit0 a = negb (Nbit0 a')). + intros. cut (N.odd a = N.odd a' \/ N.odd a = negb (N.odd a')). intros. elim H0. intro. right. apply Ndiv2_bit_neq. assumption. assumption. intro. left. assumption. - case (Nbit0 a); case (Nbit0 a'); auto. + case (N.odd a), (N.odd a'); auto. Qed. -Lemma Ndouble_or_double_plus_un : - forall a, - {a0 : N | a = Ndouble a0} + {a1 : N | a = Ndouble_plus_one a1}. +Lemma Ndouble_or_double_plus_un a : + {a0 : N | a = N.double a0} + {a1 : N | a = N.succ_double a1}. Proof. - intro. elim (sumbool_of_bool (Nbit0 a)). intro H. right. split with (Ndiv2 a). - rewrite (Ndiv2_double_plus_one a H). reflexivity. - intro H. left. split with (Ndiv2 a). rewrite (Ndiv2_double a H). reflexivity. + elim (sumbool_of_bool (N.odd a)); intros H; [right|left]; + exists (N.div2 a); symmetry; + apply Ndiv2_double_plus_one || apply Ndiv2_double; auto. Qed. -(** A boolean order on [N] *) +(** An inefficient boolean order on [N]. Please use [N.leb] instead now. *) -Definition Nleb (a b:N) := leb (nat_of_N a) (nat_of_N b). +Definition Nleb (a b:N) := leb (N.to_nat a) (N.to_nat b). -Lemma Nleb_Nle : forall a b, Nleb a b = true <-> Nle a b. +Lemma Nleb_alt a b : Nleb a b = N.leb a b. Proof. - intros; unfold Nle; rewrite nat_of_Ncompare. - unfold Nleb; apply leb_compare. + unfold Nleb. + now rewrite eq_iff_eq_true, N.leb_le, leb_compare, <- N2Nat.inj_compare. Qed. -Lemma Nleb_refl : forall a, Nleb a a = true. -Proof. - intro. unfold Nleb in |- *. apply leb_correct. apply le_n. -Qed. +Lemma Nleb_Nle a b : Nleb a b = true <-> a <= b. +Proof. now rewrite Nleb_alt, N.leb_le. Qed. -Lemma Nleb_antisym : - forall a b, Nleb a b = true -> Nleb b a = true -> a = b. -Proof. - unfold Nleb in |- *. intros. rewrite <- (N_of_nat_of_N a). rewrite <- (N_of_nat_of_N b). - rewrite (le_antisym _ _ (leb_complete _ _ H) (leb_complete _ _ H0)). reflexivity. -Qed. +Lemma Nleb_refl a : Nleb a a = true. +Proof. rewrite Nleb_Nle; apply N.le_refl. Qed. -Lemma Nleb_trans : - forall a b c, Nleb a b = true -> Nleb b c = true -> Nleb a c = true. -Proof. - unfold Nleb in |- *. intros. apply leb_correct. apply le_trans with (m := nat_of_N b). - apply leb_complete. assumption. - apply leb_complete. assumption. -Qed. +Lemma Nleb_antisym a b : Nleb a b = true -> Nleb b a = true -> a = b. +Proof. rewrite !Nleb_Nle. apply N.le_antisymm. Qed. + +Lemma Nleb_trans a b c : Nleb a b = true -> Nleb b c = true -> Nleb a c = true. +Proof. rewrite !Nleb_Nle. apply N.le_trans. Qed. -Lemma Nleb_ltb_trans : - forall a b c, - Nleb a b = true -> Nleb c b = false -> Nleb c a = false. +Lemma Nleb_ltb_trans a b c : + Nleb a b = true -> Nleb c b = false -> Nleb c a = false. Proof. - unfold Nleb in |- *. intros. apply leb_correct_conv. apply le_lt_trans with (m := nat_of_N b). + unfold Nleb. intros. apply leb_correct_conv. + apply le_lt_trans with (m := N.to_nat b). apply leb_complete. assumption. apply leb_complete_conv. assumption. Qed. -Lemma Nltb_leb_trans : - forall a b c, - Nleb b a = false -> Nleb b c = true -> Nleb c a = false. +Lemma Nltb_leb_trans a b c : + Nleb b a = false -> Nleb b c = true -> Nleb c a = false. Proof. - unfold Nleb in |- *. intros. apply leb_correct_conv. apply lt_le_trans with (m := nat_of_N b). + unfold Nleb. intros. apply leb_correct_conv. + apply lt_le_trans with (m := N.to_nat b). apply leb_complete_conv. assumption. apply leb_complete. assumption. Qed. -Lemma Nltb_trans : - forall a b c, - Nleb b a = false -> Nleb c b = false -> Nleb c a = false. +Lemma Nltb_trans a b c : + Nleb b a = false -> Nleb c b = false -> Nleb c a = false. Proof. - unfold Nleb in |- *. intros. apply leb_correct_conv. apply lt_trans with (m := nat_of_N b). + unfold Nleb. intros. apply leb_correct_conv. + apply lt_trans with (m := N.to_nat b). apply leb_complete_conv. assumption. apply leb_complete_conv. assumption. Qed. -Lemma Nltb_leb_weak : forall a b:N, Nleb b a = false -> Nleb a b = true. +Lemma Nltb_leb_weak a b : Nleb b a = false -> Nleb a b = true. Proof. - unfold Nleb in |- *. intros. apply leb_correct. apply lt_le_weak. + unfold Nleb. intros. apply leb_correct. apply lt_le_weak. apply leb_complete_conv. assumption. Qed. -Lemma Nleb_double_mono : - forall a b, - Nleb a b = true -> Nleb (Ndouble a) (Ndouble b) = true. +Lemma Nleb_double_mono a b : + Nleb a b = true -> Nleb (N.double a) (N.double b) = true. Proof. - unfold Nleb in |- *. intros. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. apply leb_correct. - simpl in |- *. apply plus_le_compat. apply leb_complete. assumption. - apply plus_le_compat. apply leb_complete. assumption. - apply le_n. + unfold Nleb. intros. rewrite !N2Nat.inj_double. apply leb_correct. + apply mult_le_compat_l. now apply leb_complete. Qed. -Lemma Nleb_double_plus_one_mono : - forall a b, - Nleb a b = true -> - Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = true. +Lemma Nleb_double_plus_one_mono a b : + Nleb a b = true -> + Nleb (N.succ_double a) (N.succ_double b) = true. Proof. - unfold Nleb in |- *. intros. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one. - apply leb_correct. apply le_n_S. simpl in |- *. apply plus_le_compat. apply leb_complete. - assumption. - apply plus_le_compat. apply leb_complete. assumption. - apply le_n. + unfold Nleb. intros. rewrite !N2Nat.inj_succ_double. apply leb_correct. + apply le_n_S, mult_le_compat_l. now apply leb_complete. Qed. -Lemma Nleb_double_mono_conv : - forall a b, - Nleb (Ndouble a) (Ndouble b) = true -> Nleb a b = true. +Lemma Nleb_double_mono_conv a b : + Nleb (N.double a) (N.double b) = true -> Nleb a b = true. Proof. - unfold Nleb in |- *. intros a b. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. intro. - apply leb_correct. apply (mult_S_le_reg_l 1). apply leb_complete. assumption. + unfold Nleb. rewrite !N2Nat.inj_double. intro. apply leb_correct. + apply (mult_S_le_reg_l 1). now apply leb_complete. Qed. -Lemma Nleb_double_plus_one_mono_conv : - forall a b, - Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = true -> +Lemma Nleb_double_plus_one_mono_conv a b : + Nleb (N.succ_double a) (N.succ_double b) = true -> Nleb a b = true. Proof. - unfold Nleb in |- *. intros a b. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one. - intro. apply leb_correct. apply (mult_S_le_reg_l 1). apply le_S_n. apply leb_complete. - assumption. + unfold Nleb. rewrite !N2Nat.inj_succ_double. intro. apply leb_correct. + apply (mult_S_le_reg_l 1). apply le_S_n. now apply leb_complete. Qed. -Lemma Nltb_double_mono : - forall a b, - Nleb a b = false -> Nleb (Ndouble a) (Ndouble b) = false. +Lemma Nltb_double_mono a b : + Nleb a b = false -> Nleb (N.double a) (N.double b) = false. Proof. - intros. elim (sumbool_of_bool (Nleb (Ndouble a) (Ndouble b))). intro H0. + intros. elim (sumbool_of_bool (Nleb (N.double a) (N.double b))). intro H0. rewrite (Nleb_double_mono_conv _ _ H0) in H. discriminate H. trivial. Qed. -Lemma Nltb_double_plus_one_mono : - forall a b, - Nleb a b = false -> - Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = false. +Lemma Nltb_double_plus_one_mono a b : + Nleb a b = false -> + Nleb (N.succ_double a) (N.succ_double b) = false. Proof. - intros. elim (sumbool_of_bool (Nleb (Ndouble_plus_one a) (Ndouble_plus_one b))). intro H0. + intros. elim (sumbool_of_bool (Nleb (N.succ_double a) (N.succ_double b))). + intro H0. rewrite (Nleb_double_plus_one_mono_conv _ _ H0) in H. discriminate H. trivial. Qed. -Lemma Nltb_double_mono_conv : - forall a b, - Nleb (Ndouble a) (Ndouble b) = false -> Nleb a b = false. +Lemma Nltb_double_mono_conv a b : + Nleb (N.double a) (N.double b) = false -> Nleb a b = false. Proof. - intros. elim (sumbool_of_bool (Nleb a b)). intro H0. rewrite (Nleb_double_mono _ _ H0) in H. - discriminate H. + intros. elim (sumbool_of_bool (Nleb a b)). intro H0. + rewrite (Nleb_double_mono _ _ H0) in H. discriminate H. trivial. Qed. -Lemma Nltb_double_plus_one_mono_conv : - forall a b, - Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = false -> +Lemma Nltb_double_plus_one_mono_conv a b : + Nleb (N.succ_double a) (N.succ_double b) = false -> Nleb a b = false. Proof. intros. elim (sumbool_of_bool (Nleb a b)). intro H0. @@ -331,110 +254,52 @@ Proof. trivial. Qed. -(* Nleb and Ncompare *) +(* Nleb and N.compare *) -(* NB: No need to prove that Nleb a b = true <-> Ncompare a b <> Gt, +(* NB: No need to prove that Nleb a b = true <-> N.compare a b <> Gt, this statement is in fact Nleb_Nle! *) -Lemma Nltb_Ncompare : forall a b, - Nleb a b = false <-> Ncompare a b = Gt. +Lemma Nltb_Ncompare a b : Nleb a b = false <-> N.compare a b = Gt. Proof. - intros. - assert (IFF : forall x:bool, x = false <-> ~ x = true) - by (destruct x; intuition). - rewrite IFF, Nleb_Nle; unfold Nle. - destruct (Ncompare a b); split; intro H; auto; - elim H; discriminate. + now rewrite N.compare_nle_iff, <- Nleb_Nle, not_true_iff_false. Qed. -Lemma Ncompare_Gt_Nltb : forall a b, - Ncompare a b = Gt -> Nleb a b = false. -Proof. - intros; apply <- Nltb_Ncompare; auto. -Qed. +Lemma Ncompare_Gt_Nltb a b : N.compare a b = Gt -> Nleb a b = false. +Proof. apply <- Nltb_Ncompare; auto. Qed. -Lemma Ncompare_Lt_Nltb : forall a b, - Ncompare a b = Lt -> Nleb b a = false. +Lemma Ncompare_Lt_Nltb a b : N.compare a b = Lt -> Nleb b a = false. Proof. - intros a b H. - rewrite Nltb_Ncompare, <- Ncompare_antisym, H; auto. + intros H. rewrite Nltb_Ncompare, N.compare_antisym, H; auto. Qed. -(* An alternate [min] function over [N] *) +(* Old results about [N.min] *) -Definition Nmin' (a b:N) := if Nleb a b then a else b. +Notation Nmin_choice := N.min_dec (compat "8.3"). -Lemma Nmin_Nmin' : forall a b, Nmin a b = Nmin' a b. -Proof. - unfold Nmin, Nmin', Nleb; intros. - rewrite nat_of_Ncompare. - generalize (leb_compare (nat_of_N a) (nat_of_N b)); - destruct (nat_compare (nat_of_N a) (nat_of_N b)); - destruct (leb (nat_of_N a) (nat_of_N b)); intuition. - lapply H1; intros; discriminate. - lapply H1; intros; discriminate. -Qed. +Lemma Nmin_le_1 a b : Nleb (N.min a b) a = true. +Proof. rewrite Nleb_Nle. apply N.le_min_l. Qed. -Lemma Nmin_choice : forall a b, {Nmin a b = a} + {Nmin a b = b}. -Proof. - unfold Nmin in *; intros; destruct (Ncompare a b); auto. -Qed. +Lemma Nmin_le_2 a b : Nleb (N.min a b) b = true. +Proof. rewrite Nleb_Nle. apply N.le_min_r. Qed. -Lemma Nmin_le_1 : forall a b, Nleb (Nmin a b) a = true. -Proof. - intros; rewrite Nmin_Nmin'. - unfold Nmin'; elim (sumbool_of_bool (Nleb a b)). intro H. rewrite H. - apply Nleb_refl. - intro H. rewrite H. apply Nltb_leb_weak. assumption. -Qed. +Lemma Nmin_le_3 a b c : Nleb a (N.min b c) = true -> Nleb a b = true. +Proof. rewrite !Nleb_Nle. apply N.min_glb_l. Qed. -Lemma Nmin_le_2 : forall a b, Nleb (Nmin a b) b = true. -Proof. - intros; rewrite Nmin_Nmin'. - unfold Nmin'; elim (sumbool_of_bool (Nleb a b)). intro H. rewrite H. assumption. - intro H. rewrite H. apply Nleb_refl. -Qed. +Lemma Nmin_le_4 a b c : Nleb a (N.min b c) = true -> Nleb a c = true. +Proof. rewrite !Nleb_Nle. apply N.min_glb_r. Qed. -Lemma Nmin_le_3 : - forall a b c, Nleb a (Nmin b c) = true -> Nleb a b = true. -Proof. - intros; rewrite Nmin_Nmin' in *. - unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. - assumption. - intro H0. rewrite H0 in H. apply Nltb_leb_weak. apply Nleb_ltb_trans with (b := c); assumption. -Qed. +Lemma Nmin_le_5 a b c : + Nleb a b = true -> Nleb a c = true -> Nleb a (N.min b c) = true. +Proof. rewrite !Nleb_Nle. apply N.min_glb. Qed. -Lemma Nmin_le_4 : - forall a b c, Nleb a (Nmin b c) = true -> Nleb a c = true. +Lemma Nmin_lt_3 a b c : Nleb (N.min b c) a = false -> Nleb b a = false. Proof. - intros; rewrite Nmin_Nmin' in *. - unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. - apply Nleb_trans with (b := b); assumption. - intro H0. rewrite H0 in H. assumption. -Qed. - -Lemma Nmin_le_5 : - forall a b c, - Nleb a b = true -> Nleb a c = true -> Nleb a (Nmin b c) = true. -Proof. - intros. elim (Nmin_choice b c). intro H1. rewrite H1. assumption. - intro H1. rewrite H1. assumption. -Qed. - -Lemma Nmin_lt_3 : - forall a b c, Nleb (Nmin b c) a = false -> Nleb b a = false. -Proof. - intros; rewrite Nmin_Nmin' in *. - unfold Nmin' in *. intros. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. - assumption. - intro H0. rewrite H0 in H. apply Nltb_trans with (b := c); assumption. + rewrite <- !not_true_iff_false, !Nleb_Nle. + rewrite N.min_le_iff; auto. Qed. -Lemma Nmin_lt_4 : - forall a b c, Nleb (Nmin b c) a = false -> Nleb c a = false. +Lemma Nmin_lt_4 a b c : Nleb (N.min b c) a = false -> Nleb c a = false. Proof. - intros; rewrite Nmin_Nmin' in *. - unfold Nmin' in *. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. - apply Nltb_leb_trans with (b := b); assumption. - intro H0. rewrite H0 in H. assumption. + rewrite <- !not_true_iff_false, !Nleb_Nle. + rewrite N.min_le_iff; auto. Qed. diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index b0c33595..4ea8e1d4 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -15,41 +15,41 @@ Local Open Scope N_scope. (** Compatibility names for some bitwise operations *) -Notation Pxor := Pos.lxor (only parsing). -Notation Nxor := N.lxor (only parsing). -Notation Pbit := Pos.testbit_nat (only parsing). -Notation Nbit := N.testbit_nat (only parsing). +Notation Pxor := Pos.lxor (compat "8.3"). +Notation Nxor := N.lxor (compat "8.3"). +Notation Pbit := Pos.testbit_nat (compat "8.3"). +Notation Nbit := N.testbit_nat (compat "8.3"). -Notation Nxor_eq := N.lxor_eq (only parsing). -Notation Nxor_comm := N.lxor_comm (only parsing). -Notation Nxor_assoc := N.lxor_assoc (only parsing). -Notation Nxor_neutral_left := N.lxor_0_l (only parsing). -Notation Nxor_neutral_right := N.lxor_0_r (only parsing). -Notation Nxor_nilpotent := N.lxor_nilpotent (only parsing). +Notation Nxor_eq := N.lxor_eq (compat "8.3"). +Notation Nxor_comm := N.lxor_comm (compat "8.3"). +Notation Nxor_assoc := N.lxor_assoc (compat "8.3"). +Notation Nxor_neutral_left := N.lxor_0_l (compat "8.3"). +Notation Nxor_neutral_right := N.lxor_0_r (compat "8.3"). +Notation Nxor_nilpotent := N.lxor_nilpotent (compat "8.3"). (** Equivalence of bit-testing functions, either with index in [N] or in [nat]. *) Lemma Ptestbit_Pbit : - forall p n, Pos.testbit p (N.of_nat n) = Pbit p n. + forall p n, Pos.testbit p (N.of_nat n) = Pos.testbit_nat p n. Proof. induction p as [p IH|p IH| ]; intros [|n]; simpl; trivial; - rewrite <- IH; f_equal; rewrite (pred_Sn n) at 2; now rewrite N_of_pred. + rewrite <- IH; f_equal; rewrite (pred_Sn n) at 2; now rewrite Nat2N.inj_pred. Qed. -Lemma Ntestbit_Nbit : forall a n, N.testbit a (N.of_nat n) = Nbit a n. +Lemma Ntestbit_Nbit : forall a n, N.testbit a (N.of_nat n) = N.testbit_nat a n. Proof. destruct a. trivial. apply Ptestbit_Pbit. Qed. Lemma Pbit_Ptestbit : - forall p n, Pbit p (N.to_nat n) = Pos.testbit p n. + forall p n, Pos.testbit_nat p (N.to_nat n) = Pos.testbit p n. Proof. intros; now rewrite <- Ptestbit_Pbit, N2Nat.id. Qed. Lemma Nbit_Ntestbit : - forall a n, Nbit a (N.to_nat n) = N.testbit a n. + forall a n, N.testbit_nat a (N.to_nat n) = N.testbit a n. Proof. destruct a. trivial. apply Pbit_Ptestbit. Qed. @@ -73,7 +73,7 @@ Lemma Nshiftr_nat_equiv : Proof. intros a [|n]; simpl. unfold N.shiftr_nat. trivial. - symmetry. apply iter_nat_of_P. + symmetry. apply Pos2Nat.inj_iter. Qed. Lemma Nshiftr_equiv_nat : @@ -99,7 +99,7 @@ Qed. (** Correctness proofs for shifts, nat version *) Lemma Nshiftr_nat_spec : forall a n m, - Nbit (N.shiftr_nat a n) m = Nbit a (m+n). + N.testbit_nat (N.shiftr_nat a n) m = N.testbit_nat a (m+n). Proof. induction n; intros m. now rewrite <- plus_n_O. @@ -108,7 +108,7 @@ Proof. Qed. Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat -> - Nbit (N.shiftl_nat a n) m = Nbit a (m-n). + N.testbit_nat (N.shiftl_nat a n) m = N.testbit_nat a (m-n). Proof. induction n; intros m H. now rewrite <- minus_n_O. @@ -118,7 +118,7 @@ Proof. Qed. Lemma Nshiftl_nat_spec_low : forall a n m, (m<n)%nat -> - Nbit (N.shiftl_nat a n) m = false. + N.testbit_nat (N.shiftl_nat a n) m = false. Proof. induction n; intros m H. inversion H. rewrite Nshiftl_nat_S. @@ -151,52 +151,52 @@ Proof. rewrite 2 Pshiftl_nat_S. now f_equal. Qed. -(** Semantics of bitwise operations with respect to [Nbit] *) +(** Semantics of bitwise operations with respect to [N.testbit_nat] *) Lemma Pxor_semantics p p' n : - Nbit (Pos.lxor p p') n = xorb (Pbit p n) (Pbit p' n). + N.testbit_nat (Pos.lxor p p') n = xorb (Pos.testbit_nat p n) (Pos.testbit_nat p' n). Proof. rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_lxor_spec. Qed. Lemma Nxor_semantics a a' n : - Nbit (N.lxor a a') n = xorb (Nbit a n) (Nbit a' n). + N.testbit_nat (N.lxor a a') n = xorb (N.testbit_nat a n) (N.testbit_nat a' n). Proof. rewrite <- !Ntestbit_Nbit. apply N.lxor_spec. Qed. Lemma Por_semantics p p' n : - Pbit (Pos.lor p p') n = (Pbit p n) || (Pbit p' n). + Pos.testbit_nat (Pos.lor p p') n = (Pos.testbit_nat p n) || (Pos.testbit_nat p' n). Proof. rewrite <- !Ptestbit_Pbit. apply N.pos_lor_spec. Qed. Lemma Nor_semantics a a' n : - Nbit (N.lor a a') n = (Nbit a n) || (Nbit a' n). + N.testbit_nat (N.lor a a') n = (N.testbit_nat a n) || (N.testbit_nat a' n). Proof. rewrite <- !Ntestbit_Nbit. apply N.lor_spec. Qed. Lemma Pand_semantics p p' n : - Nbit (Pos.land p p') n = (Pbit p n) && (Pbit p' n). + N.testbit_nat (Pos.land p p') n = (Pos.testbit_nat p n) && (Pos.testbit_nat p' n). Proof. rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_land_spec. Qed. Lemma Nand_semantics a a' n : - Nbit (N.land a a') n = (Nbit a n) && (Nbit a' n). + N.testbit_nat (N.land a a') n = (N.testbit_nat a n) && (N.testbit_nat a' n). Proof. rewrite <- !Ntestbit_Nbit. apply N.land_spec. Qed. Lemma Pdiff_semantics p p' n : - Nbit (Pos.ldiff p p') n = (Pbit p n) && negb (Pbit p' n). + N.testbit_nat (Pos.ldiff p p') n = (Pos.testbit_nat p n) && negb (Pos.testbit_nat p' n). Proof. rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_ldiff_spec. Qed. Lemma Ndiff_semantics a a' n : - Nbit (N.ldiff a a') n = (Nbit a n) && negb (Nbit a' n). + N.testbit_nat (N.ldiff a a') n = (N.testbit_nat a n) && negb (N.testbit_nat a' n). Proof. rewrite <- !Ntestbit_Nbit. apply N.ldiff_spec. Qed. @@ -213,13 +213,13 @@ Local Infix "==" := eqf (at level 70, no associativity). Local Notation Step H := (fun n => H (S n)). -Lemma Pbit_faithful_0 : forall p, ~(Pbit p == (fun _ => false)). +Lemma Pbit_faithful_0 : forall p, ~(Pos.testbit_nat p == (fun _ => false)). Proof. induction p as [p IHp|p IHp| ]; intros H; try discriminate (H O). apply (IHp (Step H)). Qed. -Lemma Pbit_faithful : forall p p', Pbit p == Pbit p' -> p = p'. +Lemma Pbit_faithful : forall p p', Pos.testbit_nat p == Pos.testbit_nat p' -> p = p'. Proof. induction p as [p IHp|p IHp| ]; intros [p'|p'|] H; trivial; try discriminate (H O). @@ -229,7 +229,7 @@ Proof. symmetry in H. destruct (Pbit_faithful_0 _ (Step H)). Qed. -Lemma Nbit_faithful : forall n n', Nbit n == Nbit n' -> n = n'. +Lemma Nbit_faithful : forall n n', N.testbit_nat n == N.testbit_nat n' -> n = n'. Proof. intros [|p] [|p'] H; trivial. symmetry in H. destruct (Pbit_faithful_0 _ H). @@ -237,7 +237,7 @@ Proof. f_equal. apply Pbit_faithful, H. Qed. -Lemma Nbit_faithful_iff : forall n n', Nbit n == Nbit n' <-> n = n'. +Lemma Nbit_faithful_iff : forall n n', N.testbit_nat n == N.testbit_nat n' <-> n = n'. Proof. split. apply Nbit_faithful. intros; now subst. Qed. @@ -247,30 +247,30 @@ Local Close Scope N_scope. (** Checking whether a number is odd, i.e. if its lower bit is set. *) -Notation Nbit0 := N.odd (only parsing). +Notation Nbit0 := N.odd (compat "8.3"). -Definition Nodd (n:N) := Nbit0 n = true. -Definition Neven (n:N) := Nbit0 n = false. +Definition Nodd (n:N) := N.odd n = true. +Definition Neven (n:N) := N.odd n = false. -Lemma Nbit0_correct : forall n:N, Nbit n 0 = Nbit0 n. +Lemma Nbit0_correct : forall n:N, N.testbit_nat n 0 = N.odd n. Proof. destruct n; trivial. destruct p; trivial. Qed. -Lemma Ndouble_bit0 : forall n:N, Nbit0 (Ndouble n) = false. +Lemma Ndouble_bit0 : forall n:N, N.odd (N.double n) = false. Proof. destruct n; trivial. Qed. Lemma Ndouble_plus_one_bit0 : - forall n:N, Nbit0 (Ndouble_plus_one n) = true. + forall n:N, N.odd (N.succ_double n) = true. Proof. destruct n; trivial. Qed. Lemma Ndiv2_double : - forall n:N, Neven n -> Ndouble (Ndiv2 n) = n. + forall n:N, Neven n -> N.double (N.div2 n) = n. Proof. destruct n. trivial. destruct p. intro H. discriminate H. intros. reflexivity. @@ -278,7 +278,7 @@ Proof. Qed. Lemma Ndiv2_double_plus_one : - forall n:N, Nodd n -> Ndouble_plus_one (Ndiv2 n) = n. + forall n:N, Nodd n -> N.succ_double (N.div2 n) = n. Proof. destruct n. intro. discriminate H. destruct p. intros. reflexivity. @@ -287,31 +287,31 @@ Proof. Qed. Lemma Ndiv2_correct : - forall (a:N) (n:nat), Nbit (Ndiv2 a) n = Nbit a (S n). + forall (a:N) (n:nat), N.testbit_nat (N.div2 a) n = N.testbit_nat a (S n). Proof. destruct a; trivial. destruct p; trivial. Qed. Lemma Nxor_bit0 : - forall a a':N, Nbit0 (Nxor a a') = xorb (Nbit0 a) (Nbit0 a'). + forall a a':N, N.odd (N.lxor a a') = xorb (N.odd a) (N.odd a'). Proof. intros. rewrite <- Nbit0_correct, (Nxor_semantics a a' O). rewrite Nbit0_correct, Nbit0_correct. reflexivity. Qed. Lemma Nxor_div2 : - forall a a':N, Ndiv2 (Nxor a a') = Nxor (Ndiv2 a) (Ndiv2 a'). + forall a a':N, N.div2 (N.lxor a a') = N.lxor (N.div2 a) (N.div2 a'). Proof. intros. apply Nbit_faithful. unfold eqf. intro. - rewrite (Nxor_semantics (Ndiv2 a) (Ndiv2 a') n), Ndiv2_correct, (Nxor_semantics a a' (S n)). + rewrite (Nxor_semantics (N.div2 a) (N.div2 a') n), Ndiv2_correct, (Nxor_semantics a a' (S n)). rewrite 2! Ndiv2_correct. reflexivity. Qed. Lemma Nneg_bit0 : forall a a':N, - Nbit0 (Nxor a a') = true -> Nbit0 a = negb (Nbit0 a'). + N.odd (N.lxor a a') = true -> N.odd a = negb (N.odd a'). Proof. intros. rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, @@ -320,24 +320,24 @@ Proof. Qed. Lemma Nneg_bit0_1 : - forall a a':N, Nxor a a' = Npos 1 -> Nbit0 a = negb (Nbit0 a'). + forall a a':N, N.lxor a a' = Npos 1 -> N.odd a = negb (N.odd a'). Proof. intros. apply Nneg_bit0. rewrite H. reflexivity. Qed. Lemma Nneg_bit0_2 : forall (a a':N) (p:positive), - Nxor a a' = Npos (xI p) -> Nbit0 a = negb (Nbit0 a'). + N.lxor a a' = Npos (xI p) -> N.odd a = negb (N.odd a'). Proof. intros. apply Nneg_bit0. rewrite H. reflexivity. Qed. Lemma Nsame_bit0 : forall (a a':N) (p:positive), - Nxor a a' = Npos (xO p) -> Nbit0 a = Nbit0 a'. + N.lxor a a' = Npos (xO p) -> N.odd a = N.odd a'. Proof. - intros. rewrite <- (xorb_false (Nbit0 a)). - assert (H0: Nbit0 (Npos (xO p)) = false) by reflexivity. + intros. rewrite <- (xorb_false (N.odd a)). + assert (H0: N.odd (Npos (xO p)) = false) by reflexivity. rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb. reflexivity. Qed. @@ -346,77 +346,77 @@ Qed. Fixpoint Nless_aux (a a':N) (p:positive) : bool := match p with - | xO p' => Nless_aux (Ndiv2 a) (Ndiv2 a') p' - | _ => andb (negb (Nbit0 a)) (Nbit0 a') + | xO p' => Nless_aux (N.div2 a) (N.div2 a') p' + | _ => andb (negb (N.odd a)) (N.odd a') end. Definition Nless (a a':N) := - match Nxor a a' with + match N.lxor a a' with | N0 => false | Npos p => Nless_aux a a' p end. Lemma Nbit0_less : forall a a', - Nbit0 a = false -> Nbit0 a' = true -> Nless a a' = true. + N.odd a = false -> N.odd a' = true -> Nless a a' = true. Proof. - intros. destruct (Ndiscr (Nxor a a')) as [(p,H2)|H1]. unfold Nless. + intros. destruct (N.discr (N.lxor a a')) as [(p,H2)|H1]. unfold Nless. rewrite H2. destruct p. simpl. rewrite H, H0. reflexivity. - assert (H1: Nbit0 (Nxor a a') = false) by (rewrite H2; reflexivity). + assert (H1: N.odd (N.lxor a a') = false) by (rewrite H2; reflexivity). rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1. simpl. rewrite H, H0. reflexivity. - assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity). + assert (H2: N.odd (N.lxor a a') = false) by (rewrite H1; reflexivity). rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2. Qed. Lemma Nbit0_gt : forall a a', - Nbit0 a = true -> Nbit0 a' = false -> Nless a a' = false. + N.odd a = true -> N.odd a' = false -> Nless a a' = false. Proof. - intros. destruct (Ndiscr (Nxor a a')) as [(p,H2)|H1]. unfold Nless. + intros. destruct (N.discr (N.lxor a a')) as [(p,H2)|H1]. unfold Nless. rewrite H2. destruct p. simpl. rewrite H, H0. reflexivity. - assert (H1: Nbit0 (Nxor a a') = false) by (rewrite H2; reflexivity). + assert (H1: N.odd (N.lxor a a') = false) by (rewrite H2; reflexivity). rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1. simpl. rewrite H, H0. reflexivity. - assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity). + assert (H2: N.odd (N.lxor a a') = false) by (rewrite H1; reflexivity). rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2. Qed. Lemma Nless_not_refl : forall a, Nless a a = false. Proof. - intro. unfold Nless. rewrite (Nxor_nilpotent a). reflexivity. + intro. unfold Nless. rewrite (N.lxor_nilpotent a). reflexivity. Qed. Lemma Nless_def_1 : - forall a a', Nless (Ndouble a) (Ndouble a') = Nless a a'. + forall a a', Nless (N.double a) (N.double a') = Nless a a'. Proof. destruct a; destruct a'. reflexivity. trivial. unfold Nless. simpl. destruct p; trivial. - unfold Nless. simpl. destruct (Pxor p p0). reflexivity. + unfold Nless. simpl. destruct (Pos.lxor p p0). reflexivity. trivial. Qed. Lemma Nless_def_2 : forall a a', - Nless (Ndouble_plus_one a) (Ndouble_plus_one a') = Nless a a'. + Nless (N.succ_double a) (N.succ_double a') = Nless a a'. Proof. destruct a; destruct a'. reflexivity. trivial. unfold Nless. simpl. destruct p; trivial. - unfold Nless. simpl. destruct (Pxor p p0). reflexivity. + unfold Nless. simpl. destruct (Pos.lxor p p0). reflexivity. trivial. Qed. Lemma Nless_def_3 : - forall a a', Nless (Ndouble a) (Ndouble_plus_one a') = true. + forall a a', Nless (N.double a) (N.succ_double a') = true. Proof. intros. apply Nbit0_less. apply Ndouble_bit0. apply Ndouble_plus_one_bit0. Qed. Lemma Nless_def_4 : - forall a a', Nless (Ndouble_plus_one a) (Ndouble a') = false. + forall a a', Nless (N.succ_double a) (N.double a') = false. Proof. intros. apply Nbit0_gt. apply Ndouble_plus_one_bit0. apply Ndouble_bit0. @@ -425,7 +425,7 @@ Qed. Lemma Nless_z : forall a, Nless a N0 = false. Proof. induction a. reflexivity. - unfold Nless. rewrite (Nxor_neutral_right (Npos p)). induction p; trivial. + unfold Nless. rewrite (N.lxor_0_r (Npos p)). induction p; trivial. Qed. Lemma N0_less_1 : @@ -445,26 +445,26 @@ Lemma Nless_trans : forall a a' a'', Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true. Proof. - induction a as [|a IHa|a IHa] using N_ind_double; intros a' a'' H H0. + induction a as [|a IHa|a IHa] using N.binary_ind; intros a' a'' H H0. case_eq (Nless N0 a'') ; intros Heqn. trivial. rewrite (N0_less_2 a'' Heqn), (Nless_z a') in H0. discriminate H0. - induction a' as [|a' _|a' _] using N_ind_double. - rewrite (Nless_z (Ndouble a)) in H. discriminate H. + induction a' as [|a' _|a' _] using N.binary_ind. + rewrite (Nless_z (N.double a)) in H. discriminate H. rewrite (Nless_def_1 a a') in H. - induction a'' using N_ind_double. - rewrite (Nless_z (Ndouble a')) in H0. discriminate H0. + induction a'' using N.binary_ind. + rewrite (Nless_z (N.double a')) in H0. discriminate H0. rewrite (Nless_def_1 a' a'') in H0. rewrite (Nless_def_1 a a''). exact (IHa _ _ H H0). apply Nless_def_3. - induction a'' as [|a'' _|a'' _] using N_ind_double. - rewrite (Nless_z (Ndouble_plus_one a')) in H0. discriminate H0. + induction a'' as [|a'' _|a'' _] using N.binary_ind. + rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0. rewrite (Nless_def_4 a' a'') in H0. discriminate H0. apply Nless_def_3. - induction a' as [|a' _|a' _] using N_ind_double. - rewrite (Nless_z (Ndouble_plus_one a)) in H. discriminate H. + induction a' as [|a' _|a' _] using N.binary_ind. + rewrite (Nless_z (N.succ_double a)) in H. discriminate H. rewrite (Nless_def_4 a a') in H. discriminate H. - induction a'' using N_ind_double. - rewrite (Nless_z (Ndouble_plus_one a')) in H0. discriminate H0. + induction a'' using N.binary_ind. + rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0. rewrite (Nless_def_4 a' a'') in H0. discriminate H0. rewrite (Nless_def_2 a' a'') in H0. rewrite (Nless_def_2 a a') in H. rewrite (Nless_def_2 a a''). exact (IHa _ _ H H0). @@ -473,17 +473,17 @@ Qed. Lemma Nless_total : forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}. Proof. - induction a using N_rec_double; intro a'. + induction a using N.binary_rec; intro a'. case_eq (Nless N0 a') ; intros Heqb. left. left. auto. right. rewrite (N0_less_2 a' Heqb). reflexivity. - induction a' as [|a' _|a' _] using N_rec_double. - case_eq (Nless N0 (Ndouble a)) ; intros Heqb. left. right. auto. + induction a' as [|a' _|a' _] using N.binary_rec. + case_eq (Nless N0 (N.double a)) ; intros Heqb. left. right. auto. right. exact (N0_less_2 _ Heqb). rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->]. left. assumption. right. reflexivity. left. left. apply Nless_def_3. - induction a' as [|a' _|a' _] using N_rec_double. + induction a' as [|a' _|a' _] using N.binary_rec. left. right. destruct a; reflexivity. left. right. apply Nless_def_3. rewrite 2!Nless_def_2. destruct (IHa a') as [ | ->]. @@ -493,19 +493,19 @@ Qed. (** Number of digits in a number *) -Notation Nsize := N.size_nat (only parsing). +Notation Nsize := N.size_nat (compat "8.3"). (** conversions between N and bit vectors. *) -Fixpoint P2Bv (p:positive) : Bvector (Psize p) := - match p return Bvector (Psize p) with +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 (Psize p) (P2Bv p) - | xI p => Bcons true (Psize p) (P2Bv p) + | xO p => Bcons false (Pos.size_nat p) (P2Bv p) + | xI p => Bcons true (Pos.size_nat p) (P2Bv p) end. -Definition N2Bv (n:N) : Bvector (Nsize n) := - match n as n0 return Bvector (Nsize n0) with +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. @@ -513,8 +513,8 @@ Definition N2Bv (n:N) : Bvector (Nsize n) := Fixpoint Bv2N (n:nat)(bv:Bvector n) : N := match bv with | Vector.nil => N0 - | Vector.cons false n bv => Ndouble (Bv2N n bv) - | Vector.cons true n bv => Ndouble_plus_one (Bv2N n bv) + | Vector.cons false n bv => N.double (Bv2N n bv) + | Vector.cons true n bv => N.succ_double (Bv2N n bv) end. Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n. @@ -528,7 +528,7 @@ Qed. bit vector has some zeros on its right, they will disappear during the return [Bv2N] translation: *) -Lemma Bv2N_Nsize : forall n (bv:Bvector n), Nsize (Bv2N n bv) <= n. +Lemma Bv2N_Nsize : forall n (bv:Bvector n), N.size_nat (Bv2N n bv) <= n. Proof. induction bv; intros. auto. @@ -543,7 +543,7 @@ Qed. Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)), Bsign _ bv = true <-> - Nsize (Bv2N _ bv) = (S n). + N.size_nat (Bv2N _ bv) = (S n). Proof. apply Vector.rectS ; intros ; simpl. destruct a ; compute ; split ; intros x ; now inversion x. @@ -567,7 +567,7 @@ Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n := (** The first [N2Bv] is then a special case of [N2Bv_gen] *) -Lemma N2Bv_N2Bv_gen : forall (a:N), N2Bv a = N2Bv_gen (Nsize a) a. +Lemma N2Bv_N2Bv_gen : forall (a:N), N2Bv a = N2Bv_gen (N.size_nat a) a. Proof. destruct a; simpl. auto. @@ -578,7 +578,7 @@ Qed. [a] plus some zeros. *) Lemma N2Bv_N2Bv_gen_above : forall (a:N)(k:nat), - N2Bv_gen (Nsize a + k) a = Vector.append (N2Bv a) (Bvect_false k). + N2Bv_gen (N.size_nat a + k) a = Vector.append (N2Bv a) (Bvect_false k). Proof. destruct a; simpl. destruct k; simpl; auto. @@ -603,7 +603,7 @@ Qed. (** accessing some precise bits. *) Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)), - Nbit0 (Bv2N _ bv) = Blow _ bv. + N.odd (Bv2N _ bv) = Blow _ bv. Proof. apply Vector.caseS. intros. @@ -616,7 +616,7 @@ Qed. Notation Bnth := (@Vector.nth_order bool). Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n), - Bnth bv H = Nbit (Bv2N _ bv) p. + Bnth bv H = N.testbit_nat (Bv2N _ bv) p. Proof. induction bv; intros. inversion H. @@ -626,7 +626,7 @@ destruct p ; simpl. simpl in * ; destruct (Bv2N n bv); destruct h; simpl in *; auto. Qed. -Lemma Nbit_Nsize : forall n p, Nsize n <= p -> Nbit n p = false. +Lemma Nbit_Nsize : forall n p, N.size_nat n <= p -> N.testbit_nat n p = false. Proof. destruct n as [|n]. simpl; auto. @@ -635,7 +635,8 @@ inversion H. inversion H. Qed. -Lemma Nbit_Bth: forall n p (H:p < Nsize n), Nbit n p = Bnth (N2Bv n) H. +Lemma Nbit_Bth: forall n p (H:p < N.size_nat n), + N.testbit_nat n p = Bnth (N2Bv n) H. Proof. destruct n as [|n]. inversion H. @@ -646,7 +647,7 @@ Qed. (** Binary bitwise operations are the same in the two worlds. *) Lemma Nxor_BVxor : forall n (bv bv' : Bvector n), - Bv2N _ (BVxor _ bv bv') = Nxor (Bv2N _ bv) (Bv2N _ bv'). + Bv2N _ (BVxor _ bv bv') = N.lxor (Bv2N _ bv) (Bv2N _ bv'). Proof. apply Vector.rect2 ; intros. now simpl. diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v index 22adc505..ce4f7663 100644 --- a/theories/NArith/Ndist.v +++ b/theories/NArith/Ndist.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -33,12 +33,12 @@ Definition Nplength (a:N) := Lemma Nplength_infty : forall a:N, Nplength a = infty -> a = N0. Proof. simple induction a; trivial. - unfold Nplength in |- *; intros; discriminate H. + unfold Nplength; intros; discriminate H. Qed. Lemma Nplength_zeros : forall (a:N) (n:nat), - Nplength a = ni n -> forall k:nat, k < n -> Nbit a k = false. + Nplength a = ni n -> forall k:nat, k < n -> N.testbit_nat a k = false. Proof. simple induction a; trivial. simple induction p. simple induction n. intros. inversion H1. @@ -46,33 +46,33 @@ Proof. intros. simpl in H1. discriminate H1. simple induction k. trivial. generalize H0. case n. intros. inversion H3. - intros. simpl in |- *. unfold Nbit in H. apply (H n0). simpl in H1. inversion H1. reflexivity. + intros. simpl. unfold N.testbit_nat in H. apply (H n0). simpl in H1. inversion H1. reflexivity. exact (lt_S_n n1 n0 H3). - simpl in |- *. intros n H. inversion H. intros. inversion H0. + simpl. intros n H. inversion H. intros. inversion H0. Qed. Lemma Nplength_one : - forall (a:N) (n:nat), Nplength a = ni n -> Nbit a n = true. + forall (a:N) (n:nat), Nplength a = ni n -> N.testbit_nat a n = true. Proof. simple induction a. intros. inversion H. simple induction p. intros. simpl in H0. inversion H0. reflexivity. - intros. simpl in H0. inversion H0. simpl in |- *. unfold Nbit in H. apply H. reflexivity. + intros. simpl in H0. inversion H0. simpl. unfold N.testbit_nat in H. apply H. reflexivity. intros. simpl in H. inversion H. reflexivity. Qed. Lemma Nplength_first_one : forall (a:N) (n:nat), - (forall k:nat, k < n -> Nbit a k = false) -> - Nbit a n = true -> Nplength a = ni n. + (forall k:nat, k < n -> N.testbit_nat a k = false) -> + N.testbit_nat a n = true -> Nplength a = ni n. Proof. simple induction a. intros. simpl in H0. discriminate H0. simple induction p. intros. generalize H0. case n. intros. reflexivity. - intros. absurd (Nbit (Npos (xI p0)) 0 = false). trivial with bool. + intros. absurd (N.testbit_nat (Npos (xI p0)) 0 = false). trivial with bool. auto with bool arith. intros. generalize H0 H1. case n. intros. simpl in H3. discriminate H3. - intros. simpl in |- *. unfold Nplength in H. + intros. simpl. unfold Nplength in H. cut (ni (Pplength p0) = ni n0). intro. inversion H4. reflexivity. - apply H. intros. change (Nbit (Npos (xO p0)) (S k) = false) in |- *. apply H2. apply lt_n_S. exact H4. + apply H. intros. change (N.testbit_nat (Npos (xO p0)) (S k) = false). apply H2. apply lt_n_S. exact H4. exact H3. intro. case n. trivial. intros. simpl in H0. discriminate H0. @@ -90,10 +90,10 @@ Definition ni_min (d d':natinf) := Lemma ni_min_idemp : forall d:natinf, ni_min d d = d. Proof. simple induction d; trivial. - unfold ni_min in |- *. + unfold ni_min. simple induction n; trivial. intros. - simpl in |- *. + simpl. inversion H. rewrite H1. rewrite H1. @@ -105,7 +105,7 @@ Proof. simple induction d. simple induction d'; trivial. simple induction d'; trivial. elim n. simple induction n0; trivial. intros. elim n1; trivial. intros. unfold ni_min in H. cut (min n0 n2 = min n2 n0). - intro. unfold ni_min in |- *. simpl in |- *. rewrite H1. reflexivity. + intro. unfold ni_min. simpl. rewrite H1. reflexivity. cut (ni (min n0 n2) = ni (min n2 n0)). intros. inversion H1; trivial. exact (H n2). @@ -116,11 +116,11 @@ Lemma ni_min_assoc : Proof. simple induction d; trivial. simple induction d'; trivial. simple induction d''; trivial. - unfold ni_min in |- *. intro. cut (min (min n n0) n1 = min n (min n0 n1)). + unfold ni_min. intro. cut (min (min n n0) n1 = min n (min n0 n1)). intro. rewrite H. reflexivity. generalize n0 n1. elim n; trivial. simple induction n3; trivial. simple induction n5; trivial. - intros. simpl in |- *. auto. + intros. simpl. auto. Qed. Lemma ni_min_O_l : forall d:natinf, ni_min (ni 0) d = ni 0. @@ -152,42 +152,42 @@ Qed. Lemma ni_le_antisym : forall d d':natinf, ni_le d d' -> ni_le d' d -> d = d'. Proof. - unfold ni_le in |- *. intros d d'. rewrite ni_min_comm. intro H. rewrite H. trivial. + unfold ni_le. intros d d'. rewrite ni_min_comm. intro H. rewrite H. trivial. Qed. Lemma ni_le_trans : forall d d' d'':natinf, ni_le d d' -> ni_le d' d'' -> ni_le d d''. Proof. - unfold ni_le in |- *. intros. rewrite <- H. rewrite ni_min_assoc. rewrite H0. reflexivity. + unfold ni_le. intros. rewrite <- H. rewrite ni_min_assoc. rewrite H0. reflexivity. Qed. Lemma ni_le_min_1 : forall d d':natinf, ni_le (ni_min d d') d. Proof. - unfold ni_le in |- *. intros. rewrite (ni_min_comm d d'). rewrite ni_min_assoc. + unfold ni_le. intros. rewrite (ni_min_comm d d'). rewrite ni_min_assoc. rewrite ni_min_idemp. reflexivity. Qed. Lemma ni_le_min_2 : forall d d':natinf, ni_le (ni_min d d') d'. Proof. - unfold ni_le in |- *. intros. rewrite ni_min_assoc. rewrite ni_min_idemp. reflexivity. + unfold ni_le. intros. rewrite ni_min_assoc. rewrite ni_min_idemp. reflexivity. Qed. Lemma ni_min_case : forall d d':natinf, ni_min d d' = d \/ ni_min d d' = d'. Proof. simple induction d. intro. right. exact (ni_min_inf_l d'). simple induction d'. left. exact (ni_min_inf_r (ni n)). - unfold ni_min in |- *. cut (forall n0:nat, min n n0 = n \/ min n n0 = n0). + unfold ni_min. cut (forall n0:nat, min n n0 = n \/ min n n0 = n0). intros. case (H n0). intro. left. rewrite H0. reflexivity. intro. right. rewrite H0. reflexivity. elim n. intro. left. reflexivity. simple induction n1. right. reflexivity. - intros. case (H n2). intro. left. simpl in |- *. rewrite H1. reflexivity. - intro. right. simpl in |- *. rewrite H1. reflexivity. + intros. case (H n2). intro. left. simpl. rewrite H1. reflexivity. + intro. right. simpl. rewrite H1. reflexivity. Qed. Lemma ni_le_total : forall d d':natinf, ni_le d d' \/ ni_le d' d. Proof. - unfold ni_le in |- *. intros. rewrite (ni_min_comm d' d). apply ni_min_case. + unfold ni_le. intros. rewrite (ni_min_comm d' d). apply ni_min_case. Qed. Lemma ni_le_min_induc : @@ -201,7 +201,7 @@ Proof. apply ni_le_antisym. apply H1. apply ni_le_refl. exact H2. exact H. - intro. rewrite H2. apply ni_le_antisym. apply H1. unfold ni_le in |- *. rewrite ni_min_comm. exact H2. + intro. rewrite H2. apply ni_le_antisym. apply H1. unfold ni_le. rewrite ni_min_comm. exact H2. apply ni_le_refl. exact H0. Qed. @@ -209,40 +209,40 @@ Qed. Lemma le_ni_le : forall m n:nat, m <= n -> ni_le (ni m) (ni n). Proof. cut (forall m n:nat, m <= n -> min m n = m). - intros. unfold ni_le, ni_min in |- *. rewrite (H m n H0). reflexivity. + intros. unfold ni_le, ni_min. rewrite (H m n H0). reflexivity. simple induction m. trivial. simple induction n0. intro. inversion H0. - intros. simpl in |- *. rewrite (H n1 (le_S_n n n1 H1)). reflexivity. + intros. simpl. rewrite (H n1 (le_S_n n n1 H1)). reflexivity. Qed. Lemma ni_le_le : forall m n:nat, ni_le (ni m) (ni n) -> m <= n. Proof. - unfold ni_le in |- *. unfold ni_min in |- *. intros. inversion H. apply le_min_r. + unfold ni_le. unfold ni_min. intros. inversion H. apply le_min_r. Qed. Lemma Nplength_lb : forall (a:N) (n:nat), - (forall k:nat, k < n -> Nbit a k = false) -> ni_le (ni n) (Nplength a). + (forall k:nat, k < n -> N.testbit_nat a k = false) -> ni_le (ni n) (Nplength a). Proof. simple induction a. intros. exact (ni_min_inf_r (ni n)). - intros. unfold Nplength in |- *. apply le_ni_le. case (le_or_lt n (Pplength p)). trivial. - intro. absurd (Nbit (Npos p) (Pplength p) = false). + intros. unfold Nplength. apply le_ni_le. case (le_or_lt n (Pplength p)). trivial. + intro. absurd (N.testbit_nat (Npos p) (Pplength p) = false). rewrite (Nplength_one (Npos p) (Pplength p) - (refl_equal (Nplength (Npos p)))). + (eq_refl (Nplength (Npos p)))). discriminate. apply H. exact H0. Qed. Lemma Nplength_ub : - forall (a:N) (n:nat), Nbit a n = true -> ni_le (Nplength a) (ni n). + forall (a:N) (n:nat), N.testbit_nat a n = true -> ni_le (Nplength a) (ni n). Proof. simple induction a. intros. discriminate H. - intros. unfold Nplength in |- *. apply le_ni_le. case (le_or_lt (Pplength p) n). trivial. - intro. absurd (Nbit (Npos p) n = true). + intros. unfold Nplength. apply le_ni_le. case (le_or_lt (Pplength p) n). trivial. + intro. absurd (N.testbit_nat (Npos p) n = true). rewrite (Nplength_zeros (Npos p) (Pplength p) - (refl_equal (Nplength (Npos p))) n H0). + (eq_refl (Nplength (Npos p))) n H0). discriminate. exact H. Qed. @@ -255,26 +255,26 @@ Qed. Instead of working with $d$, we work with $pd$, namely [Npdist]: *) -Definition Npdist (a a':N) := Nplength (Nxor a a'). +Definition Npdist (a a':N) := Nplength (N.lxor a a'). (** d is a distance, so $d(a,a')=0$ iff $a=a'$; this means that $pd(a,a')=infty$ iff $a=a'$: *) Lemma Npdist_eq_1 : forall a:N, Npdist a a = infty. Proof. - intros. unfold Npdist in |- *. rewrite Nxor_nilpotent. reflexivity. + intros. unfold Npdist. rewrite N.lxor_nilpotent. reflexivity. Qed. Lemma Npdist_eq_2 : forall a a':N, Npdist a a' = infty -> a = a'. Proof. - intros. apply Nxor_eq. apply Nplength_infty. exact H. + intros. apply N.lxor_eq. apply Nplength_infty. exact H. Qed. (** $d$ is a distance, so $d(a,a')=d(a',a)$: *) Lemma Npdist_comm : forall a a':N, Npdist a a' = Npdist a' a. Proof. - unfold Npdist in |- *. intros. rewrite Nxor_comm. reflexivity. + unfold Npdist. intros. rewrite N.lxor_comm. reflexivity. Qed. (** $d$ is an ultrametric distance, that is, not only $d(a,a')\leq @@ -292,21 +292,21 @@ Qed. Lemma Nplength_ultra_1 : forall a a':N, ni_le (Nplength a) (Nplength a') -> - ni_le (Nplength a) (Nplength (Nxor a a')). + ni_le (Nplength a) (Nplength (N.lxor a a')). Proof. simple induction a. intros. unfold ni_le in H. unfold Nplength at 1 3 in H. rewrite (ni_min_inf_l (Nplength a')) in H. - rewrite (Nplength_infty a' H). simpl in |- *. apply ni_le_refl. - intros. unfold Nplength at 1 in |- *. apply Nplength_lb. intros. - cut (forall a'':N, Nxor (Npos p) a' = a'' -> Nbit a'' k = false). + rewrite (Nplength_infty a' H). simpl. apply ni_le_refl. + intros. unfold Nplength at 1. apply Nplength_lb. intros. + cut (forall a'':N, N.lxor (Npos p) a' = a'' -> N.testbit_nat a'' k = false). intros. apply H1. reflexivity. intro a''. case a''. intro. reflexivity. intros. rewrite <- H1. rewrite (Nxor_semantics (Npos p) a' k). rewrite (Nplength_zeros (Npos p) (Pplength p) - (refl_equal (Nplength (Npos p))) k H0). + (eq_refl (Nplength (Npos p))) k H0). generalize H. case a'. trivial. - intros. cut (Nbit (Npos p1) k = false). intros. rewrite H3. reflexivity. + intros. cut (N.testbit_nat (Npos p1) k = false). intros. rewrite H3. reflexivity. apply Nplength_zeros with (n := Pplength p1). reflexivity. apply (lt_le_trans k (Pplength p) (Pplength p1)). exact H0. apply ni_le_le. exact H2. @@ -314,14 +314,14 @@ Qed. Lemma Nplength_ultra : forall a a':N, - ni_le (ni_min (Nplength a) (Nplength a')) (Nplength (Nxor a a')). + ni_le (ni_min (Nplength a) (Nplength a')) (Nplength (N.lxor a a')). Proof. intros. case (ni_le_total (Nplength a) (Nplength a')). intro. cut (ni_min (Nplength a) (Nplength a') = Nplength a). intro. rewrite H0. apply Nplength_ultra_1. exact H. exact H. intro. cut (ni_min (Nplength a) (Nplength a') = Nplength a'). - intro. rewrite H0. rewrite Nxor_comm. apply Nplength_ultra_1. exact H. + intro. rewrite H0. rewrite N.lxor_comm. apply Nplength_ultra_1. exact H. rewrite ni_min_comm. exact H. Qed. @@ -329,8 +329,8 @@ Lemma Npdist_ultra : forall a a' a'':N, ni_le (ni_min (Npdist a a'') (Npdist a'' a')) (Npdist a a'). Proof. - intros. unfold Npdist in |- *. cut (Nxor (Nxor a a'') (Nxor a'' a') = Nxor a a'). + intros. unfold Npdist. cut (N.lxor (N.lxor a a'') (N.lxor a'' a') = N.lxor a a'). intro. rewrite <- H. apply Nplength_ultra. - rewrite Nxor_assoc. rewrite <- (Nxor_assoc a'' a'' a'). rewrite Nxor_nilpotent. - rewrite Nxor_neutral_left. reflexivity. + rewrite N.lxor_assoc. rewrite <- (N.lxor_assoc a'' a'' a'). rewrite N.lxor_nilpotent. + rewrite N.lxor_0_l. reflexivity. Qed. diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v index 559f01f1..0b220f5d 100644 --- a/theories/NArith/Ndiv_def.v +++ b/theories/NArith/Ndiv_def.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -22,10 +22,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 (only parsing). -Notation Ndiv := N.div (only parsing). -Notation Nmod := N.modulo (only parsing). +Notation Ndiv_eucl := N.div_eucl (compat "8.3"). +Notation Ndiv := N.div (compat "8.3"). +Notation Nmod := N.modulo (compat "8.3"). -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 (only parsing). +Notation Ndiv_eucl_correct := N.div_eucl_spec (compat "8.3"). +Notation Ndiv_mod_eq := N.div_mod' (compat "8.3"). +Notation Nmod_lt := N.mod_lt (compat "8.3"). diff --git a/theories/NArith/Ngcd_def.v b/theories/NArith/Ngcd_def.v index 13211f46..737cd450 100644 --- a/theories/NArith/Ngcd_def.v +++ b/theories/NArith/Ngcd_def.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 133d4c23..1b7e2f24 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -203,30 +203,30 @@ Hint Rewrite Nat2N.id : Nnat. (** Compatibility notations *) -Notation nat_of_N_inj := N2Nat.inj (only parsing). -Notation N_of_nat_of_N := N2Nat.id (only parsing). -Notation nat_of_Ndouble := N2Nat.inj_double (only parsing). -Notation nat_of_Ndouble_plus_one := N2Nat.inj_succ_double (only parsing). -Notation nat_of_Nsucc := N2Nat.inj_succ (only parsing). -Notation nat_of_Nplus := N2Nat.inj_add (only parsing). -Notation nat_of_Nmult := N2Nat.inj_mul (only parsing). -Notation nat_of_Nminus := N2Nat.inj_sub (only parsing). -Notation nat_of_Npred := N2Nat.inj_pred (only parsing). -Notation nat_of_Ndiv2 := N2Nat.inj_div2 (only parsing). -Notation nat_of_Ncompare := N2Nat.inj_compare (only parsing). -Notation nat_of_Nmax := N2Nat.inj_max (only parsing). -Notation nat_of_Nmin := N2Nat.inj_min (only parsing). - -Notation nat_of_N_of_nat := Nat2N.id (only parsing). -Notation N_of_nat_inj := Nat2N.inj (only parsing). -Notation N_of_double := Nat2N.inj_double (only parsing). -Notation N_of_double_plus_one := Nat2N.inj_succ_double (only parsing). -Notation N_of_S := Nat2N.inj_succ (only parsing). -Notation N_of_pred := Nat2N.inj_pred (only parsing). -Notation N_of_plus := Nat2N.inj_add (only parsing). -Notation N_of_minus := Nat2N.inj_sub (only parsing). -Notation N_of_mult := Nat2N.inj_mul (only parsing). -Notation N_of_div2 := Nat2N.inj_div2 (only parsing). -Notation N_of_nat_compare := Nat2N.inj_compare (only parsing). -Notation N_of_min := Nat2N.inj_min (only parsing). -Notation N_of_max := Nat2N.inj_max (only parsing). +Notation nat_of_N_inj := N2Nat.inj (compat "8.3"). +Notation N_of_nat_of_N := N2Nat.id (compat "8.3"). +Notation nat_of_Ndouble := N2Nat.inj_double (compat "8.3"). +Notation nat_of_Ndouble_plus_one := N2Nat.inj_succ_double (compat "8.3"). +Notation nat_of_Nsucc := N2Nat.inj_succ (compat "8.3"). +Notation nat_of_Nplus := N2Nat.inj_add (compat "8.3"). +Notation nat_of_Nmult := N2Nat.inj_mul (compat "8.3"). +Notation nat_of_Nminus := N2Nat.inj_sub (compat "8.3"). +Notation nat_of_Npred := N2Nat.inj_pred (compat "8.3"). +Notation nat_of_Ndiv2 := N2Nat.inj_div2 (compat "8.3"). +Notation nat_of_Ncompare := N2Nat.inj_compare (compat "8.3"). +Notation nat_of_Nmax := N2Nat.inj_max (compat "8.3"). +Notation nat_of_Nmin := N2Nat.inj_min (compat "8.3"). + +Notation nat_of_N_of_nat := Nat2N.id (compat "8.3"). +Notation N_of_nat_inj := Nat2N.inj (compat "8.3"). +Notation N_of_double := Nat2N.inj_double (compat "8.3"). +Notation N_of_double_plus_one := Nat2N.inj_succ_double (compat "8.3"). +Notation N_of_S := Nat2N.inj_succ (compat "8.3"). +Notation N_of_pred := Nat2N.inj_pred (compat "8.3"). +Notation N_of_plus := Nat2N.inj_add (compat "8.3"). +Notation N_of_minus := Nat2N.inj_sub (compat "8.3"). +Notation N_of_mult := Nat2N.inj_mul (compat "8.3"). +Notation N_of_div2 := Nat2N.inj_div2 (compat "8.3"). +Notation N_of_nat_compare := Nat2N.inj_compare (compat "8.3"). +Notation N_of_min := Nat2N.inj_min (compat "8.3"). +Notation N_of_max := Nat2N.inj_max (compat "8.3"). diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v index edb6b289..240d7469 100644 --- a/theories/NArith/Nsqrt_def.v +++ b/theories/NArith/Nsqrt_def.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,8 +11,8 @@ Require Import BinNat. (** Obsolete file, see [BinNat] now, only compatibility notations remain here. *) -Notation Nsqrtrem := N.sqrtrem (only parsing). -Notation Nsqrt := N.sqrt (only parsing). -Notation Nsqrtrem_spec := N.sqrtrem_spec (only parsing). -Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (only parsing). -Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (only parsing). +Notation Nsqrtrem := N.sqrtrem (compat "8.3"). +Notation Nsqrt := N.sqrt (compat "8.3"). +Notation Nsqrtrem_spec := N.sqrtrem_spec (compat "8.3"). +Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (compat "8.3"). +Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (compat "8.3"). |