Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
(** * Converting an Arrival Curve + Worst-Case/Best-Case to a Request-Bound Function (RBF) *) (** 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. *) Section ArrivalCurveToRBF. (** Consider any type of tasks with a given cost ... *) Context {Task : TaskType} `{TaskCost Task} `{TaskMinCost Task}. (** ... and any type of jobs associated with these tasks. *) Context {Job : JobType} `{JobTask Job Task} `{JobCost Job}. (** 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. *) Context `{MaxArr : MaxArrivals Task} `{MinArr : MinArrivals Task}. (** 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 Δ. (** 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. (** 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. *) Section Facts. (** First, we establish the validity of the transformation for a single, given task. *) Section SingleTask. (** Consider an arbitrary task [tsk] ... *) Variable tsk : Task. (** ... and any job arrival sequence. *) Variable arr_seq : arrival_sequence Job. (** First, note that any valid upper-bounding arrival curve, after being converted, is a valid request-bound function. *)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)

valid_request_bound_function (task_max_rbf ARR tsk)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)

task_max_rbf ARR tsk 0 = 0
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)
monotone leq (task_max_rbf ARR tsk)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)

task_max_rbf ARR tsk 0 = 0
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)
monotone leq (task_max_rbf ARR tsk)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)

monotone leq (task_max_rbf ARR tsk)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)

monotone leq (task_max_rbf ARR tsk)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)
x, y: nat
LEQ: x <= y

task_max_rbf ARR tsk x <= task_max_rbf ARR tsk y
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)
x, y: nat
LEQ: x <= y

task_cost tsk * ARR tsk x <= task_cost tsk * ARR tsk y
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)
x, y: nat
LEQ: x <= y
d: nat

d.+1 * ARR tsk x <= d.+1 * ARR tsk y
by rewrite leq_pmul2l //; apply MONO. Qed. (** The same idea can be applied in the lower-bounding case. *)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)

valid_request_bound_function (task_min_rbf ARR tsk)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)

task_min_rbf ARR tsk 0 = 0
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)
monotone leq (task_min_rbf ARR tsk)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)

task_min_rbf ARR tsk 0 = 0
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)
monotone leq (task_min_rbf ARR tsk)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)

monotone leq (task_min_rbf ARR tsk)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)

monotone leq (task_min_rbf ARR tsk)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)
x, y: nat
LEQ: x <= y

task_min_rbf ARR tsk x <= task_min_rbf ARR tsk y
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)
x, y: nat
LEQ: x <= y

task_min_cost tsk * ARR tsk x <= task_min_cost tsk * ARR tsk y
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
MaxArr: MaxArrivals Task
MinArr: MinArrivals Task
tsk: Task
arr_seq: arrival_sequence Job
ARR: Task -> duration -> nat
ZERO: ARR tsk 0 = 0
MONO: monotone leq (ARR tsk)
x, y: nat
LEQ: x <= y
d: nat

d.+1 * ARR tsk x <= d.+1 * ARR tsk y
by rewrite leq_pmul2l //; apply MONO. 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). *)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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. 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). *)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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. Qed. End SingleTask. (** Next, we lift the results to the previous section to an arbitrary task set. *) Section TaskSet. (** Let [ts] be an arbitrary task set... *) Variable ts : TaskSet Task. (** ... and consider any job arrival sequence. *) Variable arr_seq : arrival_sequence Job. (** First, we generalize the validity of the transformation to a task set both in the upper-bounding case ... *)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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. Qed. (** ... and in the lower-bounding case. *)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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. 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... *)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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. Qed. (** ...as well as in the lower-bounding case. *)
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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
Task: TaskType
H: TaskCost Task
H0: TaskMinCost Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
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. Qed. End TaskSet. End Facts. End ArrivalCurveToRBF.