Library prosa.util.div_mod
Require Export prosa.util.nat prosa.util.subadditivity.
From mathcomp Require Export ssreflect ssrbool eqtype ssrnat seq fintype bigop div ssrfun.
From mathcomp Require Export ssreflect ssrbool eqtype ssrnat seq fintype bigop div ssrfun.
Additional lemmas about divn and modn.
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); ssrlia. }
destruct EX as [k EX]; subst t2; clear LT.
rewrite modnD //; replace (h ≤ t1 %% h + k %% h) with false; first by ssrlia.
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.
∀ 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); ssrlia. }
destruct EX as [k EX]; subst t2; clear LT.
rewrite modnD //; replace (h ≤ t1 %% h + k %% h) with false; first by ssrlia.
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.
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 //; ssrlia. }
}
Qed.
∀ 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 //; ssrlia. }
}
Qed.
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 ssrlia.
by rewrite modnS DIV.
Qed.
∀ 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 ssrlia.
by rewrite modnS DIV.
Qed.
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.
∀ 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.
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.
Definition div_ceil (x y : nat) := if y %| x then x %/ y else (x %/ y).+1.
Lemma div_ceil0:
∀ b, div_ceil 0 b = 0.
Proof.
intros b; unfold div_ceil.
by rewrite dvdn0; apply div0n.
Qed.
∀ b, div_ceil 0 b = 0.
Proof.
intros b; unfold div_ceil.
by rewrite dvdn0; apply div0n.
Qed.
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.
∀ 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 ssrlia.
rewrite ltn_divRL //.
apply ltn_leq_trans with m ⇒ //.
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.
∀ 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 ssrlia.
rewrite ltn_divRL //.
apply ltn_leq_trans with m ⇒ //.
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 //; try ssrlia.
by rewrite divn_gt0.
}
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.
∀ Δ 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 //; try ssrlia.
by rewrite divn_gt0.
}
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 //=; ssrlia.
- have DIVab: T %| a+b = false by rewrite -DIVa; apply dvdn_addl.
by rewrite /div_ceil DIVa DIVb DIVab divnDr //=; ssrlia.
- destruct (T %| a + b) eqn:DIVab.
+ rewrite /div_ceil DIVa DIVb DIVab.
apply leq_trans with (a %/ T + b %/T + 1); last by ssrlia.
by apply leq_divDl.
+ rewrite /div_ceil DIVa DIVb DIVab.
apply leq_ltn_trans with (a %/ T + b %/T + 1); last by ssrlia.
by apply leq_divDl.
Qed.
∀ 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 //=; ssrlia.
- have DIVab: T %| a+b = false by rewrite -DIVa; apply dvdn_addl.
by rewrite /div_ceil DIVa DIVb DIVab divnDr //=; ssrlia.
- destruct (T %| a + b) eqn:DIVab.
+ rewrite /div_ceil DIVa DIVb DIVab.
apply leq_trans with (a %/ T + b %/T + 1); last by ssrlia.
by apply leq_divDl.
+ rewrite /div_ceil DIVa DIVb DIVab.
apply leq_ltn_trans with (a %/ T + b %/T + 1); last by ssrlia.
by apply leq_divDl.
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.
∀ 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 ssrlia.
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; ssrlia.
- by rewrite modn_small; ssrlia.
Qed.
End DivFloorCeil.
∀ 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 ssrlia.
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; ssrlia.
- by rewrite modn_small; ssrlia.
Qed.
End DivFloorCeil.