diff options
Diffstat (limited to 'theories/Numbers/Integer')
24 files changed, 271 insertions, 260 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index 647ab0ac..ac113dfd 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.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/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index 423cdf58..06ac0ba0 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.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/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index fd20ce72..f2947c30 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.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/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 51054852..bc78a4b9 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.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/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index 92afbcb5..1d410a02 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.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 *) @@ -292,7 +292,7 @@ Proof. Qed. (** Hence the number of bits of [a] is [1+log2 a] - (see [Psize] and [Psize_pos]). + (see [Pos.size_nat] and [Pos.size]). *) (** For negative numbers, things are the other ways around: diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index fe951a75..dd8aa100 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.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/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index 14003d89..2ccc79e9 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.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 *) @@ -16,7 +16,7 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. [a = bq+r /\ 0 <= |r| < |b| /\ Sign(r) = Sign(b)] - This is the convention followed historically by [Zdiv] in Coq, and + This is the convention followed historically by [Z.div] in Coq, and corresponds to convention "F" in the following paper: R. Boute, "The Euclidean definition of the functions div and mod", diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index bd8b6ce2..d69d0e10 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.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/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v index 404fc0c4..feac10b3 100644 --- a/theories/Numbers/Integer/Abstract/ZGcd.v +++ b/theories/Numbers/Integer/Abstract/ZGcd.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/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v index 06af04d1..45da2dee 100644 --- a/theories/Numbers/Integer/Abstract/ZLcm.v +++ b/theories/Numbers/Integer/Abstract/ZLcm.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/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index 3a8e1f38..96be5811 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.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/Numbers/Integer/Abstract/ZMaxMin.v b/theories/Numbers/Integer/Abstract/ZMaxMin.v index 4e653fee..dc7598e3 100644 --- a/theories/Numbers/Integer/Abstract/ZMaxMin.v +++ b/theories/Numbers/Integer/Abstract/ZMaxMin.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/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v index 36f9c3d5..c5fbd450 100644 --- a/theories/Numbers/Integer/Abstract/ZMul.v +++ b/theories/Numbers/Integer/Abstract/ZMul.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/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index d0d64faa..8edf97f4 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.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/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v index b364ec3f..13541309 100644 --- a/theories/Numbers/Integer/Abstract/ZParity.v +++ b/theories/Numbers/Integer/Abstract/ZParity.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/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v index 53d84dce..d30cea33 100644 --- a/theories/Numbers/Integer/Abstract/ZPow.v +++ b/theories/Numbers/Integer/Abstract/ZPow.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 *) @@ -18,6 +18,17 @@ Module Type ZPowProp Include NZPowProp A A B. +(** A particular case of [pow_add_r], with no precondition *) + +Lemma pow_twice_r a b : a^(2*b) == a^b * a^b. +Proof. + rewrite two_succ. nzsimpl. + destruct (le_gt_cases 0 b). + - now rewrite pow_add_r. + - rewrite !pow_neg_r. now nzsimpl. trivial. + now apply add_neg_neg. +Qed. + (** Parity of power *) Lemma even_pow : forall a b, 0<b -> even (a^b) = even a. diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index c0455196..8973df35 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.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/Numbers/Integer/Abstract/ZSgnAbs.v b/theories/Numbers/Integer/Abstract/ZSgnAbs.v index b2f6cc84..24b6003c 100644 --- a/theories/Numbers/Integer/Abstract/ZSgnAbs.v +++ b/theories/Numbers/Integer/Abstract/ZSgnAbs.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/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 443777f5..a56f90b0 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.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 @@ Infix "÷" := BigZ.quot (at level 40, left associativity) : bigZ_scope. (** Some additional results about [BigZ] *) Theorem spec_to_Z: forall n : bigZ, - BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z. + BigN.to_Z (BigZ.to_N n) = ((Z.sgn [n]) * [n])%Z. Proof. intros n; case n; simpl; intros p; generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. @@ -85,7 +85,7 @@ intros p1 H1; case H1; auto. Qed. Theorem spec_to_N n: - ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z. + ([n] = Z.sgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z. Proof. case n; simpl; intros p; generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. @@ -118,7 +118,7 @@ Qed. Lemma BigZeqb_correct : forall x y, (x =? y) = true -> x==y. Proof. now apply BigZ.eqb_eq. Qed. -Definition BigZ_of_N n := BigZ.of_Z (Z_of_N n). +Definition BigZ_of_N n := BigZ.of_Z (Z.of_N n). Lemma BigZpower : power_theory 1 BigZ.mul BigZ.eq BigZ_of_N BigZ.pow. Proof. @@ -139,7 +139,7 @@ BigZ.zify. auto with zarith. intros NEQ. generalize (BigZ.spec_div_eucl a b). generalize (Z_div_mod_full [a] [b] NEQ). -destruct BigZ.div_eucl as (q,r), Zdiv_eucl as (q',r'). +destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r'). intros (EQ,_). injection 1. intros EQr EQq. BigZ.zify. rewrite EQr, EQq; auto. Qed. diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 0142b36b..180fe0a9 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.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 *) @@ -21,92 +21,92 @@ Open Scope Z_scope. [NSig.NType] to a structure of integers [ZSig.ZType]. *) -Module Make (N:NType) <: ZType. +Module Make (NN:NType) <: ZType. Inductive t_ := - | Pos : N.t -> t_ - | Neg : N.t -> t_. + | Pos : NN.t -> t_ + | Neg : NN.t -> t_. Definition t := t_. Bind Scope abstract_scope with t t_. - Definition zero := Pos N.zero. - Definition one := Pos N.one. - Definition two := Pos N.two. - Definition minus_one := Neg N.one. + Definition zero := Pos NN.zero. + Definition one := Pos NN.one. + Definition two := Pos NN.two. + Definition minus_one := Neg NN.one. Definition of_Z x := match x with - | Zpos x => Pos (N.of_N (Npos x)) + | Zpos x => Pos (NN.of_N (Npos x)) | Z0 => zero - | Zneg x => Neg (N.of_N (Npos x)) + | Zneg x => Neg (NN.of_N (Npos x)) end. Definition to_Z x := match x with - | Pos nx => N.to_Z nx - | Neg nx => Zopp (N.to_Z nx) + | Pos nx => NN.to_Z nx + | Neg nx => Z.opp (NN.to_Z nx) end. Theorem spec_of_Z: forall x, to_Z (of_Z x) = x. Proof. intros x; case x; unfold to_Z, of_Z, zero. - exact N.spec_0. - intros; rewrite N.spec_of_N; auto. - intros; rewrite N.spec_of_N; auto. + exact NN.spec_0. + intros; rewrite NN.spec_of_N; auto. + intros; rewrite NN.spec_of_N; auto. Qed. Definition eq x y := (to_Z x = to_Z y). Theorem spec_0: to_Z zero = 0. - exact N.spec_0. + exact NN.spec_0. Qed. Theorem spec_1: to_Z one = 1. - exact N.spec_1. + exact NN.spec_1. Qed. Theorem spec_2: to_Z two = 2. - exact N.spec_2. + exact NN.spec_2. Qed. Theorem spec_m1: to_Z minus_one = -1. - simpl; rewrite N.spec_1; auto. + simpl; rewrite NN.spec_1; auto. Qed. Definition compare x y := match x, y with - | Pos nx, Pos ny => N.compare nx ny + | Pos nx, Pos ny => NN.compare nx ny | Pos nx, Neg ny => - match N.compare nx N.zero with + match NN.compare nx NN.zero with | Gt => Gt - | _ => N.compare ny N.zero + | _ => NN.compare ny NN.zero end | Neg nx, Pos ny => - match N.compare N.zero nx with + match NN.compare NN.zero nx with | Lt => Lt - | _ => N.compare N.zero ny + | _ => NN.compare NN.zero ny end - | Neg nx, Neg ny => N.compare ny nx + | Neg nx, Neg ny => NN.compare ny nx end. Theorem spec_compare : - forall x y, compare x y = Zcompare (to_Z x) (to_Z y). + forall x y, compare x y = Z.compare (to_Z x) (to_Z y). Proof. unfold compare, to_Z. destruct x as [x|x], y as [y|y]; - rewrite ?N.spec_compare, ?N.spec_0, <-?Zcompare_opp; auto; - assert (Hx:=N.spec_pos x); assert (Hy:=N.spec_pos y); - set (X:=N.to_Z x) in *; set (Y:=N.to_Z y) in *; clearbody X Y. - destruct (Zcompare_spec X 0) as [EQ|LT|GT]. - rewrite EQ. rewrite <- Zopp_0 at 2. apply Zcompare_opp. - exfalso. omega. - symmetry. change (X > -Y). omega. - destruct (Zcompare_spec 0 X) as [EQ|LT|GT]. - rewrite <- EQ. rewrite Zopp_0; auto. - symmetry. change (-X < Y). omega. - exfalso. omega. + rewrite ?NN.spec_compare, ?NN.spec_0, ?Z.compare_opp; auto; + assert (Hx:=NN.spec_pos x); assert (Hy:=NN.spec_pos y); + set (X:=NN.to_Z x) in *; set (Y:=NN.to_Z y) in *; clearbody X Y. + - destruct (Z.compare_spec X 0) as [EQ|LT|GT]. + + rewrite <- Z.opp_0 in EQ. now rewrite EQ, Z.compare_opp. + + exfalso. omega. + + symmetry. change (X > -Y). omega. + - destruct (Z.compare_spec 0 X) as [EQ|LT|GT]. + + rewrite <- EQ, Z.opp_0; auto. + + symmetry. change (-X < Y). omega. + + exfalso. omega. Qed. Definition eqb x y := @@ -155,14 +155,14 @@ Module Make (N:NType) <: ZType. Definition min n m := match compare n m with Gt => m | _ => n end. Definition max n m := match compare n m with Lt => m | _ => n end. - Theorem spec_min : forall n m, to_Z (min n m) = Zmin (to_Z n) (to_Z m). + Theorem spec_min : forall n m, to_Z (min n m) = Z.min (to_Z n) (to_Z m). Proof. - unfold min, Zmin. intros. rewrite spec_compare. destruct Zcompare; auto. + unfold min, Z.min. intros. rewrite spec_compare. destruct Z.compare; auto. Qed. - Theorem spec_max : forall n m, to_Z (max n m) = Zmax (to_Z n) (to_Z m). + Theorem spec_max : forall n m, to_Z (max n m) = Z.max (to_Z n) (to_Z m). Proof. - unfold max, Zmax. intros. rewrite spec_compare. destruct Zcompare; auto. + unfold max, Z.max. intros. rewrite spec_compare. destruct Z.compare; auto. Qed. Definition to_N x := @@ -173,11 +173,11 @@ Module Make (N:NType) <: ZType. Definition abs x := Pos (to_N x). - Theorem spec_abs: forall x, to_Z (abs x) = Zabs (to_Z x). + Theorem spec_abs: forall x, to_Z (abs x) = Z.abs (to_Z x). Proof. - intros x; case x; clear x; intros x; assert (F:=N.spec_pos x). - simpl; rewrite Zabs_eq; auto. - simpl; rewrite Zabs_non_eq; simpl; auto with zarith. + intros x; case x; clear x; intros x; assert (F:=NN.spec_pos x). + simpl; rewrite Z.abs_eq; auto. + simpl; rewrite Z.abs_neq; simpl; auto with zarith. Qed. Definition opp x := @@ -193,10 +193,10 @@ Module Make (N:NType) <: ZType. Definition succ x := match x with - | Pos n => Pos (N.succ n) + | Pos n => Pos (NN.succ n) | Neg n => - match N.compare N.zero n with - | Lt => Neg (N.pred n) + match NN.compare NN.zero n with + | Lt => Neg (NN.pred n) | _ => one end end. @@ -204,134 +204,134 @@ Module Make (N:NType) <: ZType. Theorem spec_succ: forall n, to_Z (succ n) = to_Z n + 1. Proof. intros x; case x; clear x; intros x. - exact (N.spec_succ x). - simpl. rewrite N.spec_compare. case Zcompare_spec; rewrite ?N.spec_0; simpl. - intros HH; rewrite <- HH; rewrite N.spec_1; ring. - intros HH; rewrite N.spec_pred, Zmax_r; auto with zarith. - generalize (N.spec_pos x); auto with zarith. + exact (NN.spec_succ x). + simpl. rewrite NN.spec_compare. case Z.compare_spec; rewrite ?NN.spec_0; simpl. + intros HH; rewrite <- HH; rewrite NN.spec_1; ring. + intros HH; rewrite NN.spec_pred, Z.max_r; auto with zarith. + generalize (NN.spec_pos x); auto with zarith. Qed. Definition add x y := match x, y with - | Pos nx, Pos ny => Pos (N.add nx ny) + | Pos nx, Pos ny => Pos (NN.add nx ny) | Pos nx, Neg ny => - match N.compare nx ny with - | Gt => Pos (N.sub nx ny) + match NN.compare nx ny with + | Gt => Pos (NN.sub nx ny) | Eq => zero - | Lt => Neg (N.sub ny nx) + | Lt => Neg (NN.sub ny nx) end | Neg nx, Pos ny => - match N.compare nx ny with - | Gt => Neg (N.sub nx ny) + match NN.compare nx ny with + | Gt => Neg (NN.sub nx ny) | Eq => zero - | Lt => Pos (N.sub ny nx) + | Lt => Pos (NN.sub ny nx) end - | Neg nx, Neg ny => Neg (N.add nx ny) + | Neg nx, Neg ny => Neg (NN.add nx ny) end. Theorem spec_add: forall x y, to_Z (add x y) = to_Z x + to_Z y. Proof. unfold add, to_Z; intros [x | x] [y | y]; - try (rewrite N.spec_add; auto with zarith); - rewrite N.spec_compare; case Zcompare_spec; - unfold zero; rewrite ?N.spec_0, ?N.spec_sub; omega with *. + try (rewrite NN.spec_add; auto with zarith); + rewrite NN.spec_compare; case Z.compare_spec; + unfold zero; rewrite ?NN.spec_0, ?NN.spec_sub; omega with *. Qed. Definition pred x := match x with | Pos nx => - match N.compare N.zero nx with - | Lt => Pos (N.pred nx) + match NN.compare NN.zero nx with + | Lt => Pos (NN.pred nx) | _ => minus_one end - | Neg nx => Neg (N.succ nx) + | Neg nx => Neg (NN.succ nx) end. Theorem spec_pred: forall x, to_Z (pred x) = to_Z x - 1. Proof. unfold pred, to_Z, minus_one; intros [x | x]; - try (rewrite N.spec_succ; ring). - rewrite N.spec_compare; case Zcompare_spec; - rewrite ?N.spec_0, ?N.spec_1, ?N.spec_pred; - generalize (N.spec_pos x); omega with *. + try (rewrite NN.spec_succ; ring). + rewrite NN.spec_compare; case Z.compare_spec; + rewrite ?NN.spec_0, ?NN.spec_1, ?NN.spec_pred; + generalize (NN.spec_pos x); omega with *. Qed. Definition sub x y := match x, y with | Pos nx, Pos ny => - match N.compare nx ny with - | Gt => Pos (N.sub nx ny) + match NN.compare nx ny with + | Gt => Pos (NN.sub nx ny) | Eq => zero - | Lt => Neg (N.sub ny nx) + | Lt => Neg (NN.sub ny nx) end - | Pos nx, Neg ny => Pos (N.add nx ny) - | Neg nx, Pos ny => Neg (N.add nx ny) + | Pos nx, Neg ny => Pos (NN.add nx ny) + | Neg nx, Pos ny => Neg (NN.add nx ny) | Neg nx, Neg ny => - match N.compare nx ny with - | Gt => Neg (N.sub nx ny) + match NN.compare nx ny with + | Gt => Neg (NN.sub nx ny) | Eq => zero - | Lt => Pos (N.sub ny nx) + | Lt => Pos (NN.sub ny nx) end end. Theorem spec_sub: forall x y, to_Z (sub x y) = to_Z x - to_Z y. Proof. unfold sub, to_Z; intros [x | x] [y | y]; - try (rewrite N.spec_add; auto with zarith); - rewrite N.spec_compare; case Zcompare_spec; - unfold zero; rewrite ?N.spec_0, ?N.spec_sub; omega with *. + try (rewrite NN.spec_add; auto with zarith); + rewrite NN.spec_compare; case Z.compare_spec; + unfold zero; rewrite ?NN.spec_0, ?NN.spec_sub; omega with *. Qed. Definition mul x y := match x, y with - | Pos nx, Pos ny => Pos (N.mul nx ny) - | Pos nx, Neg ny => Neg (N.mul nx ny) - | Neg nx, Pos ny => Neg (N.mul nx ny) - | Neg nx, Neg ny => Pos (N.mul nx ny) + | Pos nx, Pos ny => Pos (NN.mul nx ny) + | Pos nx, Neg ny => Neg (NN.mul nx ny) + | Neg nx, Pos ny => Neg (NN.mul nx ny) + | Neg nx, Neg ny => Pos (NN.mul nx ny) end. Theorem spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y. Proof. - unfold mul, to_Z; intros [x | x] [y | y]; rewrite N.spec_mul; ring. + unfold mul, to_Z; intros [x | x] [y | y]; rewrite NN.spec_mul; ring. Qed. Definition square x := match x with - | Pos nx => Pos (N.square nx) - | Neg nx => Pos (N.square nx) + | Pos nx => Pos (NN.square nx) + | Neg nx => Pos (NN.square nx) end. Theorem spec_square: forall x, to_Z (square x) = to_Z x * to_Z x. Proof. - unfold square, to_Z; intros [x | x]; rewrite N.spec_square; ring. + unfold square, to_Z; intros [x | x]; rewrite NN.spec_square; ring. Qed. Definition pow_pos x p := match x with - | Pos nx => Pos (N.pow_pos nx p) + | Pos nx => Pos (NN.pow_pos nx p) | Neg nx => match p with | xH => x - | xO _ => Pos (N.pow_pos nx p) - | xI _ => Neg (N.pow_pos nx p) + | xO _ => Pos (NN.pow_pos nx p) + | xI _ => Neg (NN.pow_pos nx p) end end. Theorem spec_pow_pos: forall x n, to_Z (pow_pos x n) = to_Z x ^ Zpos n. Proof. assert (F0: forall x, (-x)^2 = x^2). - intros x; rewrite Zpower_2; ring. + intros x; rewrite Z.pow_2_r; ring. unfold pow_pos, to_Z; intros [x | x] [p | p |]; - try rewrite N.spec_pow_pos; try ring. + try rewrite NN.spec_pow_pos; try ring. assert (F: 0 <= 2 * Zpos p). assert (0 <= Zpos p); auto with zarith. - rewrite Zpos_xI; repeat rewrite Zpower_exp; auto with zarith. - repeat rewrite Zpower_mult; auto with zarith. + rewrite Pos2Z.inj_xI; repeat rewrite Zpower_exp; auto with zarith. + repeat rewrite Z.pow_mul_r; auto with zarith. rewrite F0; ring. assert (F: 0 <= 2 * Zpos p). assert (0 <= Zpos p); auto with zarith. - rewrite Zpos_xO; repeat rewrite Zpower_exp; auto with zarith. - repeat rewrite Zpower_mult; auto with zarith. + rewrite Pos2Z.inj_xO; repeat rewrite Zpower_exp; auto with zarith. + repeat rewrite Z.pow_mul_r; auto with zarith. rewrite F0; ring. Qed. @@ -341,9 +341,9 @@ Module Make (N:NType) <: ZType. | Npos p => pow_pos x p end. - Theorem spec_pow_N: forall x n, to_Z (pow_N x n) = to_Z x ^ Z_of_N n. + Theorem spec_pow_N: forall x n, to_Z (pow_N x n) = to_Z x ^ Z.of_N n. Proof. - destruct n; simpl. apply N.spec_1. + destruct n; simpl. apply NN.spec_1. apply spec_pow_pos. Qed. @@ -357,38 +357,38 @@ Module Make (N:NType) <: ZType. Theorem spec_pow: forall x y, to_Z (pow x y) = to_Z x ^ to_Z y. Proof. intros. unfold pow. destruct (to_Z y); simpl. - apply N.spec_1. + apply NN.spec_1. apply spec_pow_pos. - apply N.spec_0. + apply NN.spec_0. Qed. Definition log2 x := match x with - | Pos nx => Pos (N.log2 nx) + | Pos nx => Pos (NN.log2 nx) | Neg nx => zero end. Theorem spec_log2: forall x, to_Z (log2 x) = Z.log2 (to_Z x). Proof. - intros. destruct x as [p|p]; simpl. apply N.spec_log2. - rewrite N.spec_0. - destruct (Z_le_lt_eq_dec _ _ (N.spec_pos p)) as [LT|EQ]. + intros. destruct x as [p|p]; simpl. apply NN.spec_log2. + rewrite NN.spec_0. + destruct (Z_le_lt_eq_dec _ _ (NN.spec_pos p)) as [LT|EQ]. rewrite Z.log2_nonpos; auto with zarith. now rewrite <- EQ. Qed. Definition sqrt x := match x with - | Pos nx => Pos (N.sqrt nx) - | Neg nx => Neg N.zero + | Pos nx => Pos (NN.sqrt nx) + | Neg nx => Neg NN.zero end. Theorem spec_sqrt: forall x, to_Z (sqrt x) = Z.sqrt (to_Z x). Proof. destruct x as [p|p]; simpl. - apply N.spec_sqrt. - rewrite N.spec_0. - destruct (Z_le_lt_eq_dec _ _ (N.spec_pos p)) as [LT|EQ]. + apply NN.spec_sqrt. + rewrite NN.spec_0. + destruct (Z_le_lt_eq_dec _ _ (NN.spec_pos p)) as [LT|EQ]. rewrite Z.sqrt_neg; auto with zarith. now rewrite <- EQ. Qed. @@ -396,68 +396,68 @@ Module Make (N:NType) <: ZType. Definition div_eucl x y := match x, y with | Pos nx, Pos ny => - let (q, r) := N.div_eucl nx ny in + let (q, r) := NN.div_eucl nx ny in (Pos q, Pos r) | Pos nx, Neg ny => - let (q, r) := N.div_eucl nx ny in - if N.eqb N.zero r + let (q, r) := NN.div_eucl nx ny in + if NN.eqb NN.zero r then (Neg q, zero) - else (Neg (N.succ q), Neg (N.sub ny r)) + else (Neg (NN.succ q), Neg (NN.sub ny r)) | Neg nx, Pos ny => - let (q, r) := N.div_eucl nx ny in - if N.eqb N.zero r + let (q, r) := NN.div_eucl nx ny in + if NN.eqb NN.zero r then (Neg q, zero) - else (Neg (N.succ q), Pos (N.sub ny r)) + else (Neg (NN.succ q), Pos (NN.sub ny r)) | Neg nx, Neg ny => - let (q, r) := N.div_eucl nx ny in + let (q, r) := NN.div_eucl nx ny in (Pos q, Neg r) end. Ltac break_nonneg x px EQx := let H := fresh "H" in - assert (H:=N.spec_pos x); - destruct (N.to_Z x) as [|px|px]_eqn:EQx; + assert (H:=NN.spec_pos x); + destruct (NN.to_Z x) as [|px|px] eqn:EQx; [clear H|clear H|elim H; reflexivity]. Theorem spec_div_eucl: forall x y, let (q,r) := div_eucl x y in - (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y). + (to_Z q, to_Z r) = Z.div_eucl (to_Z x) (to_Z y). Proof. unfold div_eucl, to_Z. intros [x | x] [y | y]. (* Pos Pos *) - generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y); auto. + generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y); auto. (* Pos Neg *) - generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r). + generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite N.spec_eqb, N.spec_0, Hr; - simpl; rewrite Hq, N.spec_0; auto). + try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr; + simpl; rewrite Hq, NN.spec_0; auto). change (- Zpos py) with (Zneg py). assert (GT : Zpos py > 0) by (compute; auto). generalize (Z_div_mod (Zpos px) (Zpos py) GT). - unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r'). + unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). intros (EQ,MOD). injection 1. intros Hr' Hq'. - rewrite N.spec_eqb, N.spec_0, Hr'. + rewrite NN.spec_eqb, NN.spec_0, Hr'. break_nonneg r pr EQr. - subst; simpl. rewrite N.spec_0; auto. + subst; simpl. rewrite NN.spec_0; auto. subst. lazy iota beta delta [Z.eqb]. - rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *. + rewrite NN.spec_sub, NN.spec_succ, EQy, EQr. f_equal. omega with *. (* Neg Pos *) - generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r). + generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite N.spec_eqb, N.spec_0, Hr; - simpl; rewrite Hq, N.spec_0; auto). + try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr; + simpl; rewrite Hq, NN.spec_0; auto). change (- Zpos px) with (Zneg px). assert (GT : Zpos py > 0) by (compute; auto). generalize (Z_div_mod (Zpos px) (Zpos py) GT). - unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r'). + unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). intros (EQ,MOD). injection 1. intros Hr' Hq'. - rewrite N.spec_eqb, N.spec_0, Hr'. + rewrite NN.spec_eqb, NN.spec_0, Hr'. break_nonneg r pr EQr. - subst; simpl. rewrite N.spec_0; auto. + subst; simpl. rewrite NN.spec_0; auto. subst. lazy iota beta delta [Z.eqb]. - rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *. + rewrite NN.spec_sub, NN.spec_succ, EQy, EQr. f_equal. omega with *. (* Neg Neg *) - generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r). + generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; try (injection 1; intros Hr Hq; rewrite Hr, Hq; auto). simpl. intros <-; auto. @@ -468,8 +468,8 @@ Module Make (N:NType) <: ZType. Definition spec_div: forall x y, to_Z (div x y) = to_Z x / to_Z y. Proof. - intros x y; generalize (spec_div_eucl x y); unfold div, Zdiv. - case div_eucl; case Zdiv_eucl; simpl; auto. + intros x y; generalize (spec_div_eucl x y); unfold div, Z.div. + case div_eucl; case Z.div_eucl; simpl; auto. intros q r q11 r1 H; injection H; auto. Qed. @@ -478,38 +478,38 @@ Module Make (N:NType) <: ZType. Theorem spec_modulo: forall x y, to_Z (modulo x y) = to_Z x mod to_Z y. Proof. - intros x y; generalize (spec_div_eucl x y); unfold modulo, Zmod. - case div_eucl; case Zdiv_eucl; simpl; auto. + intros x y; generalize (spec_div_eucl x y); unfold modulo, Z.modulo. + case div_eucl; case Z.div_eucl; simpl; auto. intros q r q11 r1 H; injection H; auto. Qed. Definition quot x y := match x, y with - | Pos nx, Pos ny => Pos (N.div nx ny) - | Pos nx, Neg ny => Neg (N.div nx ny) - | Neg nx, Pos ny => Neg (N.div nx ny) - | Neg nx, Neg ny => Pos (N.div nx ny) + | Pos nx, Pos ny => Pos (NN.div nx ny) + | Pos nx, Neg ny => Neg (NN.div nx ny) + | Neg nx, Pos ny => Neg (NN.div nx ny) + | Neg nx, Neg ny => Pos (NN.div nx ny) end. Definition rem x y := if eqb y zero then x else match x, y with - | Pos nx, Pos ny => Pos (N.modulo nx ny) - | Pos nx, Neg ny => Pos (N.modulo nx ny) - | Neg nx, Pos ny => Neg (N.modulo nx ny) - | Neg nx, Neg ny => Neg (N.modulo nx ny) + | Pos nx, Pos ny => Pos (NN.modulo nx ny) + | Pos nx, Neg ny => Pos (NN.modulo nx ny) + | Neg nx, Pos ny => Neg (NN.modulo nx ny) + | Neg nx, Neg ny => Neg (NN.modulo nx ny) end. Lemma spec_quot : forall x y, to_Z (quot x y) = (to_Z x) ÷ (to_Z y). Proof. - intros [x|x] [y|y]; simpl; symmetry; rewrite N.spec_div; + intros [x|x] [y|y]; simpl; symmetry; rewrite NN.spec_div; (* Nota: we rely here on [forall a b, a ÷ 0 = b / 0] *) - destruct (Z.eq_dec (N.to_Z y) 0) as [EQ|NEQ]; - try (rewrite EQ; now destruct (N.to_Z x)); + destruct (Z.eq_dec (NN.to_Z y) 0) as [EQ|NEQ]; + try (rewrite EQ; now destruct (NN.to_Z x)); rewrite ?Z.quot_opp_r, ?Z.quot_opp_l, ?Z.opp_involutive, ?Z.opp_inj_wd; trivial; apply Z.quot_div_nonneg; - generalize (N.spec_pos x) (N.spec_pos y); Z.order. + generalize (NN.spec_pos x) (NN.spec_pos y); Z.order. Qed. Lemma spec_rem : forall x y, @@ -521,26 +521,26 @@ Module Make (N:NType) <: ZType. rewrite Hy. now destruct (to_Z x). destruct x as [x|x], y as [y|y]; simpl in *; symmetry; rewrite ?Z.eq_opp_l, ?Z.opp_0 in Hy; - rewrite N.spec_modulo, ?Z.rem_opp_r, ?Z.rem_opp_l, ?Z.opp_involutive, + rewrite NN.spec_modulo, ?Z.rem_opp_r, ?Z.rem_opp_l, ?Z.opp_involutive, ?Z.opp_inj_wd; trivial; apply Z.rem_mod_nonneg; - generalize (N.spec_pos x) (N.spec_pos y); Z.order. + generalize (NN.spec_pos x) (NN.spec_pos y); Z.order. Qed. Definition gcd x y := match x, y with - | Pos nx, Pos ny => Pos (N.gcd nx ny) - | Pos nx, Neg ny => Pos (N.gcd nx ny) - | Neg nx, Pos ny => Pos (N.gcd nx ny) - | Neg nx, Neg ny => Pos (N.gcd nx ny) + | Pos nx, Pos ny => Pos (NN.gcd nx ny) + | Pos nx, Neg ny => Pos (NN.gcd nx ny) + | Neg nx, Pos ny => Pos (NN.gcd nx ny) + | Neg nx, Neg ny => Pos (NN.gcd nx ny) end. - Theorem spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (to_Z a) (to_Z b). + Theorem spec_gcd: forall a b, to_Z (gcd a b) = Z.gcd (to_Z a) (to_Z b). Proof. - unfold gcd, Zgcd, to_Z; intros [x | x] [y | y]; rewrite N.spec_gcd; unfold Zgcd; - auto; case N.to_Z; simpl; auto with zarith; - try rewrite Zabs_Zopp; auto; - case N.to_Z; simpl; auto with zarith. + unfold gcd, Z.gcd, to_Z; intros [x | x] [y | y]; rewrite NN.spec_gcd; unfold Z.gcd; + auto; case NN.to_Z; simpl; auto with zarith; + try rewrite Z.abs_opp; auto; + case NN.to_Z; simpl; auto with zarith. Qed. Definition sgn x := @@ -550,124 +550,124 @@ Module Make (N:NType) <: ZType. | Gt => minus_one end. - Lemma spec_sgn : forall x, to_Z (sgn x) = Zsgn (to_Z x). + Lemma spec_sgn : forall x, to_Z (sgn x) = Z.sgn (to_Z x). Proof. - intros. unfold sgn. rewrite spec_compare. case Zcompare_spec. + intros. unfold sgn. rewrite spec_compare. case Z.compare_spec. rewrite spec_0. intros <-; auto. - rewrite spec_0, spec_1. symmetry. rewrite Zsgn_pos; auto. - rewrite spec_0, spec_m1. symmetry. rewrite Zsgn_neg; auto with zarith. + rewrite spec_0, spec_1. symmetry. rewrite Z.sgn_pos_iff; auto. + rewrite spec_0, spec_m1. symmetry. rewrite Z.sgn_neg_iff; auto with zarith. Qed. Definition even z := match z with - | Pos n => N.even n - | Neg n => N.even n + | Pos n => NN.even n + | Neg n => NN.even n end. Definition odd z := match z with - | Pos n => N.odd n - | Neg n => N.odd n + | Pos n => NN.odd n + | Neg n => NN.odd n end. - Lemma spec_even : forall z, even z = Zeven_bool (to_Z z). + Lemma spec_even : forall z, even z = Z.even (to_Z z). Proof. - intros [n|n]; simpl; rewrite N.spec_even; trivial. - destruct (N.to_Z n) as [|p|p]; now try destruct p. + intros [n|n]; simpl; rewrite NN.spec_even; trivial. + destruct (NN.to_Z n) as [|p|p]; now try destruct p. Qed. - Lemma spec_odd : forall z, odd z = Zodd_bool (to_Z z). + Lemma spec_odd : forall z, odd z = Z.odd (to_Z z). Proof. - intros [n|n]; simpl; rewrite N.spec_odd; trivial. - destruct (N.to_Z n) as [|p|p]; now try destruct p. + intros [n|n]; simpl; rewrite NN.spec_odd; trivial. + destruct (NN.to_Z n) as [|p|p]; now try destruct p. Qed. Definition norm_pos z := match z with | Pos _ => z - | Neg n => if N.eqb n N.zero then Pos n else z + | Neg n => if NN.eqb n NN.zero then Pos n else z end. Definition testbit a n := match norm_pos n, norm_pos a with - | Pos p, Pos a => N.testbit a p - | Pos p, Neg a => negb (N.testbit (N.pred a) p) + | Pos p, Pos a => NN.testbit a p + | Pos p, Neg a => negb (NN.testbit (NN.pred a) p) | Neg p, _ => false end. Definition shiftl a n := match norm_pos a, n with - | Pos a, Pos n => Pos (N.shiftl a n) - | Pos a, Neg n => Pos (N.shiftr a n) - | Neg a, Pos n => Neg (N.shiftl a n) - | Neg a, Neg n => Neg (N.succ (N.shiftr (N.pred a) n)) + | Pos a, Pos n => Pos (NN.shiftl a n) + | Pos a, Neg n => Pos (NN.shiftr a n) + | Neg a, Pos n => Neg (NN.shiftl a n) + | Neg a, Neg n => Neg (NN.succ (NN.shiftr (NN.pred a) n)) end. Definition shiftr a n := shiftl a (opp n). Definition lor a b := match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (N.lor a b) - | Neg a, Pos b => Neg (N.succ (N.ldiff (N.pred a) b)) - | Pos a, Neg b => Neg (N.succ (N.ldiff (N.pred b) a)) - | Neg a, Neg b => Neg (N.succ (N.land (N.pred a) (N.pred b))) + | Pos a, Pos b => Pos (NN.lor a b) + | Neg a, Pos b => Neg (NN.succ (NN.ldiff (NN.pred a) b)) + | Pos a, Neg b => Neg (NN.succ (NN.ldiff (NN.pred b) a)) + | Neg a, Neg b => Neg (NN.succ (NN.land (NN.pred a) (NN.pred b))) end. Definition land a b := match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (N.land a b) - | Neg a, Pos b => Pos (N.ldiff b (N.pred a)) - | Pos a, Neg b => Pos (N.ldiff a (N.pred b)) - | Neg a, Neg b => Neg (N.succ (N.lor (N.pred a) (N.pred b))) + | Pos a, Pos b => Pos (NN.land a b) + | Neg a, Pos b => Pos (NN.ldiff b (NN.pred a)) + | Pos a, Neg b => Pos (NN.ldiff a (NN.pred b)) + | Neg a, Neg b => Neg (NN.succ (NN.lor (NN.pred a) (NN.pred b))) end. Definition ldiff a b := match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (N.ldiff a b) - | Neg a, Pos b => Neg (N.succ (N.lor (N.pred a) b)) - | Pos a, Neg b => Pos (N.land a (N.pred b)) - | Neg a, Neg b => Pos (N.ldiff (N.pred b) (N.pred a)) + | Pos a, Pos b => Pos (NN.ldiff a b) + | Neg a, Pos b => Neg (NN.succ (NN.lor (NN.pred a) b)) + | Pos a, Neg b => Pos (NN.land a (NN.pred b)) + | Neg a, Neg b => Pos (NN.ldiff (NN.pred b) (NN.pred a)) end. Definition lxor a b := match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (N.lxor a b) - | Neg a, Pos b => Neg (N.succ (N.lxor (N.pred a) b)) - | Pos a, Neg b => Neg (N.succ (N.lxor a (N.pred b))) - | Neg a, Neg b => Pos (N.lxor (N.pred a) (N.pred b)) + | Pos a, Pos b => Pos (NN.lxor a b) + | Neg a, Pos b => Neg (NN.succ (NN.lxor (NN.pred a) b)) + | Pos a, Neg b => Neg (NN.succ (NN.lxor a (NN.pred b))) + | Neg a, Neg b => Pos (NN.lxor (NN.pred a) (NN.pred b)) end. Definition div2 x := shiftr x one. Lemma Zlnot_alt1 : forall x, -(x+1) = Z.lnot x. Proof. - unfold Z.lnot, Zpred; auto with zarith. + unfold Z.lnot, Z.pred; auto with zarith. Qed. Lemma Zlnot_alt2 : forall x, Z.lnot (x-1) = -x. Proof. - unfold Z.lnot, Zpred; auto with zarith. + unfold Z.lnot, Z.pred; auto with zarith. Qed. Lemma Zlnot_alt3 : forall x, Z.lnot (-x) = x-1. Proof. - unfold Z.lnot, Zpred; auto with zarith. + unfold Z.lnot, Z.pred; auto with zarith. Qed. Lemma spec_norm_pos : forall x, to_Z (norm_pos x) = to_Z x. Proof. intros [x|x]; simpl; trivial. - rewrite N.spec_eqb, N.spec_0. + rewrite NN.spec_eqb, NN.spec_0. case Z.eqb_spec; simpl; auto with zarith. Qed. Lemma spec_norm_pos_pos : forall x y, norm_pos x = Neg y -> - 0 < N.to_Z y. + 0 < NN.to_Z y. Proof. intros [x|x] y; simpl; try easy. - rewrite N.spec_eqb, N.spec_0. + rewrite NN.spec_eqb, NN.spec_0. case Z.eqb_spec; simpl; try easy. - inversion 2. subst. generalize (N.spec_pos y); auto with zarith. + inversion 2. subst. generalize (NN.spec_pos y); auto with zarith. Qed. Ltac destr_norm_pos x := @@ -682,9 +682,9 @@ Module Make (N:NType) <: ZType. Proof. intros x p. unfold testbit. destr_norm_pos p; simpl. destr_norm_pos x; simpl. - apply N.spec_testbit. - rewrite N.spec_testbit, N.spec_pred, Zmax_r by auto with zarith. - symmetry. apply Z.bits_opp. apply N.spec_pos. + apply NN.spec_testbit. + rewrite NN.spec_testbit, NN.spec_pred, Z.max_r by auto with zarith. + symmetry. apply Z.bits_opp. apply NN.spec_pos. symmetry. apply Z.testbit_neg_r; auto with zarith. Qed. @@ -692,13 +692,13 @@ Module Make (N:NType) <: ZType. Proof. intros x p. unfold shiftl. destr_norm_pos x; destruct p as [p|p]; simpl; - assert (Hp := N.spec_pos p). - apply N.spec_shiftl. - rewrite Z.shiftl_opp_r. apply N.spec_shiftr. - rewrite !N.spec_shiftl. - rewrite !Z.shiftl_mul_pow2 by apply N.spec_pos. - apply Zopp_mult_distr_l. - rewrite Z.shiftl_opp_r, N.spec_succ, N.spec_shiftr, N.spec_pred, Zmax_r + assert (Hp := NN.spec_pos p). + apply NN.spec_shiftl. + rewrite Z.shiftl_opp_r. apply NN.spec_shiftr. + rewrite !NN.spec_shiftl. + rewrite !Z.shiftl_mul_pow2 by apply NN.spec_pos. + symmetry. apply Z.mul_opp_l. + rewrite Z.shiftl_opp_r, NN.spec_succ, NN.spec_shiftr, NN.spec_pred, Z.max_r by auto with zarith. now rewrite Zlnot_alt1, Z.lnot_shiftr, Zlnot_alt2. Qed. @@ -713,8 +713,8 @@ Module Make (N:NType) <: ZType. Proof. intros x y. unfold land. destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?N.spec_succ, ?N.spec_land, ?N.spec_ldiff, ?N.spec_lor, - ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1; auto with zarith. + rewrite ?NN.spec_succ, ?NN.spec_land, ?NN.spec_ldiff, ?NN.spec_lor, + ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith. now rewrite Z.ldiff_land, Zlnot_alt2. now rewrite Z.ldiff_land, Z.land_comm, Zlnot_alt2. now rewrite Z.lnot_lor, !Zlnot_alt2. @@ -724,8 +724,8 @@ Module Make (N:NType) <: ZType. Proof. intros x y. unfold lor. destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?N.spec_succ, ?N.spec_land, ?N.spec_ldiff, ?N.spec_lor, - ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1; auto with zarith. + rewrite ?NN.spec_succ, ?NN.spec_land, ?NN.spec_ldiff, ?NN.spec_lor, + ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith. now rewrite Z.lnot_ldiff, Z.lor_comm, Zlnot_alt2. now rewrite Z.lnot_ldiff, Zlnot_alt2. now rewrite Z.lnot_land, !Zlnot_alt2. @@ -735,8 +735,8 @@ Module Make (N:NType) <: ZType. Proof. intros x y. unfold ldiff. destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?N.spec_succ, ?N.spec_land, ?N.spec_ldiff, ?N.spec_lor, - ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1; auto with zarith. + rewrite ?NN.spec_succ, ?NN.spec_land, ?NN.spec_ldiff, ?NN.spec_lor, + ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith. now rewrite Z.ldiff_land, Zlnot_alt3. now rewrite Z.lnot_lor, Z.ldiff_land, <- Zlnot_alt2. now rewrite 2 Z.ldiff_land, Zlnot_alt2, Z.land_comm, Zlnot_alt3. @@ -746,7 +746,7 @@ Module Make (N:NType) <: ZType. Proof. intros x y. unfold lxor. destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?N.spec_succ, ?N.spec_lxor, ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1; + rewrite ?NN.spec_succ, ?NN.spec_lxor, ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith. now rewrite !Z.lnot_lxor_r, Zlnot_alt2. now rewrite !Z.lnot_lxor_l, Zlnot_alt2. diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index d7c0abd8..fc600eae 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.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 *) @@ -36,7 +36,7 @@ End TestOrder. (** Z forms a ring *) -(*Lemma Zring : ring_theory 0 1 NZadd NZmul NZsub Zopp NZeq. +(*Lemma Zring : ring_theory 0 1 NZadd NZmul NZsub Z.opp NZeq. Proof. constructor. exact Zadd_0_l. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index dbcc1961..b5e1fa5b 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.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 *) @@ -59,7 +59,7 @@ Definition le (n m : t) := n#1 + m#2 <= m#1 + n#2. Definition min (n m : t) : t := (min (n#1 + m#2) (m#1 + n#2), n#2 + m#2). Definition max (n m : t) : t := (max (n#1 + m#2) (m#1 + n#2), n#2 + m#2). -(** NB : We do not have [Zpred (Zsucc n) = n] but only [Zpred (Zsucc n) == n]. +(** NB : We do not have [Z.pred (Z.succ n) = n] but only [Z.pred (Z.succ n) == n]. It could be possible to consider as canonical only pairs where one of the elements is 0, and make all operations convert canonical values into other canonical values. In that case, we diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index 98ac5dfc..0a26a910 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.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/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index bfbc063c..e2ec3482 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.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 *) @@ -93,7 +93,7 @@ replace z with (-(-z))%Z in * by (auto with zarith). remember (-z)%Z as z'. pattern z'; apply natlike_ind. apply B0. -intros; rewrite Zopp_succ; unfold Zpred; apply BP; auto. +intros; rewrite Z.opp_succ; unfold Z.pred; apply BP; auto. subst z'; auto with zarith. Qed. @@ -364,7 +364,7 @@ Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. Theorem div_mod : forall a b, ~b==0 -> a == b*(div a b) + (modulo a b). Proof. -intros a b. zify. intros. apply Z_div_mod_eq_full; auto. +intros a b. zify. intros. apply Z.div_mod; auto. Qed. Theorem mod_pos_bound : |