Library prosa.model.task.arrival.arrival_curve_to_rbf
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.util.all.
Require Export prosa.model.task.arrival.request_bound_functions.
Require Export prosa.model.task.arrival.curves.
Converting an Arrival Curve + Worst-Case/Best-Case to a Request-Bound Function (RBF)
... and any type of jobs associated with these tasks.
In the following, we show a way to convert a given arrival curve,
paired with a worst-case/best-case execution time, to a request-bound function.
Definitions and proofs will handle both lower-bounding and upper-bounding arrival
curves.
Let [MaxArr] and [MinArr] represent two arrivals curves. [MaxArr] upper-bounds
the possible number or arrivals for a given task, whereas [MinArr] lower-bounds it.
We define the conversion to a request-bound function as the product of the task cost and the
number of arrivals during [Δ]. In the upper-bounding case, the cost of a task will represent
the WCET of its jobs. Symmetrically, in the lower-bounding case, the cost of a task will
represent the BCET of its jobs.
Definition task_max_rbf (arrivals : Task → duration → nat) task Δ := task_cost task × arrivals task Δ.
Definition task_min_rbf (arrivals : Task → duration → nat) task Δ := task_min_cost task × arrivals task Δ.
Definition task_min_rbf (arrivals : Task → duration → nat) task Δ := task_min_cost task × arrivals task Δ.
Finally, we show that the newly defined functions are indeed request-bound functions.
Global Program Instance MaxArrivalsRBF : MaxRequestBound Task := task_max_rbf max_arrivals.
Global Program Instance MinArrivalsRBF : MinRequestBound Task := task_min_rbf min_arrivals.
Global Program Instance MinArrivalsRBF : MinRequestBound Task := task_min_rbf min_arrivals.
In the following section, we prove that the transformation yields a request-bound
function that conserves correctness properties in both the upper-bounding
and lower-bounding cases.
First, we establish the validity of the transformation for a single, given task.
Consider an arbitrary task [tsk] ...
... and any job arrival sequence.
First, note that any valid upper-bounding arrival curve, after being
converted, is a valid request-bound function.
Theorem valid_arrival_curve_to_max_rbf:
∀ (arrivals : Task → duration → nat),
valid_arrival_curve (arrivals tsk) →
valid_request_bound_function ((task_max_rbf arrivals) tsk).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 30)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
============================
forall arrivals : Task -> duration -> nat,
valid_arrival_curve (arrivals tsk) ->
valid_request_bound_function (task_max_rbf arrivals tsk)
----------------------------------------------------------------------------- *)
Proof.
move ⇒ ARR [ZERO MONO].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 42)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
============================
valid_request_bound_function (task_max_rbf ARR tsk)
----------------------------------------------------------------------------- *)
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 44)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
============================
task_max_rbf ARR tsk 0 = 0
subgoal 2 (ID 45) is:
monotone (task_max_rbf ARR tsk) leq
----------------------------------------------------------------------------- *)
- by rewrite /task_max_rbf ZERO muln0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
============================
monotone (task_max_rbf ARR tsk) leq
----------------------------------------------------------------------------- *)
- move ⇒ x y LEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 57)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
x, y : duration
LEQ : x <= y
============================
task_max_rbf ARR tsk x <= task_max_rbf ARR tsk y
----------------------------------------------------------------------------- *)
rewrite /task_max_rbf.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
x, y : duration
LEQ : x <= y
============================
task_cost tsk * ARR tsk x <= task_cost tsk * ARR tsk y
----------------------------------------------------------------------------- *)
destruct (task_cost tsk); first by rewrite mul0n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 69)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
x, y : duration
LEQ : x <= y
d : nat
============================
d.+1 * ARR tsk x <= d.+1 * ARR tsk y
----------------------------------------------------------------------------- *)
by rewrite leq_pmul2l //; apply MONO.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ (arrivals : Task → duration → nat),
valid_arrival_curve (arrivals tsk) →
valid_request_bound_function ((task_max_rbf arrivals) tsk).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 30)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
============================
forall arrivals : Task -> duration -> nat,
valid_arrival_curve (arrivals tsk) ->
valid_request_bound_function (task_max_rbf arrivals tsk)
----------------------------------------------------------------------------- *)
Proof.
move ⇒ ARR [ZERO MONO].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 42)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
============================
valid_request_bound_function (task_max_rbf ARR tsk)
----------------------------------------------------------------------------- *)
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 44)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
============================
task_max_rbf ARR tsk 0 = 0
subgoal 2 (ID 45) is:
monotone (task_max_rbf ARR tsk) leq
----------------------------------------------------------------------------- *)
- by rewrite /task_max_rbf ZERO muln0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
============================
monotone (task_max_rbf ARR tsk) leq
----------------------------------------------------------------------------- *)
- move ⇒ x y LEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 57)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
x, y : duration
LEQ : x <= y
============================
task_max_rbf ARR tsk x <= task_max_rbf ARR tsk y
----------------------------------------------------------------------------- *)
rewrite /task_max_rbf.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
x, y : duration
LEQ : x <= y
============================
task_cost tsk * ARR tsk x <= task_cost tsk * ARR tsk y
----------------------------------------------------------------------------- *)
destruct (task_cost tsk); first by rewrite mul0n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 69)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
x, y : duration
LEQ : x <= y
d : nat
============================
d.+1 * ARR tsk x <= d.+1 * ARR tsk y
----------------------------------------------------------------------------- *)
by rewrite leq_pmul2l //; apply MONO.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
The same idea can be applied in the lower-bounding case.
Theorem valid_arrival_curve_to_min_rbf:
∀ (arrivals : Task → duration → nat),
valid_arrival_curve (arrivals tsk) →
valid_request_bound_function ((task_min_rbf arrivals) tsk).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 31)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
============================
forall arrivals : Task -> duration -> nat,
valid_arrival_curve (arrivals tsk) ->
valid_request_bound_function (task_min_rbf arrivals tsk)
----------------------------------------------------------------------------- *)
Proof.
move ⇒ ARR [ZERO MONO].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
============================
valid_request_bound_function (task_min_rbf ARR tsk)
----------------------------------------------------------------------------- *)
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 45)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
============================
task_min_rbf ARR tsk 0 = 0
subgoal 2 (ID 46) is:
monotone (task_min_rbf ARR tsk) leq
----------------------------------------------------------------------------- *)
- by rewrite /task_min_rbf ZERO muln0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 46)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
============================
monotone (task_min_rbf ARR tsk) leq
----------------------------------------------------------------------------- *)
- move ⇒ x y LEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
x, y : duration
LEQ : x <= y
============================
task_min_rbf ARR tsk x <= task_min_rbf ARR tsk y
----------------------------------------------------------------------------- *)
rewrite /task_min_rbf.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
x, y : duration
LEQ : x <= y
============================
task_min_cost tsk * ARR tsk x <= task_min_cost tsk * ARR tsk y
----------------------------------------------------------------------------- *)
destruct (task_min_cost tsk); first by rewrite mul0n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 70)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
x, y : duration
LEQ : x <= y
d : nat
============================
d.+1 * ARR tsk x <= d.+1 * ARR tsk y
----------------------------------------------------------------------------- *)
by rewrite leq_pmul2l //; apply MONO.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ (arrivals : Task → duration → nat),
valid_arrival_curve (arrivals tsk) →
valid_request_bound_function ((task_min_rbf arrivals) tsk).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 31)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
============================
forall arrivals : Task -> duration -> nat,
valid_arrival_curve (arrivals tsk) ->
valid_request_bound_function (task_min_rbf arrivals tsk)
----------------------------------------------------------------------------- *)
Proof.
move ⇒ ARR [ZERO MONO].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
============================
valid_request_bound_function (task_min_rbf ARR tsk)
----------------------------------------------------------------------------- *)
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 45)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
============================
task_min_rbf ARR tsk 0 = 0
subgoal 2 (ID 46) is:
monotone (task_min_rbf ARR tsk) leq
----------------------------------------------------------------------------- *)
- by rewrite /task_min_rbf ZERO muln0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 46)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
============================
monotone (task_min_rbf ARR tsk) leq
----------------------------------------------------------------------------- *)
- move ⇒ x y LEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
x, y : duration
LEQ : x <= y
============================
task_min_rbf ARR tsk x <= task_min_rbf ARR tsk y
----------------------------------------------------------------------------- *)
rewrite /task_min_rbf.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
x, y : duration
LEQ : x <= y
============================
task_min_cost tsk * ARR tsk x <= task_min_cost tsk * ARR tsk y
----------------------------------------------------------------------------- *)
destruct (task_min_cost tsk); first by rewrite mul0n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 70)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
ARR : Task -> duration -> nat
ZERO : ARR tsk 0 = 0
MONO : monotone (ARR tsk) leq
x, y : duration
LEQ : x <= y
d : nat
============================
d.+1 * ARR tsk x <= d.+1 * ARR tsk y
----------------------------------------------------------------------------- *)
by rewrite leq_pmul2l //; apply MONO.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Next, we prove that the task respects the request-bound function in
the upper-bounding case. Note that, for this to work, we assume that the
cost of tasks upper-bounds the cost of the jobs belonging to them (i.e.,
the task cost is the worst-case).
Theorem respects_arrival_curve_to_max_rbf:
jobs_have_valid_job_costs →
respects_max_arrivals arr_seq tsk (MaxArr tsk) →
respects_max_request_bound arr_seq tsk ((task_max_rbf MaxArr) tsk).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 44)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
============================
jobs_have_valid_job_costs ->
respects_max_arrivals arr_seq tsk (MaxArr tsk) ->
respects_max_request_bound arr_seq tsk (task_max_rbf MaxArr tsk)
----------------------------------------------------------------------------- *)
Proof.
move⇒ TASK_COST RESPECT t1 t2 LEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
RESPECT : respects_max_arrivals arr_seq tsk (MaxArr tsk)
t1, t2 : instant
LEQ : t1 <= t2
============================
cost_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
----------------------------------------------------------------------------- *)
specialize (RESPECT t1 t2 LEQ).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 52)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
t1, t2 : instant
RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <= MaxArr tsk (t2 - t1)
LEQ : t1 <= t2
============================
cost_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
----------------------------------------------------------------------------- *)
apply leq_trans with (n := task_cost tsk × number_of_task_arrivals arr_seq tsk t1 t2) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 58)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
t1, t2 : instant
RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <= MaxArr tsk (t2 - t1)
LEQ : t1 <= t2
============================
cost_of_task_arrivals arr_seq tsk t1 t2 <=
task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2
subgoal 2 (ID 59) is:
task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
----------------------------------------------------------------------------- *)
- rewrite /max_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // ⇒ j.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 192)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
t1, t2 : instant
RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <= MaxArr tsk (t2 - t1)
LEQ : t1 <= t2
j : Job
============================
j \in task_arrivals_between arr_seq tsk t1 t2 ->
true -> job_cost j <= task_cost tsk
subgoal 2 (ID 59) is:
task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
----------------------------------------------------------------------------- *)
rewrite mem_filter ⇒ /andP [/eqP TSK _] _.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 269)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
t1, t2 : instant
RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <= MaxArr tsk (t2 - t1)
LEQ : t1 <= t2
j : Job
TSK : job_task j = tsk
============================
job_cost j <= task_cost tsk
subgoal 2 (ID 59) is:
task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
----------------------------------------------------------------------------- *)
rewrite -TSK.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 271)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
t1, t2 : instant
RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <= MaxArr tsk (t2 - t1)
LEQ : t1 <= t2
j : Job
TSK : job_task j = tsk
============================
job_cost j <= task_cost (job_task j)
subgoal 2 (ID 59) is:
task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
----------------------------------------------------------------------------- *)
by apply TASK_COST.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
t1, t2 : instant
RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <= MaxArr tsk (t2 - t1)
LEQ : t1 <= t2
============================
task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
----------------------------------------------------------------------------- *)
- by destruct (task_cost tsk) eqn:C; rewrite /task_max_rbf C // leq_pmul2l.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
jobs_have_valid_job_costs →
respects_max_arrivals arr_seq tsk (MaxArr tsk) →
respects_max_request_bound arr_seq tsk ((task_max_rbf MaxArr) tsk).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 44)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
============================
jobs_have_valid_job_costs ->
respects_max_arrivals arr_seq tsk (MaxArr tsk) ->
respects_max_request_bound arr_seq tsk (task_max_rbf MaxArr tsk)
----------------------------------------------------------------------------- *)
Proof.
move⇒ TASK_COST RESPECT t1 t2 LEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
RESPECT : respects_max_arrivals arr_seq tsk (MaxArr tsk)
t1, t2 : instant
LEQ : t1 <= t2
============================
cost_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
----------------------------------------------------------------------------- *)
specialize (RESPECT t1 t2 LEQ).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 52)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
t1, t2 : instant
RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <= MaxArr tsk (t2 - t1)
LEQ : t1 <= t2
============================
cost_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
----------------------------------------------------------------------------- *)
apply leq_trans with (n := task_cost tsk × number_of_task_arrivals arr_seq tsk t1 t2) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 58)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
t1, t2 : instant
RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <= MaxArr tsk (t2 - t1)
LEQ : t1 <= t2
============================
cost_of_task_arrivals arr_seq tsk t1 t2 <=
task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2
subgoal 2 (ID 59) is:
task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
----------------------------------------------------------------------------- *)
- rewrite /max_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // ⇒ j.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 192)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
t1, t2 : instant
RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <= MaxArr tsk (t2 - t1)
LEQ : t1 <= t2
j : Job
============================
j \in task_arrivals_between arr_seq tsk t1 t2 ->
true -> job_cost j <= task_cost tsk
subgoal 2 (ID 59) is:
task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
----------------------------------------------------------------------------- *)
rewrite mem_filter ⇒ /andP [/eqP TSK _] _.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 269)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
t1, t2 : instant
RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <= MaxArr tsk (t2 - t1)
LEQ : t1 <= t2
j : Job
TSK : job_task j = tsk
============================
job_cost j <= task_cost tsk
subgoal 2 (ID 59) is:
task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
----------------------------------------------------------------------------- *)
rewrite -TSK.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 271)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
t1, t2 : instant
RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <= MaxArr tsk (t2 - t1)
LEQ : t1 <= t2
j : Job
TSK : job_task j = tsk
============================
job_cost j <= task_cost (job_task j)
subgoal 2 (ID 59) is:
task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
----------------------------------------------------------------------------- *)
by apply TASK_COST.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
t1, t2 : instant
RESPECT : number_of_task_arrivals arr_seq tsk t1 t2 <= MaxArr tsk (t2 - t1)
LEQ : t1 <= t2
============================
task_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2 <=
task_max_rbf MaxArr tsk (t2 - t1)
----------------------------------------------------------------------------- *)
- by destruct (task_cost tsk) eqn:C; rewrite /task_max_rbf C // leq_pmul2l.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Finally, we prove that the task respects the request-bound function also in
the lower-bounding case. This time, we assume that the cost of tasks lower-bounds
the cost of the jobs belonging to them. (i.e., the task cost is the best-case).
Theorem respects_arrival_curve_to_min_rbf:
jobs_have_valid_min_job_costs →
respects_min_arrivals arr_seq tsk (MinArr tsk) →
respects_min_request_bound arr_seq tsk ((task_min_rbf MinArr) tsk).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 57)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
============================
jobs_have_valid_min_job_costs ->
respects_min_arrivals arr_seq tsk (MinArr tsk) ->
respects_min_request_bound arr_seq tsk (task_min_rbf MinArr tsk)
----------------------------------------------------------------------------- *)
Proof.
move⇒ TASK_COST RESPECT t1 t2 LEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 63)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
RESPECT : respects_min_arrivals arr_seq tsk (MinArr tsk)
t1, t2 : instant
LEQ : t1 <= t2
============================
task_min_rbf MinArr tsk (t2 - t1) <=
cost_of_task_arrivals arr_seq tsk t1 t2
----------------------------------------------------------------------------- *)
specialize (RESPECT t1 t2 LEQ).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 65)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
t1, t2 : instant
RESPECT : MinArr tsk (t2 - t1) <= number_of_task_arrivals arr_seq tsk t1 t2
LEQ : t1 <= t2
============================
task_min_rbf MinArr tsk (t2 - t1) <=
cost_of_task_arrivals arr_seq tsk t1 t2
----------------------------------------------------------------------------- *)
apply leq_trans with (n := task_min_cost tsk × number_of_task_arrivals arr_seq tsk t1 t2) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 71)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
t1, t2 : instant
RESPECT : MinArr tsk (t2 - t1) <= number_of_task_arrivals arr_seq tsk t1 t2
LEQ : t1 <= t2
============================
task_min_rbf MinArr tsk (t2 - t1) <=
task_min_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2
subgoal 2 (ID 72) is:
task_min_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2 <=
cost_of_task_arrivals arr_seq tsk t1 t2
----------------------------------------------------------------------------- *)
- by destruct (task_min_cost tsk) eqn:C; rewrite /task_min_rbf C // leq_pmul2l.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 72)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
t1, t2 : instant
RESPECT : MinArr tsk (t2 - t1) <= number_of_task_arrivals arr_seq tsk t1 t2
LEQ : t1 <= t2
============================
task_min_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2 <=
cost_of_task_arrivals arr_seq tsk t1 t2
----------------------------------------------------------------------------- *)
- rewrite /min_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // ⇒ j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 255)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
t1, t2 : instant
RESPECT : MinArr tsk (t2 - t1) <= number_of_task_arrivals arr_seq tsk t1 t2
LEQ : t1 <= t2
j : Job
============================
j \in task_arrivals_between arr_seq tsk t1 t2 ->
true -> task_min_cost tsk <= job_cost j
----------------------------------------------------------------------------- *)
rewrite mem_filter ⇒ /andP [/eqP TSK _] _.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 332)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
t1, t2 : instant
RESPECT : MinArr tsk (t2 - t1) <= number_of_task_arrivals arr_seq tsk t1 t2
LEQ : t1 <= t2
j : Job
TSK : job_task j = tsk
============================
task_min_cost tsk <= job_cost j
----------------------------------------------------------------------------- *)
rewrite -TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 334)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
t1, t2 : instant
RESPECT : MinArr tsk (t2 - t1) <= number_of_task_arrivals arr_seq tsk t1 t2
LEQ : t1 <= t2
j : Job
TSK : job_task j = tsk
============================
task_min_cost (job_task j) <= job_cost j
----------------------------------------------------------------------------- *)
by apply TASK_COST.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End SingleTask.
jobs_have_valid_min_job_costs →
respects_min_arrivals arr_seq tsk (MinArr tsk) →
respects_min_request_bound arr_seq tsk ((task_min_rbf MinArr) tsk).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 57)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
============================
jobs_have_valid_min_job_costs ->
respects_min_arrivals arr_seq tsk (MinArr tsk) ->
respects_min_request_bound arr_seq tsk (task_min_rbf MinArr tsk)
----------------------------------------------------------------------------- *)
Proof.
move⇒ TASK_COST RESPECT t1 t2 LEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 63)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
RESPECT : respects_min_arrivals arr_seq tsk (MinArr tsk)
t1, t2 : instant
LEQ : t1 <= t2
============================
task_min_rbf MinArr tsk (t2 - t1) <=
cost_of_task_arrivals arr_seq tsk t1 t2
----------------------------------------------------------------------------- *)
specialize (RESPECT t1 t2 LEQ).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 65)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
t1, t2 : instant
RESPECT : MinArr tsk (t2 - t1) <= number_of_task_arrivals arr_seq tsk t1 t2
LEQ : t1 <= t2
============================
task_min_rbf MinArr tsk (t2 - t1) <=
cost_of_task_arrivals arr_seq tsk t1 t2
----------------------------------------------------------------------------- *)
apply leq_trans with (n := task_min_cost tsk × number_of_task_arrivals arr_seq tsk t1 t2) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 71)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
t1, t2 : instant
RESPECT : MinArr tsk (t2 - t1) <= number_of_task_arrivals arr_seq tsk t1 t2
LEQ : t1 <= t2
============================
task_min_rbf MinArr tsk (t2 - t1) <=
task_min_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2
subgoal 2 (ID 72) is:
task_min_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2 <=
cost_of_task_arrivals arr_seq tsk t1 t2
----------------------------------------------------------------------------- *)
- by destruct (task_min_cost tsk) eqn:C; rewrite /task_min_rbf C // leq_pmul2l.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 72)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
t1, t2 : instant
RESPECT : MinArr tsk (t2 - t1) <= number_of_task_arrivals arr_seq tsk t1 t2
LEQ : t1 <= t2
============================
task_min_cost tsk * number_of_task_arrivals arr_seq tsk t1 t2 <=
cost_of_task_arrivals arr_seq tsk t1 t2
----------------------------------------------------------------------------- *)
- rewrite /min_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // ⇒ j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 255)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
t1, t2 : instant
RESPECT : MinArr tsk (t2 - t1) <= number_of_task_arrivals arr_seq tsk t1 t2
LEQ : t1 <= t2
j : Job
============================
j \in task_arrivals_between arr_seq tsk t1 t2 ->
true -> task_min_cost tsk <= job_cost j
----------------------------------------------------------------------------- *)
rewrite mem_filter ⇒ /andP [/eqP TSK _] _.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 332)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
t1, t2 : instant
RESPECT : MinArr tsk (t2 - t1) <= number_of_task_arrivals arr_seq tsk t1 t2
LEQ : t1 <= t2
j : Job
TSK : job_task j = tsk
============================
task_min_cost tsk <= job_cost j
----------------------------------------------------------------------------- *)
rewrite -TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 334)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
tsk : Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
t1, t2 : instant
RESPECT : MinArr tsk (t2 - t1) <= number_of_task_arrivals arr_seq tsk t1 t2
LEQ : t1 <= t2
j : Job
TSK : job_task j = tsk
============================
task_min_cost (job_task j) <= job_cost j
----------------------------------------------------------------------------- *)
by apply TASK_COST.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End SingleTask.
Next, we lift the results to the previous section to an arbitrary task set.
Let [ts] be an arbitrary task set...
... and consider any job arrival sequence.
First, we generalize the validity of the transformation to a task set both in
the upper-bounding case ...
Corollary valid_taskset_arrival_curve_to_max_rbf:
valid_taskset_arrival_curve ts MaxArr →
valid_taskset_request_bound_function ts MaxArrivalsRBF.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 32)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
============================
valid_taskset_arrival_curve ts MaxArr ->
valid_taskset_request_bound_function ts MaxArrivalsRBF
----------------------------------------------------------------------------- *)
Proof.
move⇒ VALID tsk IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 36)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
VALID : valid_taskset_arrival_curve ts MaxArr
tsk : Task
IN : tsk \in ts
============================
valid_request_bound_function (MaxArrivalsRBF tsk)
----------------------------------------------------------------------------- *)
specialize (VALID tsk IN).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 38)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
tsk : Task
VALID : valid_arrival_curve (MaxArr tsk)
IN : tsk \in ts
============================
valid_request_bound_function (MaxArrivalsRBF tsk)
----------------------------------------------------------------------------- *)
by apply valid_arrival_curve_to_max_rbf.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
valid_taskset_arrival_curve ts MaxArr →
valid_taskset_request_bound_function ts MaxArrivalsRBF.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 32)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
============================
valid_taskset_arrival_curve ts MaxArr ->
valid_taskset_request_bound_function ts MaxArrivalsRBF
----------------------------------------------------------------------------- *)
Proof.
move⇒ VALID tsk IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 36)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
VALID : valid_taskset_arrival_curve ts MaxArr
tsk : Task
IN : tsk \in ts
============================
valid_request_bound_function (MaxArrivalsRBF tsk)
----------------------------------------------------------------------------- *)
specialize (VALID tsk IN).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 38)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
tsk : Task
VALID : valid_arrival_curve (MaxArr tsk)
IN : tsk \in ts
============================
valid_request_bound_function (MaxArrivalsRBF tsk)
----------------------------------------------------------------------------- *)
by apply valid_arrival_curve_to_max_rbf.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
... and in the lower-bounding case.
Corollary valid_taskset_arrival_curve_to_min_rbf:
valid_taskset_arrival_curve ts MinArr →
valid_taskset_request_bound_function ts MinArrivalsRBF.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 35)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
============================
valid_taskset_arrival_curve ts MinArr ->
valid_taskset_request_bound_function ts MinArrivalsRBF
----------------------------------------------------------------------------- *)
Proof.
move⇒ VALID tsk IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 39)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
VALID : valid_taskset_arrival_curve ts MinArr
tsk : Task
IN : tsk \in ts
============================
valid_request_bound_function (MinArrivalsRBF tsk)
----------------------------------------------------------------------------- *)
specialize (VALID tsk IN).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 41)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
tsk : Task
VALID : valid_arrival_curve (MinArr tsk)
IN : tsk \in ts
============================
valid_request_bound_function (MinArrivalsRBF tsk)
----------------------------------------------------------------------------- *)
by apply valid_arrival_curve_to_min_rbf.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
valid_taskset_arrival_curve ts MinArr →
valid_taskset_request_bound_function ts MinArrivalsRBF.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 35)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
============================
valid_taskset_arrival_curve ts MinArr ->
valid_taskset_request_bound_function ts MinArrivalsRBF
----------------------------------------------------------------------------- *)
Proof.
move⇒ VALID tsk IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 39)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
VALID : valid_taskset_arrival_curve ts MinArr
tsk : Task
IN : tsk \in ts
============================
valid_request_bound_function (MinArrivalsRBF tsk)
----------------------------------------------------------------------------- *)
specialize (VALID tsk IN).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 41)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
tsk : Task
VALID : valid_arrival_curve (MinArr tsk)
IN : tsk \in ts
============================
valid_request_bound_function (MinArrivalsRBF tsk)
----------------------------------------------------------------------------- *)
by apply valid_arrival_curve_to_min_rbf.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Second, we show that a task set that respects a given arrival curve also respects
the produced request-bound function, lifting the result obtained in the single-task
case. The result is valid in the upper-bounding case...
Corollary taskset_respects_arrival_curve_to_max_rbf:
jobs_have_valid_job_costs →
taskset_respects_max_arrivals arr_seq ts →
taskset_respects_max_request_bound arr_seq ts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
============================
jobs_have_valid_job_costs ->
taskset_respects_max_arrivals arr_seq ts ->
taskset_respects_max_request_bound arr_seq ts
----------------------------------------------------------------------------- *)
Proof.
move⇒ TASK_COST SET_RESPECTS tsk IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 55)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
SET_RESPECTS : taskset_respects_max_arrivals arr_seq ts
tsk : Task
IN : tsk \in ts
============================
respects_max_request_bound arr_seq tsk (max_request_bound tsk)
----------------------------------------------------------------------------- *)
by apply respects_arrival_curve_to_max_rbf, SET_RESPECTS.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
jobs_have_valid_job_costs →
taskset_respects_max_arrivals arr_seq ts →
taskset_respects_max_request_bound arr_seq ts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
============================
jobs_have_valid_job_costs ->
taskset_respects_max_arrivals arr_seq ts ->
taskset_respects_max_request_bound arr_seq ts
----------------------------------------------------------------------------- *)
Proof.
move⇒ TASK_COST SET_RESPECTS tsk IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 55)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_job_costs
SET_RESPECTS : taskset_respects_max_arrivals arr_seq ts
tsk : Task
IN : tsk \in ts
============================
respects_max_request_bound arr_seq tsk (max_request_bound tsk)
----------------------------------------------------------------------------- *)
by apply respects_arrival_curve_to_max_rbf, SET_RESPECTS.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
...as well as in the lower-bounding case.
Corollary taskset_respects_arrival_curve_to_min_rbf:
jobs_have_valid_min_job_costs →
taskset_respects_min_arrivals arr_seq ts →
taskset_respects_min_request_bound arr_seq ts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 65)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
============================
jobs_have_valid_min_job_costs ->
taskset_respects_min_arrivals arr_seq ts ->
taskset_respects_min_request_bound arr_seq ts
----------------------------------------------------------------------------- *)
Proof.
move⇒ TASK_COST SET_RESPECTS tsk IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 70)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
SET_RESPECTS : taskset_respects_min_arrivals arr_seq ts
tsk : Task
IN : tsk \in ts
============================
respects_min_request_bound arr_seq tsk (min_request_bound tsk)
----------------------------------------------------------------------------- *)
by apply respects_arrival_curve_to_min_rbf, SET_RESPECTS.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TaskSet.
End Facts.
End ArrivalCurveToRBF.
jobs_have_valid_min_job_costs →
taskset_respects_min_arrivals arr_seq ts →
taskset_respects_min_request_bound arr_seq ts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 65)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
============================
jobs_have_valid_min_job_costs ->
taskset_respects_min_arrivals arr_seq ts ->
taskset_respects_min_request_bound arr_seq ts
----------------------------------------------------------------------------- *)
Proof.
move⇒ TASK_COST SET_RESPECTS tsk IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 70)
MaxArr : MaxArrivals Task
MinArr : MinArrivals Task
ts : TaskSet Task
arr_seq : arrival_sequence Job
TASK_COST : jobs_have_valid_min_job_costs
SET_RESPECTS : taskset_respects_min_arrivals arr_seq ts
tsk : Task
IN : tsk \in ts
============================
respects_min_request_bound arr_seq tsk (min_request_bound tsk)
----------------------------------------------------------------------------- *)
by apply respects_arrival_curve_to_min_rbf, SET_RESPECTS.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TaskSet.
End Facts.
End ArrivalCurveToRBF.