Library prosa.util.div_mod

From mathcomp Require Export ssreflect ssrbool eqtype ssrnat seq fintype bigop div ssrfun.
Require Export prosa.util.nat prosa.util.subadditivity.

Additional lemmas about divn and modn.

Section DivMod.

First, we show that if t1 / h is equal to t2 / h and t1 ≤ t2, then t1 mod h is bounded by t2 mod h.

  Lemma eqdivn_leqmodn :
    ∀ t1 t2 h,
      t1 ≤ t2 →
      t1 %/ h = t2 %/ h →
      t1 %% h ≤ t2 %% h.
  Proof.
    move⇒ t1 t2 h LT EQ.
    destruct (posnP h) as [Z | POSh].
    { by subst; rewrite !modn0. }
    { have EX: ∃ k , t1 + k = t2.
      { ∃ (t2 - t1); lia. }
      destruct EX as [k EX]; subst t2; clear LT.
      rewrite modnD //; replace (h ≤ t1 %% h + k %% h) with false; first by lia.
      symmetry; apply/negP/negP; rewrite -ltnNge.
      symmetry in EQ; rewrite divnD // in EQ; move: EQ ⇒ /eqP.
      rewrite -{2}[t1 %/ h]addn0 -addnA eqn_add2l addn_eq0 ⇒ /andP [_ /eqP Z2].
      by move: Z2 ⇒ /eqP; rewrite eqb0 -ltnNge.
    }
  Qed.

Given two natural numbers x and y, the fact that x / y < (x + 1) / y implies that y divides x + 1.

  Lemma ltdivn_dvdn :
    ∀ x y,
      x %/ y < (x + 1) %/ y →
      y %| (x + 1).
  Proof.
    move⇒ x y LT.
    destruct (posnP y) as [Z | POS]; first by subst y.
    move: LT; rewrite divnD // -addn1 -addnA leq_add2l addn_gt0 ⇒ /orP [ONE | LE].
    { by destruct y as [ | []]. }
    { rewrite lt0b in LE.
      destruct (leqP 2 y) as [LT2 | GE2]; last by destruct y as [ | []].
      clear POS; rewrite [1 %% _]modn_small // in LE.
      move: LE; rewrite leq_eqVlt ⇒ /orP [/eqP EQ | LT].
      { rewrite [x](divn_eq x y) -addnA -EQ; apply dvdn_add.
        - by apply dvdn_mull, dvdnn.
        - by apply dvdnn.
      }
      { by move: LT; rewrite -addn1 leq_add2r leqNgt ltn_pmod //; lia. }
    }
  Qed.

We prove an auxiliary lemma allowing us to change the order of operations _ + 1 and _ %% h.

  Lemma addn1_modn_commute :
    ∀ x h,
      h > 0 →
      x %/ h = (x + 1) %/ h →
      (x + 1) %% h = x %% h + 1 .
  Proof.
    intros x h POS EQ.
    rewrite !addnS !addn0.
    rewrite addnS divnS // addn0 in EQ.
    destruct (h %| x.+1) eqn:DIV ; rewrite /= in EQ; first by lia.
    by rewrite modnS DIV.
  Qed.

We show that the fact that x / h = (x + y) / h implies that h is larder than x mod h + y mod h.

  Lemma addmod_le_mod :
    ∀ x y h,
      h > 0 →
      x %/ h = (x + y ) %/ h →
      h > x %% h + y %% h.
  Proof.
    intros x y h POS EQ.
    move: EQ ⇒ /eqP; rewrite divnD // -{1}[x %/ h]addn0 -addnA eqn_add2l eq_sym addn_eq0 ⇒ /andP [/eqP Z1 /eqP Z2].
    by move: Z2 ⇒ /eqP; rewrite eqb0 -ltnNge ⇒ LT.
  Qed.

End DivMod.

In this section, we define notions of div_floor and div_ceil and prove a few basic lemmas.

Section DivFloorCeil.

We define functions div_floor and div_ceil, which are divisions rounded down and up, respectively.

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.

We start with an observation that div_ceil 0 b is equal to 0 for any b.

  Lemma div_ceil0:
    ∀ b, div_ceil 0 b = 0.
  Proof.
    intros b; unfold div_ceil.
    by rewrite dvdn0; apply div0n.
  Qed.

Next, we show that, given two positive integers a and b, div_ceil a b is also positive.

  Lemma div_ceil_gt0:
    ∀ a b,
      a > 0 → b > 0 →
      div_ceil a b > 0.
  Proof.
    intros a b POSa POSb.
    unfold div_ceil.
    destruct (b %| a) eqn:EQ; last by done.
    by rewrite divn_gt0 //; apply dvdn_leq.
  Qed.

We show that div_ceil is monotone with respect to the first argument.

  Lemma div_ceil_monotone1:
    ∀ d m n,
      m ≤ n → div_ceil m d ≤ div_ceil n d.
  Proof.
    move ⇒ d m n LEQ.
    rewrite /div_ceil.
    have LEQd: m %/ d ≤ n %/ d by apply leq_div2r.
    destruct (d %| m) eqn:Mm; destruct (d %| n) eqn:Mn ⇒ //; first by lia.
    rewrite ltn_divRL //.
    apply: (leq_trans _ LEQ).
    move: (leq_trunc_div m d) ⇒ LEQm.
    destruct (ltngtP (m %/ d × d) m) as [| |e] ⇒ //.
    move: e ⇒ /eqP EQ; rewrite -dvdn_eq in EQ.
    by rewrite EQ in Mm.
  Qed.

Given T and Δ such that Δ ≥ T > 0, we show that div_ceil Δ T is strictly greater than div_ceil (Δ - T) T.

  Lemma leq_div_ceil_add1:
    ∀ Δ T,
      T > 0 → Δ ≥ T →
      div_ceil (Δ - T) T < div_ceil Δ T.
  Proof.
    move⇒ Δ T POS LE. rewrite /div_ceil.
    have lkc: (Δ - T) %/ T < Δ %/ T.
    { rewrite divnBr; last by auto.
      rewrite divnn POS.
      rewrite ltn_psubCl //; lia.
    }
    destruct (T %| Δ) eqn:EQ1.
    { have divck: (T %| Δ) → (T %| (Δ - T)) by auto.
      apply divck in EQ1 as EQ2.
      rewrite EQ2; apply lkc.
    }
    by destruct (T %| Δ - T) eqn:EQ, (T %| Δ) eqn:EQ3; auto.
  Qed.

We show that the division with ceiling by a constant T is a subadditive function.

  Lemma div_ceil_subadditive:
    ∀ T, subadditive (div_ceil ^~T).
  Proof.
    move⇒ T ab a b SUM.
    rewrite -SUM.
    destruct (T %| a) eqn:DIVa, (T %| b) eqn:DIVb.
    - have DIVab: T %| a + b by apply dvdn_add.
      by rewrite /div_ceil DIVa DIVb DIVab divnDl.
    - have DIVab: T %| a+b = false by rewrite -DIVb; apply dvdn_addr.
      by rewrite /div_ceil DIVa DIVb DIVab divnDl //=; lia.
    - have DIVab: T %| a+b = false by rewrite -DIVa; apply dvdn_addl.
      by rewrite /div_ceil DIVa DIVb DIVab divnDr //=; lia.
    - destruct (T %| a + b) eqn:DIVab.
      + rewrite /div_ceil DIVa DIVb DIVab.
        apply leq_trans with (a %/ T + b %/T + 1); last by lia.
        by apply leq_divDl.
      + rewrite /div_ceil DIVa DIVb DIVab.
        apply leq_ltn_trans with (a %/ T + b %/T + 1); last by lia.
        by apply leq_divDl.
  Qed.

We observe that when dividing a value exceeding T × n, then the ceiling exceeds n.

  Lemma div_ceil_multiple :
    ∀ Δ T n,
      T > 0 →
      (T × n ) < Δ →
      n < div_ceil Δ T.
  Proof.
    move⇒ delta T n GT0 LT.
    rewrite /div_ceil.
    case DIV: (T %| delta);
      first by rewrite -(ltn_pmul2l GT0) [_ × (_ %/ _)]mulnC divnK.
    rewrite -[(_ %/ _).+1]addn1 -divnDMl // -(ltn_pmul2l GT0) [_ × (_ %/ _)]mulnC mul1n.
    by lia.
  Qed.

We show that for any two integers a and b, a is less than a %/ b × b + b given that b is positive.

  Lemma div_floor_add_g:
    ∀ a b,
      b > 0 →
      a < a %/ b × b + b.
  Proof.
    move⇒ a b POS.
    specialize (divn_eq a b) ⇒ DIV.
    rewrite [in X in X < _]DIV.
    rewrite ltn_add2l.
    by apply ltn_pmod.
  Qed.

We prove a technical lemma stating that for any three integers a, b, c such that c > b, mod can be swapped with subtraction in the expression (a + c - b) %% c.

  Lemma mod_elim:
    ∀ a b c,
      c > b →
      (a + c - b ) %% c = if a %% c ≥ b then (a %% c - b ) else (a %% c + c - b ).
  Proof.
    move⇒ a b c BC.
    have POS : c > 0 by lia.
    have G : a %% c < c by apply ltn_pmod.
    case (b ≤ a %% c) eqn:CASE; rewrite -addnBA; auto; rewrite -modnDml.
    - rewrite addnABC; auto.
      by rewrite -modnDmr modnn addn0 modn_small; auto; lia.
    - by rewrite modn_small; lia.
  Qed.

End DivFloorCeil.