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)

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}.

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.
  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.
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:
         (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.
        moveARR [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

----------------------------------------------------------------------------- *)


        - movex 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.
        moveARR [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

----------------------------------------------------------------------------- *)


        - movex 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.
        moveTASK_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.
        moveTASK_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.
    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.

(* ----------------------------------[ 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.
        moveVALID 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.
        moveVALID 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.
        moveTASK_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.
        moveTASK_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.