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 => z ≡ x.(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, x ⊔ x = 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.
Generated by coq2html