# Library Coqtail.Arith.Ztools

Require Import ZArith Omega Znumtheory.

# Contains some useful lemmas not in stdlib and a tactic

A convenient and simple tactic to prove 0<x or 0<>x

Lemma Zmult_neq_0_compat : a b, 0 a → 0 b → 0 a × b.
Proof.
intros [] [] P Q I; simpl in *;
inversion I; tauto.
Qed.

Lemma Zmult_le_1_compat : a b, 1 a → 1 b → 1 a × b.
Proof.
intros [|[]|[]][|[]|[]] H I; compute in *; eauto.
Qed.

Lemma Zsquare_pos : x, 0 x → 0 < x × x.
Proof.
intros [] E; simpl; reflexivity || tauto.
Qed.

Ltac notzero :=
lazymatch goal with
| |- ?a 0 ⇒ apply not_eq_sym; notzero
| |- ?a > 0 ⇒ cut (0 < a); [ apply Zcompare_Gt_Lt_antisym | ]; notzero
| |- 0 < ?a × ?aapply Zsquare_pos; notzero
| |- 0 < ?a ^ 2 ⇒ replace (a ^ 2) with (a × a) by ring; notzero
| |- 0 < ?a × ?bapply Zmult_lt_0_compat; notzero
| |- 0 ?a × ?bapply Zmult_neq_0_compat; notzero
| |- 0 < Zpos _reflexivity
| |- 0 > Zneg _reflexivity
| |- 0 Zpos _let I := fresh "I" in intros I; inversion I
| |- 0 Zneg _let I := fresh "I" in intros I; inversion I
| Pp : prime ?p |- 0 < ?ppose proof prime_ge_2 p Pp; omega
| Pp : prime ?p |- 0 ?ppose proof prime_ge_2 p Pp; omega
| |- 0 < _auto with *; try (zify; omega)
| |- 0 _auto with *; try (zify; omega)
| |- _idtac
end.

Extraction from the Zdivide predicate

Lemma Zdivide_inf : a b, (a | b){ q | b = q × a }.
Proof.
intros a b D.
(b / a).
rewrite Zmult_comm.
destruct (Z_eq_dec a 0).
subst; destruct D; omega.

apply Z_div_exact_full_2; auto with ×.
apply Zdivide_mod; auto.
Defined.

Lemma Z_mult_div_mod : a b, b 0 → b × (a / b) = a - a mod b.
Proof.
intros a b N.
pose proof Z_div_mod_eq_full a b N; omega.
Qed.

Lemma Zdivide_square : a b, (a | b)(a × a | b × b).
Proof.
intros a b (k, Ek).
(k × k); subst; ring.
Qed.

Lemma Zmult_divide_compat_rev_l: a b c : Z, c 0 → (c × a | c × b)(a | b).
Proof.
intros a b c Nc (k, Hk).
k.
eapply Zmult_reg_l; eauto.
rewrite Hk; ring.
Qed.

Lemma Z_mult_div_bounds : a b, 0 < ba - b < b × (a / b) a.
Proof.
intros a b N; split.
pose proof Z_mod_lt a b.
rewrite Z_mult_div_mod; omega.

apply Z_mult_div_ge; omega.
Qed.

Lemma Zle_0_square : a, 0 a × a.
Proof.
intros []; intuition.
simpl; intro H; inversion H.
Qed.

Lemma Zeq_0_square : a, a × a = 0 → a = 0.
Proof.
intros [] H; intuition simpl; inversion H.
Qed.

Lemma rewrite_power_2 : x, x ^ 2 = x × x.
Proof.
intros; ring.
Qed.

Lemma sqrt_eq_compat : a b, 0 a → 0 b
a × a = b × ba = b.
Proof.
intros a b Pa Pb E.
destruct (Z_eq_dec 0 (a + b)) as [F|F].
omega.

cut (a - b = 0); [ omega | ].
apply (Zmult_reg_l _ _ (a + b)); notzero.
ring_simplify.
rewrite rewrite_power_2, E.
ring.
Qed.

Lemma sqrt_eq_compat_abs : a b, a × a = b × bZabs a = Zabs b.
Proof.
intros a b E.
destruct (Z_eq_dec 0 (Zabs a + Zabs b)) as [F|F].
zify; omega.

cut (Zabs a - Zabs b = 0); [ omega | ].
apply (Zmult_reg_l _ _ (Zabs a + Zabs b)); notzero.
ring_simplify.
rewrite <- Zabs_square, <- (Zabs_square b) in E.
rewrite rewrite_power_2, E.
ring.
Qed.

Lemma sqrt_le_compat : a b, 0 a → 0 b
a × a b × ba b.
Proof.
intros a b Pa Pb E.
destruct (Z_eq_dec 0 (a + b)) as [F|F].
omega.

cut (0 b - a); [ omega | ].
apply Zmult_le_reg_r with (a + b); notzero.
ring_simplify.
do 2 rewrite rewrite_power_2; omega.
Qed.

Lemma Zabs_nat_inj : a b, 0 a → 0 bZabs_nat a = Zabs_nat ba = b.
Proof.
intros a b Pa Pb E.
rewrite <- (Zabs_eq a), <- (Zabs_eq b); eauto.
do 2 rewrite <- inj_Zabs_nat.
auto.
Qed.

Lemma Zdivide_square_rev : a b, (a × a | b × b)(a | b).
Proof.
intros a b D.
destruct (Z_eq_dec a 0).
subst; simpl in D.
destruct D as (q, Hq); ring_simplify (q × 0) in Hq.
destruct b; inversion Hq.
0; ring.

(b / a).
rewrite Zmult_comm, Z_mult_div_mod; auto.