Library prosa.analysis.facts.periodic.sporadic
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.task.arrival.periodic.
Treating Periodic Tasks as Sporadic Tasks
Any type of periodic tasks ...
... and their corresponding jobs from a consistent arrival sequence with
non-duplicate arrivals ...
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
... may be interpreted as a type of sporadic tasks by using each task's
period as its minimum inter-arrival time ...
Global Instance periodic_as_sporadic : SporadicModel Task :=
{
task_min_inter_arrival_time := task_period
}.
{
task_min_inter_arrival_time := task_period
}.
... such that the model interpretation is valid, both w.r.t. the minimum
inter-arrival time parameter ...
Remark valid_period_is_valid_inter_arrival_time:
∀ tsk, valid_period tsk → valid_task_min_inter_arrival_time tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 44)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
============================
forall tsk : Task,
valid_period tsk -> valid_task_min_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
Proof. trivial.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ tsk, valid_period tsk → valid_task_min_inter_arrival_time tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 44)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
============================
forall tsk : Task,
valid_period tsk -> valid_task_min_inter_arrival_time tsk
----------------------------------------------------------------------------- *)
Proof. trivial.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
... and the separation of job arrivals.
Remark periodic_task_respects_sporadic_task_model:
∀ tsk, valid_period tsk →
respects_periodic_task_model arr_seq tsk →
respects_sporadic_task_model arr_seq tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
============================
forall tsk : Task,
valid_period tsk ->
respects_periodic_task_model arr_seq tsk ->
respects_sporadic_task_model arr_seq tsk
----------------------------------------------------------------------------- *)
Proof.
intros tsk VALID_PERIOD H_PERIODIC j1 j2 NEQ ARR ARR' TSK TSK' ARR_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 73)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
H_PERIODIC : respects_periodic_task_model arr_seq tsk
j1, j2 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
============================
job_arrival j1 + task_min_inter_arrival_time tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
rewrite /task_min_inter_arrival_time /periodic_as_sporadic.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 79)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
H_PERIODIC : respects_periodic_task_model arr_seq tsk
j1, j2 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
============================
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
have IND_LT : job_index arr_seq j1 < job_index arr_seq j2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 88)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
H_PERIODIC : respects_periodic_task_model arr_seq tsk
j1, j2 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
============================
job_index arr_seq j1 < job_index arr_seq j2
subgoal 2 (ID 90) is:
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 88)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
H_PERIODIC : respects_periodic_task_model arr_seq tsk
j1, j2 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
============================
job_index arr_seq j1 < job_index arr_seq j2
----------------------------------------------------------------------------- *)
rewrite → diff_jobs_iff_diff_indices in NEQ ⇒ //; auto; last by rewrite TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 107)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
H_PERIODIC : respects_periodic_task_model arr_seq tsk
j1, j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
============================
job_index arr_seq j1 < job_index arr_seq j2
----------------------------------------------------------------------------- *)
move_neq_up IND_LTE; move_neq_down ARR_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 342)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
H_PERIODIC : respects_periodic_task_model arr_seq tsk
j1, j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
============================
job_arrival j2 < job_arrival j1
----------------------------------------------------------------------------- *)
specialize (H_PERIODIC j1); feed_n 3 H_PERIODIC ⇒ //; try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 362)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j1 : Job
H_PERIODIC : exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j1 - 1 /\
job_task j' = tsk /\
job_arrival j1 = job_arrival j' + task_period tsk
j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
============================
job_arrival j2 < job_arrival j1
----------------------------------------------------------------------------- *)
move : H_PERIODIC ⇒ [pj [ARR_PJ [IND_PJ [TSK_PJ PJ_ARR]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1234)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j1, j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j1 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j1 = job_arrival pj + task_period tsk
============================
job_arrival j2 < job_arrival j1
----------------------------------------------------------------------------- *)
have JB_IND_LTE : job_index arr_seq j2 ≤ job_index arr_seq pj by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1503)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j1, j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j1 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j1 = job_arrival pj + task_period tsk
JB_IND_LTE : job_index arr_seq j2 <= job_index arr_seq pj
============================
job_arrival j2 < job_arrival j1
----------------------------------------------------------------------------- *)
apply index_lte_implies_arrival_lte in JB_IND_LTE ⇒ //; try by rewrite TSK_PJ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1508)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j1, j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j1 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j1 = job_arrival pj + task_period tsk
JB_IND_LTE : job_arrival j2 <= job_arrival pj
============================
job_arrival j2 < job_arrival j1
----------------------------------------------------------------------------- *)
rewrite PJ_ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1582)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j1, j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j1 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j1 = job_arrival pj + task_period tsk
JB_IND_LTE : job_arrival j2 <= job_arrival pj
============================
job_arrival j2 < job_arrival pj + task_period tsk
----------------------------------------------------------------------------- *)
have POS_PERIOD : task_period tsk > 0 by auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1587)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j1, j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j1 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j1 = job_arrival pj + task_period tsk
JB_IND_LTE : job_arrival j2 <= job_arrival pj
POS_PERIOD : 0 < task_period tsk
============================
job_arrival j2 < job_arrival pj + task_period tsk
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 90)
subgoal 1 (ID 90) is:
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 90)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
H_PERIODIC : respects_periodic_task_model arr_seq tsk
j1, j2 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
IND_LT : job_index arr_seq j1 < job_index arr_seq j2
============================
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
specialize (H_PERIODIC j2); feed_n 3 H_PERIODIC ⇒ //; try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1945)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j2 : Job
H_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
j1 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
IND_LT : job_index arr_seq j1 < job_index arr_seq j2
============================
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
move: H_PERIODIC ⇒ [pj [ARR_PJ [IND_PJ [TSK_PJ PJ_ARR]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2876)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j2, j1 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
IND_LT : job_index arr_seq j1 < job_index arr_seq j2
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j2 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j2 = job_arrival pj + task_period tsk
============================
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
have JB_IND_LTE : job_index arr_seq j1 ≤ job_index arr_seq pj by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3173)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j2, j1 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
IND_LT : job_index arr_seq j1 < job_index arr_seq j2
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j2 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j2 = job_arrival pj + task_period tsk
JB_IND_LTE : job_index arr_seq j1 <= job_index arr_seq pj
============================
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
apply index_lte_implies_arrival_lte in JB_IND_LTE ⇒ //; try by rewrite TSK_PJ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3178)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j2, j1 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
IND_LT : job_index arr_seq j1 < job_index arr_seq j2
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j2 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j2 = job_arrival pj + task_period tsk
JB_IND_LTE : job_arrival j1 <= job_arrival pj
============================
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
now rewrite PJ_ARR; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ tsk, valid_period tsk →
respects_periodic_task_model arr_seq tsk →
respects_sporadic_task_model arr_seq tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
============================
forall tsk : Task,
valid_period tsk ->
respects_periodic_task_model arr_seq tsk ->
respects_sporadic_task_model arr_seq tsk
----------------------------------------------------------------------------- *)
Proof.
intros tsk VALID_PERIOD H_PERIODIC j1 j2 NEQ ARR ARR' TSK TSK' ARR_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 73)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
H_PERIODIC : respects_periodic_task_model arr_seq tsk
j1, j2 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
============================
job_arrival j1 + task_min_inter_arrival_time tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
rewrite /task_min_inter_arrival_time /periodic_as_sporadic.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 79)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
H_PERIODIC : respects_periodic_task_model arr_seq tsk
j1, j2 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
============================
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
have IND_LT : job_index arr_seq j1 < job_index arr_seq j2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 88)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
H_PERIODIC : respects_periodic_task_model arr_seq tsk
j1, j2 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
============================
job_index arr_seq j1 < job_index arr_seq j2
subgoal 2 (ID 90) is:
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 88)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
H_PERIODIC : respects_periodic_task_model arr_seq tsk
j1, j2 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
============================
job_index arr_seq j1 < job_index arr_seq j2
----------------------------------------------------------------------------- *)
rewrite → diff_jobs_iff_diff_indices in NEQ ⇒ //; auto; last by rewrite TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 107)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
H_PERIODIC : respects_periodic_task_model arr_seq tsk
j1, j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
============================
job_index arr_seq j1 < job_index arr_seq j2
----------------------------------------------------------------------------- *)
move_neq_up IND_LTE; move_neq_down ARR_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 342)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
H_PERIODIC : respects_periodic_task_model arr_seq tsk
j1, j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
============================
job_arrival j2 < job_arrival j1
----------------------------------------------------------------------------- *)
specialize (H_PERIODIC j1); feed_n 3 H_PERIODIC ⇒ //; try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 362)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j1 : Job
H_PERIODIC : exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j1 - 1 /\
job_task j' = tsk /\
job_arrival j1 = job_arrival j' + task_period tsk
j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
============================
job_arrival j2 < job_arrival j1
----------------------------------------------------------------------------- *)
move : H_PERIODIC ⇒ [pj [ARR_PJ [IND_PJ [TSK_PJ PJ_ARR]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1234)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j1, j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j1 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j1 = job_arrival pj + task_period tsk
============================
job_arrival j2 < job_arrival j1
----------------------------------------------------------------------------- *)
have JB_IND_LTE : job_index arr_seq j2 ≤ job_index arr_seq pj by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1503)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j1, j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j1 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j1 = job_arrival pj + task_period tsk
JB_IND_LTE : job_index arr_seq j2 <= job_index arr_seq pj
============================
job_arrival j2 < job_arrival j1
----------------------------------------------------------------------------- *)
apply index_lte_implies_arrival_lte in JB_IND_LTE ⇒ //; try by rewrite TSK_PJ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1508)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j1, j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j1 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j1 = job_arrival pj + task_period tsk
JB_IND_LTE : job_arrival j2 <= job_arrival pj
============================
job_arrival j2 < job_arrival j1
----------------------------------------------------------------------------- *)
rewrite PJ_ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1582)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j1, j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j1 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j1 = job_arrival pj + task_period tsk
JB_IND_LTE : job_arrival j2 <= job_arrival pj
============================
job_arrival j2 < job_arrival pj + task_period tsk
----------------------------------------------------------------------------- *)
have POS_PERIOD : task_period tsk > 0 by auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1587)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j1, j2 : Job
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j1 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j1 = job_arrival pj + task_period tsk
JB_IND_LTE : job_arrival j2 <= job_arrival pj
POS_PERIOD : 0 < task_period tsk
============================
job_arrival j2 < job_arrival pj + task_period tsk
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 90)
subgoal 1 (ID 90) is:
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 90)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
H_PERIODIC : respects_periodic_task_model arr_seq tsk
j1, j2 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
IND_LT : job_index arr_seq j1 < job_index arr_seq j2
============================
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
specialize (H_PERIODIC j2); feed_n 3 H_PERIODIC ⇒ //; try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1945)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j2 : Job
H_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
j1 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
IND_LT : job_index arr_seq j1 < job_index arr_seq j2
============================
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
move: H_PERIODIC ⇒ [pj [ARR_PJ [IND_PJ [TSK_PJ PJ_ARR]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2876)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j2, j1 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
IND_LT : job_index arr_seq j1 < job_index arr_seq j2
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j2 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j2 = job_arrival pj + task_period tsk
============================
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
have JB_IND_LTE : job_index arr_seq j1 ≤ job_index arr_seq pj by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3173)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j2, j1 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
IND_LT : job_index arr_seq j1 < job_index arr_seq j2
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j2 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j2 = job_arrival pj + task_period tsk
JB_IND_LTE : job_index arr_seq j1 <= job_index arr_seq pj
============================
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
apply index_lte_implies_arrival_lte in JB_IND_LTE ⇒ //; try by rewrite TSK_PJ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3178)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
VALID_PERIOD : valid_period tsk
j2, j1 : Job
NEQ : j1 <> j2
ARR : arrives_in arr_seq j1
ARR' : arrives_in arr_seq j2
TSK : job_task j1 = tsk
TSK' : job_task j2 = tsk
ARR_LT : job_arrival j1 <= job_arrival j2
IND_LT : job_index arr_seq j1 < job_index arr_seq j2
pj : Job
ARR_PJ : arrives_in arr_seq pj
IND_PJ : job_index arr_seq pj = job_index arr_seq j2 - 1
TSK_PJ : job_task pj = tsk
PJ_ARR : job_arrival j2 = job_arrival pj + task_period tsk
JB_IND_LTE : job_arrival j1 <= job_arrival pj
============================
job_arrival j1 + task_period tsk <= job_arrival j2
----------------------------------------------------------------------------- *)
now rewrite PJ_ARR; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
For convenience, we state these obvious correspondences also at the level
of entire task sets.
First, we show that all tasks in a task set with valid periods
also have valid min inter-arrival times.
Remark valid_periods_are_valid_inter_arrival_times:
∀ ts, valid_periods ts → valid_taskset_inter_arrival_times ts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 69)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
============================
forall ts : TaskSet Task,
valid_periods ts -> valid_taskset_inter_arrival_times ts
----------------------------------------------------------------------------- *)
Proof. trivial.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ ts, valid_periods ts → valid_taskset_inter_arrival_times ts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 69)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
============================
forall ts : TaskSet Task,
valid_periods ts -> valid_taskset_inter_arrival_times ts
----------------------------------------------------------------------------- *)
Proof. trivial.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Second, we show that each task in a periodic task set respects
the sporadic task model.
Remark periodic_task_sets_respect_sporadic_task_model:
∀ ts,
valid_periods ts →
taskset_respects_periodic_task_model arr_seq ts →
taskset_respects_sporadic_task_model ts arr_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 86)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
============================
forall ts : TaskSet Task,
valid_periods ts ->
taskset_respects_periodic_task_model arr_seq ts ->
taskset_respects_sporadic_task_model ts arr_seq
----------------------------------------------------------------------------- *)
Proof.
intros ts VALID_PERIODS H_PERIODIC tsk TSK_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 92)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
ts : TaskSet Task
VALID_PERIODS : valid_periods ts
H_PERIODIC : taskset_respects_periodic_task_model arr_seq ts
tsk : Task
TSK_IN : tsk \in ts
============================
respects_sporadic_task_model arr_seq tsk
----------------------------------------------------------------------------- *)
specialize (H_PERIODIC tsk TSK_IN).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 94)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
ts : TaskSet Task
VALID_PERIODS : valid_periods ts
tsk : Task
H_PERIODIC : respects_periodic_task_model arr_seq tsk
TSK_IN : tsk \in ts
============================
respects_sporadic_task_model arr_seq tsk
----------------------------------------------------------------------------- *)
apply periodic_task_respects_sporadic_task_model ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 95)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
ts : TaskSet Task
VALID_PERIODS : valid_periods ts
tsk : Task
H_PERIODIC : respects_periodic_task_model arr_seq tsk
TSK_IN : tsk \in ts
============================
valid_period tsk
----------------------------------------------------------------------------- *)
now apply VALID_PERIODS.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PeriodicTasksAsSporadicTasks.
∀ ts,
valid_periods ts →
taskset_respects_periodic_task_model arr_seq ts →
taskset_respects_sporadic_task_model ts arr_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 86)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
============================
forall ts : TaskSet Task,
valid_periods ts ->
taskset_respects_periodic_task_model arr_seq ts ->
taskset_respects_sporadic_task_model ts arr_seq
----------------------------------------------------------------------------- *)
Proof.
intros ts VALID_PERIODS H_PERIODIC tsk TSK_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 92)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
ts : TaskSet Task
VALID_PERIODS : valid_periods ts
H_PERIODIC : taskset_respects_periodic_task_model arr_seq ts
tsk : Task
TSK_IN : tsk \in ts
============================
respects_sporadic_task_model arr_seq tsk
----------------------------------------------------------------------------- *)
specialize (H_PERIODIC tsk TSK_IN).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 94)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
ts : TaskSet Task
VALID_PERIODS : valid_periods ts
tsk : Task
H_PERIODIC : respects_periodic_task_model arr_seq tsk
TSK_IN : tsk \in ts
============================
respects_sporadic_task_model arr_seq tsk
----------------------------------------------------------------------------- *)
apply periodic_task_respects_sporadic_task_model ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 95)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
ts : TaskSet Task
VALID_PERIODS : valid_periods ts
tsk : Task
H_PERIODIC : respects_periodic_task_model arr_seq tsk
TSK_IN : tsk \in ts
============================
valid_period tsk
----------------------------------------------------------------------------- *)
now apply VALID_PERIODS.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PeriodicTasksAsSporadicTasks.
We add the [periodic_task_respects_sporadic_task_model] lemma into a "Hint Database" basic_facts,
so Coq will be able to apply it automatically.