From 319404c23cd45ee3cbbf3bbf0b264981509a3bd0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Fri, 28 Feb 2025 09:43:51 +0100
Subject: [PATCH] fixup finish_time proof to match changed `completes_at`
definition
---
analysis/definitions/finish_time.v | 6 ++----
1 file changed, 2 insertions(+), 4 deletions(-)
diff --git a/analysis/definitions/finish_time.v b/analysis/definitions/finish_time.v
index 18d92487d..4cf10e0da 100644
--- a/analysis/definitions/finish_time.v
+++ b/analysis/definitions/finish_time.v
@@ -65,14 +65,12 @@ 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. *)
+ (** Third, 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/orP; case FIN: finish_time; [by right|left].
apply: contra_ltnN => [?|];
first by apply: earliest_finish_time.
by lia.
--
GitLab