Library prosa.util.div_mod
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.util.nat prosa.util.subadditivity.
From mathcomp Require Export ssreflect ssrbool eqtype ssrnat seq fintype bigop div ssrfun.
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.
Lemma mod_elim:
∀ a b c,
c>0 →
b<c →
(a + c - b)%%c = ( if a%%c ≥ b then (a%%c - b) else (a%%c + c - b)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 22)
============================
forall a b c : nat,
0 < c ->
b < c ->
(a + c - b) %% c = (if b <= a %% c then a %% c - b else a %% c + c - b)
----------------------------------------------------------------------------- *)
Proof.
intros× CP BC.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 27)
a, b, c : nat
CP : 0 < c
BC : b < c
============================
(a + c - b) %% c = (if b <= a %% c then a %% c - b else a %% c + c - b)
----------------------------------------------------------------------------- *)
have G: a%%c < c by apply ltn_pmod.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 31)
a, b, c : nat
CP : 0 < c
BC : b < c
G : a %% c < c
============================
(a + c - b) %% c = (if b <= a %% c then a %% c - b else a %% c + c - b)
----------------------------------------------------------------------------- *)
case (b ≤ a %% c)eqn:CASE;rewrite -addnBA;auto;rewrite -modnDml.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 69)
a, b, c : nat
CP : 0 < c
BC : b < c
G : a %% c < c
CASE : (b <= a %% c) = true
============================
(a %% c + (c - b)) %% c = a %% c - b
subgoal 2 (ID 74) is:
(a %% c + (c - b)) %% c = a %% c + c - b
----------------------------------------------------------------------------- *)
- rewrite add_subC;auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 81)
a, b, c : nat
CP : 0 < c
BC : b < c
G : a %% c < c
CASE : (b <= a %% c) = true
============================
(a %% c - b + c) %% c = a %% c - b
subgoal 2 (ID 74) is:
(a %% c + (c - b)) %% c = a %% c + c - b
----------------------------------------------------------------------------- *)
rewrite -modnDmr modnn addn0 modn_small;auto;ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 74)
a, b, c : nat
CP : 0 < c
BC : b < c
G : a %% c < c
CASE : (b <= a %% c) = false
============================
(a %% c + (c - b)) %% c = a %% c + c - b
----------------------------------------------------------------------------- *)
- rewrite modn_small;try ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We show that for any two integers [a] and [c],
[a] is less than [a %/ c * c + c] given that [c] is positive.
Lemma div_floor_add_g:
∀ a c,
c > 0 →
a < a %/ c × c + c.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 25)
============================
forall a c : nat, 0 < c -> a < a %/ c * c + c
----------------------------------------------------------------------------- *)
Proof.
intros × POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 28)
a, c : nat
POS : 0 < c
============================
a < a %/ c * c + c
----------------------------------------------------------------------------- *)
specialize (divn_eq a c) ⇒ DIV.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 31)
a, c : nat
POS : 0 < c
DIV : a = a %/ c * c + a %% c
============================
a < a %/ c * c + c
----------------------------------------------------------------------------- *)
rewrite [in X in X < _]DIV.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 38)
a, c : nat
POS : 0 < c
DIV : a = a %/ c * c + a %% c
============================
a %/ c * c + a %% c < a %/ c * c + c
----------------------------------------------------------------------------- *)
rewrite ltn_add2l.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
a, c : nat
POS : 0 < c
DIV : a = a %/ c * c + a %% c
============================
a %% c < c
----------------------------------------------------------------------------- *)
now apply ltn_pmod.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ a c,
c > 0 →
a < a %/ c × c + c.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 25)
============================
forall a c : nat, 0 < c -> a < a %/ c * c + c
----------------------------------------------------------------------------- *)
Proof.
intros × POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 28)
a, c : nat
POS : 0 < c
============================
a < a %/ c * c + c
----------------------------------------------------------------------------- *)
specialize (divn_eq a c) ⇒ DIV.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 31)
a, c : nat
POS : 0 < c
DIV : a = a %/ c * c + a %% c
============================
a < a %/ c * c + c
----------------------------------------------------------------------------- *)
rewrite [in X in X < _]DIV.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 38)
a, c : nat
POS : 0 < c
DIV : a = a %/ c * c + a %% c
============================
a %/ c * c + a %% c < a %/ c * c + c
----------------------------------------------------------------------------- *)
rewrite ltn_add2l.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
a, c : nat
POS : 0 < c
DIV : a = a %/ c * c + a %% c
============================
a %% c < c
----------------------------------------------------------------------------- *)
now apply ltn_pmod.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 28)
============================
forall T : nat, subadditive (div_ceil^~ T)
----------------------------------------------------------------------------- *)
Proof.
move⇒ T ab a b SUM.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 35)
T, ab, a, b : nat
SUM : a + b = ab
============================
div_ceil ab T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
rewrite -SUM.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 37)
T, ab, a, b : nat
SUM : a + b = ab
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
destruct (T %| a) eqn:DIVa, (T %| b) eqn:DIVb.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 58)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = true
DIVb : (T %| b) = true
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 2 (ID 59) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 3 (ID 69) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 4 (ID 70) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
- have DIVab: T %| a + b by apply dvdn_add.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 75)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = true
DIVb : (T %| b) = true
DIVab : T %| a + b
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 2 (ID 59) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 3 (ID 69) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 4 (ID 70) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
by rewrite /div_ceil DIVa DIVb DIVab divnDl.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 59)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = true
DIVb : (T %| b) = false
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 2 (ID 69) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 3 (ID 70) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
- have DIVab: T %| a+b = false by rewrite -DIVb; apply dvdn_addr.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 96)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = true
DIVb : (T %| b) = false
DIVab : (T %| a + b) = false
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 2 (ID 69) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 3 (ID 70) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
by rewrite /div_ceil DIVa DIVb DIVab divnDl //=; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 69)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = true
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 2 (ID 70) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
- have DIVab: T %| a+b = false by rewrite -DIVa; apply dvdn_addl.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 283)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = true
DIVab : (T %| a + b) = false
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 2 (ID 70) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
by rewrite /div_ceil DIVa DIVb DIVab divnDr //=; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 70)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = false
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
- destruct (T %| a + b) eqn:DIVab.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 309)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = false
DIVab : (T %| a + b) = true
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 2 (ID 310) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
+ rewrite /div_ceil DIVa DIVb DIVab.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 317)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = false
DIVab : (T %| a + b) = true
============================
(a + b) %/ T <= (a %/ T).+1 + (b %/ T).+1
subgoal 2 (ID 310) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
apply leq_trans with (a %/ T + b %/T + 1); last by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 318)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = false
DIVab : (T %| a + b) = true
============================
(a + b) %/ T <= a %/ T + b %/ T + 1
subgoal 2 (ID 310) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
by apply leq_divDl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 310)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = false
DIVab : (T %| a + b) = false
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
+ rewrite /div_ceil DIVa DIVb DIVab.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 486)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = false
DIVab : (T %| a + b) = false
============================
(a + b) %/ T < (a %/ T).+1 + (b %/ T).+1
----------------------------------------------------------------------------- *)
apply leq_ltn_trans with (a %/ T + b %/T + 1); last by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 487)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = false
DIVab : (T %| a + b) = false
============================
(a + b) %/ T <= a %/ T + b %/ T + 1
----------------------------------------------------------------------------- *)
by apply leq_divDl.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ T,
subadditive (div_ceil^~T).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 28)
============================
forall T : nat, subadditive (div_ceil^~ T)
----------------------------------------------------------------------------- *)
Proof.
move⇒ T ab a b SUM.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 35)
T, ab, a, b : nat
SUM : a + b = ab
============================
div_ceil ab T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
rewrite -SUM.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 37)
T, ab, a, b : nat
SUM : a + b = ab
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
destruct (T %| a) eqn:DIVa, (T %| b) eqn:DIVb.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 58)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = true
DIVb : (T %| b) = true
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 2 (ID 59) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 3 (ID 69) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 4 (ID 70) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
- have DIVab: T %| a + b by apply dvdn_add.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 75)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = true
DIVb : (T %| b) = true
DIVab : T %| a + b
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 2 (ID 59) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 3 (ID 69) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 4 (ID 70) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
by rewrite /div_ceil DIVa DIVb DIVab divnDl.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 59)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = true
DIVb : (T %| b) = false
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 2 (ID 69) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 3 (ID 70) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
- have DIVab: T %| a+b = false by rewrite -DIVb; apply dvdn_addr.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 96)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = true
DIVb : (T %| b) = false
DIVab : (T %| a + b) = false
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 2 (ID 69) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 3 (ID 70) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
by rewrite /div_ceil DIVa DIVb DIVab divnDl //=; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 69)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = true
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 2 (ID 70) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
- have DIVab: T %| a+b = false by rewrite -DIVa; apply dvdn_addl.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 283)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = true
DIVab : (T %| a + b) = false
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 2 (ID 70) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
by rewrite /div_ceil DIVa DIVb DIVab divnDr //=; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 70)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = false
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
- destruct (T %| a + b) eqn:DIVab.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 309)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = false
DIVab : (T %| a + b) = true
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
subgoal 2 (ID 310) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
+ rewrite /div_ceil DIVa DIVb DIVab.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 317)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = false
DIVab : (T %| a + b) = true
============================
(a + b) %/ T <= (a %/ T).+1 + (b %/ T).+1
subgoal 2 (ID 310) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
apply leq_trans with (a %/ T + b %/T + 1); last by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 318)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = false
DIVab : (T %| a + b) = true
============================
(a + b) %/ T <= a %/ T + b %/ T + 1
subgoal 2 (ID 310) is:
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
by apply leq_divDl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 310)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = false
DIVab : (T %| a + b) = false
============================
div_ceil (a + b) T <= div_ceil a T + div_ceil b T
----------------------------------------------------------------------------- *)
+ rewrite /div_ceil DIVa DIVb DIVab.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 486)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = false
DIVab : (T %| a + b) = false
============================
(a + b) %/ T < (a %/ T).+1 + (b %/ T).+1
----------------------------------------------------------------------------- *)
apply leq_ltn_trans with (a %/ T + b %/T + 1); last by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 487)
T, ab, a, b : nat
SUM : a + b = ab
DIVa : (T %| a) = false
DIVb : (T %| b) = false
DIVab : (T %| a + b) = false
============================
(a + b) %/ T <= a %/ T + b %/ T + 1
----------------------------------------------------------------------------- *)
by apply leq_divDl.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.