Library prosa.implementation.facts.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.
Next, we show that the relation leq_steps is reflexive...
... and transitive.
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.
Consider an arbitrary leq-sorted arrival-curve prefix without infinite arrivals.
We prove that value_at is monotone with respect to the relation .
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 :
      value_at ac_prefix t < value_at ac_prefix (t + ε)
       v, (t + ε, v) \in steps_of ac_prefix.

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.
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).
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).
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 + ε.
Consider an arbitrary leq-sorted arrival-curve prefix without infinite arrivals.
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.
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 :
      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).
End ExtrapolatedArrivalCurve.