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.
Local Open 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 Zdiv_gcd_zero :
forall a b,
b / Zgcd a b = 0 ->
b <> 0 ->
Zgcd a b = 0.
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.