Library prosa.implementation.facts.job_constructor

In this file, we prove facts about the job-constructor function when used in pair with the concrete arrival sequence.
Section JobConstructor.

Assume that an arrival curve based on a concrete prefix is given.
  #[local] Existing Instance ConcreteMaxArrivals.

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

First, we show that generate_jobs_at tsk n t generates n jobs ...
  Lemma job_generation_valid_number:
     tsk n t,
      tsk \in ts size (generate_jobs_at tsk n t) = n.

... and that each generated job is unique.
  Lemma generate_jobs_at_unique:
     tsk n t,
      uniq (generate_jobs_at tsk n t).

Next, for convenience, we define arr_seq as the concrete arrival sequence used with the job constructor.
We start by proving that the arrival time of a job is consistent with its positioning inside the arrival sequence.
  Lemma job_arrival_consistent:
     j t,
      j \in arrivals_at arr_seq t job_arrival j = t.

Next, we show that the list of arrivals at any time t is unique ...
  Lemma arrivals_at_unique:
      uniq (arrivals_at arr_seq t).

... and generalize the above result to arbitrary time intervals.
  Lemma arrivals_between_unique:
     t1 t2,
      uniq (arrivals_between arr_seq t1 t2).

Finally, we observe that generate_jobs_at tsk n t indeed generates jobs of task tsk that arrive at t
  Corollary job_generation_valid_jobs:
     tsk n t j,
      j \in generate_jobs_at tsk n t
            job_task j = tsk
             job_arrival j = t
             job_cost j task_cost tsk.

End JobConstructor.