Library prosa.analysis.facts.shifted_job_costs
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.periodic.arrival_times.
Require Export prosa.analysis.facts.periodic.task_arrivals_size.
Require Export prosa.model.task.concept.
Require Export prosa.analysis.facts.hyperperiod.
In this file we define a new function for job costs
in an observation interval and prove its validity.
Consider any type of periodic tasks ...
Context {Task : TaskType}.
Context `{TaskOffset Task}.
Context `{PeriodicModel Task}.
Context `{TaskCost Task}.
Context `{TaskOffset Task}.
Context `{PeriodicModel Task}.
Context `{TaskCost Task}.
... and any type of jobs.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobDeadline Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobDeadline Job}.
Consider a consistent arrival sequence with non-duplicate arrivals.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
Furthermore, assume that arrivals have valid job costs.
Consider a periodic task set [ts] such that all tasks in
[ts] have valid periods and offsets.
Variable ts : TaskSet Task.
Hypothesis H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts.
Hypothesis H_valid_periods_in_taskset: valid_periods ts.
Hypothesis H_valid_offsets_in_taskset: valid_offsets arr_seq ts.
Hypothesis H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts.
Hypothesis H_valid_periods_in_taskset: valid_periods ts.
Hypothesis H_valid_offsets_in_taskset: valid_offsets arr_seq ts.
Consider a job [j] that stems from the arrival sequence.
Let [O_max] denote the maximum task offset of all tasks in [ts] ...
... and let [HP] denote the hyperperiod of all tasks in [ts].
We now define a new function for job costs in the observation interval.
Given that job [j] arrives after [O_max], the cost of a job [j']
that arrives in the interval
[O_max + HP, O_max + 2HP)
is defined to
be the same as the job cost of its corresponding job in [j]'s hyperperiod.
Definition job_costs_shifted (j' : Job) :=
if (job_arrival j ≥ O_max) && (O_max + HP ≤ job_arrival j' < O_max + 2 × HP) then
job_cost (corresponding_job_in_hyperperiod ts arr_seq j' (starting_instant_of_corresponding_hyperperiod ts j) (job_task j'))
else job_cost j'.
if (job_arrival j ≥ O_max) && (O_max + HP ≤ job_arrival j' < O_max + 2 × HP) then
job_cost (corresponding_job_in_hyperperiod ts arr_seq j' (starting_instant_of_corresponding_hyperperiod ts j) (job_task j'))
else job_cost j'.
Assume that we have an infinite sequence of jobs.
Assume all jobs in the arrival sequence [arr_seq] belong to some task
in [ts].
We assign the job costs as defined by the [job_costs_shifted] function.
We show that the [job_costs_shifted] function is valid.
Lemma job_costs_shifted_valid: arrivals_have_valid_job_costs arr_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
============================
arrivals_have_valid_job_costs arr_seq
----------------------------------------------------------------------------- *)
Proof.
rewrite /arrivals_have_valid_job_costs /valid_job_cost.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 102)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
============================
forall j0 : Job,
arrives_in arr_seq j0 -> job_cost j0 <= task_cost (job_task j0)
----------------------------------------------------------------------------- *)
intros j' ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 104)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
============================
job_cost j' <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
unfold job_cost; rewrite /job_costs_in_oi /job_costs_shifted.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 107)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
============================
(if
[&& O_max <= job_arrival j, O_max + HP <= job_arrival j'
& job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
destruct (leqP O_max (job_arrival j)) as [A | B].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 164)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
============================
(if
[&& true, O_max + HP <= job_arrival j' & job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
subgoal 2 (ID 165) is:
(if
[&& false, O_max + HP <= job_arrival j' & job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
destruct (leqP (O_max + HP) (job_arrival j')) as [NEQ | NEQ].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 222)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
============================
(if [&& true, true & job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
subgoal 2 (ID 223) is:
(if [&& true, false & job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
subgoal 3 (ID 165) is:
(if
[&& false, O_max + HP <= job_arrival j' & job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
destruct (leqP (O_max + 2 × HP) (job_arrival j')) as [LT | LT].
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 280)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : O_max + 2 * HP <= job_arrival j'
============================
(if [&& true, true & false]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
subgoal 2 (ID 281) is:
(if [&& true, true & true]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
subgoal 3 (ID 223) is:
(if [&& true, false & job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
subgoal 4 (ID 165) is:
(if
[&& false, O_max + HP <= job_arrival j' & job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
all : try by apply H_arrivals_have_valid_job_costs ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 281)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
============================
(if [&& true, true & true]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
simpl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 285)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
============================
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
specialize (corresponding_jobs_have_same_task arr_seq ts j' j) ⇒ TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 294)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
TSK : job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) = job_task j'
============================
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
rewrite -[in X in _ ≤ task_cost X]TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 307)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
TSK : job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) = job_task j'
============================
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) <=
task_cost
(job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')))
----------------------------------------------------------------------------- *)
have IN : job_task j' \in ts by apply H_jobs_from_taskset.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 318)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
TSK : job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) = job_task j'
IN : job_task j' \in ts
============================
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) <=
task_cost
(job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')))
----------------------------------------------------------------------------- *)
apply H_arrivals_have_valid_job_costs, corresponding_job_arrives ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 330)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
TSK : job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) = job_task j'
IN : job_task j' \in ts
============================
valid_offset arr_seq (job_task j')
subgoal 2 (ID 331) is:
valid_period (job_task j')
subgoal 3 (ID 332) is:
respects_periodic_task_model arr_seq (job_task j')
subgoal 4 (ID 336) is:
max_task_offset ts <= job_arrival j'
----------------------------------------------------------------------------- *)
+ now apply H_valid_offsets_in_taskset.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 331)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
TSK : job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) = job_task j'
IN : job_task j' \in ts
============================
valid_period (job_task j')
subgoal 2 (ID 332) is:
respects_periodic_task_model arr_seq (job_task j')
subgoal 3 (ID 336) is:
max_task_offset ts <= job_arrival j'
----------------------------------------------------------------------------- *)
+ now apply H_valid_periods_in_taskset.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 332)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
TSK : job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) = job_task j'
IN : job_task j' \in ts
============================
respects_periodic_task_model arr_seq (job_task j')
subgoal 2 (ID 336) is:
max_task_offset ts <= job_arrival j'
----------------------------------------------------------------------------- *)
+ now apply H_periodic_taskset.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 336)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
TSK : job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) = job_task j'
IN : job_task j' \in ts
============================
max_task_offset ts <= job_arrival j'
----------------------------------------------------------------------------- *)
+ now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ValidJobCostsShifted.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
============================
arrivals_have_valid_job_costs arr_seq
----------------------------------------------------------------------------- *)
Proof.
rewrite /arrivals_have_valid_job_costs /valid_job_cost.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 102)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
============================
forall j0 : Job,
arrives_in arr_seq j0 -> job_cost j0 <= task_cost (job_task j0)
----------------------------------------------------------------------------- *)
intros j' ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 104)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
============================
job_cost j' <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
unfold job_cost; rewrite /job_costs_in_oi /job_costs_shifted.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 107)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
============================
(if
[&& O_max <= job_arrival j, O_max + HP <= job_arrival j'
& job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
destruct (leqP O_max (job_arrival j)) as [A | B].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 164)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
============================
(if
[&& true, O_max + HP <= job_arrival j' & job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
subgoal 2 (ID 165) is:
(if
[&& false, O_max + HP <= job_arrival j' & job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
destruct (leqP (O_max + HP) (job_arrival j')) as [NEQ | NEQ].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 222)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
============================
(if [&& true, true & job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
subgoal 2 (ID 223) is:
(if [&& true, false & job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
subgoal 3 (ID 165) is:
(if
[&& false, O_max + HP <= job_arrival j' & job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
destruct (leqP (O_max + 2 × HP) (job_arrival j')) as [LT | LT].
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 280)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : O_max + 2 * HP <= job_arrival j'
============================
(if [&& true, true & false]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
subgoal 2 (ID 281) is:
(if [&& true, true & true]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
subgoal 3 (ID 223) is:
(if [&& true, false & job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
subgoal 4 (ID 165) is:
(if
[&& false, O_max + HP <= job_arrival j' & job_arrival j' < O_max + 2 * HP]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
all : try by apply H_arrivals_have_valid_job_costs ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 281)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
============================
(if [&& true, true & true]
then
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j'))
else job_cost j') <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
simpl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 285)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
============================
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
specialize (corresponding_jobs_have_same_task arr_seq ts j' j) ⇒ TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 294)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
TSK : job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) = job_task j'
============================
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) <= task_cost (job_task j')
----------------------------------------------------------------------------- *)
rewrite -[in X in _ ≤ task_cost X]TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 307)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
TSK : job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) = job_task j'
============================
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) <=
task_cost
(job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')))
----------------------------------------------------------------------------- *)
have IN : job_task j' \in ts by apply H_jobs_from_taskset.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 318)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
TSK : job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) = job_task j'
IN : job_task j' \in ts
============================
job_cost
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) <=
task_cost
(job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')))
----------------------------------------------------------------------------- *)
apply H_arrivals_have_valid_job_costs, corresponding_job_arrives ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 330)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
TSK : job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) = job_task j'
IN : job_task j' \in ts
============================
valid_offset arr_seq (job_task j')
subgoal 2 (ID 331) is:
valid_period (job_task j')
subgoal 3 (ID 332) is:
respects_periodic_task_model arr_seq (job_task j')
subgoal 4 (ID 336) is:
max_task_offset ts <= job_arrival j'
----------------------------------------------------------------------------- *)
+ now apply H_valid_offsets_in_taskset.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 331)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
TSK : job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) = job_task j'
IN : job_task j' \in ts
============================
valid_period (job_task j')
subgoal 2 (ID 332) is:
respects_periodic_task_model arr_seq (job_task j')
subgoal 3 (ID 336) is:
max_task_offset ts <= job_arrival j'
----------------------------------------------------------------------------- *)
+ now apply H_valid_periods_in_taskset.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 332)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
TSK : job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) = job_task j'
IN : job_task j' \in ts
============================
respects_periodic_task_model arr_seq (job_task j')
subgoal 2 (ID 336) is:
max_task_offset ts <= job_arrival j'
----------------------------------------------------------------------------- *)
+ now apply H_periodic_taskset.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 336)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
H1 : TaskCost Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
H4 : JobCost Job
H5 : JobDeadline Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
ts : TaskSet Task
H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
H_valid_periods_in_taskset : valid_periods ts
H_valid_offsets_in_taskset : valid_offsets arr_seq ts
j : Job
H_j_from_arrival_sequence : arrives_in arr_seq j
O_max := max_task_offset ts : nat
HP := hyperperiod ts : duration
H_infinite_jobs : infinite_jobs arr_seq
H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
j' : Job
ARR : arrives_in arr_seq j'
A : O_max <= job_arrival j
NEQ : O_max + HP <= job_arrival j'
LT : job_arrival j' < O_max + 2 * HP
TSK : job_task
(corresponding_job_in_hyperperiod ts arr_seq j'
(starting_instant_of_corresponding_hyperperiod ts j)
(job_task j')) = job_task j'
IN : job_task j' \in ts
============================
max_task_offset ts <= job_arrival j'
----------------------------------------------------------------------------- *)
+ now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ValidJobCostsShifted.