Introduce extrapolated arrival curve

Add an implementation of arrival curves via fast
extrapolation of a finite arrival-curve prefix. 

implementation/definitions/extrapolated_arrival_curve.v

+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)])]. *) 
+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.
+
+  (** 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 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.

implementation/facts/extrapolated_arrival_curve.v

+From mathcomp Require Export ssreflect ssrbool eqtype ssrnat div seq path fintype bigop.
+Require Export prosa.behavior.time.
+Require Export prosa.util.all.
+Require Export prosa.implementation.definitions.extrapolated_arrival_curve.
+
+(** In this file, we prove basic properties of the arrival-curve
+    prefix and the [extrapolated_arrival_curve] function. *) 
+
+(** We start with basic facts about the relations [ltn_steps] and [leq_steps]. *)
+Section BasicFacts.
+
+  (** We show that the relation [ltn_steps] is transitive. *) 
+  Lemma ltn_steps_is_transitive :
+    transitive ltn_steps.
+  Proof.
+    move=> a b c /andP [FSTab SNDab] /andP [FSTbc SNDbc].
+    by apply /andP; split; ssrlia. 
+  Qed.
+
+  (** Next, we show that the relation [leq_steps] is reflexive... *) 
+  Lemma leq_steps_is_reflexive :
+    reflexive leq_steps.
+  Proof.
+    move=> [l r].
+    rewrite /leq_steps.
+    by apply /andP; split.
+  Qed.
+
+  (** ... and transitive. *) 
+  Lemma leq_steps_is_transitive :
+    transitive leq_steps.
+  Proof.
+    move=> a b c /andP [FSTab SNDab] /andP [FSTbc SNDbc].
+    by apply /andP; split; ssrlia. 
+  Qed.
+
+End BasicFacts.
+
+(** In the following section, we prove a few properties of
+    arrival-curve prefixes assuming that there are no infinite
+    arrivals and that the list of steps is sorted according to the
+    [leq_steps] relation. *)
+Section ArrivalCurvePrefixSortedLeq.
+
+  (** Consider an arbitrary [leq]-sorted arrival-curve prefix without
+      infinite arrivals. *)
+  Variable ac_prefix : ArrivalCurvePrefix.
+  Hypothesis H_sorted_leq : sorted_leq_steps ac_prefix.
+  Hypothesis H_no_inf_arrivals : no_inf_arrivals ac_prefix.
+  
+  (** We prove that [value_at] is monotone with respect to the relation [<=]. *)
+  Lemma value_at_monotone :
+    monotone leq (value_at ac_prefix).
+  Proof.
+    intros t1 t2 LE; clear H_no_inf_arrivals.
+    unfold sorted_leq_steps, value_at, step_at, steps_of in *.
+    destruct ac_prefix as [h steps]; simpl.
+    have GenLem:
+      forall t__d1 v__d1 t__d2 v__d2,
+        v__d1 <= v__d2 ->
+        all (leq_steps (t__d1, v__d1)) steps ->
+        all (leq_steps (t__d2, v__d2)) steps ->              
+        snd (last (t__d1, v__d1) [seq step <- steps | fst step <= t1]) <= snd (last (t__d2, v__d2) [seq step <- steps | fst step <= t2]).
+    { induction steps as [ | [t__c v__c] steps]; first by done.
+      simpl; intros *; move => LEv /andP [LTN1 /allP ALL1] /andP [LTN2 /allP ALL2].
+      move: (H_sorted_leq); rewrite //= (@path_sorted_inE _ predT leq_steps); first last.
+      { by apply/allP. } 
+      { by intros ? ? ? _ _ _; apply leq_steps_is_transitive. }
+      move => /andP [ALL SORT].          
+      destruct (leqP (fst (t__c, v__c)) t1) as [R1 | R1], (leqP (fst (t__c, v__c)) t2) as [R2 | R2]; simpl in *. 
+      { rewrite R1 R2 //=; apply IHsteps; try done. } 
+      { by ssrlia. }
+      { rewrite ltnNge -eqbF_neg in R1; move: R1 => /eqP ->; rewrite R2 //=; apply IHsteps; try done.
+        - by move: LTN1; rewrite /leq_steps => /andP //= [_ LEc]. 
+        - by apply/allP.
+      } 
+      { rewrite ltnNge -eqbF_neg in R1; move: R1 => /eqP ->.
+        rewrite ltnNge -eqbF_neg in R2; move: R2 => /eqP ->.
+        apply IHsteps; try done.
+        - by apply/allP.
+        - by apply/allP.
+      }
+    }
+    apply GenLem; first by done.
+    all: by apply/allP; intros x _; rewrite /leq_steps //=.
+  Qed.
+
+  (** Next, we prove a correctness claim stating that if [value_at]
+      makes a step at time instant [t + ε] (that is, [value_at t <
+      value_at (t + ε)]), then [steps_of ac_prefix] contains a step
+      [(t + ε, v)] for some [v]. *)
+  Lemma value_at_change_is_in_steps_of :
+    forall t,
+      value_at ac_prefix t < value_at ac_prefix (t + ε) ->
+      exists v, (t + ε, v) \in steps_of ac_prefix.
+  Proof.
+    intros ? LT.
+    unfold prefix, value_at, step_at in LT.
+    destruct ac_prefix as [h2 steps]; simpl in LT.
+    rewrite [in X in _ < X](sorted_split _ _ fst t) in LT.
+    { rewrite [in X in _ ++ X](eq_filter (a2 := fun x => fst x == t + ε)) in LT; last first.
+      { by intros [a b]; simpl; rewrite -addn1 /ε eqn_leq. } 
+      { destruct ([seq x <- steps | fst x == t + ε]) eqn:LST.
+        { rewrite LST in LT.
+          rewrite [in X in X ++ _](eq_filter (a2 := fun x => fst x <= t)) in LT; last first.
+          { clear; intros [a b]; simpl.
+            destruct (leqP a t).
+            - by rewrite Bool.andb_true_r; apply/eqP; ssrlia.
+            - by rewrite Bool.andb_false_r.
+          } 
+          { by rewrite cats0 ltnn in LT. }
+        }
+        { destruct p as [t__c v__c]; exists v__c.
+          rewrite /steps_of //=; symmetry in LST.
+          apply mem_head_impl in LST.
+          by move: LST; rewrite mem_filter //= => /andP [/eqP -> IN].
+        }
+      }
+    }
+    { move: (H_sorted_leq); clear H_sorted_leq; rewrite /sorted_leq_steps //= => SORT; clear H_no_inf_arrivals.
+      induction steps; [by done | simpl in *].
+      move: SORT; rewrite path_sortedE; auto using leq_steps_is_transitive; move => /andP [LE SORT].
+      apply IHsteps in SORT.
+      rewrite path_sortedE; last by intros ? ? ? LE1 LE2; ssrlia.
+      apply/andP; split; last by done.
+      apply/allP; intros [x y] IN.
+      by move: LE => /allP LE; specialize (LE _ IN); move: LE => /andP [LT _].
+    }
+  Qed.
+  
+End ArrivalCurvePrefixSortedLeq.
+
+(* In the next section, we make the stronger assumption that
+   arrival-curve prefixes are sorted according to the [ltn_steps]
+   relation. *)
+Section ArrivalCurvePrefixSortedLtn.
+
+  (** Consider an arbitrary [ltn]-sorted arrival-curve prefix without
+      infinite arrivals. *)
+  Variable ac_prefix : ArrivalCurvePrefix.
+  Hypothesis H_sorted_ltn : sorted_ltn_steps ac_prefix. (* Stronger assumption. *)
+  Hypothesis H_no_inf_arrivals : no_inf_arrivals ac_prefix.
+  
+  (** First, we show that an [ltn]-sorted arrival-curve prefix is an
+      [leq]-sorted arrival-curve prefix. *)
+  Lemma sorted_ltn_steps_imply_sorted_leq_steps_steps : 
+    sorted_leq_steps ac_prefix.
+  Proof.
+    destruct ac_prefix; unfold sorted_leq_steps, sorted_ltn_steps in *; simpl in *.
+    clear H_no_inf_arrivals d.
+    destruct l; simpl in *; first by done.
+    eapply sub_path; last by apply H_sorted_ltn.
+    intros [a1 b1] [a2 b2] LT.
+    by unfold ltn_steps, leq_steps in *; simpl in *; ssrlia.
+  Qed.
+
+  (** Next, we show that [step_at 0] is equal to [(0, 0)]. *)
+  Lemma step_at_0_is_00 :
+    step_at ac_prefix 0 = (0, 0).
+  Proof.
+    unfold step_at; destruct ac_prefix as [h [ | [t v] steps]]; first by done.
+    have TR := ltn_steps_is_transitive.
+    move: (H_sorted_ltn); clear H_sorted_ltn; rewrite /sorted_ltn_steps //= path_sortedE // => /andP [ALL LT].
+    have EM : [seq step <- steps | fst step <= 0] = [::].
+    { apply filter_in_pred0; intros [t' v'] IN.
+      move: ALL => /allP ALL; specialize (ALL _ IN); simpl in ALL.
+      by rewrite -ltnNge //=; move: ALL; rewrite /ltn_steps //= => /andP [T _ ]; ssrlia.
+    }
+    rewrite EM; destruct (posnP t) as [Z | POS].
+    { subst t; simpl.
+      move: H_no_inf_arrivals; rewrite /no_inf_arrivals /value_at /step_at //= EM //=.
+      by move => EQ; subst v.
+    } 
+    { by rewrite leqNgt POS //=. } 
+  Qed.
+  
+  (** We show that functions [steps_of] and [step_at] are consistent.
+      That is, if a pair [(t, v)] is in steps of [ac_prefix], then
+      [step_at t] is equal to [(t, v)]. *)
+  Lemma step_at_agrees_with_steps_of :
+    forall t v, (t, v) \in steps_of ac_prefix -> step_at ac_prefix t = (t, v).
+  Proof.
+    intros * IN; destruct ac_prefix as [h steps].
+    unfold step_at; simpl in *.
+    apply in_cat in IN; move: IN => [steps__l [steps__r EQ]]; subst steps.
+    apply sorted_cat in H_sorted_ltn; destruct H_sorted_ltn; clear H_sorted_ltn; last by apply ltn_steps_is_transitive.
+    rewrite filter_cat last_cat (nonnil_last _ _ (0,0)); last by rewrite //= leqnn.
+    move: H0; rewrite //= path_sortedE; auto using ltn_steps_is_transitive; rewrite //= leqnn => /andP [ALL SORT].
+    simpl; replace (filter _ _ ) with (@nil (nat * nat)); first by done.
+    symmetry; apply filter_in_pred0; intros x IN; rewrite -ltnNge.
+    by move: ALL => /allP ALL; specialize (ALL _ IN); move: ALL; rewrite /ltn_steps //= => /andP [LT _ ]. 
+  Qed.
+  
+End ArrivalCurvePrefixSortedLtn.
+
+(** In this section, we prove a few basic properties of
+    [extrapolated_arrival_curve] function, such as (1) monotonicity of
+    [extrapolated_arrival_curve] or (2) implications of the fact that
+    [extrapolated_arrival_curve] makes a step at time [t + ε]. *)
+Section ExtrapolatedArrivalCurve.
+
+  (** Consider an arbitrary [leq]-sorted arrival-curve prefix without infinite arrivals. *)    
+  Variable ac_prefix : ArrivalCurvePrefix.    
+  Hypothesis H_positive : positive_horizon ac_prefix.
+  Hypothesis H_sorted_leq : sorted_leq_steps ac_prefix.
+
+  (** Let [h] denote the horizon of [ac_prefix] ... *)
+  Let h := horizon_of ac_prefix.
+
+  (** ... and [prefix] be shorthand for [value_at ac_prefix]. *) 
+  Let prefix := value_at ac_prefix.
+  
+  (** We show that [extrapolated_arrival_curve] is monotone. *) 
+  Lemma extrapolated_arrival_curve_is_monotone :
+    monotone leq (extrapolated_arrival_curve ac_prefix).
+  Proof.
+    intros t1 t2 LE; unfold extrapolated_arrival_curve.
+    replace (horizon_of _) with h; last by done. 
+    move: LE; rewrite leq_eqVlt => /orP [/eqP EQ | LTs].
+    { by subst t2. }
+    { have ALT : (t1 %/ h == t2 %/ h) \/ (t1 %/ h < t2 %/ h).
+      { by apply/orP; rewrite -leq_eqVlt; apply leq_div2r, ltnW. }
+      move: ALT => [/eqP EQ | LT].
+      { rewrite EQ leq_add2l; apply value_at_monotone => //.
+        by apply eqdivn_leqmodn; ssrlia.
+      } 
+      { have EQ: exists k, t1 + k = t2 /\ k > 0.
+        { exists (t2 - t1); split; ssrlia. } 
+        destruct EQ as [k [EQ POS]]; subst t2; clear LTs.
+        rewrite divnD; last by done.
+        rewrite !mulnDl -!addnA leq_add2l.          
+        destruct (leqP h k) as [LEk|LTk].
+        { eapply leq_trans; last by apply leq_addr.
+          move: LEk; rewrite leq_eqVlt => /orP [/eqP EQk | LTk].
+          { by subst; rewrite divnn POS mul1n; apply value_at_monotone, ltnW, ltn_pmod. }
+          { rewrite -[value_at _ (t1 %% h)]mul1n; apply leq_mul.
+            rewrite divn_gt0; [by apply ltnW | by done].
+            by apply value_at_monotone, ltnW, ltn_pmod.
+          }
+        }
+        { rewrite divn_small // mul0n add0n.
+          rewrite divnD // in LT; move: LT; rewrite -addnA -addn1 leq_add2l divn_small // add0n.
+          rewrite lt0b => F; rewrite F; clear F.
+          rewrite mul1n; eapply leq_trans; last by apply leq_addr.
+          by apply value_at_monotone, ltnW, ltn_pmod.
+        }
+      }
+    }
+  Qed.
+
+  (** Finally, we show that if 
+      [extrapolated_arrival_curve t <> extrapolated_arrival_curve (t + ε)], 
+      then either (1) [t + ε] divides [h] or (2) [prefix (t mod h) < prefix ((t + ε) mod h)]. *) 
+  Lemma extrapolated_arrival_curve_change :
+    forall t,
+      extrapolated_arrival_curve ac_prefix t != extrapolated_arrival_curve ac_prefix (t + ε) ->
+      (* 1 *) t %/ h < (t + ε) %/ h
+      \/ (* 2 *) t %/ h = (t + ε) %/ h /\ prefix (t %% h) < prefix ((t + ε) %% h).
+  Proof.
+    intros t NEQ.
+    have LT := ltn_neqAle (extrapolated_arrival_curve ac_prefix t) (extrapolated_arrival_curve ac_prefix (t + ε)).
+    rewrite NEQ in LT; rewrite extrapolated_arrival_curve_is_monotone in LT; last by apply leq_addr.
+    clear NEQ; simpl in LT.
+    unfold extrapolated_arrival_curve in LT.
+    replace (horizon_of _) with h in LT; last by done.
+    have AF : forall s1 s2 m x y,
+        s1 <= s2 ->
+        m * s1 + x < m * s2 + y ->
+        s1 < s2 \/ s1 = s2 /\ x < y.
+    {  clear; intros * LEs LT.
+       move: LEs; rewrite leq_eqVlt => /orP [/eqP EQ | LTs].
+       { by subst s2; rename s1 into s; right; split; [ done | ssrlia]. } 
+       { by left. }
+    }         
+    apply AF with (m := prefix h).
+    { by apply leq_div2r, leq_addr. }
+    { by rewrite ![prefix _ * _]mulnC; apply LT. }
+  Qed.
+  
+End ExtrapolatedArrivalCurve.

scripts/wordlist.pws

@@ -64,6 +64,8 @@ subadditivity
 subadditive
 subinterval
 subsequences
+summand
+afore
 ad
 hoc
 mailinglist