# Library prosa.implementation.facts.extrapolated_arrival_curve

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.
We show that the relation ltn_steps is transitive.
Lemma ltn_steps_is_transitive :
transitive ltn_steps.
Next, we show that the relation leq_steps is reflexive...
Lemma leq_steps_is_reflexive :
reflexive leq_steps.
... and transitive.
Lemma leq_steps_is_transitive :
transitive leq_steps.
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).
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 :
∀ t,
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.
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.
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).
Lemma step_at_agrees_with_steps_of :
∀ t v, (t, v) \in steps_of ac_prefix → step_at ac_prefix t = (t, v).
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).
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 :
∀ t,
extrapolated_arrival_curve ac_prefix t != extrapolated_arrival_curve ac_prefix (t + ε) →
t %/ h < (t + ε) %/ h
∨ t %/ h = (t + ε) %/ h ∧ prefix (t %% h) < prefix ((t + ε) %% h).
End ExtrapolatedArrivalCurve.