Require Export prosa.util.all.
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]
Require Export prosa.model.task.arrival.request_bound_functions.
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]
Require Export prosa.model.task.arrival.curves.
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. *)
      Theorem valid_arrival_curve_to_max_rbf:
        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)
      Proof.
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)
        move => ARR [ZERO MONO].
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)
        split.
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) by rewrite /task_max_rbf ZERO muln0.
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) move => x y LEQ.
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
          rewrite /task_max_rbf.
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
          destruct (task_cost tsk); first by rewrite mul0n.
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. *)
      Theorem valid_arrival_curve_to_min_rbf:
        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)
      Proof.
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)
        move => ARR [ZERO MONO].
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)
        split.
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) by rewrite /task_min_rbf ZERO muln0.
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) move => x y LEQ.
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
          rewrite /task_min_rbf.
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
          destruct (task_min_cost tsk); first by rewrite mul0n.
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). *)
      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).
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)
      Proof.
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)
        move=> TASK_COST RESPECT t1 t2 LEQ.
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)
        specialize (RESPECT t1 t2 LEQ).
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)
        apply leq_trans with (n := 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
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) rewrite /max_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // => 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
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)
          rewrite mem_filter => /andP [/eqP 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
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)
          rewrite -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
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)
          by apply TASK_COST.
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). *)
      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).
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)
      Proof.
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)
        move=> TASK_COST RESPECT t1 t2 LEQ.
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
        specialize (RESPECT t1 t2 LEQ).
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
        apply leq_trans with (n := 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_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 by destruct (task_min_cost tsk) eqn:C; rewrite /task_min_rbf C // leq_pmul2l.
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 rewrite /min_arrivals /number_of_task_arrivals -sum1_size big_distrr //= muln1 leq_sum_seq // => 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
j \in task_arrivals_between arr_seq tsk t1 t2 ->
true -> task_min_cost tsk <= job_cost j
          rewrite mem_filter => /andP [/eqP 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
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.
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 ... *)
      Corollary valid_taskset_arrival_curve_to_max_rbf:
        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
      Proof.
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
        move=> VALID tsk IN.
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)
        specialize (VALID tsk IN).
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. *)
      Corollary valid_taskset_arrival_curve_to_min_rbf:
        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
      Proof.
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
        move=> VALID tsk IN.
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)
        specialize (VALID tsk IN).
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... *) 
      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.
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
      Proof.
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
        move=> TASK_COST SET_RESPECTS tsk IN.
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. *)
      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.
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
      Proof.
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
        move=> TASK_COST SET_RESPECTS tsk IN.
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.

(** We add the lemmas into the "Hint Database" basic_rt_facts so that
    they become available for proof automation. *)
Global Hint Resolve
  valid_arrival_curve_to_max_rbf
  respects_arrival_curve_to_max_rbf
  valid_taskset_arrival_curve_to_max_rbf
  taskset_respects_arrival_curve_to_max_rbf
  : basic_rt_facts.