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

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.

We prove that if x lies in an interval [kT, (k+1)T), then x %/ T is equal to k.

Lemma divn_leq :
  ∀ k T x,
    k × T ≤ x < k .+1 × T →
    x %/ T = k.
Proof.
  move ⇒ k T x NEQ.
  have [Z|POS] := posnP T.
  { subst; rewrite !muln0 in NEQ; lia. }
  apply/eqP; rewrite -(eqn_pmul2r POS); apply/eqP.
  move: x NEQ; induction k as [| k IHk] ⇒ x NEQ; first by rewrite divn_small; lia.
  rewrite -addn1 mulnDl mul1n.
  specialize (IHk (x - T)); feed IHk; first by lia.
  rewrite -IHk {6}(divn_eq T T) modnn addn0.
  by rewrite -mulnDl -divnDr ?dvdnn // subnK //; lia.
Qed.

Floors and Ceilings of Fractions

We define notions of div_floor and div_ceil and prove a few basic lemmas.

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_divM 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.