From d6ce34a8c62b25a63f6f33f8dbcce34bbfb9a697 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Wed, 16 Mar 2022 14:19:16 +0100
Subject: [PATCH] add lemma on `div_ceil` on integer multiples
---
util/div_mod.v | 18 +++++++++++++++++-
1 file changed, 17 insertions(+), 1 deletion(-)
diff --git a/util/div_mod.v b/util/div_mod.v
index aa417e75b..f10b4fe2f 100644
--- a/util/div_mod.v
+++ b/util/div_mod.v
@@ -170,7 +170,23 @@ Section DivFloorCeil.
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 :
+ forall Δ 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:
--
GitLab