(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* 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. End section1. (* Exporting notation "^" *) 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. 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. (** 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. 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 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 := 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. End power_div_with_rest.