Library prosa.analysis.facts.job_index

Require Export prosa.analysis.facts.model.task_arrivals.

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, ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and any two jobs j1 and j2 from this arrival sequence that stem from the same task.
  Variable j1 j2 : Job.
  Hypothesis H_j1_from_arrival_sequence: arrives_in arr_seq j1.
  Hypothesis H_j2_from_arrival_sequence: arrives_in arr_seq j2.
  Hypothesis H_same_task: job_task j1 = job_task j2.

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.
    Hypothesis H_equal_index: job_index arr_seq j1 = job_index arr_seq j2.

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.
    Lemma case_arrival_lte_implies_equal_job:
      job_arrival j1 ≤ job_arrival j2 → j1 = j2.

And similarly if j1 arrives after j2, we show that the jobs are equal.
    Lemma case_arrival_gt_implies_equal_job:
      job_arrival j1 > job_arrival j2 → j1 = j2.

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.
  Lemma diff_jobs_iff_diff_indices:
    j1 ≠ j2 ↔
    job_index arr_seq j1 ≠ job_index arr_seq j2.

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)).
  Lemma index_as_sum_size_and_index:
    job_index arr_seq j1 =
    size (task_arrivals_before_job_arrival arr_seq j1)
    + index j1 (task_arrivals_at_job_arrival arr_seq j1).

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).
  Lemma arrival_lt_implies_job_in_arrivals_between_P:
    ∀ (P : Job → bool) (t1 t2 : instant),
      (j1 \in arrivals_between_P arr_seq P t1 t2) →
      (j2 \in arrivals_between_P arr_seq P t1 t2) →
      job_arrival j2 < job_arrival j1 →
      j2 \in 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.
  Lemma index_lte_implies_arrival_lte_P:
    ∀ (P : Job → bool) (t1 t2 : instant),
      (j1 \in arrivals_between_P arr_seq P t1 t2) →
      (j2 \in arrivals_between_P arr_seq P t1 t2) →
      index j1 (arrivals_between_P arr_seq P t1 t2) ≤ index j2 (arrivals_between_P arr_seq P t1 t2) →
      job_arrival j1 ≤ job_arrival j2.

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.
  Lemma job_index_same_in_task_arrivals:
    job_arrival j1 ≤ job_arrival j2 →
    index j1 (task_arrivals_up_to_job_arrival arr_seq j1) = index j1 (task_arrivals_up_to_job_arrival arr_seq j2).

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.
  Lemma index_job_lt_size_task_arrivals_up_to_job:
    job_index arr_seq j1 < size (task_arrivals_up_to_job_arrival arr_seq j1).

Finally, we show that a lower job index implies an earlier arrival time.
  Lemma index_lte_implies_arrival_lte:
    job_index arr_seq j2 ≤ job_index arr_seq j1 →
    job_arrival j2 ≤ job_arrival j1.

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.
  Lemma earlier_arrival_implies_lower_index:
    job_arrival j1 < job_arrival j2 →
    job_index arr_seq j1 < 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.
  Lemma job_index_minus_one_lt_size_task_arrivals_up_to:
    job_index arr_seq j1 - 1 < size (task_arrivals_up_to_job_arrival arr_seq j1).

Since task_arrivals_up_to_job_arrival arr_seq j has at least the job j in it, its size has to be positive.
  Lemma positive_job_index_implies_positive_size_of_task_arrivals:
    size (task_arrivals_up_to_job_arrival arr_seq j1) > 0.

End JobIndexLemmas.

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 ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... 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.
  Lemma prev_job_arr:
    arrives_in arr_seq (prev_job arr_seq j).

We show that the index of prev_job j in task arrivals up to j is one less than job_index arr_seq j.
  Lemma prev_job_index:
    index (prev_job arr_seq j) (task_arrivals_up_to_job_arrival arr_seq j) = job_index arr_seq j - 1.

Observe that job j and prev_job j stem from the same task.
  Lemma prev_job_task:
    job_task (prev_job arr_seq j) = job_task j.

We show that prev_job arr_seq j belongs in task_arrivals_up_to_job_arrival arr_seq j.
  Lemma prev_job_in_task_arrivals_up_to_j:
    prev_job arr_seq j \in task_arrivals_up_to_job_arrival arr_seq j.

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.
  Lemma prev_job_arr_lte:
    job_arrival (prev_job arr_seq j) ≤ job_arrival j.

We show that for any job j the job index of prev_job j is one less than the job index of j.
  Lemma prev_job_index_j:
    job_index arr_seq j > 0 →
    job_index arr_seq (prev_job arr_seq j) = job_index arr_seq j - 1.

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.