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...
... with arrival times and costs ...
... and any kind of processor state model.
Consider any arrival sequence ...
... and any schedule of this arrival sequence ...
... 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.
∀ 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.