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_as_sporadic.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.sporadic.arrival_times.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]
(** In this section we show that the separation between job
arrivals of a periodic task is some multiple of their
corresponding task's period. *)
Section JobArrivalSeparation .
(** Consider periodic tasks with an offset ... *)
Context {Task : TaskType}.
Context `{PeriodicModel 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_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and any task [tsk] that is to be analyzed. *)
Variable tsk : Task.
(** Assume all tasks have a valid period and respect the periodic task model. *)
Hypothesis H_periodic_model : respects_periodic_task_model arr_seq tsk.
Hypothesis H_valid_period : valid_period tsk.
(** In this section we show that two consecutive jobs of a periodic
task have their arrival times separated by their task's
period. *)
Section ConsecutiveJobSeparation .
(** Consider any two _consecutive_ jobs [j1] and [j2] of task [tsk]. *)
Variable j1 : Job.
Variable j2 : Job.
Hypothesis H_j1_from_arr_seq : arrives_in arr_seq j1.
Hypothesis H_j2_from_arr_seq : arrives_in arr_seq j2.
Hypothesis H_j1_of_task : job_task j1 = tsk.
Hypothesis H_j2_of_task : job_task j2 = tsk.
Hypothesis H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1 .
(** We show that if job [j1] and [j2] are consecutive jobs with [j2]
arriving after [j1], then their arrival times are separated by
their task's period. *)
Lemma consecutive_job_separation :
job_arrival j2 = job_arrival j1 + task_period tsk.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_consecutive_jobs : job_index arr_seq j2 =
job_index arr_seq j1 + 1
job_arrival j2 = job_arrival j1 + task_period tsk
Proof .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_consecutive_jobs : job_index arr_seq j2 =
job_index arr_seq j1 + 1
job_arrival j2 = job_arrival j1 + task_period tsk
move : (H_periodic_model j2) => PERIODIC.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_consecutive_jobs : job_index arr_seq j2 =
job_index arr_seq j1 + 1 PERIODIC : arrives_in arr_seq j2 ->
0 < job_index arr_seq j2 ->
job_task j2 = tsk ->
exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' =
job_index arr_seq j2 - 1 /\
job_task j' = tsk /\
job_arrival j2 =
job_arrival j' + task_period tsk
job_arrival j2 = job_arrival j1 + task_period tsk
feed_n 3 PERIODIC => //; first by rewrite H_consecutive_jobs; lia . Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_consecutive_jobs : job_index arr_seq j2 =
job_index arr_seq j1 + 1 PERIODIC : exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' =
job_index arr_seq j2 - 1 /\
job_task j' = tsk /\
job_arrival j2 =
job_arrival j' + task_period tsk
job_arrival j2 = job_arrival j1 + task_period tsk
move : PERIODIC => [pj' [ARR_IN_PJ' [INDPJ'J' [TSKPJ' ARRPJ']]]].Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_consecutive_jobs : job_index arr_seq j2 =
job_index arr_seq j1 + 1 pj' : Job ARR_IN_PJ' : arrives_in arr_seq pj' INDPJ'J' : job_index arr_seq pj' =
job_index arr_seq j2 - 1 TSKPJ' : job_task pj' = tsk ARRPJ' : job_arrival j2 =
job_arrival pj' + task_period tsk
job_arrival j2 = job_arrival j1 + task_period tsk
rewrite H_consecutive_jobs addnK in INDPJ'J'.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_consecutive_jobs : job_index arr_seq j2 =
job_index arr_seq j1 + 1 pj' : Job ARR_IN_PJ' : arrives_in arr_seq pj' TSKPJ' : job_task pj' = tsk ARRPJ' : job_arrival j2 =
job_arrival pj' + task_period tsk INDPJ'J' : job_index arr_seq pj' =
job_index arr_seq j1
job_arrival j2 = job_arrival j1 + task_period tsk
apply equal_index_implies_equal_jobs in INDPJ'J' => //; last by rewrite TSKPJ'.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_consecutive_jobs : job_index arr_seq j2 =
job_index arr_seq j1 + 1 pj' : Job ARR_IN_PJ' : arrives_in arr_seq pj' TSKPJ' : job_task pj' = tsk ARRPJ' : job_arrival j2 =
job_arrival pj' + task_period tsk INDPJ'J' : pj' = j1
job_arrival j2 = job_arrival j1 + task_period tsk
by rewrite INDPJ'J' in ARRPJ'; lia .
Qed .
End ConsecutiveJobSeparation .
(** In this section we show that for two unequal jobs of a task,
there exists a non-zero multiple of their task's period which separates
their arrival times. *)
Section ArrivalSeparationWithGivenIndexDifference .
(** Consider any two _consecutive_ jobs [j1] and [j2] of task [tsk]
that stem from the arrival sequence. *)
Variable j1 j2 : Job.
Hypothesis H_j1_from_arr_seq : arrives_in arr_seq j1.
Hypothesis H_j2_from_arr_seq : arrives_in arr_seq j2.
Hypothesis H_j1_of_task : job_task j1 = tsk.
Hypothesis H_j2_of_task : job_task j2 = tsk.
(** We'll assume that job [j1] arrives before [j2] and that
their indices differ by an integer [k]. *)
Variable k : nat.
Hypothesis H_index_difference_k : job_index arr_seq j1 + k = job_index arr_seq j2 .
Hypothesis H_job_arrival_lt : job_arrival j1 < job_arrival j2.
(** We prove that arrival of unequal jobs of a task [tsk] are
separated by a non-zero multiple of [task_period tsk] provided
their index differs by a number [k]. *)
Lemma job_arrival_separation_when_index_diff_is_k :
exists n ,
n > 0 /\
job_arrival j2 = job_arrival j1 + n * task_period tsk.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk k : nat H_index_difference_k : job_index arr_seq j1 + k =
job_index arr_seq j2 H_job_arrival_lt : job_arrival j1 < job_arrival j2
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
Proof .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk k : nat H_index_difference_k : job_index arr_seq j1 + k =
job_index arr_seq j2 H_job_arrival_lt : job_arrival j1 < job_arrival j2
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
move : j1 j2 H_j1_of_task H_j2_of_task H_index_difference_k H_job_arrival_lt H_j2_from_arr_seq H_j1_from_arr_seq;
clear H_index_difference_k H_job_arrival_lt H_j2_from_arr_seq H_j1_from_arr_seq H_j1_of_task H_j2_of_task j1 j2.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k : nat
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + k = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
move : k => s.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
induction s.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k : nat
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
{ Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k : nat
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
intros j1 j2 TSKj1 TSKj2 STEP LT ARRj1 ARRj2; exfalso .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k : nat j1, j2 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + 0 = job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj1 : arrives_in arr_seq j2 ARRj2 : arrives_in arr_seq j1
False
specialize (earlier_arrival_implies_lower_index arr_seq H_valid_arrival_sequence j1 j2) => LT_IND.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k : nat j1, j2 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + 0 = job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj1 : arrives_in arr_seq j2 ARRj2 : arrives_in arr_seq j1 LT_IND : arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = job_task j2 ->
job_arrival j1 < job_arrival j2 ->
job_index arr_seq j1 < job_index arr_seq j2
False
feed_n 4 LT_IND => //; first by rewrite TSKj2. Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k : nat j1, j2 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + 0 = job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj1 : arrives_in arr_seq j2 ARRj2 : arrives_in arr_seq j1 LT_IND : job_index arr_seq j1 < job_index arr_seq j2
False
by lia .
} Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s.+1 = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
{ Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s.+1 = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
intros j1 j2 TSKj1 TSKj2 STEP LT ARRj2 ARRj1.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tskj1, j2 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+1 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
specialize (exists_jobs_before_j
arr_seq H_valid_arrival_sequence j2 ARRj2 (job_index arr_seq j2 - s)) => BEFORE.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tskj1, j2 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+1 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 BEFORE : job_index arr_seq j2 - s <
job_index arr_seq j2 ->
exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' =
job_index arr_seq j2 - s
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
destruct s.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k : nat IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tskj1, j2 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + 1 = job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 BEFORE : job_index arr_seq j2 - 0 <
job_index arr_seq j2 ->
exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' =
job_index arr_seq j2 - 0
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
- Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k : nat IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tskj1, j2 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + 1 = job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 BEFORE : job_index arr_seq j2 - 0 <
job_index arr_seq j2 ->
exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' =
job_index arr_seq j2 - 0
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
exists 1 ; repeat split .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k : nat IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tskj1, j2 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + 1 = job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 BEFORE : job_index arr_seq j2 - 0 <
job_index arr_seq j2 ->
exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' =
job_index arr_seq j2 - 0
job_arrival j2 = job_arrival j1 + 1 * task_period tsk
by rewrite (consecutive_job_separation j1) //; lia .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s.+1 =
job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tskj1, j2 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+2 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 BEFORE : job_index arr_seq j2 - s.+1 <
job_index arr_seq j2 ->
exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' =
job_index arr_seq j2 - s.+1
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
- Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s.+1 =
job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tskj1, j2 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+2 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 BEFORE : job_index arr_seq j2 - s.+1 <
job_index arr_seq j2 ->
exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' =
job_index arr_seq j2 - s.+1
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
feed BEFORE; first by lia . Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s.+1 =
job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tskj1, j2 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+2 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 BEFORE : exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' =
job_index arr_seq j2 - s.+1
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
move : BEFORE => [nj [NEQNJ [TSKNJ [ARRNJ INDNJ]]]]; rewrite TSKj2 in TSKNJ.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s.+1 =
job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tskj1, j2 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+2 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 nj : Job NEQNJ : j2 <> nj ARRNJ : arrives_in arr_seq nj INDNJ : job_index arr_seq nj =
job_index arr_seq j2 - s.+1 TSKNJ : job_task nj = tsk
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
specialize (IHs nj j2); feed_n 6 IHs => //; first by lia .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat j2, nj : Job IHs : job_arrival nj < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq nj ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival nj + n * task_period tsk j1 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+2 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 NEQNJ : j2 <> nj ARRNJ : arrives_in arr_seq nj INDNJ : job_index arr_seq nj =
job_index arr_seq j2 - s.+1 TSKNJ : job_task nj = tsk
job_arrival nj < job_arrival j2
{ Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat j2, nj : Job IHs : job_arrival nj < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq nj ->
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival nj + n * task_period tsk j1 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+2 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 NEQNJ : j2 <> nj ARRNJ : arrives_in arr_seq nj INDNJ : job_index arr_seq nj =
job_index arr_seq j2 - s.+1 TSKNJ : job_task nj = tsk
job_arrival nj < job_arrival j2
by apply (lower_index_implies_earlier_arrival _ H_valid_arrival_sequence tsk);
rt_eauto; lia .
} Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat j2, nj : Job IHs : exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival nj + n * task_period tskj1 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+2 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 NEQNJ : j2 <> nj ARRNJ : arrives_in arr_seq nj INDNJ : job_index arr_seq nj =
job_index arr_seq j2 - s.+1 TSKNJ : job_task nj = tsk
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
move : IHs => [n [NZN ARRJ'NJ]].Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat j2, nj, j1 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+2 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 NEQNJ : j2 <> nj ARRNJ : arrives_in arr_seq nj INDNJ : job_index arr_seq nj =
job_index arr_seq j2 - s.+1 TSKNJ : job_task nj = tsk n : nat NZN : 0 < nARRJ'NJ : job_arrival j2 =
job_arrival nj + n * task_period tsk
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
move : (H_periodic_model nj) => PERIODIC; feed_n 3 PERIODIC => //; first by lia .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat j2, nj, j1 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+2 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 NEQNJ : j2 <> nj ARRNJ : arrives_in arr_seq nj INDNJ : job_index arr_seq nj =
job_index arr_seq j2 - s.+1 TSKNJ : job_task nj = tsk n : nat NZN : 0 < nARRJ'NJ : job_arrival j2 =
job_arrival nj + n * task_period tsk PERIODIC : exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' =
job_index arr_seq nj - 1 /\
job_task j' = tsk /\
job_arrival nj =
job_arrival j' + task_period tsk
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
move : PERIODIC => [sj [ARR_IN_SJ [INDSJ [TSKSJ ARRSJ]]]]; rewrite ARRSJ in ARRJ'NJ.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat j2, nj, j1 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+2 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 NEQNJ : j2 <> nj ARRNJ : arrives_in arr_seq nj INDNJ : job_index arr_seq nj =
job_index arr_seq j2 - s.+1 TSKNJ : job_task nj = tsk n : nat NZN : 0 < nsj : Job ARR_IN_SJ : arrives_in arr_seq sj INDSJ : job_index arr_seq sj =
job_index arr_seq nj - 1 TSKSJ : job_task sj = tsk ARRSJ : job_arrival nj =
job_arrival sj + task_period tsk ARRJ'NJ : job_arrival j2 =
job_arrival sj + task_period tsk +
n * task_period tsk
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
have INDJ : (job_index arr_seq j1 = job_index arr_seq j2 - s.+2 ) by lia .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat j2, nj, j1 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+2 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 NEQNJ : j2 <> nj ARRNJ : arrives_in arr_seq nj INDNJ : job_index arr_seq nj =
job_index arr_seq j2 - s.+1 TSKNJ : job_task nj = tsk n : nat NZN : 0 < nsj : Job ARR_IN_SJ : arrives_in arr_seq sj INDSJ : job_index arr_seq sj =
job_index arr_seq nj - 1 TSKSJ : job_task sj = tsk ARRSJ : job_arrival nj =
job_arrival sj + task_period tsk ARRJ'NJ : job_arrival j2 =
job_arrival sj + task_period tsk +
n * task_period tsk INDJ : job_index arr_seq j1 =
job_index arr_seq j2 - s.+2
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
rewrite INDNJ -subnDA addn1 -INDJ in INDSJ.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat j2, nj, j1 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+2 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 NEQNJ : j2 <> nj ARRNJ : arrives_in arr_seq nj INDNJ : job_index arr_seq nj =
job_index arr_seq j2 - s.+1 TSKNJ : job_task nj = tsk n : nat NZN : 0 < nsj : Job ARR_IN_SJ : arrives_in arr_seq sj TSKSJ : job_task sj = tsk ARRSJ : job_arrival nj =
job_arrival sj + task_period tsk ARRJ'NJ : job_arrival j2 =
job_arrival sj + task_period tsk +
n * task_period tsk INDJ : job_index arr_seq j1 =
job_index arr_seq j2 - s.+2 INDSJ : job_index arr_seq sj = job_index arr_seq j1
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
apply equal_index_implies_equal_jobs in INDSJ => //; last by rewrite TSKj1 => //.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat j2, nj, j1 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+2 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 NEQNJ : j2 <> nj ARRNJ : arrives_in arr_seq nj INDNJ : job_index arr_seq nj =
job_index arr_seq j2 - s.+1 TSKNJ : job_task nj = tsk n : nat NZN : 0 < nsj : Job ARR_IN_SJ : arrives_in arr_seq sj TSKSJ : job_task sj = tsk ARRSJ : job_arrival nj =
job_arrival sj + task_period tsk ARRJ'NJ : job_arrival j2 =
job_arrival sj + task_period tsk +
n * task_period tsk INDJ : job_index arr_seq j1 =
job_index arr_seq j2 - s.+2 INDSJ : sj = j1
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
exists (n .+1 ); split ; try by lia .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat j2, nj, j1 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+2 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 NEQNJ : j2 <> nj ARRNJ : arrives_in arr_seq nj INDNJ : job_index arr_seq nj =
job_index arr_seq j2 - s.+1 TSKNJ : job_task nj = tsk n : nat NZN : 0 < nsj : Job ARR_IN_SJ : arrives_in arr_seq sj TSKSJ : job_task sj = tsk ARRSJ : job_arrival nj =
job_arrival sj + task_period tsk ARRJ'NJ : job_arrival j2 =
job_arrival sj + task_period tsk +
n * task_period tsk INDJ : job_index arr_seq j1 =
job_index arr_seq j2 - s.+2 INDSJ : sj = j1
job_arrival j2 =
job_arrival j1 + n.+1 * task_period tsk
rewrite INDSJ in ARRJ'NJ; rewrite mulSnr.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk k, s : nat j2, nj, j1 : Job TSKj1 : job_task j1 = tsk TSKj2 : job_task j2 = tsk STEP : job_index arr_seq j1 + s.+2 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2 ARRj2 : arrives_in arr_seq j2 ARRj1 : arrives_in arr_seq j1 NEQNJ : j2 <> nj ARRNJ : arrives_in arr_seq nj INDNJ : job_index arr_seq nj =
job_index arr_seq j2 - s.+1 TSKNJ : job_task nj = tsk n : nat NZN : 0 < nsj : Job ARR_IN_SJ : arrives_in arr_seq sj TSKSJ : job_task sj = tsk ARRSJ : job_arrival nj =
job_arrival sj + task_period tsk INDJ : job_index arr_seq j1 =
job_index arr_seq j2 - s.+2 INDSJ : sj = j1 ARRJ'NJ : job_arrival j2 =
job_arrival j1 + task_period tsk +
n * task_period tsk
job_arrival j2 =
job_arrival j1 +
(n * task_period tsk + task_period tsk)
by lia .
}
Qed .
End ArrivalSeparationWithGivenIndexDifference .
(** Consider any two _distinct_ jobs [j1] and [j2] of task [tsk]
that stem from the arrival sequence. *)
Variable j1 j2 : Job.
Hypothesis H_j1_neq_j2 : j1 <> j2.
Hypothesis H_j1_from_arr_seq : arrives_in arr_seq j1.
Hypothesis H_j2_from_arr_seq : arrives_in arr_seq j2.
Hypothesis H_j1_of_task : job_task j1 = tsk.
Hypothesis H_j2_of_task : job_task j2 = tsk.
(** Without loss of generality, we assume that
job [j1] arrives before job [j2]. *)
Hypothesis H_j1_before_j2 : job_arrival j1 <= job_arrival j2.
(** We generalize the above lemma to show that any two unequal
jobs of task [tsk] are separated by a non-zero multiple
of [task_period tsk]. *)
Lemma job_sep_periodic :
exists n ,
n > 0 /\
job_arrival j2 = job_arrival j1 + n * task_period tsk.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
Proof .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2
exists n : nat,
0 < n /\
job_arrival j2 =
job_arrival j1 + n * task_period tsk
apply job_arrival_separation_when_index_diff_is_k with (k := (job_index arr_seq j2 - job_index arr_seq j1)); try done .Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2
job_index arr_seq j1 +
(job_index arr_seq j2 - job_index arr_seq j1) =
job_index arr_seq j2
- Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2
job_index arr_seq j1 +
(job_index arr_seq j2 - job_index arr_seq j1) =
job_index arr_seq j2
apply subnKC.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2
job_index arr_seq j1 <= job_index arr_seq j2
move_neq_up IND. Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2 IND : job_index arr_seq j2 < job_index arr_seq j1
False
eapply lower_index_implies_earlier_arrival in IND; rt_eauto.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2 IND : job_arrival j2 < job_arrival j1
False
by move_neq_down IND.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2
job_arrival j1 < job_arrival j2
- Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2
job_arrival j1 < job_arrival j2
case : (boolP (job_index arr_seq j1 == job_index arr_seq j2)) => [/eqP EQ_IND|NEQ_IND].Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2 EQ_IND : job_index arr_seq j1 = job_index arr_seq j2
job_arrival j1 < job_arrival j2
+ Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2 EQ_IND : job_index arr_seq j1 = job_index arr_seq j2
job_arrival j1 < job_arrival j2
by apply equal_index_implies_equal_jobs in EQ_IND => //; rewrite H_j1_of_task.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2 NEQ_IND : job_index arr_seq j1 != job_index arr_seq j2
job_arrival j1 < job_arrival j2
+ Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2 NEQ_IND : job_index arr_seq j1 != job_index arr_seq j2
job_arrival j1 < job_arrival j2
move : NEQ_IND; rewrite neq_ltn => /orP [LT|LT].Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2 LT : job_index arr_seq j1 < job_index arr_seq j2
job_arrival j1 < job_arrival j2
* Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2 LT : job_index arr_seq j1 < job_index arr_seq j2
job_arrival j1 < job_arrival j2
by eapply (lower_index_implies_earlier_arrival) in LT; rt_eauto.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2 LT : job_index arr_seq j2 < job_index arr_seq j1
job_arrival j1 < job_arrival j2
* Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2 LT : job_index arr_seq j2 < job_index arr_seq j1
job_arrival j1 < job_arrival j2
eapply (lower_index_implies_earlier_arrival) in LT; rt_eauto.Task : TaskType H : PeriodicModel Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_periodic_model : respects_periodic_task_model
arr_seq tsk H_valid_period : valid_period tsk j1, j2 : Job H_j1_neq_j2 : j1 <> j2 H_j1_from_arr_seq : arrives_in arr_seq j1 H_j2_from_arr_seq : arrives_in arr_seq j2 H_j1_of_task : job_task j1 = tsk H_j2_of_task : job_task j2 = tsk H_j1_before_j2 : job_arrival j1 <= job_arrival j2 LT : job_arrival j2 < job_arrival j1
job_arrival j1 < job_arrival j2
by move_neq_down LT.
Qed .
End JobArrivalSeparation .