Built with
Alectryon , running Coq+SerAPI v8.20.0+0.20.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 analysis.facts.sporadic.arrival_times.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted. [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
(** * Job Arrival Sequence in the Sporadic Model *)
(** In this file, we prove basic facts about a task's arrival sequence
in the sporadic task model. *)
Section SporadicArrivals .
(** Consider sporadic tasks ... *)
Context {Task : TaskType} `{SporadicModel Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
(** Consider any unique arrival sequence with consistent arrivals, ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence 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.
(** 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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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
move : H_valid_arrival_sequence => [CONSISTENT UNIQ].Task : TaskType H : SporadicModel 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_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_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 jCONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq
False
destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by [] | by apply filter_uniq | ].Task : TaskType H : SporadicModel 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_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_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) CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq 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 : SporadicModel 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_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_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) CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq 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 : SporadicModel 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_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_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) CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq 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 : SporadicModel 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_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_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) CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq 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 : SporadicModel 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_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_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) CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq 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 [].Task : TaskType H : SporadicModel 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_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_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) CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq 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 [].Task : TaskType H : SporadicModel 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_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_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) CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq 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
apply uneq_job_uneq_arr with (arr_seq := arr_seq) (tsk := job_task j) in NEQ => //.Task : TaskType H : SporadicModel 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_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_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) CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq 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
by 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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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]
by rewrite Z in J_IN_FILTER.
- Task : TaskType H : SporadicModel 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_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_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]
case : seq ONE J_IN_FILTER => [//| s [|//]] J_ONE.Task : TaskType H : SporadicModel 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_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_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_ONE : size [:: s] = 1
j1 \in [:: s] -> [:: s] = [:: j1]
by rewrite mem_seq1 => /eqP ->.
- Task : TaskType H : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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)
by 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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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]
by 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 : SporadicModel 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_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_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 : SporadicModel 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_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_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
by 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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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
apply uneq_job_uneq_arr with (arr_seq := arr_seq) (tsk := job_task j1) => //; try by rewrite H_j1_task.Task : TaskType H : SporadicModel 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_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_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 : SporadicModel 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_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_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)
by apply prev_job_arr.
- Task : TaskType H : SporadicModel 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_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_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
by apply prev_job_task.
- Task : TaskType H : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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
by lia .
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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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]
by 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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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 : SporadicModel 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_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_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
by rewrite cat0s H_j1_task.
Qed .
End SporadicArrivals .