Library prosa.implementation.definitions.extrapolated_arrival_curve

From mathcomp Require Export ssreflect ssrbool eqtype ssrnat div seq path fintype bigop.
Require Export prosa.behavior.time.
Require Export prosa.util.all.

This file introduces an implementation of arrival curves via the periodic extension of finite arrival-curve prefix. An arrival-curve prefix is a pair comprising a horizon and a list of steps. The horizon defines the domain of the prefix, in which no extrapolation is necessary. The list of steps (duration × value) describes the value changes of the corresponding arrival curve within the domain.
For time instances outside of an arrival-curve prefix's domain, extrapolation is necessary. Therefore, past the domain, arrival-curve values are extrapolated assuming that the arrival-curve prefix is repeated with a period equal to the horizon.
Note that such a periodic extension does not necessarily give the tightest curve, and hence it is not optimal. The advantage is speed of calculation: periodic extension can be done in constant time, whereas the optimal extension takes roughly quadratic time in the number of steps.
An arrival-curve prefix is defined as a pair comprised of a horizon and a list of steps (duration × value) that describe the value changes of the described arrival curve.
For example, an arrival-curve prefix (5, [:: (1, 3)]) describes an arrival sequence with job bursts of size 3 happening every 5 time instances.
Definition ArrivalCurvePrefix : Type := duration × seq (duration × nat).

Given an inter-arrival time p (or period p), the corresponding arrival-curve prefix can be defined as (p, [:: (1, 1)]).
The first component of arrival-curve prefix ac_prefix is called horizon.
The second component of ac_prefix is called steps.
The time steps of ac_prefix are the first components of the steps. That is, these are time instances before the horizon where the corresponding arrival curve makes a step.
The function step_at returns the last step (duration × value) such that duration t.
Definition step_at (ac_prefix : ArrivalCurvePrefix) (t : duration) :=
  last (0, 0) [ seq step <- steps_of ac_prefix | fst step t ].

(* The function value_at returns the _value_ of the last step
   (duration × value) such that duration t *)

Definition value_at (ac_prefix : ArrivalCurvePrefix) (t : duration) :=
  snd (step_at ac_prefix t).

Finally, we define a function extrapolated_arrival_curve that performs the periodic extension of the arrival-curve prefix (and hence, defines an arrival curve).
Value of extrapolated_arrival_curve t is defined as t %/ h × value_at horizon plus value_at (t mod horizon). The first summand corresponds to k full repetitions of the arrival-curve prefix inside interval [0,t). The second summand corresponds to the residual change inside interval [k*h, t).
In the following section, we define a few validity predicates.
Horizon should be positive.
Horizon should bound time steps.
We define an alternative, decidable version of large_horizon...
... and prove that the two definitions are equivalent.
  Lemma large_horizon_P :
     (ac_prefix : ArrivalCurvePrefix),
      reflect (large_horizon ac_prefix) (large_horizon_dec ac_prefix).
  Proof.
    moveac.
    apply /introP; first by move⇒ /allP ?.
    apply ssr.ssrbool.contraNnot ⇒ ?.
    by apply /allP.
  Qed.

There should be no infinite arrivals; that is, value_at 0 = 0.
  Definition no_inf_arrivals (ac_prefix : ArrivalCurvePrefix) :=
    value_at ac_prefix 0 == 0.

Bursts must be specified; that is, steps_of should contain a pair (ε, b).
Steps should be strictly increasing both in time steps and values.
  Definition ltn_steps a b := (fst a < fst b) && (snd a < snd b).
  Definition sorted_ltn_steps (ac_prefix : ArrivalCurvePrefix) :=
    sorted ltn_steps (steps_of ac_prefix).

The conjunction of the 5 afore-defined properties defines a valid arrival-curve prefix.
We define an alternative, decidable version of valid_arrival_curve_prefix...
... and prove that the two definitions are equivalent.
  Lemma valid_arrival_curve_prefix_P :
     (ac_prefix : ArrivalCurvePrefix),
      reflect (valid_arrival_curve_prefix ac_prefix) (valid_arrival_curve_prefix_dec ac_prefix).
  Proof.
    moveac.
    apply /introP.
    - by move ⇒ /andP[/andP[/andP[/andP[? /large_horizon_P ?] ?]?]?].
    - apply ssr.ssrbool.contraNnot.
      move⇒ [?[/large_horizon_P ?[?[??]]]].
      by repeat (apply /andP; split ⇒ //).
  Qed.

We also define a predicate for non-decreasing order that is more convenient for proving some of the claims.