Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.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.
Require Export prosa.behavior.time.

[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]


(** 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)])]. *)
Definition inter_arrival_to_prefix (p : nat) : ArrivalCurvePrefix := (p, [:: (1, 1)]).

(** The first component of arrival-curve prefix [ac_prefix] is called horizon. *)
Definition horizon_of (ac_prefix : ArrivalCurvePrefix) := fst ac_prefix.

(** The second component of [ac_prefix] is called steps. *)
Definition steps_of (ac_prefix : ArrivalCurvePrefix) := snd ac_prefix.

(** 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. *)
Definition time_steps_of (ac_prefix : ArrivalCurvePrefix) :=
  map fst (steps_of ac_prefix).

(** 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)>>. *)
Definition extrapolated_arrival_curve (ac_prefix : ArrivalCurvePrefix) (t : duration) :=
  let h := horizon_of ac_prefix in
  t %/ h * value_at ac_prefix h + value_at ac_prefix (t %% h).

(** In the following section, we define a few validity predicates. *)
Section ValidArrivalCurvePrefix.

  (** Horizon should be positive. *)
  Definition positive_horizon (ac_prefix : ArrivalCurvePrefix) :=
    horizon_of ac_prefix > 0.

  (** Horizon should bound time steps. *)
  Definition large_horizon (ac_prefix : ArrivalCurvePrefix) :=
    forall s, s \in time_steps_of ac_prefix -> s <= horizon_of ac_prefix.

  (** We define an alternative, decidable version of [large_horizon]... *)
  Definition large_horizon_dec (ac_prefix : ArrivalCurvePrefix) : bool :=
    all (fun s => s <= horizon_of ac_prefix) (time_steps_of ac_prefix).

  (** ... and prove that the two definitions are equivalent. *)
  
forall ac_prefix : ArrivalCurvePrefix,
reflect (large_horizon ac_prefix)
  (large_horizon_dec ac_prefix)

  
forall ac_prefix : ArrivalCurvePrefix,
reflect (large_horizon ac_prefix)
  (large_horizon_dec ac_prefix)

    
ac: ArrivalCurvePrefix
reflect (large_horizon ac) (large_horizon_dec ac)

    
ac: ArrivalCurvePrefix
~~ large_horizon_dec ac -> ~ large_horizon ac

    
ac: ArrivalCurvePrefix
_Hyp_: large_horizon ac
large_horizon_dec ac

    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)]. *)
  Definition specified_bursts (ac_prefix : ArrivalCurvePrefix) :=
    ε \in time_steps_of ac_prefix.

  (** 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. *)
  Definition valid_arrival_curve_prefix (ac_prefix : ArrivalCurvePrefix) :=
    positive_horizon ac_prefix
    /\ large_horizon ac_prefix
    /\ no_inf_arrivals ac_prefix
    /\ specified_bursts ac_prefix
    /\ sorted_ltn_steps ac_prefix.

  (** We define an alternative, decidable version of [valid_arrival_curve_prefix]... *)
  Definition valid_arrival_curve_prefix_dec (ac_prefix : ArrivalCurvePrefix) : bool :=
    (positive_horizon ac_prefix)
    && (large_horizon_dec ac_prefix)
    && (no_inf_arrivals ac_prefix)
    && (specified_bursts ac_prefix)
    && (sorted_ltn_steps ac_prefix).

  (** ... and prove that the two definitions are equivalent. *)
  
forall ac_prefix : ArrivalCurvePrefix,
reflect (valid_arrival_curve_prefix ac_prefix)
  (valid_arrival_curve_prefix_dec ac_prefix)

  
forall ac_prefix : ArrivalCurvePrefix,
reflect (valid_arrival_curve_prefix ac_prefix)
  (valid_arrival_curve_prefix_dec ac_prefix)

    
ac: ArrivalCurvePrefix
reflect (valid_arrival_curve_prefix ac)
  (valid_arrival_curve_prefix_dec ac)

    
ac: ArrivalCurvePrefix
valid_arrival_curve_prefix_dec ac ->
valid_arrival_curve_prefix ac
ac: ArrivalCurvePrefix
~~ valid_arrival_curve_prefix_dec ac ->
~ valid_arrival_curve_prefix ac

    
ac: ArrivalCurvePrefix
valid_arrival_curve_prefix_dec ac ->
valid_arrival_curve_prefix ac
 by move => /andP[/andP[/andP[/andP[? /large_horizon_P ?] ?]?]?].
    
ac: ArrivalCurvePrefix
~~ valid_arrival_curve_prefix_dec ac ->
~ valid_arrival_curve_prefix ac
 
ac: ArrivalCurvePrefix
valid_arrival_curve_prefix ac ->
valid_arrival_curve_prefix_dec ac

      
ac: ArrivalCurvePrefix
_a_: positive_horizon ac
__view_subject_1_: large_horizon_dec ac
_a1_: no_inf_arrivals ac
_a2_: specified_bursts ac
_b_: sorted_ltn_steps ac
valid_arrival_curve_prefix_dec ac

      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. *)
  Definition leq_steps a b := (fst a <= fst b) && (snd a <= snd b).
  Definition sorted_leq_steps (ac_prefix : ArrivalCurvePrefix) :=
    sorted leq_steps (steps_of ac_prefix).

End ValidArrivalCurvePrefix.