Library prosa.analysis.facts.edf
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Import prosa.model.priority.edf.
Require Import prosa.model.task.absolute_deadline.
In this section, we prove a few properties about EDF policy.
Consider any type of tasks with relative deadlines ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any arrival sequence.
EDF respects sequential tasks hypothesis.
Lemma EDF_respects_sequential_tasks:
policy_respects_sequential_tasks.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 338)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
============================
policy_respects_sequential_tasks
----------------------------------------------------------------------------- *)
Proof.
intros j1 j2 TSK ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 343)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
j1, j2 : Job
TSK : job_task j1 == job_task j2
ARR : job_arrival j1 <= job_arrival j2
============================
hep_job j1 j2
----------------------------------------------------------------------------- *)
move: TSK ⇒ /eqP TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 379)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
j1, j2 : Job
ARR : job_arrival j1 <= job_arrival j2
TSK : job_task j1 = job_task j2
============================
hep_job j1 j2
----------------------------------------------------------------------------- *)
unfold hep_job, EDF, job_deadline, job_deadline_from_task_deadline; rewrite TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 383)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
j1, j2 : Job
ARR : job_arrival j1 <= job_arrival j2
TSK : job_task j1 = job_task j2
============================
job_arrival j1 + task_deadline (job_task j2) <=
job_arrival j2 + task_deadline (job_task j2)
----------------------------------------------------------------------------- *)
by rewrite leq_add2r.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PropertiesOfEDF.
policy_respects_sequential_tasks.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 338)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
============================
policy_respects_sequential_tasks
----------------------------------------------------------------------------- *)
Proof.
intros j1 j2 TSK ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 343)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
j1, j2 : Job
TSK : job_task j1 == job_task j2
ARR : job_arrival j1 <= job_arrival j2
============================
hep_job j1 j2
----------------------------------------------------------------------------- *)
move: TSK ⇒ /eqP TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 379)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
j1, j2 : Job
ARR : job_arrival j1 <= job_arrival j2
TSK : job_task j1 = job_task j2
============================
hep_job j1 j2
----------------------------------------------------------------------------- *)
unfold hep_job, EDF, job_deadline, job_deadline_from_task_deadline; rewrite TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 383)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
j1, j2 : Job
ARR : job_arrival j1 <= job_arrival j2
TSK : job_task j1 = job_task j2
============================
job_arrival j1 + task_deadline (job_task j2) <=
job_arrival j2 + task_deadline (job_task j2)
----------------------------------------------------------------------------- *)
by rewrite leq_add2r.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PropertiesOfEDF.
We add the above lemma into a "Hint Database" basic_facts, so Coq
will be able to apply them automatically.
Hint Resolve EDF_respects_sequential_tasks : basic_facts.