# Module ZCongruences_defs

Require Import
Utf8 String Coqlib Util ShareTree Integers ArithLib AdomLib ToString
Axioms FastArith.

# Data type.

Record zcongr :=
ZC { zc_rem : Zfast;
zc_mod : Nfast;
zc_rem_itv : (zc_mod > 0)%N -> 0 <= zc_rem < zc_mod }.

Instance zc_gamma : gamma_op zcongr Z :=
fun x z => zx.(zc_rem) [x.(zc_mod)].

# Partial order.

Instance zc_leb : leb_op zcongr := fun (x y: zcongr) =>
if Nfasteqb y.(zc_mod) F0 then
Nfasteqb x.(zc_mod) F0 && Zfasteqb x.(zc_rem) y.(zc_rem)
else
Nfasteqb (Nfastmod x.(zc_mod) y.(zc_mod)) F0 &&
Zfasteqb (Zfastmod (Zfastsub x.(zc_rem) y.(zc_rem)) y.(zc_mod)) F0.

Instance zc_leb_correct : leb_op_correct zcongr Z.
Proof.
intros x y. simpl. unfold leb, zc_leb, zc_gamma. fastunwrap.
destruct (N.eqb_spec y.(zc_mod) 0);
rewrite Bool.andb_true_iff, N.eqb_eq, Z.eqb_eq; intros [? ?] ?.
- intros [? ?]. exists 0. Psatz.nia.
- apply N.mod_divide in H. 2:now auto. apply Zmod_divide in H0. 2:Psatz.lia.
assert (x.(zc_rem) ≡ y.(zc_rem) [y.(zc_mod)]).
{ destruct H0. exists (-x0). fastunwrap. Psatz.lia. }
intro. eapply congr_trans, H1. eapply congr_divide. eauto.
destruct H. exists x0. fastunwrap. Psatz.lia.
Qed.

Program Instance zc_top : top_op zcongr :=
let t := {| zc_rem := F0; zc_mod := F1; zc_rem_itv := _ |} in t.
Next Obligation.
omega. Qed.

Instance zc_top_correct : top_op_correct zcongr Z.
Proof.
intros i. exists (-i). simpl. ring. Qed.

Definition zc_share a a' :=
if Zfasteqb a.(zc_rem) a'.(zc_rem)
&& Nfasteqb a.(zc_mod) a'.(zc_mod) then a' else a.

Lemma zc_share_eq:
forall a a', zc_share a a' = a.
Proof.
unfold zc_share. intros. fastunwrap.
destruct (Z.eqb_spec a.(zc_rem) a'.(zc_rem)),
(N.eqb_spec a.(zc_mod) a'.(zc_mod)); auto.
destruct a as [[] []], a' as [[] []]; simpl in e, e0; subst. simpl.
f_equal; apply Axioms.proof_irr.
Qed.

# Lattice Structure.

Program Instance zc_join : join_op zcongr (zcongr+⊤) := fun x y =>
if Zfasteqb x.(zc_rem) y.(zc_rem)
&& Nfasteqb x.(zc_mod) y.(zc_mod) then Just x
else
let m := Nfastgcd (Nfastgcd x.(zc_mod) y.(zc_mod))
(Zfastabs (Zfastsub x.(zc_rem) y.(zc_rem))) in
if Nfasteqb m F1 then All
else
let res :=
{| zc_rem := if Nfasteqb m F0 then x.(zc_rem) else Zfastmod x.(zc_rem) m
; zc_mod := m |}
in
Just (zc_share (zc_share res x) y).
Next Obligation.
fastunwrap.
destruct (N.eqb_spec (N.gcd (N.gcd (zc_mod x) (zc_mod y))
(Z.abs_N (zc_rem x - zc_rem y))) 0).
- Psatz.lia.
- apply Z_mod_lt. Psatz.lia.
Qed.

Lemma zc_join_eq:
forall x:zcongr, xx = Just x.
Proof.
intros. unfold join, zc_join. fastunwrap. rewrite Z.eqb_refl, N.eqb_refl. auto.
Qed.

Instance zc_join_correct : join_op_correct zcongr (zcongr+⊤) Z.
Proof.
intros [[xr] [xm]] [[yr] [ym]] i.
simpl. unfold join, zc_join. simpl. rewrite !zc_share_eq. fastunwrap.
destruct ((xr =? yr) && (xm =? ym)%N) eqn:?.
rewrite Bool.andb_true_iff, Z.eqb_eq, N.eqb_eq in Heqb. destruct Heqb as [-> ->].
now intuition.
destruct (N.eqb_spec (Nfastgcd (Nfastgcd xm ym) (Z.abs_N (xr - yr))) 1). easy.
unfold γ, zc_gamma. simpl. fastunwrap.
case_eq (N.gcd (N.gcd xm ym) (Z.abs_N (xr - yr))).
- repeat rewrite N.gcd_eq_0.
intros ((-> & ->) & XY).
assert (xr = yr) by Psatz.lia. subst. intuition.
- unfold Neqb. intros p H; rewrite <- H. intros [X|Y].
+ eapply congr_trans. 2:eapply congr_mod_compat.
eapply congr_divide. eassumption.
repeat rewrite Ngcd_is_Zgcd.
eapply Zdivides_trans; apply Zgcd_divides_l.
rewrite H; reflexivity.
+ eapply congr_trans. 2:eapply congr_mod_compat.
2: rewrite H; reflexivity.
repeat rewrite Ngcd_is_Zgcd.
apply congr_trans with (xr + (yr - xr)).
replace (xr + (yr - xr)) with yr by ring.
eapply congr_divide. eassumption.
eapply Zdivides_trans. apply Zgcd_divides_l. apply Zgcd_divides_r.
eapply congr_divide.
2: apply Zgcd_divides_r. rewrite N2Z.inj_abs_N. apply Zabs_ind.
exists 1. ring. exists (-1). ring.
Qed.

Program Instance zc_meet : meet_op zcongr (zcongr+⊥) := fun x y =>
let '(gcd, xx, yy) := eucl_alg x.(zc_mod) y.(zc_mod) return _ in
let d := Zfastsub x.(zc_rem) y.(zc_rem) in
if divide d gcd then
let q := Zfastdiv d (Zfast_of_Nfast gcd) in
let m := Nfastmul x.(zc_mod) (Nfastdiv y.(zc_mod) gcd) in
let r := Zfastsub x.(zc_rem) (Zfastmul (Zfastmul x.(zc_mod) xx) q) in
let r := if Nfasteqb m F0 then r else Zfastmod r m in
let res := {| zc_rem := r; zc_mod := m |} in
NotBot (zc_share (zc_share res x) y)
else Bot.
Next Obligation.
fastunwrap. rewrite (proj2 (N.eqb_neq _ _)). apply Z.mod_pos_bound.
Psatz.lia. Psatz.lia.
Qed.

Instance zc_meet_correct : meet_op_correct zcongr (zcongr+⊥) Z.
Proof.
intros [[xr] [xm]] [[yr] [ym]] i.
simpl. unfold meet, zc_meet. simpl.
pose proof eucl_alg_bezout xm ym.
pose proof Nfastgcd_Ngcd xm ym. unfold Nfastgcd in H0.
destruct (eucl_alg xm ym) as [[[gcd] [xx]] [yy]]. specialize (H _ _ _ eq_refl).
simpl in *. rewrite !zc_share_eq. fastunwrap. unfold zc_gamma. simpl.
pose proof (Z.gcd_divide_l xm ym). pose proof (Z.gcd_divide_r xm ym).
intros [? ?]. fastunwrap. inv H0. rewrite <- Ngcd_is_Zgcd in H1, H2.
fold (N.lcm xm ym).
assert (Z.of_N (N.gcd xm ym) | (xr -yr)).
{ eapply congr_divide in H3; eauto. eapply congr_divide in H4; eauto.
pose proof congr_minus_compat _ _ _ _ _ H3 H4.
rewrite Z.sub_diag in H0. destruct H0. rewrite H0. exists x. auto. }
rewrite (proj2 (divide_ok (xr - yr) (N.gcd xm ym)) H0).
simpl. destruct (Z.leb_spec xm 0). 2:destruct (Z.leb_spec ym 0).
- fastunwrap. assert (xm = 0%N) by Psatz.lia. subst. simpl. rewrite Z.sub_0_r. auto.
- fastunwrap. assert (ym = 0%N) by Psatz.lia. subst.
rewrite N.lcm_0_r, N.gcd_0_r in *. simpl.
replace (Z.of_N xm * xx) with (Z.of_N xm) by Psatz.lia.
rewrite <- Zdivide_Zdiv_eq. replace (xr-(xr-yr)) with yr by ring. auto.
Psatz.lia. destruct H3, H4. exists x. Psatz.lia.
- fastunwrap.
destruct (N.eqb_spec (N.lcm xm ym) 0). apply N.lcm_eq_0 in e. Psatz.lia.
eapply congr_trans, congr_mod_compat. 2:Psatz.lia.
cut (Z.of_N (N.lcm xm ym) |
xr - Z.of_N xm * xx * ((xr - yr) / Z.of_N (N.gcd xm ym)) - i).
{ intros [x ?]. exists x. Psatz.lia. }
rewrite Nlcm_is_Zlcm. apply Z.lcm_least.
+ destruct H3. exists (x - xx * ((xr - yr) / Z.of_N (N.gcd xm ym))). Psatz.lia.
+ replace (Z.of_N xm * xx) with (Z.of_N (N.gcd xm ym) - yy * Z.of_N ym) by Psatz.lia.
rewrite Z.mul_sub_distr_r, <- Zdivide_Zdiv_eq. 3:now auto.
destruct H4. exists (x + yy * ((xr - yr) / Z.of_N (N.gcd xm ym))). Psatz.lia.
{ cut (N.gcd xm ym <> 0%N). Psatz.lia.
intro. rewrite H7 in H1. destruct H1. Psatz.lia. }
Qed.

Instance zc_to_string : ToString zcongr := λ zc,
("≡ " ++ to_string zc.(zc_rem) ++
" [" ++ to_string zc.(zc_mod) ++ "]")%string.