Require Export prosa.model.task.sequentiality.
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]

Section ExecutionOrder.
  
  (** Consider any type of job associated with any type of tasks... *)
  Context {Job: JobType}.
  Context {Task: TaskType}.
  Context `{JobTask Job Task}.

  (** ... with arrival times and costs ... *)
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

  (** ... and any kind of processor state model. *)
  Context {PState: ProcessorState Job}.


  (** Consider any arrival sequence ... *) 
  Variable arr_seq : arrival_sequence Job.
  
  (** ... and any schedule of this arrival sequence ... *)
  Variable sched : schedule PState.  
  
  (** ... in which the sequential tasks hypothesis holds. *)
  Hypothesis H_sequential_tasks: sequential_tasks arr_seq sched.

  (** A simple corollary of this hypothesis is that the scheduler
      executes a job with the earliest arrival time. *)
  Corollary scheduler_executes_job_with_earliest_arrival:
    forall j1 j2 t,
      arrives_in arr_seq j1 -> 
      arrives_in arr_seq j2 ->
      same_task j1 j2 ->
      ~~ completed_by sched j2 t ->
      scheduled_at sched j1 t ->
      job_arrival j1 <= job_arrival j2.
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
forall (j1 j2 : Job) (t : instant),
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
same_task j1 j2 ->
~~ completed_by sched j2 t ->
scheduled_at sched j1 t ->
job_arrival j1 <= job_arrival j2
  Proof.
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
forall (j1 j2 : Job) (t : instant),
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
same_task j1 j2 ->
~~ completed_by sched j2 t ->
scheduled_at sched j1 t ->
job_arrival j1 <= job_arrival j2
    intros ? ? t ARR1 ARR2 TSK NCOMPL SCHED.
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
TSK: same_task j1 j2
NCOMPL: ~~ completed_by sched j2 t
SCHED: scheduled_at sched j1 t
job_arrival j1 <= job_arrival j2
    rewrite /same_task eq_sym in TSK.
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
NCOMPL: ~~ completed_by sched j2 t
SCHED: scheduled_at sched j1 t
TSK: job_task j2 == job_task j1
job_arrival j1 <= job_arrival j2
    have SEQ := H_sequential_tasks j2 j1 t ARR2 ARR1 TSK.
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
NCOMPL: ~~ completed_by sched j2 t
SCHED: scheduled_at sched j1 t
TSK: job_task j2 == job_task j1
SEQ: job_arrival j2 < job_arrival j1 ->
scheduled_at sched j1 t ->
completed_by sched j2 t
job_arrival j1 <= job_arrival j2
    rewrite leqNgt; apply/negP; intros ARR.
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
NCOMPL: ~~ completed_by sched j2 t
SCHED: scheduled_at sched j1 t
TSK: job_task j2 == job_task j1
SEQ: job_arrival j2 < job_arrival j1 ->
scheduled_at sched j1 t ->
completed_by sched j2 t
ARR: job_arrival j2 < job_arrival j1
False
    move: NCOMPL => /negP NCOMPL; apply: NCOMPL.
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_sequential_tasks: sequential_tasks arr_seq sched
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SCHED: scheduled_at sched j1 t
TSK: job_task j2 == job_task j1
SEQ: job_arrival j2 < job_arrival j1 ->
scheduled_at sched j1 t ->
completed_by sched j2 t
ARR: job_arrival j2 < job_arrival j1
completed_by sched j2 t
    by apply SEQ.
  Qed.

End ExecutionOrder.