Library prosa.analysis.facts.job_index

In this section, we prove some properties related to job_index.
Section JobIndexLemmas.

Consider any type of tasks ...
  Context {Task : TaskType}.

... and any jobs associated with the tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

Consider any arrival sequence with consistent and non-duplicate arrivals, ...
... and any two jobs j1 and j2 from this arrival sequence that stem from the same task.
In the next section, we prove some basic properties about jobs with equal indices.
  Section EqualJobIndex.

Assume that the jobs j1 and j2 have the same job_index in the arrival sequence.
To show that jobs j1 and j2 are equal, we'll perform case analysis on the relation between their arrival times.
Jobs with equal indices have to be equal regardless of their arrival times because of the way job_index is defined (i.e., jobs are first ordered according to their arrival times and ties are broken arbitrarily due to which no two unequal jobs have the same job_index).
In case job j2 arrives after or at the same time as j1 arrives, we show that the jobs are equal.
And similarly if j1 arrives after j2, we show that the jobs are equal.
And finally we show that irrespective of the relation between the arrival of job j1 and j2, j1 must be equal to j2.
    Lemma equal_index_implies_equal_jobs:
      j1 = j2.

  End EqualJobIndex.

We show that jobs of a task are different if and only if they have different indices.
We show that job_index j can be written as a sum of size (task_arrivals_before_job_arrival j) and index j (task_arrivals_at arr_seq (job_task j) (job_arrival j)).
Given jobs j1 and j2 in arrivals_between_P arr_seq P t1 t2, the fact that j2 arrives strictly before j1 implies that j2 also belongs in the sequence arrivals_between_P arr_seq P t1 (job_arrival j1).
We show that jobs in the sequence arrivals_between_P are ordered by their arrival times, i.e., if index of a job j2 is greater than or equal to index of any other job j1 in the sequence, then job_arrival j2 must be greater than or equal to job_arrival j1.
We observe that index of job j1 is same in the sequences task_arrivals_up_to_job_arrival j1 and task_arrivals_up_to_job_arrival j2 provided j2 arrives after j1.
We show that the job_index of a job j1 is strictly less than the size of task_arrivals_up_to_job_arrival arr_seq j1.
Finally, we show that a lower job index implies an earlier arrival time.
We show that if job j1 arrives earlier than job j2 then job_index arr_seq j1 is strictly less than job_index arr_seq j2.
We prove a weaker version of the lemma index_job_lt_size_task_arrivals_up_to_job, given that the job_index of j is positive.
Since task_arrivals_up_to_job_arrival arr_seq j has at least the job j in it, its size has to be positive.
In this section, we prove a few basic properties of function prev_job.
Section PreviousJob.

Consider any type of tasks ...
  Context {Task : TaskType}.

... and any jobs associated with the tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

Consider any unique arrival sequence with consistent arrivals ...
... and an arbitrary job with a positive job_index.
  Variable j : Job.
  Hypothesis H_arrives_in_arr_seq: arrives_in arr_seq j.
  Hypothesis H_positive_job_index: job_index arr_seq j > 0.

We observe that the fact that job j is in the arrival sequence implies that job prev_job j is in the arrival sequence.
We show that the index of prev_job j in task arrivals up to j is one less than job_index arr_seq j.
Observe that job j and prev_job j stem from the same task.
We observe that for any job j the arrival time of prev_job j is strictly less than the arrival time of j in context of periodic tasks.
We show that for any job j the job index of prev_job j is one less than the job index of j.
We also show that for any job j there are no task arrivals between prev_job j and j.
  Lemma no_jobs_between_consecutive_jobs:
    job_index arr_seq j > 0
    task_arrivals_between arr_seq (job_task j)
                          (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::].

We show that there always exists a job of lesser job_index than a job with a positive job_index that arrives in the arrival sequence.
  Lemma exists_jobs_before_j:
     k,
      k < job_index arr_seq j
       j',
        j j'
        job_task j' = job_task j
        arrives_in arr_seq j'
        job_index arr_seq j' = k.
End PreviousJob.