From ce963a704e8913fd5ae3b2a433fec01ee283f05a Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <f20171026@goa.bits-pilani.ac.in>
Date: Mon, 31 Jan 2022 07:34:44 +0000
Subject: [PATCH] add new helper lemma about RBF

* Added a lemma for proving `rbf` at `\varepsilon` is more than 0. This is a general fact which can be used in the FIFO RTA to simplify a proof.
* Changed `1` to `\varepsilon` in one of the existing RBF lemmas for uniformity.
---
 analysis/facts/model/rbf.v | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/analysis/facts/model/rbf.v b/analysis/facts/model/rbf.v
index 5489c130d..bed122691 100644
--- a/analysis/facts/model/rbf.v
+++ b/analysis/facts/model/rbf.v
@@ -270,19 +270,19 @@ Section RequestBoundFunctions.
   Hypothesis H_j_arrives : arrives_in arr_seq j.
   Hypothesis H_job_of_tsk : job_task j = tsk.
 
-  (** Then we prove that [task_rbf 1] is greater than or equal to task cost. *)
+  (** Then we prove that [task_rbf] at [ε] is greater than or equal to task cost. *)
   Lemma task_rbf_1_ge_task_cost:
-    task_rbf 1 >= task_cost tsk.
+    task_rbf ε >= task_cost tsk.
   Proof.
     have ALT: forall n, n = 0 \/ n > 0 by clear; intros n; destruct n; [left | right].
     specialize (ALT (task_cost tsk)); destruct ALT as [Z | POS]; first by rewrite Z.
     rewrite leqNgt; apply/negP; intros CONTR.
     move: H_is_arrival_curve => ARRB.
-    specialize (ARRB (job_arrival j) (job_arrival j + 1)).
+    specialize (ARRB (job_arrival j) (job_arrival j + ε)).
     feed ARRB; first by rewrite leq_addr.
     move: CONTR; rewrite /task_rbf /task_request_bound_function.
     rewrite -{2}[task_cost tsk]muln1 ltn_mul2l => /andP [_ CONTR].
-    move: CONTR; rewrite -addn1 -{3}[1]add0n leq_add2r leqn0 => /eqP CONTR.
+    move: CONTR; rewrite -addn1 -[1]add0n leq_add2r leqn0 => /eqP CONTR.
     move: ARRB; rewrite addKn CONTR leqn0 eqn0Ngt => /negP T; apply: T.
     rewrite /number_of_task_arrivals -has_predT /task_arrivals_between.
     apply/hasP; exists j; last by done.
@@ -294,6 +294,16 @@ Section RequestBoundFunctions.
     by rewrite CONS.
   Qed.
 
+  (** Assume that [tsk] has a positive cost. *)
+  Hypothesis H_positive_cost : 0 < task_cost tsk.
+  
+  (** Then, we prove that [task_rbf] at [ε] is greater than [0]. *)
+  Lemma task_rbf_epsilon_gt_0 : 0 < task_rbf ε.
+  Proof.
+    apply leq_trans with (task_cost tsk); first by done.
+    by eapply task_rbf_1_ge_task_cost; eauto. 
+  Qed.
+            
   (** Consider a set of tasks [ts] containing the task [tsk]. *)
   Variable ts : seq Task.
   Hypothesis H_tsk_in_ts : tsk \in ts.
-- 
GitLab