diff options
Diffstat (limited to 'theories/ZArith/Zpower.v')
| -rw-r--r-- | theories/ZArith/Zpower.v | 671 |
1 files changed, 342 insertions, 329 deletions
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 70a2bd45..446f663c 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zpower.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Zpower.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import ZArith_base. Require Import Omega. @@ -15,81 +15,84 @@ Open Local Scope Z_scope. Section section1. +(** * 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. - -(** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for - [plus : nat->nat] and [Zmult : 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. - -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 ]. -Qed. - -(** [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]) *) - -Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1. - -(** This theorem shows that powers of unary and binary integers - are the same thing, modulo the function convert : [positive -> nat] *) - -Theorem Zpower_pos_nat : - forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p). - -intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *; - apply iter_nat_of_P. -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] *) - -Theorem Zpower_pos_is_exp : - forall (n m:positive) (z:Z), - Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m. - -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. -Qed. - -Definition Zpower (x y:Z) := - match y with - | Zpos p => Zpower_pos x p - | Z0 => 1 - | Zneg p => 0 - end. - -Infix "^" := Zpower : Z_scope. - -Hint Immediate Zpower_nat_is_exp: zarith. -Hint Immediate Zpower_pos_is_exp: zarith. -Hint Unfold Zpower_pos: zarith. -Hint Unfold Zpower_nat: zarith. - -Lemma Zpower_exp : - forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m. -destruct n; destruct m; auto with zarith. -simpl in |- *; intros; apply Zred_factor0. -simpl in |- *; auto with zarith. -intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith. -intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith. -Qed. + Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1. + + (** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for + [plus : nat->nat] and [Zmult : 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 ]. + Qed. + + (** [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]) *) + + Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1. + + (** This theorem shows that powers of unary and binary integers + are the same thing, modulo the function convert : [positive -> nat] *) + + Theorem Zpower_pos_nat : + forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p). + Proof. + intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *; + apply iter_nat_of_P. + 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] *) + + Theorem Zpower_pos_is_exp : + forall (n m:positive) (z:Z), + Zpower_pos z (n + m) = Zpower_pos z n * Zpower_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. + Qed. + + Definition Zpower (x y:Z) := + match y with + | Zpos p => Zpower_pos x p + | Z0 => 1 + | Zneg p => 0 + end. + + Infix "^" := Zpower : Z_scope. + + Hint Immediate Zpower_nat_is_exp: zarith. + Hint Immediate Zpower_pos_is_exp: zarith. + Hint Unfold Zpower_pos: zarith. + Hint Unfold Zpower_nat: zarith. + + Lemma Zpower_exp : + forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m. + Proof. + destruct n; destruct m; auto with zarith. + simpl in |- *; intros; apply Zred_factor0. + simpl in |- *; auto with zarith. + intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith. + intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith. + Qed. End section1. -(* Exporting notation "^" *) +(** Exporting notation "^" *) Infix "^" := Zpower : Z_scope. @@ -100,273 +103,283 @@ Hint Unfold Zpower_nat: zarith. Section 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 *) - -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 (n:Z) (z:positive) := - match n with - | Z0 => z - | Zpos p => iter_pos p positive 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. -intro; simpl in |- *; apply refl_equal. -Qed. - -Lemma shift_nat_plus : - forall (n m:nat) (x:positive), - shift_nat (n + m) x = shift_nat n (shift_nat m x). - -intros; unfold shift_nat in |- *; apply iter_nat_plus. -Qed. - -Theorem shift_nat_correct : - forall (n:nat) (x:positive), Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x. - -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 ] ]. -Qed. - -Theorem two_power_nat_correct : - forall n:nat, two_power_nat n = Zpower_nat 2 n. - -intro n. -unfold two_power_nat in |- *. -rewrite (shift_nat_correct n). -omega. -Qed. + (** * 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 *) + + 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 (n:Z) (z:positive) := + match n with + | Z0 => z + | Zpos p => iter_pos p positive 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. + Proof. + intro; simpl in |- *; apply refl_equal. + Qed. + + Lemma shift_nat_plus : + forall (n m:nat) (x:positive), + shift_nat (n + m) x = shift_nat n (shift_nat m x). + Proof. + intros; unfold shift_nat in |- *; apply iter_nat_plus. + Qed. + + Theorem shift_nat_correct : + forall (n:nat) (x:positive), Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x. + 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 ] ]. + Qed. + + Theorem two_power_nat_correct : + forall n:nat, two_power_nat n = Zpower_nat 2 n. + Proof. + intro n. + unfold two_power_nat in |- *. + rewrite (shift_nat_correct n). + omega. + 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. + Proof. + unfold shift_pos in |- *. + unfold shift_nat in |- *. + intros; apply iter_nat_of_P. + Qed. + + Lemma two_power_pos_nat : + forall p:positive, two_power_pos p = two_power_nat (nat_of_P p). + Proof. + intro; unfold two_power_pos in |- *; unfold two_power_nat in |- *. + apply f_equal with (f := Zpos). + apply shift_pos_nat. + 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. + Proof. + intros. + rewrite (shift_pos_nat p x). + rewrite (Zpower_pos_nat 2 p). + apply shift_nat_correct. + Qed. + + Theorem two_power_pos_correct : + forall x:positive, two_power_pos x = Zpower_pos 2 x. + Proof. + intro. + rewrite two_power_pos_nat. + rewrite Zpower_pos_nat. + apply two_power_nat_correct. + Qed. + + (** Some consequences *) + + Theorem two_power_pos_is_exp : + forall x y:positive, + two_power_pos (x + y) = two_power_pos x * two_power_pos y. + 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. + 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. *) -(** 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. - -unfold shift_pos in |- *. -unfold shift_nat in |- *. -intros; apply iter_nat_of_P. -Qed. - -Lemma two_power_pos_nat : - forall p:positive, two_power_pos p = two_power_nat (nat_of_P p). - -intro; unfold two_power_pos in |- *; unfold two_power_nat in |- *. -apply f_equal with (f := Zpos). -apply shift_pos_nat. -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. - -intros. -rewrite (shift_pos_nat p x). -rewrite (Zpower_pos_nat 2 p). -apply shift_nat_correct. -Qed. - -Theorem two_power_pos_correct : - forall x:positive, two_power_pos x = Zpower_pos 2 x. - -intro. -rewrite two_power_pos_nat. -rewrite Zpower_pos_nat. -apply two_power_nat_correct. -Qed. - -(** Some consequences *) - -Theorem two_power_pos_is_exp : - forall x y:positive, - two_power_pos (x + y) = two_power_pos x * two_power_pos y. -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. -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. *) - -Definition two_p (x:Z) := - match x with - | Z0 => 1 - | Zpos y => two_power_pos y - | Zneg y => 0 - end. - -Theorem two_p_is_exp : - forall x y:Z, 0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y. -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 ] ]. -Qed. - -Lemma two_p_gt_ZERO : forall x:Z, 0 <= x -> two_p x > 0. -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 ] ]. -Qed. - -Lemma two_p_S : forall x:Z, 0 <= x -> two_p (Zsucc x) = 2 * two_p x. -intros; unfold Zsucc in |- *. -rewrite (two_p_is_exp x 1 H (Zorder.Zle_0_pos 1)). -apply Zmult_comm. -Qed. - -Lemma two_p_pred : forall x:Z, 0 <= x -> two_p (Zpred x) < two_p x. -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 ]. -Qed. - -Lemma Zlt_lt_double : forall x y:Z, 0 <= x < y -> x < 2 * y. -intros; omega. Qed. - -End Powers_of_2. + Definition two_p (x:Z) := + match x with + | Z0 => 1 + | Zpos y => two_power_pos y + | Zneg y => 0 + end. + + Theorem two_p_is_exp : + forall x y:Z, 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 ] ]. + Qed. + + Lemma two_p_gt_ZERO : forall x:Z, 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 ] ]. + Qed. + + Lemma two_p_S : forall x:Z, 0 <= x -> two_p (Zsucc 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. + Qed. + + Lemma two_p_pred : forall x:Z, 0 <= x -> two_p (Zpred 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 ]. + Qed. + + Lemma Zlt_lt_double : forall x y:Z, 0 <= x < y -> x < 2 * y. + intros; omega. Qed. + + End Powers_of_2. Hint Resolve two_p_gt_ZERO: zarith. Hint Immediate two_p_pred two_p_S: zarith. 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] *) - -(** 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). - -Definition Zdiv_rest (x:Z) (p:positive) := - let (qr, d) := iter_pos 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. - -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 ]. -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. - -intros; - apply iter_pos_invariant with - (f := Zdiv_rest_aux) - (Inv := fun qrd:Z * Z * Z => - let (qr, d) := qrd in + (** * 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] *) + + (** 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). + + Definition Zdiv_rest (x:Z) (p:positive) := + let (qr, d) := iter_pos 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. + 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 ]. + 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. + 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 ]. -Qed. - -Inductive Zdiv_rest_proofs (x:Z) (p:positive) : Set := + [ 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 ]. + Qed. + + 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. -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. -Qed. + 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. + 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. + Qed. End power_div_with_rest.
\ No newline at end of file |