Require Import ZArith.
Require Import Zquot.
Require Import Fcore_Zaux.
Number of bits (radix 2) of a positive integer.
It serves as an upper bound on the number of digits to ensure termination.
Fixpoint digits2_Pnat (
n :
positive) :
nat :=
match n with
|
xH =>
O
|
xO p =>
S (
digits2_Pnat p)
|
xI p =>
S (
digits2_Pnat p)
end.
Theorem digits2_Pnat_correct :
forall n,
let d :=
digits2_Pnat n in
(
Zpower_nat 2
d <=
Zpos n <
Zpower_nat 2 (
S d))%
Z.
Proof.
intros n d.
unfold d.
clear.
assert (
Hp:
forall m, (
Zpower_nat 2 (
S m) = 2 *
Zpower_nat 2
m)%
Z)
by easy.
induction n ;
simpl digits2_Pnat.
rewrite Zpos_xI, 2!
Hp.
omega.
rewrite (
Zpos_xO n), 2!
Hp.
omega.
now split.
Qed.
Section Fcore_digits.
Variable beta :
radix.
Definition Zdigit n k :=
Z.rem (
Z.quot n (
Zpower beta k))
beta.
Theorem Zdigit_lt :
forall n k,
(
k < 0)%
Z ->
Zdigit n k =
Z0.
Proof.
intros n [|k|k] Hk ; try easy.
now case n.
Qed.
Theorem Zdigit_0 :
forall k,
Zdigit 0
k =
Z0.
Proof.
Theorem Zdigit_opp :
forall n k,
Zdigit (-
n)
k =
Zopp (
Zdigit n k).
Proof.
Theorem Zdigit_ge_Zpower_pos :
forall e n,
(0 <=
n <
Zpower beta e)%
Z ->
forall k, (
e <=
k)%
Z ->
Zdigit n k =
Z0.
Proof.
Theorem Zdigit_ge_Zpower :
forall e n,
(
Zabs n <
Zpower beta e)%
Z ->
forall k, (
e <=
k)%
Z ->
Zdigit n k =
Z0.
Proof.
Theorem Zdigit_not_0_pos :
forall e n, (0 <=
e)%
Z ->
(
Zpower beta e <=
n <
Zpower beta (
e + 1))%
Z ->
Zdigit n e <>
Z0.
Proof.
Theorem Zdigit_not_0 :
forall e n, (0 <=
e)%
Z ->
(
Zpower beta e <=
Zabs n <
Zpower beta (
e + 1))%
Z ->
Zdigit n e <>
Z0.
Proof.
Theorem Zdigit_mul_pow :
forall n k k', (0 <=
k')%
Z ->
Zdigit (
n *
Zpower beta k')
k =
Zdigit n (
k -
k').
Proof.
Theorem Zdigit_div_pow :
forall n k k', (0 <=
k)%
Z -> (0 <=
k')%
Z ->
Zdigit (
Z.quot n (
Zpower beta k'))
k =
Zdigit n (
k +
k').
Proof.
Theorem Zdigit_mod_pow :
forall n k k', (
k <
k')%
Z ->
Zdigit (
Z.rem n (
Zpower beta k'))
k =
Zdigit n k.
Proof.
Theorem Zdigit_mod_pow_out :
forall n k k', (0 <=
k' <=
k)%
Z ->
Zdigit (
Z.rem n (
Zpower beta k'))
k =
Z0.
Proof.
Fixpoint Zsum_digit f k :=
match k with
|
O =>
Z0
|
S k => (
Zsum_digit f k +
f (
Z_of_nat k) *
Zpower beta (
Z_of_nat k))%
Z
end.
Theorem Zsum_digit_digit :
forall n k,
Zsum_digit (
Zdigit n)
k =
Z.rem n (
Zpower beta (
Z_of_nat k)).
Proof.
Theorem Zpower_gt_id :
forall n, (
n <
Zpower beta n)%
Z.
Proof.
Theorem Zdigit_ext :
forall n1 n2,
(
forall k, (0 <=
k)%
Z ->
Zdigit n1 k =
Zdigit n2 k) ->
n1 =
n2.
Proof.
Theorem ZOmod_plus_pow_digit :
forall u v n, (0 <=
u *
v)%
Z ->
(
forall k, (0 <=
k <
n)%
Z ->
Zdigit u k =
Z0 \/
Zdigit v k =
Z0) ->
Z.rem (
u +
v) (
Zpower beta n) = (
Z.rem u (
Zpower beta n) +
Z.rem v (
Zpower beta n))%
Z.
Proof.
Theorem ZOdiv_plus_pow_digit :
forall u v n, (0 <=
u *
v)%
Z ->
(
forall k, (0 <=
k <
n)%
Z ->
Zdigit u k =
Z0 \/
Zdigit v k =
Z0) ->
Z.quot (
u +
v) (
Zpower beta n) = (
Z.quot u (
Zpower beta n) +
Z.quot v (
Zpower beta n))%
Z.
Proof.
Theorem Zdigit_plus :
forall u v, (0 <=
u *
v)%
Z ->
(
forall k, (0 <=
k)%
Z ->
Zdigit u k =
Z0 \/
Zdigit v k =
Z0) ->
forall k,
Zdigit (
u +
v)
k = (
Zdigit u k +
Zdigit v k)%
Z.
Proof.
Left and right shifts
Definition Zscale n k :=
if Zle_bool 0
k then (
n *
Zpower beta k)%
Z else Z.quot n (
Zpower beta (-
k)).
Theorem Zdigit_scale :
forall n k k', (0 <=
k')%
Z ->
Zdigit (
Zscale n k)
k' =
Zdigit n (
k' -
k).
Proof.
Theorem Zscale_0 :
forall k,
Zscale 0
k =
Z0.
Proof.
Theorem Zsame_sign_scale :
forall n k,
(0 <=
n *
Zscale n k)%
Z.
Proof.
Theorem Zscale_mul_pow :
forall n k k', (0 <=
k)%
Z ->
Zscale (
n *
Zpower beta k)
k' =
Zscale n (
k +
k').
Proof.
Theorem Zscale_scale :
forall n k k', (0 <=
k)%
Z ->
Zscale (
Zscale n k)
k' =
Zscale n (
k +
k').
Proof.
Slice of an integer
Definition Zslice n k1 k2 :=
if Zle_bool 0
k2 then Z.rem (
Zscale n (-
k1)) (
Zpower beta k2)
else Z0.
Theorem Zdigit_slice :
forall n k1 k2 k, (0 <=
k <
k2)%
Z ->
Zdigit (
Zslice n k1 k2)
k =
Zdigit n (
k1 +
k).
Proof.
Theorem Zdigit_slice_out :
forall n k1 k2 k, (
k2 <=
k)%
Z ->
Zdigit (
Zslice n k1 k2)
k =
Z0.
Proof.
Theorem Zslice_0 :
forall k k',
Zslice 0
k k' =
Z0.
Proof.
Theorem Zsame_sign_slice :
forall n k k',
(0 <=
n *
Zslice n k k')%
Z.
Proof.
Theorem Zslice_slice :
forall n k1 k2 k1'
k2', (0 <=
k1' <=
k2)%
Z ->
Zslice (
Zslice n k1 k2)
k1'
k2' =
Zslice n (
k1 +
k1') (
Zmin (
k2 -
k1')
k2').
Proof.
Theorem Zslice_mul_pow :
forall n k k1 k2, (0 <=
k)%
Z ->
Zslice (
n *
Zpower beta k)
k1 k2 =
Zslice n (
k1 -
k)
k2.
Proof.
Theorem Zslice_div_pow :
forall n k k1 k2, (0 <=
k)%
Z -> (0 <=
k1)%
Z ->
Zslice (
Z.quot n (
Zpower beta k))
k1 k2 =
Zslice n (
k1 +
k)
k2.
Proof.
Theorem Zslice_scale :
forall n k k1 k2, (0 <=
k1)%
Z ->
Zslice (
Zscale n k)
k1 k2 =
Zslice n (
k1 -
k)
k2.
Proof.
Theorem Zslice_div_pow_scale :
forall n k k1 k2, (0 <=
k)%
Z ->
Zslice (
Z.quot n (
Zpower beta k))
k1 k2 =
Zscale (
Zslice n k (
k1 +
k2)) (-
k1).
Proof.
Theorem Zplus_slice :
forall n k l1 l2, (0 <=
l1)%
Z -> (0 <=
l2)%
Z ->
(
Zslice n k l1 +
Zscale (
Zslice n (
k +
l1)
l2)
l1)%
Z =
Zslice n k (
l1 +
l2).
Proof.
Section digits_aux.
Variable p :
Z.
Fixpoint Zdigits_aux (
nb pow :
Z) (
n :
nat) {
struct n } :
Z :=
match n with
|
O =>
nb
|
S n =>
if Zlt_bool p pow then nb else Zdigits_aux (
nb + 1) (
Zmult beta pow)
n
end.
End digits_aux.
Number of digits of an integer
Definition Zdigits n :=
match n with
|
Z0 =>
Z0
|
Zneg p =>
Zdigits_aux (
Zpos p) 1
beta (
digits2_Pnat p)
|
Zpos p =>
Zdigits_aux n 1
beta (
digits2_Pnat p)
end.
Theorem Zdigits_correct :
forall n,
(
Zpower beta (
Zdigits n - 1) <=
Zabs n <
Zpower beta (
Zdigits n))%
Z.
Proof.
Theorem Zdigits_unique :
forall n d,
(
Zpower beta (
d - 1) <=
Zabs n <
Zpower beta d)%
Z ->
Zdigits n =
d.
Proof.
Theorem Zdigits_abs :
forall n,
Zdigits (
Zabs n) =
Zdigits n.
Proof.
now intros [|n|n].
Qed.
Theorem Zdigits_gt_0 :
forall n,
n <>
Z0 -> (0 <
Zdigits n)%
Z.
Proof.
Theorem Zdigits_ge_0 :
forall n, (0 <=
Zdigits n)%
Z.
Proof.
Theorem Zdigit_out :
forall n k, (
Zdigits n <=
k)%
Z ->
Zdigit n k =
Z0.
Proof.
Theorem Zdigit_digits :
forall n,
n <>
Z0 ->
Zdigit n (
Zdigits n - 1) <>
Z0.
Proof.
Theorem Zdigits_slice :
forall n k l, (0 <=
l)%
Z ->
(
Zdigits (
Zslice n k l) <=
l)%
Z.
Proof.
Theorem Zdigits_mult_Zpower :
forall m e,
m <>
Z0 -> (0 <=
e)%
Z ->
Zdigits (
m *
Zpower beta e) = (
Zdigits m +
e)%
Z.
Proof.
Theorem Zdigits_Zpower :
forall e,
(0 <=
e)%
Z ->
Zdigits (
Zpower beta e) = (
e + 1)%
Z.
Proof.
Theorem Zdigits_le :
forall x y,
(0 <=
x)%
Z -> (
x <=
y)%
Z ->
(
Zdigits x <=
Zdigits y)%
Z.
Proof.
Theorem lt_Zdigits :
forall x y,
(0 <=
y)%
Z ->
(
Zdigits x <
Zdigits y)%
Z ->
(
x <
y)%
Z.
Proof.
Theorem Zpower_le_Zdigits :
forall e x,
(
e <
Zdigits x)%
Z ->
(
Zpower beta e <=
Zabs x)%
Z.
Proof.
Theorem Zdigits_le_Zpower :
forall e x,
(
Zabs x <
Zpower beta e)%
Z ->
(
Zdigits x <=
e)%
Z.
Proof.
Theorem Zpower_gt_Zdigits :
forall e x,
(
Zdigits x <=
e)%
Z ->
(
Zabs x <
Zpower beta e)%
Z.
Proof.
Theorem Zdigits_gt_Zpower :
forall e x,
(
Zpower beta e <=
Zabs x)%
Z ->
(
e <
Zdigits x)%
Z.
Proof.
Number of digits of a product.
This strong version is needed for proofs of division and square root
algorithms, since they involve operation remainders.
Theorem Zdigits_mult_strong :
forall x y,
(0 <=
x)%
Z -> (0 <=
y)%
Z ->
(
Zdigits (
x +
y +
x *
y) <=
Zdigits x +
Zdigits y)%
Z.
Proof.
Theorem Zdigits_mult :
forall x y,
(
Zdigits (
x *
y) <=
Zdigits x +
Zdigits y)%
Z.
Proof.
Theorem Zdigits_mult_ge :
forall x y,
(
x <> 0)%
Z -> (
y <> 0)%
Z ->
(
Zdigits x +
Zdigits y - 1 <=
Zdigits (
x *
y))%
Z.
Proof.
Theorem Zdigits_div_Zpower :
forall m e,
(0 <=
m)%
Z ->
(0 <=
e <=
Zdigits m)%
Z ->
Zdigits (
m /
Zpower beta e) = (
Zdigits m -
e)%
Z.
Proof.
End Fcore_digits.
Specialized version for computing the number of bits of an integer
Section Zdigits2.
Theorem Z_of_nat_S_digits2_Pnat :
forall m :
positive,
Z_of_nat (
S (
digits2_Pnat m)) =
Zdigits radix2 (
Zpos m).
Proof.
Fixpoint digits2_pos (
n :
positive) :
positive :=
match n with
|
xH =>
xH
|
xO p =>
Psucc (
digits2_pos p)
|
xI p =>
Psucc (
digits2_pos p)
end.
Theorem Zpos_digits2_pos :
forall m :
positive,
Zpos (
digits2_pos m) =
Zdigits radix2 (
Zpos m).
Proof.
Definition Zdigits2 n :=
match n with
|
Z0 =>
n
|
Zpos p =>
Zpos (
digits2_pos p)
|
Zneg p =>
Zpos (
digits2_pos p)
end.
Lemma Zdigits2_Zdigits :
forall n,
Zdigits2 n =
Zdigits radix2 n.
Proof.
End Zdigits2.