From 4307d2985d0904797fc2590a2bd7bd1720e16ad4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 30 Jun 2022 11:45:28 +0200
Subject: [PATCH] remove redundant clause from `busy_intervals_are_bounded_by`

Busy intervals by definition always include the job arrival time, so
stating `t1 <= job_arrival j < t2` explicitly is not required.

Closes: #93
---
 analysis/abstract/abstract_rta.v        | 8 ++++----
 analysis/abstract/definitions.v         | 1 -
 results/edf/rta/bounded_pi.v            | 1 -
 results/fifo/rta.v                      | 1 -
 results/fixed_priority/rta/bounded_pi.v | 1 -
 5 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
index bfbeb31c0..438b9c0b2 100644
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -439,7 +439,7 @@ Section Abstract_RTA.
           specialize (L1 H0).
           feed_n 2 L1; try done.
           { move: (H_busy_interval_exists j H_j_arrives H_job_of_tsk H_job_cost_positive)
-            => [t1' [t2' [_ [BOUND BUSY]]]].
+            => [t1' [t2' [BOUND BUSY]]].
             have EQ:= busy_interval_is_unique _ _ _ _ _ _ _ _ H_busy_interval BUSY.
             destruct EQ as [EQ1 EQ2].
             subst t1' t2'; clear BUSY.
@@ -467,7 +467,7 @@ Section Abstract_RTA.
         Lemma relative_arrival_is_bounded: A < L.
         Proof.
           rewrite /A.
-          move: (H_busy_interval_exists j H_j_arrives H_job_of_tsk H_job_cost_positive) => [t1' [t2' [_ [BOUND BUSY]]]].
+          move: (H_busy_interval_exists j H_j_arrives H_job_of_tsk H_job_cost_positive) => [t1' [t2' [BOUND BUSY]]].
           have EQ:= busy_interval_is_unique _ _ _ _ _ _ _ _ H_busy_interval BUSY. destruct EQ as [EQ1 EQ2].
           subst t1' t2'; clear BUSY.
           apply leq_trans with (t2 - t1); last by rewrite leq_subLR.
@@ -535,8 +535,8 @@ Section Abstract_RTA.
     intros j ARR JOBtsk. unfold job_response_time_bound.
     move: (posnP (@job_cost _ H3 j)) => [ZERO|POS].
     { by rewrite /completed_by ZERO. } 
-    move: (H_busy_interval_exists j ARR JOBtsk POS) => [t1 [t2 [NEQ [T2 BUSY]]]].
-    move: (NEQ) (BUSY)=> /andP [GE LT] [_ QTt2].
+    move: (H_busy_interval_exists j ARR JOBtsk POS) => [t1 [t2 [T2 BUSY]]].
+    move: (BUSY) => [[/andP [GE LT] _] QTt2].
     have A2LTL := relative_arrival_is_bounded _ ARR JOBtsk POS _ _ BUSY.
     set (A2 := job_arrival j - t1) in *.
     move: (representative_exists tsk _ interference_bound_function _ A2LTL) => [A1 [ALEA2 [EQΦ INSP]]].
diff --git a/analysis/abstract/definitions.v b/analysis/abstract/definitions.v
index 0755c9029..1b579b9d6 100644
--- a/analysis/abstract/definitions.v
+++ b/analysis/abstract/definitions.v
@@ -175,7 +175,6 @@ Section AbstractRTADefinitions.
           job_of_task tsk j ->
           job_cost j > 0 ->
           exists t1 t2,
-            t1 <= job_arrival j < t2 /\
             t2 <= t1 + L /\
             busy_interval j t1 t2.
 
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 9a1fb488d..1554639b7 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -292,7 +292,6 @@ Section AbstractRTAforEDFwithArrivalCurves.
         with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; rt_eauto.
       { by intros; rewrite {2}H_fixed_point; apply total_workload_le_total_rbf. }
       exists t1, t2; split; first by done.
-      split; first by done.
       by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto.
     Qed.
     
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index 2b8b0f5eb..416afe07c 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -199,7 +199,6 @@ Section AbstractRTAforFIFOwithArrivalCurves.
         with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; rt_eauto.
       { by intros; rewrite {2}H_fixed_point; apply total_workload_le_total_rbf. }
       { exists t1, t2; split; first by done.
-        split; first by done.
         by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto. }
     Qed.
 
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index ac0830a0f..2efb27187 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -242,7 +242,6 @@ Section AbstractRTAforFPwithArrivalCurves.
         rt_eauto.
       { by intros; rewrite {2}H_fixed_point leq_add //; apply total_workload_le_total_hep_rbf. }
       exists t1, t2; split; first by done.
-      split; first by done.
       by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto.
     Qed.
 
-- 
GitLab