Require Export ZArith_base.
Require Import Zbool Omega ZArithRing Zcomplements Setoid Morphisms.
Local Open Scope Z_scope.

Notation Zdiv_eucl_POS := Z.pos_div_eucl (compat "8.3").
Notation Zdiv_eucl := Z.div_eucl (compat "8.3").
Notation Zdiv := Z.div (compat "8.3").
Notation Zmod := Z.modulo (compat "8.3").

Notation Zdiv_eucl_eq := Z.div_eucl_eq (compat "8.3").
Notation Z_div_mod_eq_full := Z.div_mod (compat "8.3").
Notation Zmod_POS_bound := Z.pos_div_eucl_bound (compat "8.3").
Notation Zmod_pos_bound := Z.mod_pos_bound (compat "8.3").
Notation Zmod_neg_bound := Z.mod_neg_bound (compat "8.3").

Lemma Z_div_mod_POS :
  forall b:Z,
    b > 0 ->
    forall a:positive,
      let (q, r) := Z.pos_div_eucl a b in Zpos a = b * q + r /\ 0 <= r < b.

Theorem Z_div_mod a b :
  b > 0 ->
  let (q, r) := Z.div_eucl a b in a = b * q + r /\ 0 <= r < b.

Definition Remainder r b := 0 <= r < b \/ b < r <= 0.

Definition Remainder_alt r b := Z.abs r < Z.abs b /\ Z.sgn r <> - Z.sgn b.


Lemma Remainder_equiv : forall r b, Remainder r b <-> Remainder_alt r b.

Hint Unfold Remainder.

Theorem Z_div_mod_full a b :
  b <> 0 ->
  let (q, r) := Z.div_eucl a b in a = b * q + r /\ Remainder r b.

Lemma Z_mod_remainder a b : b<>0 -> Remainder (a mod b) b.

Lemma Z_mod_lt a b : b > 0 -> 0 <= a mod b < b.

Lemma Z_mod_neg a b : b < 0 -> b < a mod b <= 0.

Lemma Z_div_mod_eq a b : b > 0 -> a = b*(a/b) + (a mod b).

Lemma Zmod_eq_full a b : b<>0 -> a mod b = a - (a/b)*b.

Lemma Zmod_eq a b : b>0 -> a mod b = a - (a/b)*b.

Theorem Zdiv_eucl_exist : forall (b:Z)(Hb:b>0)(a:Z),
 {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < b}.

Theorem Zdiv_mod_unique b q1 q2 r1 r2 :
  0 <= r1 < Z.abs b -> 0 <= r2 < Z.abs b ->
  b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2.

Theorem Zdiv_mod_unique_2 :
 forall b q1 q2 r1 r2:Z,
  Remainder r1 b -> Remainder r2 b ->
  b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2.

Theorem Zdiv_unique_full:
 forall a b q r, Remainder r b ->
   a = b*q + r -> q = a/b.

Theorem Zdiv_unique:
 forall a b q r, 0 <= r < b ->
   a = b*q + r -> q = a/b.

Theorem Zmod_unique_full:
 forall a b q r, Remainder r b ->
  a = b*q + r -> r = a mod b.

Theorem Zmod_unique:
 forall a b q r, 0 <= r < b ->
  a = b*q + r -> r = a mod b.

Lemma Zmod_0_l: forall a, 0 mod a = 0.

Lemma Zmod_0_r: forall a, a mod 0 = 0.

Lemma Zdiv_0_l: forall a, 0/a = 0.

Lemma Zdiv_0_r: forall a, a/0 = 0.

Ltac zero_or_not a :=
  destruct (Z.eq_dec a 0);
  [subst; rewrite ?Zmod_0_l, ?Zdiv_0_l, ?Zmod_0_r, ?Zdiv_0_r;
   auto with zarith|].

Lemma Zmod_1_r: forall a, a mod 1 = 0.

Lemma Zdiv_1_r: forall a, a/1 = a.

Hint Resolve Zmod_0_l Zmod_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_1_r
 : zarith.

Lemma Zdiv_1_l: forall a, 1 < a -> 1/a = 0.

Lemma Zmod_1_l: forall a, 1 < a -> 1 mod a = 1.

Lemma Z_div_same_full : forall a:Z, a<>0 -> a/a = 1.

Lemma Z_mod_same_full : forall a, a mod a = 0.

Lemma Z_mod_mult : forall a b, (a*b) mod b = 0.

Lemma Z_div_mult_full : forall a b:Z, b <> 0 -> (a*b)/b = a.

Lemma Z_div_pos: forall a b, b > 0 -> 0 <= a -> 0 <= a/b.

Lemma Z_div_ge0: forall a b, b > 0 -> a >= 0 -> a/b >=0.

Lemma Z_div_lt : forall a b:Z, b >= 2 -> a > 0 -> a/b < a.

Theorem Zdiv_small: forall a b, 0 <= a < b -> a/b = 0.

Theorem Zmod_small: forall a n, 0 <= a < n -> a mod n = a.

Lemma Z_div_ge : forall a b c:Z, c > 0 -> a >= b -> a/c >= b/c.

Lemma Z_div_le : forall a b c:Z, c > 0 -> a <= b -> a/c <= b/c.

Lemma Z_mult_div_ge : forall a b:Z, b > 0 -> b*(a/b) <= a.

Lemma Z_mult_div_ge_neg : forall a b:Z, b < 0 -> b*(a/b) >= a.

Lemma Z_div_exact_full_1 : forall a b:Z, a = b*(a/b) -> a mod b = 0.

Lemma Z_div_exact_full_2 : forall a b:Z, b <> 0 -> a mod b = 0 -> a = b*(a/b).

Theorem Zmod_le: forall a b, 0 < b -> 0 <= a -> a mod b <= a.

Theorem Zdiv_lt_upper_bound:
  forall a b q, 0 < b -> a < q*b -> a/b < q.

Theorem Zdiv_le_upper_bound:
  forall a b q, 0 < b -> a <= q*b -> a/b <= q.

Theorem Zdiv_le_lower_bound:
  forall a b q, 0 < b -> q*b <= a -> q <= a/b.

Lemma Zdiv_le_compat_l: forall p q r, 0 <= p -> 0 < q < r ->
    p / r <= p / q.

Theorem Zdiv_sgn: forall a b,
  0 <= Z.sgn (a/b) * Z.sgn a * Z.sgn b.

Lemma Z_mod_plus_full : forall a b c:Z, (a + b * c) mod c = a mod c.

Lemma Z_div_plus_full : forall a b c:Z, c <> 0 -> (a + b * c) / c = a / c + b.

Theorem Z_div_plus_full_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b.

Lemma Zdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b.

Lemma Zmod_opp_opp : forall a b:Z, (-a) mod (-b) = - (a mod b).

Lemma Z_mod_zero_opp_full : forall a b:Z, a mod b = 0 -> (-a) mod b = 0.

Lemma Z_mod_nz_opp_full : forall a b:Z, a mod b <> 0 ->
 (-a) mod b = b - (a mod b).

Lemma Z_mod_zero_opp_r : forall a b:Z, a mod b = 0 -> a mod (-b) = 0.

Lemma Z_mod_nz_opp_r : forall a b:Z, a mod b <> 0 ->
 a mod (-b) = (a mod b) - b.

Lemma Z_div_zero_opp_full : forall a b:Z, a mod b = 0 -> (-a)/b = -(a/b).

Lemma Z_div_nz_opp_full : forall a b:Z, a mod b <> 0 ->
 (-a)/b = -(a/b)-1.

Lemma Z_div_zero_opp_r : forall a b:Z, a mod b = 0 -> a/(-b) = -(a/b).

Lemma Z_div_nz_opp_r : forall a b:Z, a mod b <> 0 ->
 a/(-b) = -(a/b)-1.

Lemma Zdiv_mult_cancel_r : forall a b c:Z,
 c <> 0 -> (a*c)/(b*c) = a/b.

Lemma Zdiv_mult_cancel_l : forall a b c:Z,
 c<>0 -> (c*a)/(c*b) = a/b.

Lemma Zmult_mod_distr_l: forall a b c,
  (c*a) mod (c*b) = c * (a mod b).

Lemma Zmult_mod_distr_r: forall a b c,
  (a*c) mod (b*c) = (a mod b) * c.

Theorem Zmod_mod: forall a n, (a mod n) mod n = a mod n.

Theorem Zmult_mod: forall a b n,
 (a * b) mod n = ((a mod n) * (b mod n)) mod n.

Theorem Zplus_mod: forall a b n,
 (a + b) mod n = (a mod n + b mod n) mod n.

Theorem Zminus_mod: forall a b n,
 (a - b) mod n = (a mod n - b mod n) mod n.

Lemma Zplus_mod_idemp_l: forall a b n, (a mod n + b) mod n = (a + b) mod n.

Lemma Zplus_mod_idemp_r: forall a b n, (b + a mod n) mod n = (b + a) mod n.

Lemma Zminus_mod_idemp_l: forall a b n, (a mod n - b) mod n = (a - b) mod n.

Lemma Zminus_mod_idemp_r: forall a b n, (a - b mod n) mod n = (a - b) mod n.

Lemma Zmult_mod_idemp_l: forall a b n, (a mod n * b) mod n = (a * b) mod n.

Lemma Zmult_mod_idemp_r: forall a b n, (b * (a mod n)) mod n = (b * a) mod n.

Section EqualityModulo.
Variable N:Z.

Definition eqm a b := (a mod N = b mod N).
Infix "==" := eqm (at level 70).

Lemma eqm_refl : forall a, a == a.

Lemma eqm_sym : forall a b, a == b -> b == a.

Lemma eqm_trans : forall a b c,
  a == b -> b == c -> a == c.

Instance eqm_setoid : Equivalence eqm.

Instance Zplus_eqm : Proper (eqm ==> eqm ==> eqm) Z.add.

Instance Zminus_eqm : Proper (eqm ==> eqm ==> eqm) Z.sub.

Instance Zmult_eqm : Proper (eqm ==> eqm ==> eqm) Z.mul.

Instance Zopp_eqm : Proper (eqm ==> eqm) Z.opp.

Lemma Zmod_eqm : forall a, (a mod N) == a.


End EqualityModulo.

Lemma Zdiv_Zdiv : forall a b c, 0<=b -> 0<=c -> (a/b)/c = a/(b*c).

Theorem Zdiv_mult_le:
 forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b.

Lemma Zmod_divides : forall a b, b<>0 ->
 (a mod b = 0 <-> exists c, a = b*c).

Lemma Zdiv2_div : forall a, Z.div2 a = a/2.

Lemma Zmod_odd : forall a, a mod 2 = if Z.odd a then 1 else 0.

Lemma Zmod_even : forall a, a mod 2 = if Z.even a then 0 else 1.

Lemma Zodd_mod : forall a, Z.odd a = Zeq_bool (a mod 2) 1.

Lemma Zeven_mod : forall a, Z.even a = Zeq_bool (a mod 2) 0.

Lemma Z_mod_same : forall a, a > 0 -> a mod a = 0.

Lemma Z_div_same : forall a, a > 0 -> a/a = 1.

Lemma Z_div_plus : forall a b c:Z, c > 0 -> (a + b * c) / c = a / c + b.

Lemma Z_div_mult : forall a b:Z, b > 0 -> (a*b)/b = a.

Lemma Z_mod_plus : forall a b c:Z, c > 0 -> (a + b * c) mod c = a mod c.

Lemma Z_div_exact_1 : forall a b:Z, b > 0 -> a = b*(a/b) -> a mod b = 0.

Lemma Z_div_exact_2 : forall a b:Z, b > 0 -> a mod b = 0 -> a = b*(a/b).

Lemma Z_mod_zero_opp : forall a b:Z, b > 0 -> a mod b = 0 -> (-a) mod b = 0.

Fixpoint Zmod_POS (a : positive) (b : Z) : Z :=
  match a with
   | xI a´ =>
      let r := Zmod_POS a´ b in
      let r´ := (2 * r + 1) in
      if r´ <? b then r´ else (r´ - b)
   | xO a´ =>
      let r := Zmod_POS a´ b in
      let r´ := (2 * r) in
      if r´ <? b then r´ else (r´ - b)
   | xH => if 2 <=? b then 1 else 0
  end.

Definition Zmod´ a b :=
  match a with
   | Z0 => 0
   | Zpos a´ =>
      match b with
       | Z0 => 0
       | Zpos _ => Zmod_POS a´ b
       | Zneg b´ =>
          let r := Zmod_POS a´ (Zpos b´) in
          match r with Z0 => 0 | _ => b + r end
      end
   | Zneg a´ =>
      match b with
       | Z0 => 0
       | Zpos _ =>
          let r := Zmod_POS a´ b in
          match r with Z0 => 0 | _ => b - r end
       | Zneg b´ => - (Zmod_POS a´ (Zpos b´))
      end
  end.

Theorem Zmod_POS_correct a b : Zmod_POS a b = snd (Z.pos_div_eucl a b).

Theorem Zmod´_correct: forall a b, Zmod´ a b = a mod b.

Theorem Zdiv_eucl_extended :
  forall b:Z,
    b <> 0 ->
    forall a:Z,
      {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b}.

Require Import NPeano.

Lemma div_Zdiv (n m: nat): m <> O ->
  Z.of_nat (n / m) = Z.of_nat n / Z.of_nat m.

Lemma mod_Zmod (n m: nat): m <> O ->
  Z.of_nat (n mod m) = (Z.of_nat n) mod (Z.of_nat m).