Library Coq.Numbers.BigNumPrelude
Auxillary functions & theorems used for arbitrary precision efficient
numbers.
Require Import ArithRing.
Require Export ZArith.
Require Export Znumtheory.
Require Export Zpow_facts.
Open Local Scope Z_scope.
Lemma Zlt0_not_eq :
forall n, 0<n ->
n<>0.
Definition Zdiv_mult_cancel_r a b c H :=
Zdiv.Zdiv_mult_cancel_r a b c (
Zlt0_not_eq _ H).
Definition Zdiv_mult_cancel_l a b c H :=
Zdiv.Zdiv_mult_cancel_r a b c (
Zlt0_not_eq _ H).
Definition Z_div_plus_l a b c H :=
Zdiv.Z_div_plus_full_l a b c (
Zlt0_not_eq _ H).
Hint Extern 2 (
Zle _ _) =>
(
match goal with
|-
Zpos _ <=
Zpos _ =>
exact (
refl_equal _)
|
H:
_ <= ?p |-
_ <= ?p =>
apply Zle_trans with (2 :=
H)
|
H:
_ < ?p |-
_ <= ?p =>
apply Zlt_le_weak;
apply Zle_lt_trans with (2 :=
H)
end).
Hint Extern 2 (
Zlt _ _) =>
(
match goal with
|-
Zpos _ <
Zpos _ =>
exact (
refl_equal _)
|
H:
_ <= ?p |-
_ <= ?p =>
apply Zlt_le_trans with (2 :=
H)
|
H:
_ < ?p |-
_ <= ?p =>
apply Zle_lt_trans with (2 :=
H)
end).
Hint Resolve Zlt_gt Zle_ge Z_div_pos:
zarith.
Theorem beta_lex:
forall a b c d beta,
a *
beta +
b <=
c *
beta +
d ->
0 <=
b <
beta -> 0 <=
d <
beta ->
a <=
c.
Theorem beta_lex_inv:
forall a b c d beta,
a <
c -> 0 <=
b <
beta ->
0 <=
d <
beta ->
a *
beta +
b <
c *
beta +
d.
Lemma beta_mult :
forall h l beta,
0 <=
h <
beta -> 0 <=
l <
beta -> 0 <=
h*beta+l <
beta^2.
Lemma Zmult_lt_b :
forall b x y, 0 <=
x <
b -> 0 <=
y <
b -> 0 <=
x *
y <=
b^2 - 2*b + 1.
Lemma sum_mul_carry :
forall xh xl yh yl wc cc beta,
1 <
beta ->
0 <=
wc <
beta ->
0 <=
xh <
beta ->
0 <=
xl <
beta ->
0 <=
yh <
beta ->
0 <=
yl <
beta ->
0 <=
cc <
beta^2 ->
wc*beta^2 +
cc =
xh*yl +
xl*yh ->
0 <=
wc <= 1.
Theorem mult_add_ineq:
forall x y cross beta,
0 <=
x <
beta ->
0 <=
y <
beta ->
0 <=
cross <
beta ->
0 <=
x *
y +
cross <
beta^2.
Theorem mult_add_ineq2:
forall x y c cross beta,
0 <=
x <
beta ->
0 <=
y <
beta ->
0 <=
c*beta +
cross <= 2*beta - 2 ->
0 <=
x *
y + (
c*beta +
cross) <
beta^2.
Theorem mult_add_ineq3:
forall x y c cross beta,
0 <=
x <
beta ->
0 <=
y <
beta ->
0 <=
cross <=
beta - 2 ->
0 <=
c <= 1 ->
0 <=
x *
y + (
c*beta +
cross) <
beta^2.
Hint Rewrite Zmult_1_r Zmult_0_r Zmult_1_l Zmult_0_l Zplus_0_l Zplus_0_r Zminus_0_r:
rm10.
Theorem Zmod_le_first:
forall a b, 0 <=
a -> 0 <
b -> 0 <=
a mod b <=
a.
Theorem Zmod_distr:
forall a b r t, 0 <=
a <=
b -> 0 <=
r -> 0 <=
t < 2 ^a ->
(2 ^a *
r +
t)
mod (2 ^
b) = (2 ^a *
r)
mod (2 ^
b) +
t.
Theorem Zmod_shift_r:
forall a b r t, 0 <=
a <=
b -> 0 <=
r -> 0 <=
t < 2 ^a ->
(
r * 2 ^a +
t)
mod (2 ^
b) = (
r * 2 ^a)
mod (2 ^
b) +
t.
Theorem Zdiv_shift_r:
forall a b r t, 0 <=
a <=
b -> 0 <=
r -> 0 <=
t < 2 ^a ->
(
r * 2 ^a +
t) / (2 ^
b) = (
r * 2 ^a) / (2 ^
b).
Lemma shift_unshift_mod :
forall n p a,
0 <=
a < 2^n ->
0 <=
p <=
n ->
a * 2^p =
a / 2^(n -
p) * 2^n + (
a*2^p)
mod 2^n.
Lemma shift_unshift_mod_2 :
forall n p a, 0 <=
p <=
n ->
((
a * 2 ^ (
n -
p))
mod (2^n) / 2 ^ (
n -
p))
mod (2^n) =
a mod 2 ^
p.
Lemma div_le_0 :
forall p x, 0 <=
x -> 0 <=
x / 2 ^
p.
Lemma div_lt :
forall p x y, 0 <=
x <
y ->
x / 2^p <
y.
Theorem Zgcd_div_pos a b:
0 <
b -> 0 <
Zgcd a b -> 0 <
b /
Zgcd a b.
Theorem Zdiv_neg a b:
a < 0 -> 0 <
b ->
a /
b < 0.
Lemma Zgcd_Zabs :
forall z z',
Zgcd (
Zabs z)
z' =
Zgcd z z'.
Lemma Zgcd_sym :
forall p q,
Zgcd p q =
Zgcd q p.
Lemma Zdiv_gcd_zero :
forall a b,
b /
Zgcd a b = 0 ->
b <> 0 ->
Zgcd a b = 0.
Lemma Zgcd_1 :
forall z,
Zgcd z 1 = 1.
Hint Resolve Zgcd_1.
Lemma Zgcd_mult_rel_prime :
forall a b c,
Zgcd a c = 1 ->
Zgcd b c = 1 ->
Zgcd (
a*b)
c = 1.
Lemma Zcompare_gt :
forall (
A:Type)(a
a':A)(p
q:Z),
match (
p?=q)%Z
with Gt =>
a |
_ =>
a' end =
if Z_le_gt_dec p q then a' else a.
Theorem Zbounded_induction :
(
forall Q :
Z ->
Prop,
forall b :
Z,
Q 0 ->
(
forall n, 0 <=
n ->
n <
b - 1 ->
Q n ->
Q (
n + 1)) ->
forall n, 0 <=
n ->
n <
b ->
Q n)%Z.
Lemma Zsquare_le :
forall x,
x <=
x*x.