Library prosa.util.div_mod

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.
    intros × 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.
    intros ? ? 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 -ltnNgeLT.
  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.
    moved 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) ⇒ //.
    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.
    intros × 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.
    moveT 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.
    movedelta 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.
    intros × 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.
    intros × 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.