diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /theories/ZArith/Zpower.v | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'theories/ZArith/Zpower.v')
-rw-r--r-- | theories/ZArith/Zpower.v | 427 |
1 files changed, 192 insertions, 235 deletions
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 038748b5..5052d01a 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -1,79 +1,89 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) (************************************************************************) -(*i $Id: Zpower.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - -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] *) -Infix "^" := Zpower : Z_scope. +(** 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 [[n:positive](Zpower_pos z n)] is a morphism - for [add : 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 (nat_of_P_plus_morphism 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. @@ -81,178 +91,137 @@ Section Powers_of_2. (** * Powers of 2 *) (** For the powers of two, that will be widely used, a more direct - calculus is possible. We will also prove some properties such - as [(x:positive) x < 2^x] that are true for all integers bigger - than 2 but more difficult to prove and useless. *) - - (** [shift n m] computes [2^n * m], or [m] shifted by [n] positions *) + 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_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. - intro; simpl in |- *; apply refl_equal. + destruct n. + - trivial. + - simpl; intros. now apply Pos.iter_swap_gen. + - now destruct 1. Qed. - Lemma shift_nat_plus : - forall (n m:nat) (x:positive), - shift_nat (n + m) x = shift_nat n (shift_nat m x). + Lemma two_power_nat_equiv n : two_power_nat n = 2 ^ (Z.of_nat n). Proof. - intros; unfold shift_nat in |- *; apply iter_nat_plus. + induction n. + - trivial. + - now rewrite Nat2Z.inj_succ, Z.pow_succ_r, <- IHn by apply Nat2Z.is_nonneg. Qed. - Theorem shift_nat_correct : - forall (n:nat) (x:positive), Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x. + Lemma two_power_pos_equiv p : two_power_pos p = 2 ^ Zpos p. Proof. - unfold shift_nat in |- *; simple induction n; - [ simpl in |- *; trivial with zarith - | intros; replace (Zpower_nat 2 (S n0)) with (2 * Zpower_nat 2 n0); - [ rewrite <- Zmult_assoc; rewrite <- (H x); simpl in |- *; reflexivity - | auto with zarith ] ]. + now apply Pos.iter_swap_gen. Qed. - Theorem two_power_nat_correct : - forall n:nat, two_power_nat n = Zpower_nat 2 n. + Lemma two_p_equiv x : two_p x = 2 ^ x. Proof. - intro n. - unfold two_power_nat in |- *. - rewrite (shift_nat_correct n). - omega. + destruct x; trivial. apply two_power_pos_equiv. 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. + (** 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. - unfold shift_pos in |- *. - unfold shift_nat in |- *. - intros; apply iter_nat_of_P. + apply iter_nat_plus. Qed. - Lemma two_power_pos_nat : - forall p:positive, two_power_pos p = two_power_nat (nat_of_P p). + Theorem shift_nat_correct n x : + Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x. Proof. - intro; unfold two_power_pos in |- *; unfold two_power_nat in |- *. - apply f_equal with (f := Zpos). - apply shift_pos_nat. + induction n. + - trivial. + - now rewrite Zpower_nat_succ_r, <- Z.mul_assoc, <- IHn. Qed. - (** Then we deduce that [two_power_pos] is also correct *) + Theorem two_power_nat_correct n : two_power_nat n = Zpower_nat 2 n. + Proof. + now rewrite two_power_nat_equiv, Zpower_nat_Z. + Qed. - Theorem shift_pos_correct : - forall p x:positive, Zpos (shift_pos p x) = Zpower_pos 2 p * Zpos x. + Lemma shift_pos_nat p x : shift_pos p x = shift_nat (Pos.to_nat p) x. Proof. - intros. - rewrite (shift_pos_nat p x). - rewrite (Zpower_pos_nat 2 p). - apply shift_nat_correct. + apply Pos2Nat.inj_iter. Qed. - Theorem two_power_pos_correct : - forall x:positive, two_power_pos x = Zpower_pos 2 x. + Lemma two_power_pos_nat p : two_power_pos p = two_power_nat (Pos.to_nat p). Proof. - intro. - rewrite two_power_pos_nat. - rewrite Zpower_pos_nat. - apply two_power_nat_correct. + unfold two_power_pos. now rewrite shift_pos_nat. Qed. - (** Some consequences *) + 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. - Theorem two_power_pos_is_exp : - forall x y:positive, - two_power_pos (x + y) = two_power_pos x * two_power_pos y. + Theorem two_power_pos_correct x : two_power_pos x = Z.pow_pos 2 x. Proof. - intros. - rewrite (two_power_pos_correct (x + y)). - rewrite (two_power_pos_correct x). - rewrite (two_power_pos_correct y). - apply Zpower_pos_is_exp. + apply two_power_pos_equiv. 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 two_power_pos_is_exp x y : + two_power_pos (x + y) = two_power_pos x * two_power_pos y. + Proof. + rewrite 3 two_power_pos_equiv. now apply (Z.pow_add_r 2 (Zpos x) (Zpos y)). + Qed. - Definition two_p (x:Z) := - match x with - | Z0 => 1 - | Zpos y => two_power_pos y - | Zneg y => 0 - end. + Lemma two_p_correct x : two_p x = 2^x. + Proof (two_p_equiv x). - Theorem two_p_is_exp : - forall x y:Z, 0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y. + Theorem two_p_is_exp x y : + 0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y. Proof. - simple induction x; - [ simple induction y; simpl in |- *; auto with zarith - | simple induction y; - [ unfold two_p in |- *; rewrite (Zmult_comm (two_power_pos p) 1); - rewrite (Zmult_1_l (two_power_pos p)); auto with zarith - | unfold Zplus in |- *; unfold two_p in |- *; intros; - apply two_power_pos_is_exp - | intros; unfold Zle in H0; unfold Zcompare in H0; - absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith ] - | simple induction y; - [ simpl in |- *; auto with zarith - | intros; unfold Zle in H; unfold Zcompare in H; - absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith - | intros; unfold Zle in H; unfold Zcompare in H; - absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith ] ]. + rewrite !two_p_equiv. apply Z.pow_add_r. Qed. - Lemma two_p_gt_ZERO : forall x:Z, 0 <= x -> two_p x > 0. + Lemma two_p_gt_ZERO x : 0 <= x -> two_p x > 0. Proof. - simple induction x; intros; - [ simpl in |- *; omega - | simpl in |- *; unfold two_power_pos in |- *; apply Zorder.Zgt_pos_0 - | absurd (0 <= Zneg p); - [ simpl in |- *; unfold Zle in |- *; unfold Zcompare in |- *; - do 2 unfold not in |- *; auto with zarith - | assumption ] ]. + Z.swap_greater. rewrite two_p_equiv. now apply Z.pow_pos_nonneg. Qed. - Lemma two_p_S : forall x:Z, 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; unfold Zsucc in |- *. - rewrite (two_p_is_exp x 1 H (Zorder.Zle_0_pos 1)). - apply Zmult_comm. + rewrite !two_p_equiv. now apply Z.pow_succ_r. Qed. - Lemma two_p_pred : forall x:Z, 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; apply natlike_ind with (P := fun x:Z => two_p (Zpred x) < two_p x); - [ simpl in |- *; unfold Zlt in |- *; auto with zarith - | intros; elim (Zle_lt_or_eq 0 x0 H0); - [ intros; - replace (two_p (Zpred (Zsucc x0))) with (two_p (Zsucc (Zpred x0))); - [ rewrite (two_p_S (Zpred x0)); - [ rewrite (two_p_S x0); [ omega | assumption ] - | apply Zorder.Zlt_0_le_0_pred; assumption ] - | rewrite <- (Zsucc_pred x0); rewrite <- (Zpred_succ x0); - trivial with zarith ] - | intro Hx0; rewrite <- Hx0; simpl in |- *; unfold Zlt in |- *; - auto with zarith ] - | assumption ]. + rewrite !two_p_equiv. intros. apply Z.pow_lt_mono_r; auto with zarith. Qed. - Lemma Zlt_lt_double : forall x y:Z, 0 <= x < y -> x < 2 * y. - intros; omega. Qed. - - End Powers_of_2. +End Powers_of_2. Hint Resolve two_p_gt_ZERO: zarith. Hint Immediate two_p_pred two_p_S: zarith. @@ -261,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 (Z * Z * Z) 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 (Z * Z * Z) 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. |