Library Stdlib.ZArith.ZModOffset

Require Import BinInt Zdiv Zdiv_facts PreOmega Lia Wf_Z ZArith_dec.
Local Open Scope Z_scope.

Module Z.

Definition omodulo d a b := Z.modulo (a - d) b + d.

Lemma omodulo_0 a b : Z.omodulo 0 a b = Z.modulo a b.

Lemma div_omod d a b : b <> 0 -> a = b * ((a-d)/b) + omodulo d a b.

Lemma omod_pos_bound d a b : 0 < b -> d <= Z.omodulo d a b < d+b.

Lemma omod_neg_bound d a b : b < 0 -> d+b < Z.omodulo d a b <= d.

Definition omod_bound_or d a b (H : b <> 0) : _ \/ _ :=
  match Z_dec b 0 with
  | inleft (left neg) => or_introl (omod_neg_bound d a b neg)
  | inleft (right pos) => or_intror (omod_pos_bound d a b ltac:(lia))
  | inright zero => ltac:(lia)
  end.

Lemma omod_small_iff d a b :
  (d <= a < d+b \/ b = 0 \/ d+b < a <= d) <-> Z.omodulo d a b = a.

Lemma omod_small d a b : d <= a < d+b -> Z.omodulo d a b = a.

Lemma omod_small_neg d a b : d+b < a <= d -> Z.omodulo d a b = a.

Lemma omod_0_r d a : Z.omodulo d a 0 = a.

Local Ltac t := cbv [Z.omodulo]; repeat rewrite
  ?Zplus_mod_idemp_l, ?Zplus_mod_idemp_r, ?Zminus_mod_idemp_l, ?Zminus_mod_idemp_r, ?Z.add_simpl_r, ?Zmod_mod;
  try solve [trivial | lia | f_equal; lia].

Lemma omod_omod d a b : Z.omodulo d (Z.omodulo d a b) b = Z.omodulo d a b.

Lemma omod_mod d a b : Z.omodulo d (Z.modulo a b) b = Z.omodulo d a b.

Lemma mod_omod d a b : Z.modulo (Z.omodulo d a b) b = Z.modulo a b.

Lemma omod_inj_mod d x y m : x mod m = y mod m -> Z.omodulo d x m = Z.omodulo d y m.

Lemma mod_inj_omod d x y m : Z.omodulo d x m = Z.omodulo d y m -> x mod m = y mod m.

Lemma omod_idemp_add d x y m :
  Z.omodulo d (Z.omodulo d x m + Z.omodulo d y m) m = Z.omodulo d (x + y) m.

Lemma omod_idemp_sub d x y m :
  Z.omodulo d (Z.omodulo d x m - Z.omodulo d y m) m = Z.omodulo d (x - y) m.

Lemma omod_idemp_mul d x y m :
  Z.omodulo d (Z.omodulo d x m * Z.omodulo d y m) m = Z.omodulo d (x * y) m.

Lemma omod_diveq_iff c a b d :
  (b = 0 \/ c*b <= a - d < c*b + b \/ c*b + b < a - d <= c*b) <->
  Z.omodulo d a b = a-b*c.

Definition omod_diveq c a b d := proj1 (omod_diveq_iff c a b d).

Definition smodulo a b := Z.omodulo (- Z.quot b 2) a b.

Lemma div_smod a b : b <> 0 -> a = b * ((a+Z.quot b 2)/b) + Z.smodulo a b.

Lemma smod_eq a b : b <> 0 -> smodulo a b = a - b * ((a + Z.quot b 2) / b).

Lemma smod_pos_bound a b: 0 < b -> -b <= 2*Z.smodulo a b < b.

Lemma smod_neg_bound a b: b < 0 -> b < 2*Z.smodulo a b <= -b.

Definition smod_bound_or a b (H : b <> 0) : _ \/ _ :=
  match Z_dec b 0 with
  | inleft (left neg) => or_introl (smod_neg_bound a b neg)
  | inleft (right pos) => or_intror (smod_pos_bound a b ltac:(lia))
  | inright zero => ltac:(lia)
  end.

Lemma smod_smod a b : Z.smodulo (Z.smodulo a b) b = Z.smodulo a b.

Lemma smod_mod a b : Z.smodulo (Z.modulo a b) b = Z.smodulo a b.
Lemma mod_smod a b : Z.modulo (Z.smodulo a b) b = Z.modulo a b.

Lemma smod_inj_mod x y m : x mod m = y mod m -> Z.smodulo x m = Z.smodulo y m.

Lemma mod_inj_smod x y m : Z.smodulo x m = Z.smodulo y m -> x mod m = y mod m.

Lemma smod_idemp_add x y m :
  Z.smodulo (Z.smodulo x m + Z.smodulo y m) m = Z.smodulo (x + y) m.

Lemma smod_idemp_sub x y m :
  Z.smodulo (Z.smodulo x m - Z.smodulo y m) m = Z.smodulo (x - y) m.

Lemma smod_idemp_mul x y m :
  Z.smodulo (Z.smodulo x m * Z.smodulo y m) m = Z.smodulo (x * y) m.

Lemma smod_small_iff a b (d := - Z.quot b 2) :
  (- b <= 2*a - Z.rem b 2 < b \/ b = 0 \/ b < 2*a - Z.rem b 2 <= - b)
  <-> smodulo a b = a.

Lemma smod_even_small_iff a b (H : Z.rem b 2 = 0) :
  (-b <= 2*a < b \/ b = 0 \/ b < 2*a <= -b) <-> Z.smodulo a b = a.

Lemma smod_small a b : -b <= 2*a - Z.rem b 2 < b -> Z.smodulo a b = a.

Lemma smod_even_small a b : Z.rem b 2 = 0 -> -b <= 2*a < b -> Z.smodulo a b = a.

Lemma smod_pow2_small a w (H : 0 < w) : - 2 ^ w <= 2 * a < 2 ^ w -> Z.smodulo a (2^w) = a.

Lemma smod_small_neg a b : b < 2*a - Z.rem b 2 <= - b -> Z.smodulo a b = a.

Lemma smod_even_small_neg a b : Z.rem b 2 = 0 -> b < 2*a <= - b -> Z.smodulo a b = a.

Lemma smod_0_r a : Z.smodulo a 0 = a.

Lemma smod_0_l m : Z.smodulo 0 m = 0.

Lemma smod_diveq_iff c a b :
  (b = 0 \/ c*b <= a + Z.quot b 2 < c*b + b \/ c*b + b < a + Z.quot b 2 <= c * b) <->
  Z.smodulo a b = a-b*c.

Definition smod_diveq c a b := proj1 (smod_diveq_iff c a b).

Lemma smod_diveq_even_iff c a b :
  Z.rem b 2 = 0 ->
  (b = 0 \/ 2*c*b <= 2*a+b < 2*c*b + 2*b \/ 2*c*b+2*b < 2*a+b <= 2*c*b) <->
  Z.smodulo a b = a-b*c.

Definition smod_diveq_even c a b H := proj1 (smod_diveq_even_iff c a b H).

Lemma smod_smod_divide a b c : (c | b) -> Z.smodulo (Z.smodulo a b) c = Z.smodulo a c.

Lemma smod_complement a b h (H : b = 2*h) :
  Z.smodulo a b / h = - (Z.modulo a b / h).

Lemma smod_idemp_opp x m :
  Z.smodulo (- Z.smodulo x m) m = Z.smodulo (- x) m.

Lemma smod_pow_l a b c : Z.smodulo ((Z.smodulo a c) ^ b) c = Z.smodulo (a ^ b) c.

End Z.