Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.model.task.arrival.periodic.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.analysis.facts.job_index.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** * 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 with an offset ... *)
Context {Task : TaskType}.
Context `{TaskOffset Task}.
Context `{TaskMaxInterArrival Task}.
Context `{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 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.Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
job_index arr_seq j1 < job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2
Proof .Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
job_index arr_seq j1 < job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2
intro IND.Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : job_index arr_seq j1 < job_index arr_seq j2
job_arrival j1 < job_arrival j2
move : (H_sporadic_model j1 j2) => SPORADIC; feed_n 6 SPORADIC => //.Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : job_index arr_seq j1 < job_index arr_seq j2 SPORADIC : j1 <> j2 ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = tsk ->
job_task j2 = tsk ->
job_arrival j1 <= job_arrival j2 ->
job_arrival j1 +
task_min_inter_arrival_time tsk <=
job_arrival j2
j1 <> j2
- Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : job_index arr_seq j1 < job_index arr_seq j2 SPORADIC : j1 <> j2 ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = tsk ->
job_task j2 = tsk ->
job_arrival j1 <= job_arrival j2 ->
job_arrival j1 +
task_min_inter_arrival_time tsk <=
job_arrival j2
j1 <> j2
rewrite -> diff_jobs_iff_diff_indices => //; eauto .Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : job_index arr_seq j1 < job_index arr_seq j2 SPORADIC : j1 <> j2 ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = tsk ->
job_task j2 = tsk ->
job_arrival j1 <= job_arrival j2 ->
job_arrival j1 +
task_min_inter_arrival_time tsk <=
job_arrival j2
job_index arr_seq j1 <> job_index arr_seq j2
+ Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : job_index arr_seq j1 < job_index arr_seq j2 SPORADIC : j1 <> j2 ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = tsk ->
job_task j2 = tsk ->
job_arrival j1 <= job_arrival j2 ->
job_arrival j1 +
task_min_inter_arrival_time tsk <=
job_arrival j2
job_index arr_seq j1 <> job_index arr_seq j2
now ssrlia.Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : job_index arr_seq j1 < job_index arr_seq j2 SPORADIC : j1 <> j2 ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = tsk ->
job_task j2 = tsk ->
job_arrival j1 <= job_arrival j2 ->
job_arrival j1 +
task_min_inter_arrival_time tsk <=
job_arrival j2
job_task j1 = job_task j2
+ Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : job_index arr_seq j1 < job_index arr_seq j2 SPORADIC : j1 <> j2 ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = tsk ->
job_task j2 = tsk ->
job_arrival j1 <= job_arrival j2 ->
job_arrival j1 +
task_min_inter_arrival_time tsk <=
job_arrival j2
job_task j1 = job_task j2
now rewrite H_j1_task.Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : job_index arr_seq j1 < job_index arr_seq j2 SPORADIC : job_arrival j1 <= job_arrival j2 ->
job_arrival j1 +
task_min_inter_arrival_time tsk <=
job_arrival j2
job_arrival j1 <= job_arrival j2
- Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : job_index arr_seq j1 < job_index arr_seq j2 SPORADIC : job_arrival j1 <= job_arrival j2 ->
job_arrival j1 +
task_min_inter_arrival_time tsk <=
job_arrival j2
job_arrival j1 <= job_arrival j2
apply (index_lte_implies_arrival_lte arr_seq); try eauto .Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : job_index arr_seq j1 < job_index arr_seq j2 SPORADIC : job_arrival j1 <= job_arrival j2 ->
job_arrival j1 +
task_min_inter_arrival_time tsk <=
job_arrival j2
job_task j2 = job_task j1
now rewrite H_j1_task.Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : job_index arr_seq j1 < job_index arr_seq j2 SPORADIC : job_arrival j1 +
task_min_inter_arrival_time tsk <=
job_arrival j2
job_arrival j1 < job_arrival j2
- Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : job_index arr_seq j1 < job_index arr_seq j2 SPORADIC : job_arrival j1 +
task_min_inter_arrival_time tsk <=
job_arrival j2
job_arrival j1 < job_arrival j2
have POS_IA : task_min_inter_arrival_time tsk > 0 by auto .Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : job_index arr_seq j1 < job_index arr_seq j2 SPORADIC : job_arrival j1 +
task_min_inter_arrival_time tsk <=
job_arrival j2 POS_IA : 0 < task_min_inter_arrival_time tsk
job_arrival j1 < job_arrival j2
now ssrlia.
Qed .
End SporadicModelIndexLemmas .
(** ** Different jobs have different arrival times. *)
Section DifferentJobsImplyDifferentArrivalTimes .
(** Consider sporadic tasks with an offset ... *)
Context {Task : TaskType}.
Context `{TaskOffset Task}.
Context `{TaskMaxInterArrival Task}.
Context `{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.Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
j1 <> j2 -> job_arrival j1 <> job_arrival j2
Proof .Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
j1 <> j2 -> job_arrival j1 <> job_arrival j2
intros UNEQ EQ_ARR.Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk UNEQ : j1 <> j2 EQ_ARR : job_arrival j1 = job_arrival j2
False
rewrite -> diff_jobs_iff_diff_indices in UNEQ => //; eauto ; last by rewrite H_j1_task.Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk EQ_ARR : job_arrival j1 = job_arrival j2 UNEQ : job_index arr_seq j1 <> job_index arr_seq j2
False
move /neqP: UNEQ; rewrite neq_ltn => /orP [LT|LT].Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk EQ_ARR : job_arrival j1 = job_arrival j2 LT : job_index arr_seq j1 < job_index arr_seq j2
False
all : try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; ssrlia ) ||
now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; ssrlia.
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.Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
j1 = j2 <-> job_arrival j1 = job_arrival j2
Proof .Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
j1 = j2 <-> job_arrival j1 = job_arrival j2
split ; first by apply congr1.Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
job_arrival j1 = job_arrival j2 -> j1 = j2
intro EQ_ARR.Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk EQ_ARR : job_arrival j1 = job_arrival j2
j1 = j2
case : (boolP (j1 == j2)) => [/eqP EQ | /eqP NEQ]; first by auto .Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk EQ_ARR : job_arrival j1 = job_arrival j2 NEQ : j1 <> j2
j1 = j2
rewrite -> diff_jobs_iff_diff_indices in NEQ => //; eauto ; last by rewrite H_j1_task.Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk EQ_ARR : job_arrival j1 = job_arrival j2 NEQ : job_index arr_seq j1 <> job_index arr_seq j2
j1 = j2
move /neqP: NEQ; rewrite neq_ltn => /orP [LT|LT].Task : TaskType H : TaskOffset Task H0 : TaskMaxInterArrival Task H1 : SporadicModel Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arrseq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk j1, j2 : Job H_j1_from_arrseq : arrives_in arr_seq j1 H_j2_from_arrseq : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk EQ_ARR : job_arrival j1 = job_arrival j2 LT : job_index arr_seq j1 < job_index arr_seq j2
j1 = j2
all : try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; ssrlia ) || now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; ssrlia.
Qed .
End DifferentJobsImplyDifferentArrivalTimes .
(** In this section we prove a few properties regarding task arrivals
in context of the sporadic task model. *)
Section SporadicArrivals .
(** Consider sporadic tasks with an offset ... *)
Context {Task : TaskType}.
Context `{TaskOffset Task}.
Context `{SporadicModel Task}.
Context `{TaskMaxInterArrival 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_arr_seq : arrival_sequence_uniq arr_seq.
(** ... and any sporadic task [tsk] to be analyzed. *)
Variable tsk : Task.
(** Assume all tasks have valid minimum inter-arrival times, valid offsets, and respect the
sporadic task model. *)
Hypothesis H_sporadic_model : respects_sporadic_task_model arr_seq tsk.
Hypothesis H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk.
Hypothesis H_valid_offset : valid_offset arr_seq tsk.
(** Consider any two jobs from the arrival sequence that stem
from task [tsk]. *)
Variable j1 j2 : Job.
Hypothesis H_j1_from_arrival_sequence : arrives_in arr_seq j1.
Hypothesis H_j2_from_arrival_sequence : arrives_in arr_seq j2.
Hypothesis H_j1_task : job_task j1 = tsk.
Hypothesis H_j2_task : job_task j2 = tsk.
(** We show that a sporadic task with valid min inter-arrival time cannot
have more than one job arriving at any time. *)
Lemma size_task_arrivals_at_leq_one :
(exists j ,
size (task_arrivals_at_job_arrival arr_seq j) > 1 /\
respects_sporadic_task_model arr_seq (job_task j) /\
valid_task_min_inter_arrival_time (job_task j)) ->
False .Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
(exists j : Job,
1 < size (task_arrivals_at_job_arrival arr_seq j) /\
respects_sporadic_task_model arr_seq (job_task j) /\
valid_task_min_inter_arrival_time (job_task j)) ->
False
Proof .Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
(exists j : Job,
1 < size (task_arrivals_at_job_arrival arr_seq j) /\
respects_sporadic_task_model arr_seq (job_task j) /\
valid_task_min_inter_arrival_time (job_task j)) ->
False
move => [j [SIZE_G [PERIODIC VALID_TMIA]]].Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk j : Job SIZE_G : 1 <
size (task_arrivals_at_job_arrival arr_seq j)PERIODIC : respects_sporadic_task_model arr_seq
(job_task j) VALID_TMIA : valid_task_min_inter_arrival_time
(job_task j)
False
specialize (exists_two (task_arrivals_at_job_arrival arr_seq j)) => EXISTS_TWO.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk j : Job SIZE_G : 1 <
size (task_arrivals_at_job_arrival arr_seq j)PERIODIC : respects_sporadic_task_model arr_seq
(job_task j) VALID_TMIA : valid_task_min_inter_arrival_time
(job_task j) EXISTS_TWO : 1 <
size
(task_arrivals_at_job_arrival arr_seq j) ->
uniq
(task_arrivals_at_job_arrival arr_seq j) ->
exists a b : Job,
a <> b /\
a
\in task_arrivals_at_job_arrival
arr_seq j /\
b
\in task_arrivals_at_job_arrival
arr_seq j
False
destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by done | by apply filter_uniq | ].Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk j : Job SIZE_G : 1 <
size (task_arrivals_at_job_arrival arr_seq j)PERIODIC : respects_sporadic_task_model arr_seq
(job_task j) VALID_TMIA : valid_task_min_inter_arrival_time
(job_task j) a, b : Job NEQ : a <> b A_IN : a \in task_arrivals_at_job_arrival arr_seq j B_IN : b \in task_arrivals_at_job_arrival arr_seq j
False
rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk j : Job SIZE_G : 1 <
size (task_arrivals_at_job_arrival arr_seq j)PERIODIC : respects_sporadic_task_model arr_seq
(job_task j) VALID_TMIA : valid_task_min_inter_arrival_time
(job_task j) a, b : Job NEQ : a <> b A_IN : job_of_task (job_task j) a &&
(a \in arrivals_at arr_seq (job_arrival j)) B_IN : job_of_task (job_task j) b &&
(b \in arrivals_at arr_seq (job_arrival j))
False
move : A_IN B_IN => /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk j : Job SIZE_G : 1 <
size (task_arrivals_at_job_arrival arr_seq j)PERIODIC : respects_sporadic_task_model arr_seq
(job_task j) VALID_TMIA : valid_task_min_inter_arrival_time
(job_task j) a, b : Job NEQ : a <> b TSKA : job_task a = job_task j ARRA : a \in arrivals_at arr_seq (job_arrival j) TSKB : job_task b = job_task j ARRB : b \in arrivals_at arr_seq (job_arrival j)
False
move : (ARRA); move : (ARRB); rewrite /arrivals_at => A_IN B_IN.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk j : Job SIZE_G : 1 <
size (task_arrivals_at_job_arrival arr_seq j)PERIODIC : respects_sporadic_task_model arr_seq
(job_task j) VALID_TMIA : valid_task_min_inter_arrival_time
(job_task j) a, b : Job NEQ : a <> b TSKA : job_task a = job_task j ARRA : a \in arrivals_at arr_seq (job_arrival j) TSKB : job_task b = job_task j ARRB : b \in arrivals_at arr_seq (job_arrival j) A_IN : b \in arr_seq (job_arrival j) B_IN : a \in arr_seq (job_arrival j)
False
apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk j : Job SIZE_G : 1 <
size (task_arrivals_at_job_arrival arr_seq j)PERIODIC : respects_sporadic_task_model arr_seq
(job_task j) VALID_TMIA : valid_task_min_inter_arrival_time
(job_task j) a, b : Job NEQ : a <> b TSKA : job_task a = job_task j ARRA : a \in arrivals_at arr_seq (job_arrival j) TSKB : job_task b = job_task j ARRB : b \in arrivals_at arr_seq (job_arrival j) A_IN : arrives_in arr_seq b B_IN : arrives_in arr_seq a
False
have EQ_ARR_A : (job_arrival a = job_arrival j) by apply H_consistent_arrivals.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk j : Job SIZE_G : 1 <
size (task_arrivals_at_job_arrival arr_seq j)PERIODIC : respects_sporadic_task_model arr_seq
(job_task j) VALID_TMIA : valid_task_min_inter_arrival_time
(job_task j) a, b : Job NEQ : a <> b TSKA : job_task a = job_task j ARRA : a \in arrivals_at arr_seq (job_arrival j) TSKB : job_task b = job_task j ARRB : b \in arrivals_at arr_seq (job_arrival j) A_IN : arrives_in arr_seq b B_IN : arrives_in arr_seq a EQ_ARR_A : job_arrival a = job_arrival j
False
have EQ_ARR_B : (job_arrival b = job_arrival j) by apply H_consistent_arrivals.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk j : Job SIZE_G : 1 <
size (task_arrivals_at_job_arrival arr_seq j)PERIODIC : respects_sporadic_task_model arr_seq
(job_task j) VALID_TMIA : valid_task_min_inter_arrival_time
(job_task j) a, b : Job NEQ : a <> b TSKA : job_task a = job_task j ARRA : a \in arrivals_at arr_seq (job_arrival j) TSKB : job_task b = job_task j ARRB : b \in arrivals_at arr_seq (job_arrival j) A_IN : arrives_in arr_seq b B_IN : arrives_in arr_seq a EQ_ARR_A : job_arrival a = job_arrival j EQ_ARR_B : job_arrival b = job_arrival j
False
try ( apply uneq_job_uneq_arr with (arr_seq0 := arr_seq) (tsk0 := job_task j) in NEQ => // ) ||
apply uneq_job_uneq_arr with (arr_seq := arr_seq) (tsk := job_task j) in NEQ => //.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk j : Job SIZE_G : 1 <
size (task_arrivals_at_job_arrival arr_seq j)PERIODIC : respects_sporadic_task_model arr_seq
(job_task j) VALID_TMIA : valid_task_min_inter_arrival_time
(job_task j) a, b : Job NEQ : job_arrival a <> job_arrival b TSKA : job_task a = job_task j ARRA : a \in arrivals_at arr_seq (job_arrival j) TSKB : job_task b = job_task j ARRB : b \in arrivals_at arr_seq (job_arrival j) A_IN : arrives_in arr_seq b B_IN : arrives_in arr_seq a EQ_ARR_A : job_arrival a = job_arrival j EQ_ARR_B : job_arrival b = job_arrival j
False
now rewrite EQ_ARR_A EQ_ARR_B in NEQ.
Qed .
(** We show that no jobs of the task [tsk] other than [j1] arrive at
the same time as [j1], and thus the task arrivals at [job arrival j1]
consists only of job [j1]. *)
Lemma only_j_in_task_arrivals_at_j :
task_arrivals_at_job_arrival arr_seq j1 = [::j1].Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
task_arrivals_at_job_arrival arr_seq j1 = [:: j1]
Proof .Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
task_arrivals_at_job_arrival arr_seq j1 = [:: j1]
set (task_arrivals_at_job_arrival arr_seq j1) as seq in *.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
seq = [:: j1]
have J_IN_FILTER : (j1 \in seq) by apply arrives_in_task_arrivals_at.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job J_IN_FILTER : j1 \in seq
seq = [:: j1]
have SIZE_CASE : size seq = 0 \/ size seq = 1 \/ size seq > 1
by intros ; now destruct (size seq) as [ | [ | ]]; try auto .Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job J_IN_FILTER : j1 \in seq SIZE_CASE : size seq = 0 \/
size seq = 1 \/ 1 < size seq
seq = [:: j1]
move : SIZE_CASE => [Z|[ONE|GTONE]].Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job J_IN_FILTER : j1 \in seq Z : size seq = 0
seq = [:: j1]
- Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job J_IN_FILTER : j1 \in seq Z : size seq = 0
seq = [:: j1]
apply size0nil in Z.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job J_IN_FILTER : j1 \in seq Z : seq = [::]
seq = [:: j1]
now rewrite Z in J_IN_FILTER.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job J_IN_FILTER : j1 \in seq ONE : size seq = 1
seq = [:: j1]
- Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job J_IN_FILTER : j1 \in seq ONE : size seq = 1
seq = [:: j1]
repeat (destruct seq; try by done ).Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk s : Job J_IN_FILTER : j1 \in [:: s] ONE : size [:: s] = 1
[:: s] = [:: j1]
rewrite mem_seq1 in J_IN_FILTER; move : J_IN_FILTER => /eqP J1_S.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk s : Job ONE : size [:: s] = 1 J1_S : j1 = s
[:: s] = [:: j1]
now rewrite J1_S.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job J_IN_FILTER : j1 \in seq GTONE : 1 < size seq
seq = [:: j1]
- Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job J_IN_FILTER : j1 \in seq GTONE : 1 < size seq
seq = [:: j1]
exfalso .Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job J_IN_FILTER : j1 \in seq GTONE : 1 < size seq
False
apply size_task_arrivals_at_leq_one.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job J_IN_FILTER : j1 \in seq GTONE : 1 < size seq
exists j : Job,
1 < size (task_arrivals_at_job_arrival arr_seq j) /\
respects_sporadic_task_model arr_seq (job_task j) /\
valid_task_min_inter_arrival_time (job_task j)
exists j1 .Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job J_IN_FILTER : j1 \in seq GTONE : 1 < size seq
1 < size (task_arrivals_at_job_arrival arr_seq j1) /\
respects_sporadic_task_model arr_seq (job_task j1) /\
valid_task_min_inter_arrival_time (job_task j1)
now repeat split => //; try rewrite H_j1_task.
Qed .
(** We show that no jobs of the task [tsk] other than [j1] arrive at
the same time as [j1], and thus the task arrivals at [job arrival j1]
consists only of job [j1]. *)
Lemma only_j_at_job_arrival_j :
forall t ,
job_arrival j1 = t ->
task_arrivals_at arr_seq tsk t = [::j1].Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
forall t : instant,
job_arrival j1 = t ->
task_arrivals_at arr_seq tsk t = [:: j1]
Proof .Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
forall t : instant,
job_arrival j1 = t ->
task_arrivals_at arr_seq tsk t = [:: j1]
intros t ARR.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk t : instant ARR : job_arrival j1 = t
task_arrivals_at arr_seq tsk t = [:: j1]
rewrite -ARR.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk t : instant ARR : job_arrival j1 = t
task_arrivals_at arr_seq tsk (job_arrival j1) =
[:: j1]
specialize (only_j_in_task_arrivals_at_j) => J_AT.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk t : instant ARR : job_arrival j1 = t J_AT : task_arrivals_at_job_arrival arr_seq j1 =
[:: j1]
task_arrivals_at arr_seq tsk (job_arrival j1) =
[:: j1]
now rewrite /task_arrivals_at_job_arrival H_j1_task in J_AT.
Qed .
(** We show that a job [j1] is the first job that arrives
in task arrivals at [job_arrival j1] by showing that the
index of job [j1] in [task_arrivals_at_job_arrival arr_seq j1] is 0. *)
Lemma index_j_in_task_arrivals_at :
index j1 (task_arrivals_at_job_arrival arr_seq j1) = 0 .Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
index j1 (task_arrivals_at_job_arrival arr_seq j1) = 0
Proof .Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
index j1 (task_arrivals_at_job_arrival arr_seq j1) = 0
now rewrite only_j_in_task_arrivals_at_j //= eq_refl.
Qed .
(** We observe that for any job [j] the arrival time of [prev_job j] is
strictly less than the arrival time of [j] in context of periodic tasks. *)
Lemma prev_job_arr_lt :
job_index arr_seq j1 > 0 ->
job_arrival (prev_job arr_seq j1) < job_arrival j1.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
0 < job_index arr_seq j1 ->
job_arrival (prev_job arr_seq j1) < job_arrival j1
Proof .Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
0 < job_index arr_seq j1 ->
job_arrival (prev_job arr_seq j1) < job_arrival j1
intros IND.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : 0 < job_index arr_seq j1
job_arrival (prev_job arr_seq j1) < job_arrival j1
have PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1 by apply prev_job_arr_lte => //.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : 0 < job_index arr_seq j1PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <=
job_arrival j1
job_arrival (prev_job arr_seq j1) < job_arrival j1
rewrite ltn_neqAle; apply /andP.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : 0 < job_index arr_seq j1PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <=
job_arrival j1
job_arrival (prev_job arr_seq j1) != job_arrival j1 /\
job_arrival (prev_job arr_seq j1) <= job_arrival j1
split => //; apply /eqP.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : 0 < job_index arr_seq j1PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <=
job_arrival j1
job_arrival (prev_job arr_seq j1) <> job_arrival j1
try ( apply uneq_job_uneq_arr with (arr_seq0 := arr_seq) (tsk0 := job_task j1) => //; try by rewrite H_j1_task ) ||
apply uneq_job_uneq_arr with (arr_seq := arr_seq) (tsk := job_task j1) => //; try by rewrite H_j1_task.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : 0 < job_index arr_seq j1PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <=
job_arrival j1
arrives_in arr_seq (prev_job arr_seq j1)
- Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : 0 < job_index arr_seq j1PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <=
job_arrival j1
arrives_in arr_seq (prev_job arr_seq j1)
now apply prev_job_arr.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : 0 < job_index arr_seq j1PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <=
job_arrival j1
job_task (prev_job arr_seq j1) = job_task j1
- Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : 0 < job_index arr_seq j1PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <=
job_arrival j1
job_task (prev_job arr_seq j1) = job_task j1
now apply prev_job_task.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : 0 < job_index arr_seq j1PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <=
job_arrival j1
prev_job arr_seq j1 <> j1
- Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : 0 < job_index arr_seq j1PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <=
job_arrival j1
prev_job arr_seq j1 <> j1
intro EQ.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : 0 < job_index arr_seq j1PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <=
job_arrival j1 EQ : prev_job arr_seq j1 = j1
False
have SM_IND: job_index arr_seq j1 - 1 = job_index arr_seq j1 by rewrite -prev_job_index // EQ.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk IND : 0 < job_index arr_seq j1PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <=
job_arrival j1 EQ : prev_job arr_seq j1 = j1 SM_IND : job_index arr_seq j1 - 1 =
job_index arr_seq j1
False
now ssrlia.
Qed .
(** We show that task arrivals at [job_arrival j1] is the
same as task arrivals that arrive between [job_arrival j1]
and [job_arrival j1 + 1]. *)
Lemma task_arrivals_at_as_task_arrivals_between :
task_arrivals_at_job_arrival arr_seq j1 = task_arrivals_between arr_seq tsk (job_arrival j1) (job_arrival j1).+1 .Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
task_arrivals_at_job_arrival arr_seq j1 =
task_arrivals_between arr_seq tsk (job_arrival j1)
(job_arrival j1).+1
Proof .Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
task_arrivals_at_job_arrival arr_seq j1 =
task_arrivals_between arr_seq tsk (job_arrival j1)
(job_arrival j1).+1
rewrite /task_arrivals_at_job_arrival /task_arrivals_at /task_arrivals_between /arrivals_between.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
[seq j <- arrivals_at arr_seq (job_arrival j1)
| job_of_task (job_task j1) j] =
[seq j <- \cat_(job_arrival j1<=t<(job_arrival j1).+1 )
arrivals_at arr_seq t
| job_of_task tsk j]
now rewrite big_nat1 H_j1_task.
Qed .
(** We show that the task arrivals up to the previous job [j1] concatenated with
the sequence [::j1] (the sequence containing only the job [j1]) is same as
task arrivals up to [job_arrival j1]. *)
Lemma prev_job_cat :
job_index arr_seq j1 > 0 ->
task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++ [::j1] = task_arrivals_up_to_job_arrival arr_seq j1.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
0 < job_index arr_seq j1 ->
task_arrivals_up_to_job_arrival arr_seq
(prev_job arr_seq j1) ++ [:: j1] =
task_arrivals_up_to_job_arrival arr_seq j1
Proof .Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk
0 < job_index arr_seq j1 ->
task_arrivals_up_to_job_arrival arr_seq
(prev_job arr_seq j1) ++ [:: j1] =
task_arrivals_up_to_job_arrival arr_seq j1
intros JIND.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk JIND : 0 < job_index arr_seq j1
task_arrivals_up_to_job_arrival arr_seq
(prev_job arr_seq j1) ++ [:: j1] =
task_arrivals_up_to_job_arrival arr_seq j1
rewrite -only_j_in_task_arrivals_at_j task_arrivals_at_as_task_arrivals_between.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk JIND : 0 < job_index arr_seq j1
task_arrivals_up_to_job_arrival arr_seq
(prev_job arr_seq j1) ++
task_arrivals_between arr_seq tsk (job_arrival j1)
(job_arrival j1).+1 =
task_arrivals_up_to_job_arrival arr_seq j1
rewrite /task_arrivals_up_to_job_arrival prev_job_task => //.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk JIND : 0 < job_index arr_seq j1
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq tsk (job_arrival j1)
(job_arrival j1).+1 =
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival j1)
rewrite [in X in _ = X] (task_arrivals_cat _ _ (job_arrival (prev_job arr_seq j1))); last by
apply ltnW; apply prev_job_arr_lt.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk JIND : 0 < job_index arr_seq j1
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq tsk (job_arrival j1)
(job_arrival j1).+1 =
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)).+1
(job_arrival j1).+1
rewrite [in X in _ = _ ++ X] (task_arrivals_between_cat _ _ _ (job_arrival j1) _) => //; last by apply prev_job_arr_lt.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk JIND : 0 < job_index arr_seq j1
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq tsk (job_arrival j1)
(job_arrival j1).+1 =
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)).+1
(job_arrival j1) ++
task_arrivals_between arr_seq (job_task j1)
(job_arrival j1) (job_arrival j1).+1
rewrite no_jobs_between_consecutive_jobs => //.Task : TaskType H : TaskOffset Task H0 : SporadicModel Task H1 : TaskMaxInterArrival Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job arr_seq : arrival_sequence Job H_consistent_arrivals : consistent_arrival_times
arr_seq H_uniq_arr_seq : arrival_sequence_uniq arr_seq tsk : Task H_sporadic_model : respects_sporadic_task_model
arr_seq tsk H_valid_inter_min_arrival : valid_task_min_inter_arrival_time
tsk H_valid_offset : valid_offset arr_seq tsk j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_j1_task : job_task j1 = tsk H_j2_task : job_task j2 = tsk JIND : 0 < job_index arr_seq j1
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq tsk (job_arrival j1)
(job_arrival j1).+1 =
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
[::] ++
task_arrivals_between arr_seq (job_task j1)
(job_arrival j1) (job_arrival j1).+1
now rewrite cat0s H_j1_task.
Qed .
End SporadicArrivals .