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.
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.