summaryrefslogtreecommitdiff
path: root/theories/NArith
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-08-20 18:27:01 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-08-20 18:27:01 +0200
commite0d682ec25282a348d35c5b169abafec48555690 (patch)
tree1a46f0142a85df553388c932110793881f3af52f /theories/NArith
parent86535d84cc3cffeee1dcd8545343f234e7285530 (diff)
Imported Upstream version 8.4dfsgupstream/8.4dfsg
Diffstat (limited to 'theories/NArith')
-rw-r--r--theories/NArith/BinNat.v220
-rw-r--r--theories/NArith/BinNatDef.v94
-rw-r--r--theories/NArith/NArith.v2
-rw-r--r--theories/NArith/Ndec.v443
-rw-r--r--theories/NArith/Ndigits.v207
-rw-r--r--theories/NArith/Ndist.v104
-rw-r--r--theories/NArith/Ndiv_def.v14
-rw-r--r--theories/NArith/Ngcd_def.v2
-rw-r--r--theories/NArith/Nnat.v56
-rw-r--r--theories/NArith/Nsqrt_def.v12
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").