Module ArithLib

Require Import Znumtheory.
Require Import ZArith.
Require Import Setoid.
Require Import Ring.
Require Import Omega.
Require Import FastArith.
Require Import Coqlib.

Local Open Scope Z_scope.

Section Congruence.

Definition congr n x y : Prop :=
exists q, y = x + q * n.

Lemma congr_refl : forall n x, congr n x x.
Proof.
intros n x; exists 0; auto with zarith. Qed.

Lemma congr_sym : forall n x y, congr n x y -> congr n y x.
Proof.
intros n x y [q Hq]. exists (-q); rewrite Hq.
ring.
Qed.

Lemma congr_trans n : transitive _ (congr n).
Proof.
intros x y z [q Hq] [r Hr].
exists (q + r).
rewrite Hr; rewrite Hq.
rewrite Zmult_plus_distr_l.
rewrite Zplus_assoc.
reflexivity.
Qed.

Lemma congr_0_eq : forall x y, congr 0 x y -> x = y.
Proof.
intros x y [q Hq]; rewrite Hq.
simpl.
auto with zarith.
Qed.

Lemma congr_1 : forall x y, congr 1 x y.
Proof.
intros x y; exists (y - x). simpl.
omega.
Qed.

Lemma congr_divide : forall n m x y,
congr n x y -> (m | n) ->
congr m x y.
Proof.
intros n m x y [kn Hn] [km Hm].
exists (kn * km).
rewrite Hn; rewrite Hm.
auto with zarith.
Qed.

Lemma congr_plus_compat_l : forall n x y m,
congr n x y ->
congr n (x + m) (y + m).
Proof.
intros n x y m [q Hq].
exists q.
rewrite Hq.
ring.
Qed.

Lemma congr_minus_compat_l : forall n x y m,
congr n x y ->
congr n (x - m) (y - m).
Proof.
intros n x y m [q Hq].
exists q.
rewrite Hq.
ring.
Qed.

Lemma congr_minus_compat n x y z t :
congr n x y ->
congr n z t ->
congr n (x - z) (y - t).
Proof.
intros [a ->] [b ->].
exists (a - b). ring.
Qed.

Lemma congr_neg_compat n x y :
congr n x y ->
congr n (-x) (-y).
Proof.
intros [q ->].
exists (-q). ring.
Qed.

Lemma congr_plus_compat : forall n x y z t,
congr n x y -> congr n z t ->
congr n (x + z) (y + t).
Proof.
intros n x y z t [a Ha] [b Hb].
exists (a + b).
rewrite Ha. rewrite Hb.
ring.
Qed.

Lemma congr_diff : forall a b,
congr (a - b) a b.
Proof.
intros a b.
destruct (Z_eq_dec a b).
subst; apply congr_refl.
exists (-1); auto with zarith.
Qed.

Lemma congr_mod_compat : forall n x, n > 0 ->
congr n x (x mod n).
Proof.
intros n x H.
rewrite (Zmod_eq _ _ H).
exists (- (x / n)).
unfold Zminus.
rewrite Zopp_mult_distr_l.
reflexivity.
Qed.

Lemma congr_eqm : forall n x y, n > 0 ->
congr n x y -> eqm n x y.
Proof.
intros n x y POS (q & ->).
symmetry. apply Z_mod_plus. auto.
Qed.

Lemma eqm_congr : forall n x y, n > 0 ->
eqm n x y -> congr n x y.
Proof.
intros n x y POS EQM. unfold eqm in *.
exists (y / n - x / n).
replace (x + (y / n - x / n) * n) with (y / n * n + (x - x / n * n)) by ring.
assert (n <> 0) by intuition.
rewrite <- Zmod_eq_full; auto.
rewrite EQM.
rewrite Zmod_eq_full; auto.
ring.
Qed.

Lemma congr_mult_l_compat :
forall n p x y,
congr n x y ->
congr (p * n) (p * x) (p * y).
Proof.
intros n p x y (q & ->). exists q. ring.
Qed.

Definition divide (x:Zfast) (y:Nfast) : bool :=
if Nfasteqb y F0 then Zfasteqb x F0
else Zfasteqb (Zfastmod x y) F0.

Lemma divide_ok:
forall x y, divide x y = true <-> (Zfast_of_Nfast y | x).
Proof.
intros [x] [y]. unfold divide. fastunwrap. destruct (N.eqb_spec y 0); split.
- subst. intro. apply Z.eqb_eq in H. subst. exists 0. auto.
- subst. intros [? ?]. destruct x, x0; try discriminate; auto.
- intro. apply Zmod_divide, Z.eqb_eq, H. Psatz.lia.
- intro. apply Z.eqb_eq, Zdivide_mod, H.
Qed.

End Congruence.

Hint Resolve congr_refl congr_trans congr_sym congr_0_eq congr_1 : congr.

Notation "xy [ n ]" := (congr n x y) (at level 80).

Section on_gcd.

Variables a b : Z.

Lemma Zgcd_divides_l : (Zgcd a b | a).
Proof.
destruct (Zgcd_is_gcd a b).
assumption.
Qed.

Lemma Zgcd_divides_r : (Zgcd a b | b).
Proof.
destruct (Zgcd_is_gcd a b).
assumption.
Qed.

End on_gcd.

Require Import Utf8.
Require Psatz.

Remark Ngcd_is_Zgcd (x y: N) : (Z.of_N (N.gcd x y)) = Zgcd (Z.of_N x) (Z.of_N y).
Proof.
destruct x, y; reflexivity. Qed.

Remark Nlcm_is_Zlcm (x y: N) : (Z.of_N (N.lcm x y)) = Z.lcm (Z.of_N x) (Z.of_N y).
Proof.
unfold N.lcm, Z.lcm.
rewrite <- Ngcd_is_Zgcd, <- N2Z.inj_div, <- N2Z.inj_mul.
zify. omega.
Qed.

Lemma N_div_eucl_spec a b :
let (q, r) := N.div_eucl a b in
a = (b * q + r)%N
(b ≠ 0 → r < b)%N.
Proof.
generalize (N.div_eucl_spec a b).
generalize (N.mod_lt a b). unfold N.modulo.
destruct N.div_eucl. intuition.
Qed.