Require Export prosa.model.task.concept.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.analysis.definitions.task_schedule.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.facts.model.ideal.schedule.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
        
(** 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}.

  (** Let [sched] be any ideal uni-processor schedule. *)
  Variable sched : schedule (ideal.processor_state Job).

  (** 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 :
    forall j t,
      job_of_task tsk j -> 
      scheduled_at sched j t ->
      task_scheduled_at sched tsk t.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
sched: schedule (ideal.processor_state Job)
tsk: Task
forall (j : Job) (t : instant),
job_of_task tsk j ->
scheduled_at sched j t ->
task_scheduled_at sched tsk t
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
sched: schedule (ideal.processor_state Job)
tsk: Task
forall (j : Job) (t : instant),
job_of_task tsk j ->
scheduled_at sched j t ->
task_scheduled_at sched tsk t
    intros ? ? TSK SCHED.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
sched: schedule (ideal.processor_state Job)
tsk: Task
j: Job
t: instant
TSK: job_of_task tsk j
SCHED: scheduled_at sched j t
task_scheduled_at sched tsk t
    unfold task_scheduled_at.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
sched: schedule (ideal.processor_state Job)
tsk: Task
j: Job
t: instant
TSK: job_of_task tsk j
SCHED: scheduled_at sched j t
match sched t with
| Some j => job_task j == tsk
| None => false
end
    by move: SCHED; rewrite scheduled_at_def => /eqP ->.
  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':
    forall j t,
      ~~ job_of_task tsk j -> 
      scheduled_at sched j t ->
      ~~ task_scheduled_at sched tsk t.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
sched: schedule (ideal.processor_state Job)
tsk: Task
forall (j : Job) (t : instant),
~~ job_of_task tsk j ->
scheduled_at sched j t ->
~~ task_scheduled_at sched tsk t
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
sched: schedule (ideal.processor_state Job)
tsk: Task
forall (j : Job) (t : instant),
~~ job_of_task tsk j ->
scheduled_at sched j t ->
~~ task_scheduled_at sched tsk t
    move => j t /negP TSK SCHED; apply /negP => TSCHED; apply: TSK.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
sched: schedule (ideal.processor_state Job)
tsk: Task
j: Job
t: instant
SCHED: scheduled_at sched j t
TSCHED: task_scheduled_at sched tsk t
job_of_task tsk j
    move: SCHED; rewrite scheduled_at_def => /eqP SCHED.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
sched: schedule (ideal.processor_state Job)
tsk: Task
j: Job
t: instant
TSCHED: task_scheduled_at sched tsk t
SCHED: sched t = Some j
job_of_task tsk j
    by move: TSCHED; rewrite /task_scheduled_at SCHED.
  Qed.

End TaskSchedule.