From 84b04ff33b9268f055425fad5402658450dd63d4 Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <f20171026@goa.bits-pilani.ac.in>
Date: Mon, 16 May 2022 07:25:59 +0000
Subject: [PATCH] add lemma relating task cost and task rbf

Currently, we have lemmas stating that `task_rbf` at `\vareosilon` is greater than equal to task cost, and `task_rbf` is monotone. I combined these two lemmas to state that `tsk_rbf` at any point greater than `0` is greater than task cost. I find that this fact is regularly required in proofs and, therefore, would be good to have in the facts folder.
---
 analysis/facts/model/rbf.v | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/analysis/facts/model/rbf.v b/analysis/facts/model/rbf.v
index 3508f44bd..6832a5ec7 100644
--- a/analysis/facts/model/rbf.v
+++ b/analysis/facts/model/rbf.v
@@ -272,7 +272,7 @@ Section RequestBoundFunctions.
   Hypothesis H_j_arrives : arrives_in arr_seq j.
   Hypothesis H_job_of_tsk : job_of_task tsk j.
 
-  (** Then we prove that [task_rbf] at [ε] is greater than or equal to task cost. *)
+  (** Then we prove that [task_rbf] at [ε] is greater than or equal to the task's WCET. *)
   Lemma task_rbf_1_ge_task_cost:
     task_rbf ε >= task_cost tsk.
   Proof.
@@ -296,6 +296,18 @@ Section RequestBoundFunctions.
     by rewrite CONS.
   Qed.
 
+  (** As a corollary, we prove that the [task_rbf] at any point [A] greater than
+      [0] is no less than the task's WCET. *)
+  Lemma task_rbf_ge_task_cost:
+    forall A,
+      A > 0 ->
+      task_rbf A >= task_cost tsk.
+  Proof.
+    case => // A GEQ.
+    apply: (leq_trans task_rbf_1_ge_task_cost).
+    exact: task_rbf_monotone.
+  Qed.
+
   (** Assume that [tsk] has a positive cost. *)
   Hypothesis H_positive_cost : 0 < task_cost tsk.
   
-- 
GitLab