aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-07-01 17:38:17 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-07-01 17:38:17 +0000
commitd2204e78c2d8bfc4f46ba541749b07dedd5e7969 (patch)
treed2c9de4d986dc2f37744fad6f434ddac1506a8e0
parentae95b79d0912a7b1a5370854cb6fb1aadb1db6b2 (diff)
Cleanup of files related with power over Z.
- Zpow_def, Zpower, Zpow_facts shortened thanks to stuff in BinInt.Z - The alternative Zpower_alt is now in a separate file Zpow_alt.v, not loaded by default. - Some more injection lemmas in Znat (pow, div, mod, quot, rem) - Btw, added a "square" function in Z, N, Pos, ... (instead of Zpow_facts.Zsquare). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14253 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--theories/NArith/BinNat.v7
-rw-r--r--theories/NArith/BinNatDef.v8
-rw-r--r--theories/Numbers/Integer/Abstract/ZAxioms.v4
-rw-r--r--theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v9
-rw-r--r--theories/Numbers/NatInt/NZAxioms.v6
-rw-r--r--theories/Numbers/Natural/Abstract/NAxioms.v4
-rw-r--r--theories/Numbers/Natural/Peano/NPeano.v8
-rw-r--r--theories/Numbers/Natural/SpecViaZ/NSig.v2
-rw-r--r--theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v11
-rw-r--r--theories/PArith/BinPos.v10
-rw-r--r--theories/PArith/BinPosDef.v9
-rw-r--r--theories/ZArith/BinInt.v14
-rw-r--r--theories/ZArith/BinIntDef.v9
-rw-r--r--theories/ZArith/Znat.v119
-rw-r--r--theories/ZArith/Zpow_alt.v83
-rw-r--r--theories/ZArith/Zpow_def.v109
-rw-r--r--theories/ZArith/Zpow_facts.v506
-rw-r--r--theories/ZArith/Zpower.v372
-rw-r--r--theories/ZArith/vo.itarget1
19 files changed, 635 insertions, 656 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 228be4d1a..418fd8e58 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -442,6 +442,13 @@ Proof.
now destruct p.
Qed.
+(** Specification of square *)
+
+Lemma square_spec n : square n = n * n.
+Proof.
+ destruct n; trivial. simpl. f_equal. apply Pos.square_spec.
+Qed.
+
(** Specification of Base-2 logarithm *)
Lemma size_log2 n : n<>0 -> size n = succ (log2 n).
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index d459f8509..d7660422a 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -181,6 +181,14 @@ Definition pow n p :=
Infix "^" := pow : N_scope.
+(** Square *)
+
+Definition square n :=
+ match n with
+ | 0 => 0
+ | Npos p => Npos (Pos.square p)
+ end.
+
(** Base-2 logarithm *)
Definition log2 n :=
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index a5be98aab..fd20ce725 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -114,9 +114,9 @@ Module Type ZQuot' (Z:ZAxiomsMiniSig) := QuotRem' Z <+ QuotRemSpec Z.
Module Type ZAxiomsSig := ZAxiomsMiniSig <+ OrderFunctions
<+ HasAbs <+ HasSgn <+ NZParity.NZParity
<+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd
- <+ ZDiv <+ ZQuot <+ NZBits.NZBits.
+ <+ ZDiv <+ ZQuot <+ NZBits.NZBits <+ NZSquare.
Module Type ZAxiomsSig' := ZAxiomsMiniSig' <+ OrderFunctions'
<+ HasAbs <+ HasSgn <+ NZParity.NZParity
<+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd'
- <+ ZDiv' <+ ZQuot' <+ NZBits.NZBits'.
+ <+ ZDiv' <+ ZQuot' <+ NZBits.NZBits' <+ NZSquare.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 5a0f590ba..bfbc063ce 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -14,7 +14,7 @@ Module ZTypeIsZAxioms (Import ZZ : ZType').
Hint Rewrite
spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
- spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt
+ spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_square spec_sqrt
spec_compare spec_eqb spec_ltb spec_leb spec_max spec_min
spec_abs spec_sgn spec_pow spec_log2 spec_even spec_odd spec_gcd
spec_quot spec_rem spec_testbit spec_shiftl spec_shiftr
@@ -303,6 +303,13 @@ Proof.
intros a b. red. now rewrite spec_pow_N, spec_pow_pos.
Qed.
+(** Square *)
+
+Lemma square_spec n : square n == n * n.
+Proof.
+ now zify.
+Qed.
+
(** Sqrt *)
Lemma sqrt_spec : forall n, 0<=n ->
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 4dedcfe32..fcd98787f 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -137,3 +137,9 @@ Module Type NZDecOrdSig' := NZOrdSig' <+ HasCompare.
Module Type NZDecOrdAxiomsSig := NZOrdAxiomsSig <+ HasCompare.
Module Type NZDecOrdAxiomsSig' := NZOrdAxiomsSig' <+ HasCompare.
+(** A square function *)
+
+Module Type NZSquare (Import NZ : NZBasicFunsSig').
+ Parameter Inline square : t -> t.
+ Axiom square_spec : forall n, square n == n * n.
+End NZSquare.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 45a2cf3e1..ca6ccc1bf 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -34,11 +34,11 @@ End NDivSpecific.
Module Type NAxiomsSig := NAxiomsMiniSig <+ OrderFunctions
<+ NZParity.NZParity <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2
- <+ NZGcd.NZGcd <+ NZDiv.NZDiv <+ NZBits.NZBits.
+ <+ NZGcd.NZGcd <+ NZDiv.NZDiv <+ NZBits.NZBits <+ NZSquare.
Module Type NAxiomsSig' := NAxiomsMiniSig' <+ OrderFunctions'
<+ NZParity.NZParity <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2
- <+ NZGcd.NZGcd' <+ NZDiv.NZDiv' <+ NZBits.NZBits'.
+ <+ NZGcd.NZGcd' <+ NZDiv.NZDiv' <+ NZBits.NZBits' <+ NZSquare.
(** It could also be interesting to have a constructive recursor function. *)
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index b6b26363e..d5df6329a 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -53,6 +53,11 @@ Proof. reflexivity. Qed.
Lemma pow_succ_r : forall a b, 0<=b -> a^(S b) = a * a^b.
Proof. reflexivity. Qed.
+Definition square n := n * n.
+
+Lemma square_spec n : square n = n * n.
+Proof. reflexivity. Qed.
+
Definition Even n := exists m, n = 2*m.
Definition Odd n := exists m, n = 2*m+1.
@@ -737,6 +742,9 @@ Definition pow_succ_r := pow_succ_r.
Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. inversion 1. Qed.
Definition pow := pow.
+Definition square := square.
+Definition square_spec := square_spec.
+
Definition log2_spec := log2_spec.
Definition log2_nonpos := log2_nonpos.
Definition log2 := log2.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index cfe842b9d..aaf44ca64 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -83,7 +83,7 @@ Module Type NType.
Parameter spec_pred: forall x, [pred x] = Z.max 0 ([x] - 1).
Parameter spec_sub: forall x y, [sub x y] = Z.max 0 ([x] - [y]).
Parameter spec_mul: forall x y, [mul x y] = [x] * [y].
- Parameter spec_square: forall x, [square x] = [x] * [x].
+ Parameter spec_square: forall x, [square x] = [x] * [x].
Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n.
Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z.of_N n.
Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n].
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index adbd8223a..a0ad7643d 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -15,8 +15,8 @@ Module NTypeIsNAxioms (Import NN : NType').
Hint Rewrite
spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub
spec_div spec_modulo spec_gcd spec_compare spec_eqb spec_ltb spec_leb
- spec_sqrt spec_log2 spec_max spec_min spec_pow_pos spec_pow_N spec_pow
- spec_even spec_odd spec_testbit spec_shiftl spec_shiftr
+ spec_square spec_sqrt spec_log2 spec_max spec_min spec_pow_pos spec_pow_N
+ spec_pow spec_even spec_odd spec_testbit spec_shiftl spec_shiftr
spec_land spec_lor spec_ldiff spec_lxor spec_div2 spec_of_N
: nsimpl.
Ltac nsimpl := autorewrite with nsimpl.
@@ -256,6 +256,13 @@ Proof.
intros. now zify.
Qed.
+(** Square *)
+
+Lemma square_spec n : square n == n * n.
+Proof.
+ now zify.
+Qed.
+
(** Sqrt *)
Lemma sqrt_spec : forall n, 0<=n ->
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 956421785..2e4d52a29 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -629,6 +629,16 @@ Proof.
unfold pow. now rewrite iter_succ.
Qed.
+(** ** Properties of square *)
+
+Lemma square_spec p : square p = p * p.
+Proof.
+ induction p.
+ - rewrite square_xI. simpl. now rewrite IHp.
+ - rewrite square_xO. simpl. now rewrite IHp.
+ - trivial.
+Qed.
+
(** ** Properties of [sub_mask] *)
Lemma sub_mask_succ_r p q :
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index b6b7ab7a5..7916511a4 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -210,6 +210,15 @@ Definition pow (x y:positive) := iter y (mul x) 1.
Infix "^" := pow : positive_scope.
+(** ** Square *)
+
+Fixpoint square p :=
+ match p with
+ | p~1 => (square p + p)~0~1
+ | p~0 => (square p)~0~0
+ | 1 => 1
+ end.
+
(** ** Division by 2 rounded below but for 1 *)
Definition div2 p :=
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 9e559b68c..4f6fb39c5 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -576,6 +576,20 @@ Proof.
now destruct m.
Qed.
+(** For folding back a [pow_pos] into a [pow] *)
+
+Lemma pow_pos_fold n p : pow_pos n p = n ^ (Zpos p).
+Proof.
+ reflexivity.
+Qed.
+
+(** ** Specification of square *)
+
+Lemma square_spec n : square n = n * n.
+Proof.
+ destruct n; trivial; simpl; f_equal; apply Pos.square_spec.
+Qed.
+
(** ** Specification of square root *)
Lemma sqrtrem_spec n : 0<=n ->
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index ee9051ff8..d96d20fbb 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -132,6 +132,15 @@ Definition pow x y :=
Infix "^" := pow : Z_scope.
+(** ** Square *)
+
+Definition square x :=
+ match x with
+ | 0 => 0
+ | Zpos p => Zpos (Pos.square p)
+ | Zneg p => Zpos (Pos.square p)
+ end.
+
(** ** Comparison *)
Definition compare x y :=
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 0ae5dea81..e3843990c 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -212,6 +212,36 @@ Proof.
case N.compare_spec; intros; subst; trivial.
Qed.
+Lemma inj_div n m : Z.of_N (n/m) = Z.of_N n / Z.of_N m.
+Proof.
+ destruct m as [|m]. now destruct n.
+ apply Z.div_unique_pos with (Z.of_N (n mod (Npos m))).
+ split. apply is_nonneg. apply inj_lt. now apply N.mod_lt.
+ rewrite <- inj_mul, <- inj_add. f_equal. now apply N.div_mod.
+Qed.
+
+Lemma inj_mod n m : (m<>0)%N -> Z.of_N (n mod m) = (Z.of_N n) mod (Z.of_N m).
+Proof.
+ intros Hm.
+ apply Z.mod_unique_pos with (Z.of_N (n / m)).
+ split. apply is_nonneg. apply inj_lt. now apply N.mod_lt.
+ rewrite <- inj_mul, <- inj_add. f_equal. now apply N.div_mod.
+Qed.
+
+Lemma inj_quot n m : Z.of_N (n/m) = Z.of_N n ÷ Z.of_N m.
+Proof.
+ destruct m.
+ - now destruct n.
+ - rewrite Z.quot_div_nonneg, inj_div; trivial. apply is_nonneg. easy.
+Qed.
+
+Lemma inj_rem n m : Z.of_N (n mod m) = Z.rem (Z.of_N n) (Z.of_N m).
+Proof.
+ destruct m.
+ - now destruct n.
+ - rewrite Z.rem_mod_nonneg, inj_mod; trivial. easy. apply is_nonneg. easy.
+Qed.
+
Lemma inj_div2 n : Z.of_N (N.div2 n) = Z.div2 (Z.of_N n).
Proof.
destruct n as [|p]; trivial. now destruct p.
@@ -222,6 +252,11 @@ Proof.
destruct n as [|p]; trivial. now destruct p.
Qed.
+Lemma inj_pow n m : Z.of_N (n^m) = (Z.of_N n)^(Z.of_N m).
+Proof.
+ symmetry. destruct n, m; trivial. now apply Z.pow_0_l. apply Z.pow_Zpos.
+Qed.
+
End N2Z.
Module Z2N.
@@ -323,6 +358,56 @@ Proof.
now case Pos.compare.
Qed.
+Lemma inj_div n m : 0<=n -> 0<=m -> Z.to_N (n/m) = (Z.to_N n / Z.to_N m)%N.
+Proof.
+ destruct n, m; trivial; intros Hn Hm;
+ (now destruct Hn) || (now destruct Hm) || clear.
+ simpl. rewrite <- (N2Z.id (_ / _)). f_equal. now rewrite N2Z.inj_div.
+Qed.
+
+Lemma inj_mod n m : 0<=n -> 0<m ->
+ Z.to_N (n mod m) = ((Z.to_N n) mod (Z.to_N m))%N.
+Proof.
+ destruct n, m; trivial; intros Hn Hm;
+ (now destruct Hn) || (now destruct Hm) || clear.
+ simpl. rewrite <- (N2Z.id (_ mod _)). f_equal. now rewrite N2Z.inj_mod.
+Qed.
+
+Lemma inj_quot n m : 0<=n -> 0<=m -> Z.to_N (n÷m) = (Z.to_N n / Z.to_N m)%N.
+Proof.
+ destruct m.
+ - now destruct n.
+ - intros. now rewrite Z.quot_div_nonneg, inj_div.
+ - now destruct 2.
+Qed.
+
+Lemma inj_rem n m :0<=n -> 0<=m ->
+ Z.to_N (Z.rem n m) = ((Z.to_N n) mod (Z.to_N m))%N.
+Proof.
+ destruct m.
+ - now destruct n.
+ - intros. now rewrite Z.rem_mod_nonneg, inj_mod.
+ - now destruct 2.
+Qed.
+
+Lemma inj_div2 n : Z.to_N (Z.div2 n) = N.div2 (Z.to_N n).
+Proof.
+ destruct n as [|p|p]; trivial. now destruct p.
+Qed.
+
+Lemma inj_quot2 n : Z.to_N (Z.quot2 n) = N.div2 (Z.to_N n).
+Proof.
+ destruct n as [|p|p]; trivial; now destruct p.
+Qed.
+
+Lemma inj_pow n m : 0<=n -> 0<=m -> Z.to_N (n^m) = ((Z.to_N n)^(Z.to_N m))%N.
+Proof.
+ destruct m.
+ - trivial.
+ - intros. now rewrite <- (N2Z.id (_ ^ _)), N2Z.inj_pow, id.
+ - now destruct 2.
+Qed.
+
End Z2N.
Module Zabs2N.
@@ -369,6 +454,11 @@ Qed.
(** [Z.abs_N] and usual operations, with non-negative integers *)
+Lemma inj_opp n : Z.abs_N (-n) = Z.abs_N n.
+Proof.
+ now destruct n.
+Qed.
+
Lemma inj_succ n : 0<=n -> Z.abs_N (Z.succ n) = N.succ (Z.abs_N n).
Proof.
intros. rewrite !abs_N_nonneg; trivial. now apply Z2N.inj_succ.
@@ -430,6 +520,35 @@ Proof.
transitivity n; trivial. apply Z.le_max_l.
Qed.
+Lemma inj_quot n m : Z.abs_N (n÷m) = ((Z.abs_N n) / (Z.abs_N m))%N.
+Proof.
+ assert (forall p q, Z.abs_N (Zpos p ÷ Zpos q) = (Npos p / Npos q)%N).
+ intros. rewrite abs_N_nonneg. now apply Z2N.inj_quot. now apply Z.quot_pos.
+ destruct n, m; trivial; simpl.
+ - trivial.
+ - now rewrite <- Z.opp_Zpos, Z.quot_opp_r, inj_opp.
+ - now rewrite <- Z.opp_Zpos, Z.quot_opp_l, inj_opp.
+ - now rewrite <- 2 Z.opp_Zpos, Z.quot_opp_opp.
+Qed.
+
+Lemma inj_rem n m : Z.abs_N (Z.rem n m) = ((Z.abs_N n) mod (Z.abs_N m))%N.
+Proof.
+ assert
+ (forall p q, Z.abs_N (Z.rem (Zpos p) (Zpos q)) = ((Npos p) mod (Npos q))%N).
+ intros. rewrite abs_N_nonneg. now apply Z2N.inj_rem. now apply Z.rem_nonneg.
+ destruct n, m; trivial; simpl.
+ - trivial.
+ - now rewrite <- Z.opp_Zpos, Z.rem_opp_r.
+ - now rewrite <- Z.opp_Zpos, Z.rem_opp_l, inj_opp.
+ - now rewrite <- 2 Z.opp_Zpos, Z.rem_opp_opp, inj_opp.
+Qed.
+
+Lemma inj_pow n m : 0<=m -> Z.abs_N (n^m) = ((Z.abs_N n)^(Z.abs_N m))%N.
+Proof.
+ intros Hm. rewrite abs_N_spec, Z.abs_pow, Z2N.inj_pow, <- abs_N_spec; trivial.
+ f_equal. symmetry; now apply abs_N_nonneg. apply Z.abs_nonneg.
+Qed.
+
(** [Z.abs_N] and usual operations, statements with [Z.abs] *)
Lemma inj_succ_abs n : Z.abs_N (Z.succ (Z.abs n)) = N.succ (Z.abs_N n).
diff --git a/theories/ZArith/Zpow_alt.v b/theories/ZArith/Zpow_alt.v
new file mode 100644
index 000000000..a90eedb41
--- /dev/null
+++ b/theories/ZArith/Zpow_alt.v
@@ -0,0 +1,83 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Import BinInt.
+Local Open Scope Z_scope.
+
+(** An alternative power function for Z *)
+
+(** This [Zpower_alt] is extensionnaly equal to [Z.pow],
+ but not convertible with it. The number of
+ multiplications is logarithmic instead of linear, but
+ these multiplications are bigger. Experimentally, it seems
+ that [Zpower_alt] is slightly quicker than [Z.pow] on average,
+ but can be quite slower on powers of 2.
+*)
+
+Definition Zpower_alt n m :=
+ match m with
+ | Z0 => 1
+ | Zpos p => Pos.iter_op Z.mul p n
+ | Zneg p => 0
+ end.
+
+Infix "^^" := Zpower_alt (at level 30, right associativity) : Z_scope.
+
+Lemma Piter_mul_acc : forall f,
+ (forall x y:Z, (f x)*y = f (x*y)) ->
+ forall p k, Pos.iter p f k = (Pos.iter p f 1)*k.
+Proof.
+ intros f Hf.
+ induction p; simpl; intros.
+ - set (g := Pos.iter p f 1) in *. now rewrite !IHp, Hf, Z.mul_assoc.
+ - set (g := Pos.iter p f 1) in *. now rewrite !IHp, Z.mul_assoc.
+ - now rewrite Hf, Z.mul_1_l.
+Qed.
+
+Lemma Piter_op_square : forall p a,
+ Pos.iter_op Z.mul p (a*a) = (Pos.iter_op Z.mul p a)*(Pos.iter_op Z.mul p a).
+Proof.
+ induction p; simpl; intros; trivial. now rewrite IHp, Z.mul_shuffle1.
+Qed.
+
+Lemma Zpower_equiv a b : a^^b = a^b.
+Proof.
+ destruct b as [|p|p]; trivial.
+ unfold Zpower_alt, Z.pow, Z.pow_pos.
+ revert a.
+ induction p; simpl; intros.
+ - f_equal.
+ rewrite Piter_mul_acc.
+ now rewrite Piter_op_square, IHp.
+ intros. symmetry; apply Z.mul_assoc.
+ - rewrite Piter_mul_acc.
+ now rewrite Piter_op_square, IHp.
+ intros. symmetry; apply Z.mul_assoc.
+ - now Z.nzsimpl.
+Qed.
+
+Lemma Zpower_alt_0_r n : n^^0 = 1.
+Proof. reflexivity. Qed.
+
+Lemma Zpower_alt_succ_r a b : 0<=b -> a^^(Z.succ b) = a * a^^b.
+Proof.
+ destruct b as [|b|b]; intros Hb; simpl.
+ - now Z.nzsimpl.
+ - now rewrite Pos.add_1_r, Pos.iter_op_succ by apply Z.mul_assoc.
+ - now elim Hb.
+Qed.
+
+Lemma Zpower_alt_neg_r a b : b<0 -> a^^b = 0.
+Proof.
+ now destruct b.
+Qed.
+
+Lemma Zpower_alt_Ppow p q : (Zpos p)^^(Zpos q) = Zpos (p^q).
+Proof.
+ now rewrite Zpower_equiv, Z.pow_Zpos.
+Qed.
diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v
index 8307f7601..6f1ebc061 100644
--- a/theories/ZArith/Zpow_def.v
+++ b/theories/ZArith/Zpow_def.v
@@ -6,115 +6,26 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-Require Import BinInt BinNat Ring_theory.
-
+Require Import BinInt Ring_theory.
Local Open Scope Z_scope.
-(** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
- integer (type [positive]) and [z] a signed integer (type [Z]) *)
+(** * Power functions over [Z] *)
+
+(** Nota : this file is mostly deprecated. The definition of [Z.pow]
+ and its usual properties are now provided by module [BinInt.Z]. *)
Notation Zpower_pos := Z.pow_pos (only parsing).
Notation Zpower := Z.pow (only parsing).
Notation Zpower_0_r := Z.pow_0_r (only parsing).
Notation Zpower_succ_r := Z.pow_succ_r (only parsing).
Notation Zpower_neg_r := Z.pow_neg_r (only parsing).
+Notation Zpower_Ppow := Z.pow_Zpos (only parsing).
-Lemma Zpower_theory : power_theory 1 Zmult (eq (A:=Z)) Z_of_N Zpower.
+Lemma Zpower_theory : power_theory 1 Z.mul (@eq Z) Z.of_N Z.pow.
Proof.
constructor. intros.
destruct n;simpl;trivial.
- unfold Zpower_pos.
- rewrite <- (Zmult_1_r (pow_pos _ _ _)). generalize 1.
- induction p; simpl; intros; rewrite ?IHp, ?Zmult_assoc; trivial.
-Qed.
-
-Lemma Zpower_Ppow : forall p q, (Zpos p)^(Zpos q) = Zpos (p^q).
-Proof.
- intros. unfold Ppow, Zpower, Zpower_pos.
- symmetry. now apply iter_pos_swap_gen.
-Qed.
-
-Lemma Zpower_Npow : forall n m,
- (Z_of_N n)^(Z_of_N m) = Z_of_N (n^m).
-Proof.
- intros [|n] [|m]; simpl; trivial.
- unfold Zpower_pos. generalize 1. induction m; simpl; trivial.
- apply Zpower_Ppow.
-Qed.
-
-(** An alternative Zpower *)
-
-(** This Zpower_alt is extensionnaly equal to Zpower in ZArith,
- but not convertible with it. The number of
- multiplications is logarithmic instead of linear, but
- these multiplications are bigger. Experimentally, it seems
- that Zpower_alt is slightly quicker than Zpower on average,
- but can be quite slower on powers of 2.
-*)
-
-Definition Zpower_alt n m :=
- match m with
- | Z0 => 1
- | Zpos p => Piter_op Zmult p n
- | Zneg p => 0
- end.
-
-Infix "^^" := Zpower_alt (at level 30, right associativity) : Z_scope.
-
-Lemma iter_pos_mult_acc : forall f,
- (forall x y:Z, (f x)*y = f (x*y)) ->
- forall p k, iter_pos p _ f k = (iter_pos p _ f 1)*k.
-Proof.
- intros f Hf.
- induction p; simpl; intros.
- rewrite IHp. rewrite Hf. f_equal. rewrite (IHp (iter_pos _ _ _ _)).
- rewrite <- Zmult_assoc. f_equal. auto.
- rewrite IHp. rewrite (IHp (iter_pos _ _ _ _)).
- rewrite <- Zmult_assoc. f_equal. auto.
- rewrite Hf. f_equal. now rewrite Zmult_1_l.
-Qed.
-
-Lemma Piter_op_square : forall p a,
- Piter_op Zmult p (a*a) = (Piter_op Zmult p a)*(Piter_op Zmult p a).
-Proof.
- induction p; simpl; intros; trivial.
- rewrite IHp. rewrite <- !Zmult_assoc. f_equal.
- rewrite Zmult_comm, <- Zmult_assoc.
- f_equal. apply Zmult_comm.
-Qed.
-
-Lemma Zpower_equiv : forall a b, a^^b = a^b.
-Proof.
- intros a [|p|p]; trivial.
- unfold Zpower_alt, Zpower, Zpower_pos.
- revert a.
- induction p; simpl; intros.
- f_equal.
- rewrite iter_pos_mult_acc.
- now rewrite Piter_op_square, IHp.
- intros. symmetry; apply Zmult_assoc.
- rewrite iter_pos_mult_acc.
- now rewrite Piter_op_square, IHp.
- intros. symmetry; apply Zmult_assoc.
- now rewrite Zmult_1_r.
-Qed.
-
-Lemma Zpower_alt_0_r : forall n, n^^0 = 1.
-Proof. reflexivity. Qed.
-
-Lemma Zpower_alt_succ_r : forall a b, 0<=b -> a^^(Zsucc b) = a * a^^b.
-Proof.
- intros a [|b|b] Hb; [ | |now elim Hb]; simpl.
- now rewrite Zmult_1_r.
- rewrite <- Pplus_one_succ_r. apply Piter_op_succ. apply Zmult_assoc.
-Qed.
-
-Lemma Zpower_alt_neg_r : forall a b, b<0 -> a^^b = 0.
-Proof.
- now destruct b.
-Qed.
-
-Lemma Zpower_alt_Ppow : forall p q, (Zpos p)^^(Zpos q) = Zpos (p^q).
-Proof.
- intros. now rewrite Zpower_equiv, Zpower_Ppow.
+ unfold Z.pow_pos.
+ rewrite <- (Z.mul_1_r (pow_pos _ _ _)). generalize 1.
+ induction p; simpl; intros; rewrite ?IHp, ?Z.mul_assoc; trivial.
Qed.
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index d9c5f995b..27e3def4e 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -6,288 +6,104 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-Require Import ZArith_base.
-Require Import ZArithRing.
-Require Import Zcomplements.
+Require Import ZArith_base ZArithRing Zcomplements Zdiv Znumtheory.
Require Export Zpower.
-Require Import Zdiv.
-Require Import Znumtheory.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
-Lemma Zpower_pos_1_r: forall x, Zpower_pos x 1 = x.
-Proof.
- intros x; unfold Zpower_pos; simpl; auto with zarith.
-Qed.
-
-Lemma Zpower_pos_1_l: forall p, Zpower_pos 1 p = 1.
-Proof.
- induction p.
- (* xI *)
- rewrite xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l.
- repeat rewrite Zpower_pos_is_exp.
- rewrite Zpower_pos_1_r, IHp; auto.
- (* xO *)
- rewrite <- Pplus_diag.
- repeat rewrite Zpower_pos_is_exp.
- rewrite IHp; auto.
- (* xH *)
- rewrite Zpower_pos_1_r; auto.
-Qed.
-
-Lemma Zpower_pos_0_l: forall p, Zpower_pos 0 p = 0.
-Proof.
- induction p.
- change (xI p) with (1 + (xO p))%positive.
- rewrite Zpower_pos_is_exp, Zpower_pos_1_r; auto.
- rewrite <- Pplus_diag.
- rewrite Zpower_pos_is_exp, IHp; auto.
- rewrite Zpower_pos_1_r; auto.
-Qed.
-
-Lemma Zpower_pos_pos: forall x p,
- 0 < x -> 0 < Zpower_pos x p.
-Proof.
- induction p; intros.
- (* xI *)
- rewrite xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l.
- repeat rewrite Zpower_pos_is_exp.
- rewrite Zpower_pos_1_r.
- repeat apply Zmult_lt_0_compat; auto.
- (* xO *)
- rewrite <- Pplus_diag.
- repeat rewrite Zpower_pos_is_exp.
- repeat apply Zmult_lt_0_compat; auto.
- (* xH *)
- rewrite Zpower_pos_1_r; auto.
-Qed.
-
-
-Theorem Zpower_1_r: forall z, z^1 = z.
-Proof.
- exact Zpower_pos_1_r.
-Qed.
-
-Theorem Zpower_1_l: forall z, 0 <= z -> 1^z = 1.
-Proof.
- destruct z; simpl; auto.
- intros; apply Zpower_pos_1_l.
- intros; compute in H; elim H; auto.
-Qed.
-
-Theorem Zpower_0_l: forall z, z<>0 -> 0^z = 0.
-Proof.
- destruct z; simpl; auto with zarith.
- intros; apply Zpower_pos_0_l.
-Qed.
+(** Properties of the power function over [Z] *)
-Theorem Zpower_0_r: forall z, z^0 = 1.
-Proof.
- simpl; auto.
-Qed.
+(** Nota: the usual properties of [Z.pow] are now already provided
+ by [BinInt.Z]. Only remain here some compatibility elements,
+ as well as more specific results about power and modulo and/or
+ primality. *)
-Theorem Zpower_2: forall z, z^2 = z * z.
-Proof.
- intros; ring.
-Qed.
+Lemma Zpower_pos_1_r x : Z.pow_pos x 1 = x.
+Proof (Z.pow_1_r x).
-Theorem Zpower_gt_0: forall x y,
- 0 < x -> 0 <= y -> 0 < x^y.
-Proof.
- destruct y; simpl; auto with zarith.
- intros; apply Zpower_pos_pos; auto.
- intros; compute in H0; elim H0; auto.
-Qed.
+Lemma Zpower_pos_1_l p : Z.pow_pos 1 p = 1.
+Proof. now apply (Z.pow_1_l (Zpos p)). Qed.
-Theorem Zpower_Zabs: forall a b, Zabs (a^b) = (Zabs a)^b.
-Proof.
- intros a b; case (Zle_or_lt 0 b).
- intros Hb; pattern b; apply natlike_ind; auto with zarith.
- intros x Hx Hx1; unfold Zsucc.
- (repeat rewrite Zpower_exp); auto with zarith.
- rewrite Zabs_Zmult; rewrite Hx1.
- f_equal; auto.
- replace (a ^ 1) with a; auto.
- simpl; unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto.
- simpl; unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto.
- case b; simpl; auto with zarith.
- intros p Hp; discriminate.
-Qed.
+Lemma Zpower_pos_0_l p : Z.pow_pos 0 p = 0.
+Proof. now apply (Z.pow_0_l (Zpos p)). Qed.
-Theorem Zpower_Zsucc: forall p n, 0 <= n -> p^(Zsucc n) = p * p^n.
-Proof.
- intros p n H.
- unfold Zsucc; rewrite Zpower_exp; auto with zarith.
- rewrite Zpower_1_r; apply Zmult_comm.
-Qed.
+Lemma Zpower_pos_pos x p : 0 < x -> 0 < Z.pow_pos x p.
+Proof. intros. now apply (Z.pow_pos_nonneg x (Zpos p)). Qed.
-Theorem Zpower_mult: forall p q r, 0 <= q -> 0 <= r -> p^(q*r) = (p^q)^r.
-Proof.
- intros p q r H1 H2; generalize H2; pattern r; apply natlike_ind; auto.
- intros H3; rewrite Zmult_0_r; repeat rewrite Zpower_exp_0; auto.
- intros r1 H3 H4 H5.
- unfold Zsucc; rewrite Zpower_exp; auto with zarith.
- rewrite <- H4; try rewrite Zpower_1_r; try rewrite <- Zpower_exp; try f_equal; auto with zarith.
- ring.
- apply Zle_ge; replace 0 with (0 * r1); try apply Zmult_le_compat_r; auto.
-Qed.
+Notation Zpower_1_r := Z.pow_1_r (only parsing).
+Notation Zpower_1_l := Z.pow_1_l (only parsing).
+Notation Zpower_0_l := Z.pow_0_l' (only parsing).
+Notation Zpower_0_r := Z.pow_0_r (only parsing).
+Notation Zpower_2 := Z.pow_2_r (only parsing).
+Notation Zpower_gt_0 := Z.pow_pos_nonneg (only parsing).
+Notation Zpower_ge_0 := Z.pow_nonneg (only parsing).
+Notation Zpower_Zabs := Z.abs_pow (only parsing).
+Notation Zpower_Zsucc := Z.pow_succ_r (only parsing).
+Notation Zpower_mult := Z.pow_mul_r (only parsing).
+Notation Zpower_le_monotone2 := Z.pow_le_mono_r (only parsing).
-Theorem Zpower_le_monotone: forall a b c,
+Theorem Zpower_le_monotone a b c :
0 < a -> 0 <= b <= c -> a^b <= a^c.
-Proof.
- intros a b c H (H1, H2).
- rewrite <- (Zmult_1_r (a ^ b)); replace c with (b + (c - b)); auto with zarith.
- rewrite Zpower_exp; auto with zarith.
- apply Zmult_le_compat_l; auto with zarith.
- assert (0 < a ^ (c - b)); auto with zarith.
- apply Zpower_gt_0; auto with zarith.
- apply Zlt_le_weak; apply Zpower_gt_0; auto with zarith.
-Qed.
+Proof. intros. now apply Z.pow_le_mono_r. Qed.
-Theorem Zpower_lt_monotone: forall a b c,
+Theorem Zpower_lt_monotone a b c :
1 < a -> 0 <= b < c -> a^b < a^c.
-Proof.
- intros a b c H (H1, H2).
- rewrite <- (Zmult_1_r (a ^ b)); replace c with (b + (c - b)); auto with zarith.
- rewrite Zpower_exp; auto with zarith.
- apply Zmult_lt_compat_l; auto with zarith.
- apply Zpower_gt_0; auto with zarith.
- assert (0 < a ^ (c - b)); auto with zarith.
- apply Zpower_gt_0; auto with zarith.
- apply Zlt_le_trans with (a ^1); auto with zarith.
- rewrite Zpower_1_r; auto with zarith.
- apply Zpower_le_monotone; auto with zarith.
-Qed.
-
-Theorem Zpower_gt_1 : forall x y,
- 1 < x -> 0 < y -> 1 < x^y.
-Proof.
- intros x y H1 H2.
- replace 1 with (x ^ 0) by apply Zpower_0_r.
- apply Zpower_lt_monotone; auto with zarith.
-Qed.
+Proof. intros. apply Z.pow_lt_mono_r; auto with zarith. Qed.
-Theorem Zpower_ge_0: forall x y, 0 <= x -> 0 <= x^y.
-Proof.
- intros x y; case y; auto with zarith.
- simpl ; auto with zarith.
- intros p H1; assert (H: 0 <= Zpos p); auto with zarith.
- generalize H; pattern (Zpos p); apply natlike_ind; auto with zarith.
- intros p1 H2 H3 _; unfold Zsucc; rewrite Zpower_exp; simpl; auto with zarith.
- apply Zmult_le_0_compat; auto with zarith.
- generalize H1; case x; compute; intros; auto; try discriminate.
-Qed.
-
-Theorem Zpower_le_monotone2:
- forall a b c, 0 < a -> b <= c -> a^b <= a^c.
-Proof.
- intros a b c H H2.
- destruct (Z_le_gt_dec 0 b) as [Hb|Hb].
- apply Zpower_le_monotone; auto.
- replace (a^b) with 0.
- destruct (Z_le_gt_dec 0 c) as [Hc|Hc].
- destruct (Zle_lt_or_eq _ _ Hc) as [Hc'|Hc'].
- apply Zlt_le_weak;apply Zpower_gt_0;trivial.
- rewrite <- Hc';simpl;auto with zarith.
- replace (a^c) with 0. auto with zarith.
- destruct c;trivial;unfold Zgt in Hc;discriminate Hc.
- destruct b;trivial;unfold Zgt in Hb;discriminate Hb.
-Qed.
+Theorem Zpower_gt_1 x y : 1 < x -> 0 < y -> 1 < x^y.
+Proof. apply Z.pow_gt_1. Qed.
-Theorem Zmult_power: forall p q r, 0 <= r ->
- (p*q)^r = p^r * q^r.
-Proof.
- intros p q r H1; generalize H1; pattern r; apply natlike_ind; auto.
- clear r H1; intros r H1 H2 H3.
- unfold Zsucc; rewrite Zpower_exp; auto with zarith.
- rewrite H2; repeat rewrite Zpower_exp; auto with zarith; ring.
-Qed.
+Theorem Zmult_power p q r : 0 <= r -> (p*q)^r = p^r * q^r.
+Proof. intros. apply Z.pow_mul_l. Qed.
-Hint Resolve Zpower_ge_0 Zpower_gt_0: zarith.
+Hint Resolve Z.pow_nonneg Z.pow_pos_nonneg : zarith.
-Theorem Zpower_le_monotone3: forall a b c,
+Theorem Zpower_le_monotone3 a b c :
0 <= c -> 0 <= a <= b -> a^c <= b^c.
-Proof.
- intros a b c H (H1, H2).
- generalize H; pattern c; apply natlike_ind; auto.
- intros x HH HH1 _; unfold Zsucc; repeat rewrite Zpower_exp; auto with zarith.
- repeat rewrite Zpower_1_r.
- apply Zle_trans with (a^x * b); auto with zarith.
-Qed.
+Proof. intros. now apply Z.pow_le_mono_l. Qed.
-Lemma Zpower_le_monotone_inv: forall a b c,
+Lemma Zpower_le_monotone_inv a b c :
1 < a -> 0 < b -> a^b <= a^c -> b <= c.
Proof.
- intros a b c H H0 H1.
- destruct (Z_le_gt_dec b c);trivial.
- assert (2 <= a^b).
- apply Zle_trans with (2^b).
- pattern 2 at 1;replace 2 with (2^1);trivial.
- apply Zpower_le_monotone;auto with zarith.
- apply Zpower_le_monotone3;auto with zarith.
- assert (c > 0).
- destruct (Z_le_gt_dec 0 c) as [Hc|Hc];trivial.
- destruct (Zle_lt_or_eq _ _ Hc);auto with zarith.
- rewrite <- H3 in H1;simpl in H1; exfalso;omega.
- destruct c;try discriminate Hc. simpl in H1. exfalso;omega.
- assert (H4 := Zpower_lt_monotone a c b H). exfalso;omega.
+ intros Ha Hb H. apply (Z.pow_le_mono_r_iff a); trivial.
+ apply Z.lt_le_incl; apply (Z.pow_gt_1 a); trivial.
+ apply Z.lt_le_trans with (a^b); trivial. now apply Z.pow_gt_1.
Qed.
-Theorem Zpower_nat_Zpower: forall p q, 0 <= q ->
- p^q = Zpower_nat p (Zabs_nat q).
-Proof.
- intros p1 q1; case q1; simpl.
- intros _; exact (refl_equal _).
- intros p2 _; apply Zpower_pos_nat.
- intros p2 H1; case H1; auto.
-Qed.
+Notation Zpower_nat_Zpower := Zpower_nat_Zpower (only parsing).
-Theorem Zpower2_lt_lin: forall n, 0 <= n -> n < 2^n.
-Proof.
- intros n; apply (natlike_ind (fun n => n < 2 ^n)); clear n.
- simpl; auto with zarith.
- intros n H1 H2; unfold Zsucc.
- case (Zle_lt_or_eq _ _ H1); clear H1; intros H1.
- apply Zle_lt_trans with (n + n); auto with zarith.
- rewrite Zpower_exp; auto with zarith.
- rewrite Zpower_1_r.
- assert (tmp: forall p, p * 2 = p + p); intros; try ring;
- rewrite tmp; auto with zarith.
- subst n; simpl; unfold Zpower_pos; simpl; auto with zarith.
-Qed.
+Theorem Zpower2_lt_lin n : 0 <= n -> n < 2^n.
+Proof. intros. now apply Z.pow_gt_lin_r. Qed.
-Theorem Zpower2_le_lin: forall n, 0 <= n -> n <= 2^n.
-Proof.
- intros; apply Zlt_le_weak; apply Zpower2_lt_lin; auto.
-Qed.
+Theorem Zpower2_le_lin n : 0 <= n -> n <= 2^n.
+Proof. intros. apply Z.lt_le_incl. now apply Z.pow_gt_lin_r. Qed.
-Lemma Zpower2_Psize :
- forall n p, Zpos p < 2^(Z_of_nat n) <-> (Psize p <= n)%nat.
+Lemma Zpower2_Psize n p :
+ Zpos p < 2^(Z.of_nat n) <-> (Pos.size_nat p <= n)%nat.
Proof.
- induction n.
- destruct p; split; intros H; discriminate H || inversion H.
- destruct p; simpl Psize.
- rewrite inj_S, Zpower_Zsucc; auto with zarith.
- rewrite Zpos_xI; specialize IHn with p; omega.
- rewrite inj_S, Zpower_Zsucc; auto with zarith.
- rewrite Zpos_xO; specialize IHn with p; omega.
- split; auto with arith.
- intros _; apply Zpower_gt_1; auto with zarith.
- rewrite inj_S; generalize (Zle_0_nat n); omega.
+ revert p; induction n.
+ destruct p; now split.
+ assert (Hn := Nat2Z.is_nonneg n).
+ destruct p; simpl Pos.size_nat.
+ - specialize IHn with p.
+ rewrite Z.pos_xI, Nat2Z.inj_succ, Z.pow_succ_r; omega.
+ - specialize IHn with p.
+ rewrite Z.pos_xO, Nat2Z.inj_succ, Z.pow_succ_r; omega.
+ - split; auto with zarith.
+ intros _. apply Z.pow_gt_1. easy.
+ now rewrite Nat2Z.inj_succ, Z.lt_succ_r.
Qed.
(** * Zpower and modulo *)
-Theorem Zpower_mod: forall p q n, 0 < n ->
- (p^q) mod n = ((p mod n)^q) mod n.
+Theorem Zpower_mod p q n :
+ 0 < n -> (p^q) mod n = ((p mod n)^q) mod n.
Proof.
- intros p q n Hn; case (Zle_or_lt 0 q); intros H1.
- generalize H1; pattern q; apply natlike_ind; auto.
- intros q1 Hq1 Rec _; unfold Zsucc; repeat rewrite Zpower_exp; repeat rewrite Zpower_1_r; auto with zarith.
- rewrite (fun x => (Zmult_mod x p)); try rewrite Rec; auto with zarith.
- rewrite (fun x y => (Zmult_mod (x ^y))); try f_equal; auto with zarith.
- f_equal; auto; apply sym_equal; apply Zmod_mod; auto with zarith.
- generalize H1; case q; simpl; auto.
- intros; discriminate.
+ intros Hn; destruct (Z.le_gt_cases 0 q) as [H1|H1].
+ - pattern q; apply natlike_ind; trivial.
+ clear q H1. intros q Hq Rec. rewrite !Z.pow_succ_r; trivial.
+ rewrite Z.mul_mod_idemp_l; auto with zarith.
+ rewrite Z.mul_mod, Rec, <- Z.mul_mod; auto with zarith.
+ - rewrite !Z.pow_neg_r; auto with zarith.
Qed.
(** A direct way to compute Zpower modulo **)
@@ -311,153 +127,113 @@ Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) : Z :=
Definition Zpow_mod a m n :=
match m with
- | 0 => 1
+ | 0 => 1 mod n
| Zpos p => Zpow_mod_pos a p n
| Zneg p => 0
end.
-Theorem Zpow_mod_pos_correct: forall a m n, 0 < n ->
- Zpow_mod_pos a m n = (Zpower_pos a m) mod n.
+Theorem Zpow_mod_pos_correct a m n :
+ n <> 0 -> Zpow_mod_pos a m n = (Z.pow_pos a m) mod n.
Proof.
- intros a m; elim m; simpl; auto.
- intros p Rec n H1; rewrite xI_succ_xO, Pplus_one_succ_r, <-Pplus_diag; auto.
- repeat rewrite Zpower_pos_is_exp; auto.
- repeat rewrite Rec; auto.
- rewrite Zpower_pos_1_r.
- repeat rewrite (fun x => (Zmult_mod x a)); auto with zarith.
- rewrite (Zmult_mod (Zpower_pos a p)); auto with zarith.
- case (Zpower_pos a p mod n); auto.
- intros p Rec n H1; rewrite <- Pplus_diag; auto.
- repeat rewrite Zpower_pos_is_exp; auto.
- repeat rewrite Rec; auto.
- rewrite (Zmult_mod (Zpower_pos a p)); auto with zarith.
- case (Zpower_pos a p mod n); auto.
- unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto with zarith.
+ intros Hn. induction m.
+ - rewrite Pos.xI_succ_xO at 2. rewrite <- Pos.add_1_r, <- Pos.add_diag.
+ rewrite 2 Zpower_pos_is_exp, Zpower_pos_1_r.
+ rewrite Z.mul_mod, (Z.mul_mod (Z.pow_pos a m)) by trivial.
+ rewrite <- IHm, <- Z.mul_mod by trivial.
+ simpl. now destruct (Zpow_mod_pos a m n).
+ - rewrite <- Pos.add_diag at 2.
+ rewrite Zpower_pos_is_exp.
+ rewrite Z.mul_mod by trivial.
+ rewrite <- IHm.
+ simpl. now destruct (Zpow_mod_pos a m n).
+ - now rewrite Zpower_pos_1_r.
Qed.
-Theorem Zpow_mod_correct: forall a m n, 1 < n -> 0 <= m ->
- Zpow_mod a m n = (a ^ m) mod n.
+Theorem Zpow_mod_correct a m n :
+ n <> 0 -> Zpow_mod a m n = (a ^ m) mod n.
Proof.
- intros a m n; case m; simpl.
- intros; apply sym_equal; apply Zmod_small; auto with zarith.
- intros; apply Zpow_mod_pos_correct; auto with zarith.
- intros p H H1; case H1; auto.
+ intros Hn. destruct m; simpl.
+ - trivial.
+ - apply Zpow_mod_pos_correct; auto with zarith.
+ - rewrite Z.mod_0_l; auto with zarith.
Qed.
(* Complements about power and number theory. *)
-Lemma Zpower_divide: forall p q, 0 < q -> (p | p ^ q).
+Lemma Zpower_divide p q : 0 < q -> (p | p ^ q).
Proof.
- intros p q H; exists (p ^(q - 1)).
- pattern p at 3; rewrite <- (Zpower_1_r p); rewrite <- Zpower_exp; try f_equal; auto with zarith.
+ exists (p^(q - 1)).
+ rewrite Z.mul_comm, <- Z.pow_succ_r; f_equal; auto with zarith.
Qed.
-Theorem rel_prime_Zpower_r: forall i p q, 0 < i ->
- rel_prime p q -> rel_prime p (q^i).
+Theorem rel_prime_Zpower_r i p q :
+ 0 <= i -> rel_prime p q -> rel_prime p (q^i).
Proof.
- intros i p q Hi Hpq; generalize Hi; pattern i; apply natlike_ind; auto with zarith; clear i Hi.
- intros H; contradict H; auto with zarith.
- intros i Hi Rec _; rewrite Zpower_Zsucc; auto.
+ intros Hi Hpq; pattern i; apply natlike_ind; auto with zarith.
+ simpl. apply rel_prime_sym, rel_prime_1.
+ clear i Hi. intros i Hi Rec; rewrite Z.pow_succ_r; auto.
apply rel_prime_mult; auto.
- case Zle_lt_or_eq with (1 := Hi); intros Hi1; subst; auto.
- rewrite Zpower_0_r; apply rel_prime_sym; apply rel_prime_1.
Qed.
-Theorem rel_prime_Zpower: forall i j p q, 0 <= i -> 0 <= j ->
- rel_prime p q -> rel_prime (p^i) (q^j).
+Theorem rel_prime_Zpower i j p q :
+ 0 <= i -> 0 <= j -> rel_prime p q -> rel_prime (p^i) (q^j).
Proof.
- intros i j p q Hi; generalize Hi j p q; pattern i; apply natlike_ind; auto with zarith; clear i Hi j p q.
- intros _ j p q H H1; rewrite Zpower_0_r; apply rel_prime_1.
- intros n Hn Rec _ j p q Hj Hpq.
- rewrite Zpower_Zsucc; auto.
- case Zle_lt_or_eq with (1 := Hj); intros Hj1; subst.
- apply rel_prime_sym; apply rel_prime_mult; auto.
- apply rel_prime_sym; apply rel_prime_Zpower_r; auto with arith.
- apply rel_prime_sym; apply Rec; auto.
- rewrite Zpower_0_r; apply rel_prime_sym; apply rel_prime_1.
+ intros Hi Hj H. apply rel_prime_Zpower_r; trivial.
+ apply rel_prime_sym. apply rel_prime_Zpower_r; trivial.
+ now apply rel_prime_sym.
Qed.
-Theorem prime_power_prime: forall p q n, 0 <= n ->
- prime p -> prime q -> (p | q^n) -> p = q.
+Theorem prime_power_prime p q n :
+ 0 <= n -> prime p -> prime q -> (p | q^n) -> p = q.
Proof.
- intros p q n Hn Hp Hq; pattern n; apply natlike_ind; auto; clear n Hn.
- rewrite Zpower_0_r; intros.
- assert (2<=p) by (apply prime_ge_2; auto).
- assert (p<=1) by (apply Zdivide_le; auto with zarith).
- omega.
- intros n1 H H1.
- unfold Zsucc; rewrite Zpower_exp; try rewrite Zpower_1_r; auto with zarith.
- assert (2<=p) by (apply prime_ge_2; auto).
- assert (2<=q) by (apply prime_ge_2; auto).
- intros H3; case prime_mult with (2 := H3); auto.
- intros; apply prime_div_prime; auto.
+ intros Hn Hp Hq; pattern n; apply natlike_ind; auto; clear n Hn.
+ - simpl; intros.
+ assert (2<=p) by (apply prime_ge_2; auto).
+ assert (p<=1) by (apply Z.divide_pos_le; auto with zarith).
+ omega.
+ - intros n Hn Rec.
+ rewrite Z.pow_succ_r by trivial. intros.
+ assert (2<=p) by (apply prime_ge_2; auto).
+ assert (2<=q) by (apply prime_ge_2; auto).
+ destruct prime_mult with (2 := H); auto.
+ apply prime_div_prime; auto.
Qed.
-Theorem Zdivide_power_2: forall x p n, 0 <= n -> 0 <= x -> prime p ->
- (x | p^n) -> exists m, x = p^m.
+Theorem Zdivide_power_2 x p n :
+ 0 <= n -> 0 <= x -> prime p -> (x | p^n) -> exists m, x = p^m.
Proof.
- intros x p n Hn Hx; revert p n Hn; generalize Hx.
+ intros Hn Hx; revert p n Hn. generalize Hx.
pattern x; apply Z_lt_induction; auto.
clear x Hx; intros x IH Hx p n Hn Hp H.
- case Zle_lt_or_eq with (1 := Hx); auto; clear Hx; intros Hx; subst.
- case (Zle_lt_or_eq 1 x); auto with zarith; clear Hx; intros Hx; subst.
+ Z.le_elim Hx; subst.
+ apply Z.le_succ_l in Hx; simpl in Hx.
+ Z.le_elim Hx; subst.
(* x > 1 *)
- case (prime_dec x); intros H2.
- exists 1; rewrite Zpower_1_r; apply prime_power_prime with n; auto.
- case not_prime_divide with (2 := H2); auto.
- intros p1 ((H3, H4), (q1, Hq1)); subst.
- case (IH p1) with p n; auto with zarith.
- apply Zdivide_trans with (2 := H); exists q1; auto with zarith.
- intros r1 Hr1.
- case (IH q1) with p n; auto with zarith.
- case (Zle_lt_or_eq 0 q1).
- apply Zmult_le_0_reg_r with p1; auto with zarith.
+ case (prime_dec x); intros Hpr.
+ exists 1; rewrite Z.pow_1_r; apply prime_power_prime with n; auto.
+ case not_prime_divide with (2 := Hpr); auto.
+ intros p1 ((Hp1, Hpq1),(q1,->)).
+ assert (Hq1 : 0 < q1) by (apply Z.mul_lt_mono_pos_r with p1; auto with zarith).
+ destruct (IH p1) with p n as (r1,Hr1); auto with zarith.
+ transitivity (q1 * p1); trivial. exists q1; auto with zarith.
+ destruct (IH q1) with p n as (r2,Hr2); auto with zarith.
split; auto with zarith.
- pattern q1 at 1; replace q1 with (q1 * 1); auto with zarith.
- apply Zmult_lt_compat_l; auto with zarith.
- intros H5; subst; contradict Hx; auto with zarith.
- apply Zmult_le_0_reg_r with p1; auto with zarith.
- apply Zdivide_trans with (2 := H); exists p1; auto with zarith.
- intros r2 Hr2; exists (r2 + r1); subst.
- apply sym_equal; apply Zpower_exp.
- generalize Hx; case r2; simpl; auto with zarith.
- intros; red; simpl; intros; discriminate.
- generalize H3; case r1; simpl; auto with zarith.
- intros; red; simpl; intros; discriminate.
+ rewrite <- (Z.mul_1_r q1) at 1.
+ apply Z.mul_lt_mono_pos_l; auto with zarith.
+ transitivity (q1 * p1); trivial. exists p1; auto with zarith.
+ exists (r2 + r1); subst.
+ symmetry. apply Z.pow_add_r.
+ generalize Hq1; case r2; now auto with zarith.
+ generalize Hp1; case r1; now auto with zarith.
(* x = 1 *)
- exists 0; rewrite Zpower_0_r; auto.
+ exists 0; rewrite Z.pow_0_r; auto.
(* x = 0 *)
- exists n; destruct H; rewrite Zmult_0_r in H; auto.
+ exists n; destruct H; rewrite Z.mul_0_r in H; auto.
Qed.
(** * Zsquare: a direct definition of [z^2] *)
-Fixpoint Psquare (p: positive): positive :=
- match p with
- | xH => xH
- | xO p => xO (xO (Psquare p))
- | xI p => xI (xO (Pplus (Psquare p) p))
- end.
-
-Definition Zsquare p :=
- match p with
- | Z0 => Z0
- | Zpos p => Zpos (Psquare p)
- | Zneg p => Zpos (Psquare p)
- end.
-
-Theorem Psquare_correct: forall p, Psquare p = (p * p)%positive.
-Proof.
- induction p; simpl; auto; f_equal; rewrite IHp.
- apply trans_equal with (xO p + xO (p*p))%positive; auto.
- rewrite (Pplus_comm (xO p)); auto.
- rewrite Pmult_xI_permute_r; rewrite Pplus_assoc.
- f_equal; auto.
- symmetry; apply Pplus_diag.
- symmetry; apply Pmult_xO_permute_r.
-Qed.
-
-Theorem Zsquare_correct: forall p, Zsquare p = p * p.
-Proof.
- intro p; case p; simpl; auto; intros p1; rewrite Psquare_correct; auto.
-Qed.
+Notation Psquare := Pos.square (only parsing).
+Notation Zsquare := Z.square (only parsing).
+Notation Psquare_correct := Pos.square_spec (only parsing).
+Notation Zsquare_correct := Z.square_spec (only parsing).
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index ce99427f2..5052d01a0 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -6,70 +6,84 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-Require Import Wf_nat.
-Require Import ZArith_base.
+Require Import Wf_nat ZArith_base Omega Zcomplements.
Require Export Zpow_def.
-Require Import Omega.
-Require Import Zcomplements.
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
+
+(** * Power functions over [Z] *)
+
+(** Nota : this file is mostly deprecated. The definition of [Z.pow]
+ and its usual properties are now provided by module [BinInt.Z].
+ Powers of 2 are also available there (see [Z.shiftl] and [Z.shiftr]).
+ Only remain here:
+ - [Zpower_nat] : a power function with a [nat] exponent
+ - old-style powers of two, such as [two_p]
+ - [Zdiv_rest] : a division + modulo when the divisor is a power of 2
+*)
-(** * Definition of powers over [Z]*)
(** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary
integer (type [nat]) and [z] a signed integer (type [Z]) *)
-Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1.
+Definition Zpower_nat (z:Z) (n:nat) := nat_iter n (Z.mul z) 1.
+
+Lemma Zpower_nat_0_r z : Zpower_nat z 0 = 1.
+Proof. reflexivity. Qed.
+
+Lemma Zpower_nat_succ_r n z : Zpower_nat z (S n) = z * (Zpower_nat z n).
+Proof. reflexivity. Qed.
(** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for
- [plus : nat->nat] and [Zmult : Z->Z] *)
+ [plus : nat->nat->nat] and [Z.mul : Z->Z->Z] *)
Lemma Zpower_nat_is_exp :
forall (n m:nat) (z:Z),
Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m.
Proof.
- intros; elim n;
- [ simpl in |- *; elim (Zpower_nat z m); auto with zarith
- | unfold Zpower_nat in |- *; intros; simpl in |- *; rewrite H;
- apply Zmult_assoc ].
+ induction n.
+ - intros. now rewrite Zpower_nat_0_r, Z.mul_1_l.
+ - intros. simpl. now rewrite 2 Zpower_nat_succ_r, IHn, Z.mul_assoc.
+Qed.
+
+(** Conversions between powers of unary and binary integers *)
+
+Lemma Zpower_pos_nat (z : Z) (p : positive) :
+ Z.pow_pos z p = Zpower_nat z (Pos.to_nat p).
+Proof.
+ apply Pos2Nat.inj_iter.
Qed.
-(** This theorem shows that powers of unary and binary integers
- are the same thing, modulo the function convert : [positive -> nat] *)
+Lemma Zpower_nat_Z (z : Z) (n : nat) :
+ Zpower_nat z n = z ^ (Z.of_nat n).
+Proof.
+ induction n. trivial.
+ rewrite Zpower_nat_succ_r, Nat2Z.inj_succ, Z.pow_succ_r.
+ now f_equal.
+ apply Nat2Z.is_nonneg.
+Qed.
-Lemma Zpower_pos_nat :
- forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p).
+Theorem Zpower_nat_Zpower z n : 0 <= n ->
+ z^n = Zpower_nat z (Z.abs_nat n).
Proof.
- intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *;
- apply iter_nat_of_P.
+ intros. now rewrite Zpower_nat_Z, Zabs2Nat.id_abs, Z.abs_eq.
Qed.
-(** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we
- deduce that the function [(Zpower_pos z)] is a morphism
- for [Pplus : positive->positive] and [Zmult : Z->Z] *)
+(** The function [(Z.pow_pos z)] is a morphism
+ for [Pos.add : positive->positive->positive] and [Z.mul : Z->Z->Z] *)
-Lemma Zpower_pos_is_exp :
- forall (n m:positive) (z:Z),
- Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m.
+Lemma Zpower_pos_is_exp (n m : positive)(z:Z) :
+ Z.pow_pos z (n + m) = Z.pow_pos z n * Z.pow_pos z m.
Proof.
- intros.
- rewrite (Zpower_pos_nat z n).
- rewrite (Zpower_pos_nat z m).
- rewrite (Zpower_pos_nat z (n + m)).
- rewrite (Pplus_plus n m).
- apply Zpower_nat_is_exp.
+ now apply (Z.pow_add_r z (Zpos n) (Zpos m)).
Qed.
Hint Immediate Zpower_nat_is_exp Zpower_pos_is_exp : zarith.
Hint Unfold Zpower_pos Zpower_nat: zarith.
-Theorem Zpower_exp :
- forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m.
+Theorem Zpower_exp x n m :
+ n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m.
Proof.
- destruct n; destruct m; auto with zarith.
- simpl; intros; apply Zred_factor0.
- simpl; auto with zarith.
- intros; compute in H0; elim H0; auto.
- intros; compute in H; elim H; auto.
+ Z.swap_greater. apply Z.pow_add_r.
Qed.
Section Powers_of_2.
@@ -80,129 +94,131 @@ Section Powers_of_2.
calculus is possible. [shift n m] computes [2^n * m], i.e.
[m] shifted by [n] positions *)
- Definition shift_nat (n:nat) (z:positive) := iter_nat n positive xO z.
- Definition shift_pos (n z:positive) := iter_pos n positive xO z.
+ Definition shift_nat (n:nat) (z:positive) := nat_iter n xO z.
+ Definition shift_pos (n z:positive) := Pos.iter n xO z.
Definition shift (n:Z) (z:positive) :=
match n with
| Z0 => z
- | Zpos p => iter_pos p positive xO z
+ | Zpos p => Pos.iter p xO z
| Zneg p => z
end.
Definition two_power_nat (n:nat) := Zpos (shift_nat n 1).
Definition two_power_pos (x:positive) := Zpos (shift_pos x 1).
- Lemma two_power_nat_S :
- forall n:nat, two_power_nat (S n) = 2 * two_power_nat n.
+ Definition two_p (x:Z) :=
+ match x with
+ | Z0 => 1
+ | Zpos y => two_power_pos y
+ | Zneg y => 0
+ end.
+
+ (** Equivalence with notions defined in BinInt *)
+
+ Lemma shift_nat_equiv n p : shift_nat n p = Pos.shiftl_nat p n.
Proof. reflexivity. Qed.
- Lemma shift_nat_plus :
- forall (n m:nat) (x:positive),
- shift_nat (n + m) x = shift_nat n (shift_nat m x).
+ Lemma shift_pos_equiv n p : shift_pos n p = Pos.shiftl p (Npos n).
+ Proof. reflexivity. Qed.
+
+ Lemma shift_equiv n p : 0<=n -> Zpos (shift n p) = Z.shiftl (Zpos p) n.
Proof.
- intros; apply iter_nat_plus.
+ destruct n.
+ - trivial.
+ - simpl; intros. now apply Pos.iter_swap_gen.
+ - now destruct 1.
Qed.
- Theorem shift_nat_correct :
- forall (n:nat) (x:positive), Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x.
+ Lemma two_power_nat_equiv n : two_power_nat n = 2 ^ (Z.of_nat n).
Proof.
- unfold shift_nat; induction n.
- trivial.
- intros x. simpl.
- change (Zpower_nat 2 (S n)) with (2 * Zpower_nat 2 n).
- now rewrite <- Zmult_assoc, <- IHn.
+ induction n.
+ - trivial.
+ - now rewrite Nat2Z.inj_succ, Z.pow_succ_r, <- IHn by apply Nat2Z.is_nonneg.
Qed.
- Theorem two_power_nat_correct :
- forall n:nat, two_power_nat n = Zpower_nat 2 n.
+ Lemma two_power_pos_equiv p : two_power_pos p = 2 ^ Zpos p.
Proof.
- intro n.
- unfold two_power_nat.
- rewrite (shift_nat_correct n).
- omega.
+ now apply Pos.iter_swap_gen.
Qed.
- (** Second we show that [two_power_pos] and [two_power_nat] are the same *)
- Lemma shift_pos_nat :
- forall p x:positive, shift_pos p x = shift_nat (nat_of_P p) x.
+ Lemma two_p_equiv x : two_p x = 2 ^ x.
Proof.
- unfold shift_pos, shift_nat. intros. apply iter_nat_of_P.
+ destruct x; trivial. apply two_power_pos_equiv.
Qed.
- Lemma two_power_pos_nat :
- forall p:positive, two_power_pos p = two_power_nat (nat_of_P p).
+ (** Properties of these old versions of powers of two *)
+
+ Lemma two_power_nat_S n : two_power_nat (S n) = 2 * two_power_nat n.
+ Proof. reflexivity. Qed.
+
+ Lemma shift_nat_plus n m x :
+ shift_nat (n + m) x = shift_nat n (shift_nat m x).
Proof.
- intro. unfold two_power_pos, two_power_nat.
- f_equal. apply shift_pos_nat.
+ apply iter_nat_plus.
Qed.
- (** Then we deduce that [two_power_pos] is also correct *)
-
- Theorem shift_pos_correct :
- forall p x:positive, Zpos (shift_pos p x) = Zpower_pos 2 p * Zpos x.
+ Theorem shift_nat_correct n x :
+ Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x.
Proof.
- intros.
- rewrite (shift_pos_nat p x).
- rewrite (Zpower_pos_nat 2 p).
- apply shift_nat_correct.
+ induction n.
+ - trivial.
+ - now rewrite Zpower_nat_succ_r, <- Z.mul_assoc, <- IHn.
Qed.
- Theorem two_power_pos_correct :
- forall x:positive, two_power_pos x = Zpower_pos 2 x.
+ Theorem two_power_nat_correct n : two_power_nat n = Zpower_nat 2 n.
Proof.
- intro.
- rewrite two_power_pos_nat.
- rewrite Zpower_pos_nat.
- apply two_power_nat_correct.
+ now rewrite two_power_nat_equiv, Zpower_nat_Z.
Qed.
- (** Some consequences *)
+ Lemma shift_pos_nat p x : shift_pos p x = shift_nat (Pos.to_nat p) x.
+ Proof.
+ apply Pos2Nat.inj_iter.
+ Qed.
- Theorem two_power_pos_is_exp :
- forall x y:positive,
- two_power_pos (x + y) = two_power_pos x * two_power_pos y.
+ Lemma two_power_pos_nat p : two_power_pos p = two_power_nat (Pos.to_nat p).
Proof.
- intros. rewrite 3 two_power_pos_correct. apply Zpower_pos_is_exp.
+ unfold two_power_pos. now rewrite shift_pos_nat.
Qed.
- (** The exponentiation [z -> 2^z] for [z] a signed integer.
- For convenience, we assume that [2^z = 0] for all [z < 0]
- We could also define a inductive type [Log_result] with
- 3 contructors [ Zero | Pos positive -> | minus_infty]
- but it's more complexe and not so useful. *)
+ Theorem shift_pos_correct p x :
+ Zpos (shift_pos p x) = Zpower_pos 2 p * Zpos x.
+ Proof.
+ now rewrite shift_pos_nat, Zpower_pos_nat, shift_nat_correct.
+ Qed.
- Definition two_p (x:Z) :=
- match x with
- | Z0 => 1
- | Zpos y => two_power_pos y
- | Zneg y => 0
- end.
+ Theorem two_power_pos_correct x : two_power_pos x = Z.pow_pos 2 x.
+ Proof.
+ apply two_power_pos_equiv.
+ Qed.
- Lemma two_p_correct : forall x, two_p x = 2^x.
+ Theorem two_power_pos_is_exp x y :
+ two_power_pos (x + y) = two_power_pos x * two_power_pos y.
Proof.
- intros [|p|p]; trivial. apply two_power_pos_correct.
+ rewrite 3 two_power_pos_equiv. now apply (Z.pow_add_r 2 (Zpos x) (Zpos y)).
Qed.
- Theorem two_p_is_exp :
- forall x y, 0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y.
+ Lemma two_p_correct x : two_p x = 2^x.
+ Proof (two_p_equiv x).
+
+ Theorem two_p_is_exp x y :
+ 0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y.
Proof.
- intros. rewrite 3 two_p_correct. apply Z.pow_add_r; auto with zarith.
+ rewrite !two_p_equiv. apply Z.pow_add_r.
Qed.
- Lemma two_p_gt_ZERO : forall x, 0 <= x -> two_p x > 0.
+ Lemma two_p_gt_ZERO x : 0 <= x -> two_p x > 0.
Proof.
- intros. rewrite two_p_correct. now apply Zlt_gt, Z.pow_pos_nonneg.
+ Z.swap_greater. rewrite two_p_equiv. now apply Z.pow_pos_nonneg.
Qed.
- Lemma two_p_S : forall x, 0 <= x -> two_p (Zsucc x) = 2 * two_p x.
+ Lemma two_p_S x : 0 <= x -> two_p (Z.succ x) = 2 * two_p x.
Proof.
- intros. rewrite 2 two_p_correct. now apply Z.pow_succ_r.
+ rewrite !two_p_equiv. now apply Z.pow_succ_r.
Qed.
- Lemma two_p_pred : forall x, 0 <= x -> two_p (Zpred x) < two_p x.
+ Lemma two_p_pred x : 0 <= x -> two_p (Z.pred x) < two_p x.
Proof.
- intros. rewrite 2 two_p_correct.
- apply Z.pow_lt_mono_r; auto with zarith.
+ rewrite !two_p_equiv. intros. apply Z.pow_lt_mono_r; auto with zarith.
Qed.
End Powers_of_2.
@@ -214,100 +230,88 @@ Section power_div_with_rest.
(** * Division by a power of two. *)
- (** To [n:Z] and [p:positive], [q],[r] are associated such that
- [n = 2^p.q + r] and [0 <= r < 2^p] *)
+ (** To [x:Z] and [p:positive], [q],[r] are associated such that
+ [x = 2^p.q + r] and [0 <= r < 2^p] *)
- (** Invariant: [d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d'] *)
+ (** Invariant: [d*q + r = d'*q + r /\ d' = 2*d /\ 0<=r<d /\ 0<=r'<d'] *)
Definition Zdiv_rest_aux (qrd:Z * Z * Z) :=
- let (qr, d) := qrd in
- let (q, r) := qr in
- (match q with
- | Z0 => (0, r)
- | Zpos xH => (0, d + r)
- | Zpos (xI n) => (Zpos n, d + r)
- | Zpos (xO n) => (Zpos n, r)
- | Zneg xH => (-1, d + r)
- | Zneg (xI n) => (Zneg n - 1, d + r)
- | Zneg (xO n) => (Zneg n, r)
- end, 2 * d).
+ let '(q,r,d) := qrd in
+ (match q with
+ | Z0 => (0, r)
+ | Zpos xH => (0, d + r)
+ | Zpos (xI n) => (Zpos n, d + r)
+ | Zpos (xO n) => (Zpos n, r)
+ | Zneg xH => (-1, d + r)
+ | Zneg (xI n) => (Zneg n - 1, d + r)
+ | Zneg (xO n) => (Zneg n, r)
+ end, 2 * d).
Definition Zdiv_rest (x:Z) (p:positive) :=
- let (qr, d) := iter_pos p _ Zdiv_rest_aux (x, 0, 1) in qr.
+ let (qr, d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) in qr.
- Lemma Zdiv_rest_correct1 :
- forall (x:Z) (p:positive),
- let (qr, d) := iter_pos p _ Zdiv_rest_aux (x, 0, 1) in d = two_power_pos p.
+ Lemma Zdiv_rest_correct1 (x:Z) (p:positive) :
+ let (_, d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) in
+ d = two_power_pos p.
Proof.
- intros x p; rewrite (iter_nat_of_P p _ Zdiv_rest_aux (x, 0, 1));
- rewrite (two_power_pos_nat p); elim (nat_of_P p);
- simpl in |- *;
- [ trivial with zarith
- | intro n; rewrite (two_power_nat_S n); unfold Zdiv_rest_aux at 2 in |- *;
- elim (iter_nat n _ Zdiv_rest_aux (x, 0, 1));
- destruct a; intros; apply f_equal with (f := fun z:Z => 2 * z);
- assumption ].
+ rewrite Pos2Nat.inj_iter, two_power_pos_nat.
+ induction (Pos.to_nat p); simpl; trivial.
+ destruct (nat_iter n Zdiv_rest_aux (x,0,1)) as ((q,r),d).
+ unfold Zdiv_rest_aux. rewrite two_power_nat_S; now f_equal.
Qed.
- Lemma Zdiv_rest_correct2 :
- forall (x:Z) (p:positive),
- let (qr, d) := iter_pos p _ Zdiv_rest_aux (x, 0, 1) in
- let (q, r) := qr in x = q * d + r /\ 0 <= r < d.
+ Lemma Zdiv_rest_correct2 (x:Z) (p:positive) :
+ let '(q,r,d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) in
+ x = q * d + r /\ 0 <= r < d.
Proof.
- intros;
- apply iter_pos_invariant with
- (f := Zdiv_rest_aux)
- (Inv := fun qrd:Z * Z * Z =>
- let (qr, d) := qrd in
- let (q, r) := qr in x = q * d + r /\ 0 <= r < d);
- [ intro x0; elim x0; intro y0; elim y0; intros q r d;
- unfold Zdiv_rest_aux in |- *; elim q;
- [ omega
- | destruct p0;
- [ rewrite BinInt.Zpos_xI; intro; elim H; intros; split;
- [ rewrite H0; rewrite Zplus_assoc; rewrite Zmult_plus_distr_l;
- rewrite Zmult_1_l; rewrite Zmult_assoc;
- rewrite (Zmult_comm (Zpos p0) 2); apply refl_equal
- | omega ]
- | rewrite BinInt.Zpos_xO; intro; elim H; intros; split;
- [ rewrite H0; rewrite Zmult_assoc; rewrite (Zmult_comm (Zpos p0) 2);
- apply refl_equal
- | omega ]
- | omega ]
- | destruct p0;
- [ rewrite BinInt.Zneg_xI; unfold Zminus in |- *; intro; elim H; intros;
- split;
- [ rewrite H0; rewrite Zplus_assoc;
- apply f_equal with (f := fun z:Z => z + r);
- do 2 rewrite Zmult_plus_distr_l; rewrite Zmult_assoc;
- rewrite (Zmult_comm (Zneg p0) 2); rewrite <- Zplus_assoc;
- apply f_equal with (f := fun z:Z => 2 * Zneg p0 * d + z);
- omega
- | omega ]
- | rewrite BinInt.Zneg_xO; unfold Zminus in |- *; intro; elim H; intros;
- split;
- [ rewrite H0; rewrite Zmult_assoc; rewrite (Zmult_comm (Zneg p0) 2);
- apply refl_equal
- | omega ]
- | omega ] ]
- | omega ].
+ apply Pos.iter_invariant; [|omega].
+ intros ((q,r),d) (H,H'). unfold Zdiv_rest_aux.
+ destruct q as [ |[q|q| ]|[q|q| ]]; try omega.
+ - rewrite Z.pos_xI, Z.mul_add_distr_r in H.
+ rewrite Z.mul_shuffle3, Z.mul_assoc. omega.
+ - rewrite Z.pos_xO in H.
+ rewrite Z.mul_shuffle3, Z.mul_assoc. omega.
+ - rewrite Z.neg_xI, Z.mul_sub_distr_r in H.
+ rewrite Z.mul_sub_distr_r, Z.mul_shuffle3, Z.mul_assoc. omega.
+ - rewrite Z.neg_xO in H.
+ rewrite Z.mul_shuffle3, Z.mul_assoc. omega.
Qed.
+ (** Old-style rich specification by proof of existence *)
+
Inductive Zdiv_rest_proofs (x:Z) (p:positive) : Set :=
Zdiv_rest_proof :
forall q r:Z,
x = q * two_power_pos p + r ->
0 <= r -> r < two_power_pos p -> Zdiv_rest_proofs x p.
- Lemma Zdiv_rest_correct : forall (x:Z) (p:positive), Zdiv_rest_proofs x p.
+ Lemma Zdiv_rest_correct (x:Z) (p:positive) : Zdiv_rest_proofs x p.
Proof.
- intros x p.
generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p).
- elim (iter_pos p _ Zdiv_rest_aux (x, 0, 1)).
- simple induction a.
- intros.
- elim H; intros H1 H2; clear H.
- rewrite H0 in H1; rewrite H0 in H2; elim H2; intros;
- apply Zdiv_rest_proof with (q := a0) (r := b); assumption.
+ destruct (Pos.iter p Zdiv_rest_aux (x, 0, 1)) as ((q,r),d).
+ intros (H1,(H2,H3)) ->. now exists q r.
+ Qed.
+
+ (** Direct correctness of [Zdiv_rest] *)
+
+ Lemma Zdiv_rest_ok x p :
+ let (q,r) := Zdiv_rest x p in
+ x = q * 2^(Zpos p) + r /\ 0 <= r < 2^(Zpos p).
+ Proof.
+ unfold Zdiv_rest.
+ generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p).
+ destruct (Pos.iter p Zdiv_rest_aux (x, 0, 1)) as ((q,r),d).
+ intros H ->. now rewrite two_power_pos_equiv in H.
+ Qed.
+
+ (** Equivalence with [Z.shiftr] *)
+
+ Lemma Zdiv_rest_shiftr x p :
+ fst (Zdiv_rest x p) = Z.shiftr x (Zpos p).
+ Proof.
+ generalize (Zdiv_rest_ok x p). destruct (Zdiv_rest x p) as (q,r).
+ intros (H,H'). simpl.
+ rewrite Z.shiftr_div_pow2 by easy.
+ apply Z.div_unique_pos with r; trivial. now rewrite Z.mul_comm.
Qed.
End power_div_with_rest.
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget
index 9c1e69ac7..178111cdf 100644
--- a/theories/ZArith/vo.itarget
+++ b/theories/ZArith/vo.itarget
@@ -14,6 +14,7 @@ Zcomplements.vo
Zdiv.vo
Zeven.vo
Zgcd_alt.vo
+Zpow_alt.vo
Zhints.vo
Zlogarithm.vo
Zmax.vo