# 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.