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.

Definition Nabs_diff (x y: Z) := N_of_Z (Zmax (x - y) (y - x)).
Lemma Nabs_diff_case x y :
  x <= yNabs_diff x y = N_of_Z (y - x) ∨
  y <= xNabs_diff x y = N_of_Z (x - y).
Proof.
  unfold Nabs_diff. apply Zmax_case_strong; intuition.
Qed.

Definition Zdivides_dec (a b: Z) : { (a | b) } + { ¬ (a | b) }.
  refine (let q : Z := b / a in
          let r : Z := b - q * a in
          match Z_zerop r with
            | left H => left _
            | right H => right _
          end).
Proof.
  exists q. subst r q. omega.
  subst r q. intros (q & K). elim H. rewrite K. clear K.
  destruct (Z_zerop a). now subst; rewrite Zmult_comm.
  replace (q * a / a) with q. ring.
  rewrite Z_div_mult_full; intuition.
Defined.

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.