Library prosa.implementation.facts.maximal_arrival_sequence

Recall that, given an arrival curve max_arrivals and a job-generating function generate_jobs_at, the function concrete_arrival_sequence generates an arrival sequence. In this section, we prove a few properties of this function.
Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider a task set ts with non-duplicate tasks.
  Variable ts : seq Task.
  Hypothesis H_ts_uniq : uniq ts.

Let max_arrivals be a family of valid arrival curves, i.e., for any task tsk in ts, max_arrival tsk is (1) an arrival bound of tsk, and (2) it is a monotonic function that equals 0 for the empty interval delta = 0.
Further assume we are given a function that generates the required number of jobs of a given task at a given instant of time.
First, we assume that generate_jobs_at tsk n t generates n jobs.
  Hypothesis H_job_generation_valid_number:
     (tsk : Task) (n : nat) (t : instant), tsk \in ts size (generate_jobs_at tsk n t) = n.

Second, we assume that generate_jobs_at tsk n t generates jobs of task tsk that arrive at time t.
  Hypothesis H_job_generation_valid_jobs:
     (tsk : Task) (n : nat) (t : instant) (j : Job),
      (j \in generate_jobs_at tsk n t)
      job_task j = tsk
       job_arrival j = t
       job_cost j task_cost tsk.

Finally, we assume that all jobs generated by generate_jobs_at are unique.
  Hypothesis H_jobs_unique:
     (t1 t2 : instant),
      uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2).

Assuming such a well-behaved "constructor" generate_jobs_at, we prove a few validity claims about an arrival sequence generated by concrete_arrival_sequence.
  Section ValidityClaims.

We start by showing that the obtained arrival sequence is a set.
Next, we show that all jobs in the arrival sequence come from ts.
Further, we note that the jobs in the arrival sequence have consistent arrival times.
Lastly, we observe that the jobs in the arrival sequence have valid job costs.
In this section, we prove a series of facts regarding the maximal arrival sequence, leading up to the main theorem that all arrival-curve constraints are respected.
  Section Facts.

Let tsk be any task in ts that is to be analyzed.
    Variable tsk : Task.
    Hypothesis H_tsk_in_ts : tsk \in ts.

First, we show that the arrivals at time t are indeed generated by generate_jobs_at applied at time t.
Next, we show that the number of arrivals at time t always matches max_arrivals_at applied at time t.
    Lemma task_arrivals_at_eq:
        size (task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t)
        = max_arrivals_at tsk t.

We then generalize the previous result to an arbitrary interval [t1,t2).
We further show that, starting from an empty prefix and applying extend_arrival_prefix t times, we end up with a prefix of size t...
    Lemma extend_horizon_size :
        size (iter t (extend_arrival_prefix tsk) [::]) = t.

...and that the arrival sequence prefix up to an arbitrary horizon t is a sequence of t+1 elements.
    Lemma prefix_up_to_size :
        size (maximal_arrival_prefix tsk t) = t.+1.

Next, we prove prefix inclusion for maximal_arrival_prefix when the horizon is expanded by one...
    Lemma n_arrivals_at_prefix_inclusion1 :
       t h,
        t h
        nth 0 (maximal_arrival_prefix tsk h) t
        = nth 0 (maximal_arrival_prefix tsk h.+1) t.

...and we generalize the previous result to two arbitrary horizons h1 h2.
    Lemma n_arrivals_at_prefix_inclusion :
       t h1 h2,
        t h1 h2
        nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t.

Next, we prove that, for any positive time instant t, max_arrivals_at indeed matches the arrivals of next_max_arrival applied at t-1.
    Lemma max_arrivals_at_next_max_arrivals_eq:
        0 < t
        max_arrivals_at tsk t
        = next_max_arrival tsk (maximal_arrival_prefix tsk t.-1).

Given a time instant t and and interval Δ, we show that max_arrivals_at applied at time t is always less-or-equal to max_arrivals applied to Δ+1, even when each value of max_arrivals_at in the interval [t-Δ, t) is subtracted from it.
    Lemma n_arrivals_at_leq :
       t Δ,
        Δ t
        max_arrivals_at tsk t
         max_arrivals tsk Δ.+1 - \sum_(t - Δ i < t) max_arrivals_at tsk i.
  End Facts.

Finally, we prove our main result, that is, the proposed maximal arrival sequence instantiation indeed respects all arrival-curve constraints.