Library prosa.classic.util.div_mod

Require Export prosa.util.div_mod.

Require Import Arith Nat.
Require Import prosa.classic.util.tactics mathcomp.zify.zify prosa.classic.util.nat.

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.

  Definition div_floor (x y: nat) : nat := x %/ y.
  Definition div_ceil (x y: nat) := if y %| x then x %/ y else (x %/ y).+1.

  Lemma ltn_div_trunc :
     m n d,
      d > 0
      m %/ d < n %/ d
      m < n.
  Proof.
    intros m n d GT0 DIV; rewrite ltn_divLR in DIV; last by ins.
    by apply leq_trans with (n := n %/ d × d);
      [by ins| by apply leq_trunc_div].
  Qed.

  Lemma subndiv_eq_mod:
     n d, n - n %/ d × d = n %% d.
  Proof.
    by ins; rewrite {1}(divn_eq n d) addnC -addnBA // subnn addn0.
  Qed.

  Lemma divSn_cases :
     n d,
      d > 1
      (n %/ d = n.+1 %/d n %% d + 1 = n.+1 %% d)
      (n %/ d + 1 = n.+1 %/ d).
  Proof.
    ins; set x := n %/ d; set y := n %% d.
    assert (GT0: d > 0); first by apply ltn_trans with (n := 1).
    destruct (ltngtP y (d - 1)) as [LTN | BUG | GE]; [left | | right];
      first 1 last.
    {
      exploit (@ltn_pmod n d); [by apply GT0 | intro LTd; fold y in LTd].
      rewrite -(ltn_add2r 1) [y+1]addn1 ltnS in BUG.
      rewrite addnBAC in BUG; last by apply GT0.
      rewrite -addnBA // subnn addn0 in BUG.
      by apply (leq_ltn_trans BUG) in LTd; rewrite ltnn in LTd.
    }

    {
      (* Case 1: y = d - 1*)
      move: GE ⇒ /eqP GE; rewrite -(eqn_add2r 1) in GE.
      rewrite addnBAC in GE; last by apply GT0.
      rewrite -addnBA // subnn addn0 in GE.
      move: GE ⇒ /eqP GE.
      apply f_equal with (f := fun xx %/ d) in GE.
      rewrite divnn GT0 /= in GE.
      unfold x; rewrite -GE.
      rewrite -divnMDl; last by apply GT0.
      f_equal; rewrite addnA.
      by rewrite -divn_eq addn1.
    }
    {
      assert (EQDIV: n %/ d = n.+1 %/ d).
      {
        apply/eqP; rewrite eqn_leq; apply/andP; split;
          first by apply leq_div2r, leqnSn.
        rewrite leq_divRL; last by apply GT0.
        rewrite -ltnS {2}(divn_eq n.+1 d).
        rewrite -{1}[_ %/ d × d]addn0 ltn_add2l.
        unfold y in ×.
        rewrite ltnNge; apply/negP; unfold not; intro BUG.
        rewrite leqn0 in BUG; move: BUG ⇒ /eqP BUG.
        rewrite -(modnn d) -addn1 in BUG.
        destruct d; first by rewrite sub0n in LTN.
        move: BUG; move/eqP; rewrite -[d.+1]addn1 eqn_modDr [d+1]addn1; move ⇒ /eqP BUG.
        rewrite BUG -[d.+1]addn1 -addnBA // subnn addn0 in LTN.
        by rewrite modn_small in LTN;
          [by rewrite ltnn in LTN | by rewrite addn1 ltnSn].
      }
      (* Case 2: y < d - 1 *)
      split; first by rewrite -EQDIV.
      {
        unfold x, y in ×.
        rewrite -2!subndiv_eq_mod.
        rewrite addnBAC ?addn1; last by apply leq_trunc_div.
        rewrite EQDIV; apply/eqP.
        rewrite -(eqn_add2r (n%/d×d)).
        by rewrite addnBAC; last by apply leq_trunc_div.
      }
    }
  Qed.

  Lemma ceil_neq0 :
     x y,
      x > 0
      y > 0
      div_ceil x y > 0.
  Proof.
    unfold div_ceil; intros x y GEx GEy.
    destruct (y %| x) eqn:DIV; last by done.
    by rewrite divn_gt0; first by apply dvdn_leq.
  Qed.

  Lemma leq_divceil2r :
     d m n,
      d > 0
      m n
      div_ceil m d div_ceil n d.
  Proof.
    unfold div_ceil; intros d m n GT0 LE.
    destruct (d %| m) eqn:DIVm, (d %| n) eqn:DIVn;
      [by apply leq_div2r | | | by apply leq_div2r].
    by apply leq_trans with (n := n %/ d); first by apply leq_div2r.
    {
      rewrite leq_eqVlt in LE; move: LE ⇒ /orP [/eqP EQ | LT];
        first by subst; rewrite DIVn in DIVm.
      rewrite ltn_divLR //.
      apply leq_trans with (n := n); first by done.
      by apply eq_leq; symmetry; apply/eqP; rewrite -dvdn_eq.
    }
  Qed.

(* Versions of eqn_modDl and eqn_modDl in Prop *)

  Lemma eq_modDl: p m n d, (p + m = p + n %[mod d]) (m = n %[mod d]).
  Proof.
    split; intro G.
    - apply /eqP. rewrite <- eqn_modDl with (p:=p).
      by apply /eqP.
    - rewrite -modnDm G.
      by rewrite modnDm.
  Qed.

  Lemma eq_modDr: p m n d, (m + p = n + p %[mod d]) (m = n %[mod d]).
  Proof.
    split; intro G.
    - apply /eqP. rewrite <- eqn_modDr with (p:=p).
      by apply /eqP.
    - rewrite -modnDm G.
      by rewrite modnDm.
  Qed.

  (* If a(n)= b+a (n) then b is a multiple of c 
    Proposed name modnD_k *)


  Lemma modulo_exists: a b c,
    c>0 a = b + a %[mod c] k, b = k×c.
  Proof.
    intros× F G.
    change a with (0+a) in G.
    apply eq_modDr in G.
    rewrite mod0n in G.
    assert (X: b = b%/c ×c + b%%c) by apply divn_eq.
    rewrite -G addn0 in X.
    by (b%/c).
  Qed.

  (* If (a+1)n+1=0 then an+1=n *)
  Lemma modnS_eq : a n, a.+1 %% n.+1 =0 a %% n.+1 = n.
  Proof.
    intros.
    rewrite -(modnn (n.+1)).
    change (a.+1) with (1+a).
    change (n.+1) with (1+n).
    assert (X:n<n.+1) by lia.
    apply modn_small in X.
    split; intros× G.
    - apply eq_modDl in G.
      by rewrite G.
    - apply eq_modDl.
      by rewrite G.
  Qed.

  (* Incrementing the integer under a modulo either increments the result or yields 0 *)

  Lemma modnSor': a n, a.+1 %% n = (a %% n).+1 (a.+1 %% n =0).
  Proof.
    intros×.
    destruct (ltngtP ((a%%n).+1) (n)) as [G|G|G].
    - left. apply modn_small in G.
      by rewrite -G -addn1 -modnDml addn1.
    - destruct n.
      + left. reflexivity.
      + assert (X: a%%n.+1 < n.+1). by apply ltn_pmod. lia.
    - right. destruct n.
      + discriminate G.
      + apply modnS_eq. by injection G.
  Qed.

  Lemma modnSor: a n, a.+1 %% n.+1 = (a %% n.+1).+1 (a.+1 %% n.+1 =0).
  Proof.
    intros.
    destruct (ltngtP ((a%%n.+1).+1) (n.+1)) as [G|G|G].
    - left. apply modn_small in G.
      by rewrite -G -addn1 -modnDml addn1.
    - assert (X: a%%n.+1 < n.+1). by apply ltn_pmod. lia.
    - right. apply modnS_eq. lia.
  Qed.

  (* Old version of the lemma which is now covered by modnSor and modnS_eq *)

  Lemma modulo_cases : a c,
    a.+1 %% c.+1 = (a %% c.+1).+1 (a.+1 %% c.+1 =0 a %% c.+1 =c).
  Proof.
    intros. destruct (modnSor a c) as [G|G]; try by left.
    right; split; try done.
    by apply modnS_eq.
  Qed.

  Lemma ceil_eq1: a c, a > 0 a c div_ceil a c = 1.
  Proof.
    intros× G1. unfold div_ceil.
    rewrite leq_eqVlt. move/orP ⇒ [G2|G2].
    - move/eqP :G2G2. subst.
      rewrite dvdnn. rewrite divnn.
      destruct c; lia.
    - rewrite gtnNdvd // divn_small //.
  Qed.

  Lemma ceil_suba: a c, c > 0 a > c div_ceil a c = (div_ceil (a-c) c).+1.
  Proof.
    intros× G1 G2. unfold div_ceil.
    assert (X:a=a-c+c) by (rewrite subnK //; lia).
    case E1:(c %| a); case E2:(c %| a - c); rewrite {1} X.
    - rewrite divnDl //. rewrite divnn. by rewrite G1 addn1.
    - rewrite X in E1. apply dvdn_add_eq in E1.
      rewrite dvdnn E2 in E1. inversion E1.
    - apply dvdn_addr with (n:=c) in E2.
      rewrite dvdnn in E2. rewrite X E2 in E1. inversion E1.
    - rewrite divnDr // divnn G1 addn1 //.
  Qed.

  Lemma mod_eq: a b, a%%b = a - a%/b × b.
  Proof.
    intros.
    rewrite {2}(divn_eq a b).
    lia.
  Qed.