Library rt.restructuring.analysis.arrival.rbf

From rt.util Require Import all.
From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Import job task.
From rt.restructuring.model.aggregate Require Import task_arrivals.
From rt.restructuring.model.arrival Require Import arrival_curves.
From rt.restructuring.analysis Require Import arrival.workload_bound.

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

Request Bound Functions (RBF)

In this section, we prove some properties of Request Bound Functions (RBF).
Section RequestBoundFunctions.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent:
    consistent_arrival_times arr_seq.

Let tsk be any task.
  Variable tsk : Task.

Let max_arrivals be a family of valid arrival curves, i.e., for any task tsk in ts max_arrival tsk is (1) an arrival bound of tsk, and (2) it is a monotonic function that equals 0 for the empty interval delta = 0.
  Context `{MaxArrivals Task}.
  Hypothesis H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk).
  Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).

Let's define some local names for clarity.
  Let task_rbf := task_request_bound_function tsk.

We prove that task_rbf 0 is equal to 0.
  Lemma task_rbf_0_zero:
    task_rbf 0 = 0.

We prove that task_rbf is monotone.
  Lemma task_rbf_monotone:
    monotone task_rbf leq.

Consider any job j of tsk. This guarantees that there exists at least one job of task tsk.
  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.
  Hypothesis H_job_of_tsk : job_task j = tsk.

Then we prove that task_rbf 1 is greater than or equal to task cost.
  Lemma task_rbf_1_ge_task_cost:
    task_rbf 1 ≥ task_cost tsk.

End RequestBoundFunctions.