Library prosa.util.div_mod

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.
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.
{ 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].
- 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.
x h,
h > 0
x %/ h = (x + 1) %/ h
(x + 1) %% h = x %% h + 1 .
Proof.
intros x h POS 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.
x y h,
h > 0
x %/ h = (x + y) %/ h
h > x %% h + y %% h.
Proof.
intros x y h POS EQ.
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.
Δ 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.
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.
a b,
b > 0
a < a %/ b × b + b.
Proof.
intros × POS.
specialize (divn_eq a b) ⇒ DIV.
rewrite [in X in X < _]DIV.
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.