From c0e95f8124d6e6fd4ae68b9bdce532988140e871 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Wed, 16 Mar 2022 08:59:00 +0100
Subject: [PATCH] restructure sporadic task facts

---
 analysis/facts/periodic/arrival_separation.v  |   2 +-
 analysis/facts/periodic/task_arrivals_size.v  |   1 +
 .../arrival_sequence.v}                       | 115 +-----------------
 analysis/facts/sporadic/arrival_times.v       | 111 +++++++++++++++++
 4 files changed, 117 insertions(+), 112 deletions(-)
 rename analysis/facts/{sporadic.v => sporadic/arrival_sequence.v} (59%)
 create mode 100644 analysis/facts/sporadic/arrival_times.v

diff --git a/analysis/facts/periodic/arrival_separation.v b/analysis/facts/periodic/arrival_separation.v
index 89ed08c0e..d4cee86db 100644
--- a/analysis/facts/periodic/arrival_separation.v
+++ b/analysis/facts/periodic/arrival_separation.v
@@ -1,5 +1,5 @@
 Require Export prosa.analysis.facts.periodic.sporadic.
-Require Export prosa.analysis.facts.sporadic.
+Require Export prosa.analysis.facts.sporadic.arrival_times.
 
 (** In this section we show that the separation between job 
     arrivals of a periodic task is some multiple of their 
diff --git a/analysis/facts/periodic/task_arrivals_size.v b/analysis/facts/periodic/task_arrivals_size.v
index 587383df7..a92967c94 100644
--- a/analysis/facts/periodic/task_arrivals_size.v
+++ b/analysis/facts/periodic/task_arrivals_size.v
@@ -1,5 +1,6 @@
 Require Export prosa.analysis.facts.periodic.arrival_times.
 Require Export prosa.analysis.definitions.infinite_jobs.
+Require Export prosa.analysis.facts.sporadic.arrival_sequence.
 
 (** In this file we prove some properties concerning the size 
  of task arrivals in context of the periodic model. *)
diff --git a/analysis/facts/sporadic.v b/analysis/facts/sporadic/arrival_sequence.v
similarity index 59%
rename from analysis/facts/sporadic.v
rename to analysis/facts/sporadic/arrival_sequence.v
index 453661ca4..79fba6425 100644
--- a/analysis/facts/sporadic.v
+++ b/analysis/facts/sporadic/arrival_sequence.v
@@ -1,116 +1,9 @@
-Require Export prosa.model.task.arrival.sporadic.
-Require Export prosa.analysis.facts.job_index.
+Require Export analysis.facts.sporadic.arrival_times.
 
-(** * The Sporadic Model *)
+(** * Job Arrival Sequence in the Sporadic Model *)
 
-(** In this section we prove a few basic properties involving
-    job indices in context of the sporadic model. *)
-Section SporadicModelIndexLemmas.
-
-  (** Consider sporadic tasks ... *)
-  Context {Task : TaskType} `{SporadicModel Task}.
-
-  (** ... and any type of jobs associated with these tasks. *)
-  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
-
-  (** Consider any unique arrival sequence with consistent arrivals, ... *)
-  Variable arr_seq : arrival_sequence Job.
-  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
-
-  (** ... and any sporadic task [tsk] that is to be analyzed. *)
-  Variable tsk : Task.
-  Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
-  Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
-
-  (** Consider any two jobs from the arrival sequence that stem
-      from task [tsk]. *)
-  Variable j1 : Job.
-  Variable j2 : Job.
-  Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
-  Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
-  Hypothesis H_j1_task: job_task j1 = tsk.
-  Hypothesis H_j2_task: job_task j2 = tsk.
-
-  (** We first show that for any two jobs [j1] and [j2], [j2] arrives after [j1]
-      provided [job_index] of [j2] strictly exceeds the [job_index] of [j1]. *)
-  Lemma lower_index_implies_earlier_arrival:
-      job_index arr_seq j1 < job_index arr_seq j2 ->
-      job_arrival j1 < job_arrival j2.
-  Proof.
-    move=> LT_IND.
-    move: (H_sporadic_model j1 j2) => SPORADIC; feed_n 6 SPORADIC => //.
-    - rewrite -> diff_jobs_iff_diff_indices => //; eauto; first by lia.
-      by subst.
-    - apply (index_lte_implies_arrival_lte arr_seq); try eauto.
-      by subst.
-    - have POS_IA : task_min_inter_arrival_time tsk > 0 by auto.
-      by lia.
-  Qed.
-
-End SporadicModelIndexLemmas.
-
-(** ** Different jobs have different arrival times. *)
-Section DifferentJobsImplyDifferentArrivalTimes.
-
-  (** Consider sporadic tasks ... *)
-  Context {Task : TaskType} `{SporadicModel Task}.
-
-  (** ... and any type of jobs associated with these tasks. *)
-  Context {Job : JobType}.
-  Context `{JobTask Job Task}.
-  Context `{JobArrival Job}.
-
-  (** Consider any unique arrival sequence with consistent arrivals, ... *)
-  Variable arr_seq : arrival_sequence Job.
-  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
-
-  (** ... and any sporadic task [tsk] that is to be analyzed. *)
-  Variable tsk : Task.
-  Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
-  Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
-
-  (** Consider any two jobs from the arrival sequence that stem 
-      from task [tsk]. *)  
-  Variable j1 : Job.
-  Variable j2 : Job.
-  Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
-  Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
-  Hypothesis H_j1_task: job_task j1 = tsk.
-  Hypothesis H_j2_task: job_task j2 = tsk.
-
-  (** We observe that distinct jobs cannot have equal arrival times. *)
-  Lemma uneq_job_uneq_arr:
-      j1 <> j2 ->
-      job_arrival j1 <> job_arrival j2.
-  Proof.
-    intros UNEQ EQ_ARR.
-    rewrite -> diff_jobs_iff_diff_indices in UNEQ => //; eauto; last by rewrite H_j1_task.
-    move /neqP: UNEQ; rewrite neq_ltn => /orP [LT|LT].
-    all: try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; lia ) ||
-             now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; lia.
-  Qed.
-
-  (** We prove a stronger version of the above lemma by showing 
-   that jobs [j1] and [j2] are equal if and only if they arrive at the
-   same time. *)
-  Lemma same_jobs_iff_same_arr:
-    j1 = j2 <->
-    job_arrival j1 = job_arrival j2.
-  Proof.
-    split; first by apply congr1.
-    intro EQ_ARR.
-    case: (boolP (j1 == j2)) => [/eqP EQ | /eqP NEQ]; first by auto.
-    rewrite -> diff_jobs_iff_diff_indices in NEQ => //; eauto; last by rewrite H_j1_task.
-    move /neqP: NEQ; rewrite neq_ltn => /orP [LT|LT].
-    all: try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; lia ) || now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; lia.
-  Qed.
-
-End DifferentJobsImplyDifferentArrivalTimes.
-
-(** In this section we prove a few properties regarding task arrivals
-    in context of the sporadic task model. *)
+(** In this file, we prove basic facts about a task's arrival sequence
+    in the sporadic task model. *)
 Section SporadicArrivals.
 
   (** Consider sporadic tasks  ... *)
diff --git a/analysis/facts/sporadic/arrival_times.v b/analysis/facts/sporadic/arrival_times.v
new file mode 100644
index 000000000..493738f32
--- /dev/null
+++ b/analysis/facts/sporadic/arrival_times.v
@@ -0,0 +1,111 @@
+Require Export prosa.model.task.arrival.sporadic.
+Require Export prosa.analysis.facts.job_index.
+
+(** * Job Arrival Times in the Sporadic Model *)
+
+(** In this file, we prove a few basic facts about the arrival times
+    of jobs in the sporadic task model. *)
+Section SporadicModelIndexLemmas.
+
+  (** Consider sporadic tasks ... *)
+  Context {Task : TaskType} `{SporadicModel Task}.
+
+  (** ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
+
+  (** Consider any unique arrival sequence with consistent arrivals, ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
+  Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
+
+  (** ... and any sporadic task [tsk] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
+  Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
+
+  (** Consider any two jobs from the arrival sequence that stem
+      from task [tsk]. *)
+  Variable j1 : Job.
+  Variable j2 : Job.
+  Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
+  Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
+  Hypothesis H_j1_task: job_task j1 = tsk.
+  Hypothesis H_j2_task: job_task j2 = tsk.
+
+  (** We first show that for any two jobs [j1] and [j2], [j2] arrives after [j1]
+      provided [job_index] of [j2] strictly exceeds the [job_index] of [j1]. *)
+  Lemma lower_index_implies_earlier_arrival:
+      job_index arr_seq j1 < job_index arr_seq j2 ->
+      job_arrival j1 < job_arrival j2.
+  Proof.
+    move=> LT_IND.
+    move: (H_sporadic_model j1 j2) => SPORADIC; feed_n 6 SPORADIC => //.
+    - rewrite -> diff_jobs_iff_diff_indices => //; eauto; first by lia.
+      by subst.
+    - apply (index_lte_implies_arrival_lte arr_seq); try eauto.
+      by subst.
+    - have POS_IA : task_min_inter_arrival_time tsk > 0 by auto.
+      by lia.
+  Qed.
+
+End SporadicModelIndexLemmas.
+
+(** ** Different jobs have different arrival times. *)
+Section DifferentJobsImplyDifferentArrivalTimes.
+
+  (** Consider sporadic tasks ... *)
+  Context {Task : TaskType} `{SporadicModel Task}.
+
+  (** ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+
+  (** Consider any unique arrival sequence with consistent arrivals, ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
+  Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
+
+  (** ... and any sporadic task [tsk] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
+  Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
+
+  (** Consider any two jobs from the arrival sequence that stem 
+      from task [tsk]. *)  
+  Variable j1 : Job.
+  Variable j2 : Job.
+  Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
+  Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
+  Hypothesis H_j1_task: job_task j1 = tsk.
+  Hypothesis H_j2_task: job_task j2 = tsk.
+
+  (** We observe that distinct jobs cannot have equal arrival times. *)
+  Lemma uneq_job_uneq_arr:
+      j1 <> j2 ->
+      job_arrival j1 <> job_arrival j2.
+  Proof.
+    intros UNEQ EQ_ARR.
+    rewrite -> diff_jobs_iff_diff_indices in UNEQ => //; eauto; last by rewrite H_j1_task.
+    move /neqP: UNEQ; rewrite neq_ltn => /orP [LT|LT].
+    all: try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; lia ) ||
+             now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; lia.
+  Qed.
+
+  (** We prove a stronger version of the above lemma by showing 
+   that jobs [j1] and [j2] are equal if and only if they arrive at the
+   same time. *)
+  Lemma same_jobs_iff_same_arr:
+    j1 = j2 <->
+    job_arrival j1 = job_arrival j2.
+  Proof.
+    split; first by apply congr1.
+    intro EQ_ARR.
+    case: (boolP (j1 == j2)) => [/eqP EQ | /eqP NEQ]; first by auto.
+    rewrite -> diff_jobs_iff_diff_indices in NEQ => //; eauto; last by rewrite H_j1_task.
+    move /neqP: NEQ; rewrite neq_ltn => /orP [LT|LT].
+    all: try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; lia ) || now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; lia.
+  Qed.
+
+End DifferentJobsImplyDifferentArrivalTimes.
+
-- 
GitLab