Library prosa.analysis.facts.model.sequential


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


Require Export prosa.model.task.sequentiality.

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: Type}.
  Context `{ProcessorState Job PState}.

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.
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:
     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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 58)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  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.
    intros ? ? t ARR1 ARR2 TSK NCOMPL SCHED.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 66)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 103)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 108)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 134)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 168)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

End ExecutionOrder.