diff options
| -rw-r--r-- | theories/NArith/BinNat.v | 7 | ||||
| -rw-r--r-- | theories/NArith/BinNatDef.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAxioms.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 9 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZAxioms.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAxioms.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSig.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 11 | ||||
| -rw-r--r-- | theories/PArith/BinPos.v | 10 | ||||
| -rw-r--r-- | theories/PArith/BinPosDef.v | 9 | ||||
| -rw-r--r-- | theories/ZArith/BinInt.v | 14 | ||||
| -rw-r--r-- | theories/ZArith/BinIntDef.v | 9 | ||||
| -rw-r--r-- | theories/ZArith/Znat.v | 119 | ||||
| -rw-r--r-- | theories/ZArith/Zpow_alt.v | 83 | ||||
| -rw-r--r-- | theories/ZArith/Zpow_def.v | 109 | ||||
| -rw-r--r-- | theories/ZArith/Zpow_facts.v | 506 | ||||
| -rw-r--r-- | theories/ZArith/Zpower.v | 372 | ||||
| -rw-r--r-- | theories/ZArith/vo.itarget | 1 |
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 |