Library prosa.analysis.facts.model.offset

In this module, we prove some properties of task offsets.

Section OffsetLemmas.

Consider any type of tasks with an offset ...

Context {Task : TaskType}.
Context `{TaskOffset Task}.

... and any type of jobs associated with these tasks.

  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

Consider any arrival sequence with consistent and non-duplicate arrivals ...

... and any job j (that stems from the arrival sequence) of any task tsk with a valid offset.

  Variable tsk : Task.
  Variable j : Job.
  Hypothesis H_job_of_task: job_task j = tsk.
  Hypothesis H_valid_offset: valid_offset arr_seq tsk.
  Hypothesis H_job_from_arrseq: arrives_in arr_seq j.

We show that the if j is the first job of task tsk then j arrives at task_offset tsk.

  Lemma first_job_arrival:
    job_index arr_seq j = 0 →
    job_arrival j = task_offset tsk.
  Proof.
    intros INDX.
    move: H_valid_offset ⇒ [BEFORE [j' [ARR' [TSK ARRIVAL]]]].
    case: (boolP (j' == j)) ⇒ [/eqP EQ|NEQ]; first by rewrite -EQ.
    destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j')) as [Z | [m N]].
    - move: NEQ ⇒ /eqP NEQ; contradict NEQ.
      by eapply equal_index_implies_equal_jobs; eauto;
        [rewrite TSK | rewrite Z INDX].
    - have IND_LTE : (job_index arr_seq j ≤ job_index arr_seq j') by rewrite INDX N.
      apply index_lte_implies_arrival_lte in IND_LTE ⇒ //; last by rewrite TSK.
      by apply/eqP; rewrite eqn_leq; apply/andP; split;
        [lia | apply H_valid_offset].
  Qed.

Consider any task set ts.

Variable ts : TaskSet Task.

If task tsk is in ts, then its offset is less than or equal to the maximum offset of all tasks in ts.

  Lemma max_offset_g:
    tsk \in ts →
    task_offset tsk ≤ max_task_offset ts.
  Proof.
    intros TSK_IN.
    apply in_max0_le.
    by apply map_f.
  Qed.

End OffsetLemmas.