Library prosa.implementation.facts.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.
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.

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.

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).

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.

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.