From 260faaea714332f087e70a8deba51f73c6a0e7df Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 27 Feb 2025 22:22:13 +0100
Subject: [PATCH] to squash: one more corollary
---
analysis/definitions/finish_time.v | 13 +++++++++++++
1 file changed, 13 insertions(+)
diff --git a/analysis/definitions/finish_time.v b/analysis/definitions/finish_time.v
index af9609f2f..630a75267 100644
--- a/analysis/definitions/finish_time.v
+++ b/analysis/definitions/finish_time.v
@@ -65,6 +65,19 @@ Section JobFinishTime.
by case: find_ex_minn.
Qed.
+ (** Third, when excluding the pathological case of a job completing at time
+ zero, Prosa's notion of [completes_at] is satisfied at the finish time. *)
+ Corollary completes_at_finish_time :
+ finish_time > 0 ->
+ completes_at sched j finish_time.
+ Proof.
+ move=> GT0.
+ apply/andP; split; last exact: finished_at_finish_time.
+ apply: contra_ltnN => [?|];
+ first by apply: earliest_finish_time.
+ by lia.
+ Qed.
+
(** Finally, we can define a job's precise response time as usual as the time
from its arrival until its finish time. *)
Definition response_time : duration := finish_time - job_arrival j.
--
GitLab