Library prosa.analysis.facts.model.task_schedule

In this file we provide basic properties related to schedule of a task.
Section TaskSchedule.

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 any valid arrival sequence of such jobs ...
... and let sched be any corresponding uni-processor schedule.
Let tsk be any task.
  Variable tsk : Task.

We show that if a job of task tsk is scheduled at time t, then task tsk is scheduled at time t.
  Lemma job_of_task_scheduled_implies_task_scheduled :
     j t,
      job_of_task tsk j
      scheduled_at sched j t
      task_scheduled_at arr_seq sched tsk t.
  Proof.
    movej t TSK.
    rewrite -(scheduled_job_at_iff arr_seq) // /task_scheduled_at ⇒ →.
    by move: TSK; rewrite /job_of_task.
  Qed.

And vice versa, if no job of task tsk is scheduled at time t, then task tsk is not scheduled at time t.
  Lemma job_of_task_scheduled_implies_task_scheduled':
     j t,
      ~~ job_of_task tsk j
      scheduled_at sched j t
      ~~ task_scheduled_at arr_seq sched tsk t.
  Proof.
    movej t TSK SCHED; apply: contra; last exact: TSK.
    move: SCHED; rewrite -(scheduled_job_at_iff arr_seq) // /task_scheduled_at ⇒ →.
    by rewrite /job_of_task.
  Qed.

End TaskSchedule.