Require Import ZArith_base.
Require Import Omega.
Require Import Zcomplements.
Open Local Scope Z_scope.
Section section1.
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.
End section1.
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.