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.
Assume a schedule ...
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,
same_task j1 j2 →
~~ completed_by sched j2 t →
scheduled_at sched j1 t →
job_arrival j1 ≤ job_arrival j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
sched : schedule PState
H_sequential_tasks : sequential_tasks sched
============================
forall (j1 j2 : Job) (t : instant),
same_task j1 j2 ->
~~ completed_by sched j2 t ->
scheduled_at sched j1 t -> job_arrival j1 <= job_arrival j2
----------------------------------------------------------------------------- *)
Proof.
intros ? ? t TSK NCOMPL SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 67)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
sched : schedule PState
H_sequential_tasks : sequential_tasks sched
j1, j2 : Job
t : instant
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 101)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
sched : schedule PState
H_sequential_tasks : sequential_tasks sched
j1, j2 : Job
t : instant
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 TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 106)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
sched : schedule PState
H_sequential_tasks : sequential_tasks sched
j1, j2 : Job
t : instant
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 132)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
sched : schedule PState
H_sequential_tasks : sequential_tasks sched
j1, j2 : Job
t : instant
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 166)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
sched : schedule PState
H_sequential_tasks : sequential_tasks sched
j1, j2 : Job
t : instant
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,
same_task j1 j2 →
~~ completed_by sched j2 t →
scheduled_at sched j1 t →
job_arrival j1 ≤ job_arrival j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
sched : schedule PState
H_sequential_tasks : sequential_tasks sched
============================
forall (j1 j2 : Job) (t : instant),
same_task j1 j2 ->
~~ completed_by sched j2 t ->
scheduled_at sched j1 t -> job_arrival j1 <= job_arrival j2
----------------------------------------------------------------------------- *)
Proof.
intros ? ? t TSK NCOMPL SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 67)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
sched : schedule PState
H_sequential_tasks : sequential_tasks sched
j1, j2 : Job
t : instant
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 101)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
sched : schedule PState
H_sequential_tasks : sequential_tasks sched
j1, j2 : Job
t : instant
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 TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 106)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
sched : schedule PState
H_sequential_tasks : sequential_tasks sched
j1, j2 : Job
t : instant
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 132)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
sched : schedule PState
H_sequential_tasks : sequential_tasks sched
j1, j2 : Job
t : instant
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 166)
Job : JobType
Task : TaskType
H : JobTask Job Task
H0 : JobArrival Job
H1 : JobCost Job
PState : Type
H2 : ProcessorState Job PState
sched : schedule PState
H_sequential_tasks : sequential_tasks sched
j1, j2 : Job
t : instant
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.