Library prosa.model.priority.numeric_fixed_priority
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.priority.classes.
Numeric Fixed Task Priorities
Based on this parameter, we define the corresponding FP policy.
Instance NumericFP (Task : TaskType) `{TaskPriority Task} : FP_policy Task :=
{
hep_task (tsk1 tsk2 : Task) := task_priority tsk1 ≥ task_priority tsk2
}.
{
hep_task (tsk1 tsk2 : Task) := task_priority tsk1 ≥ task_priority tsk2
}.
In this section, we prove a few basic properties of numeric fixed priorities.
Consider any kind of tasks with specified priorities...
...and jobs stemming from these tasks.
The resulting priority policy is reflexive.
Lemma NFP_is_reflexive : reflexive_priorities.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
Task : TaskType
H : TaskPriority Task
Job : JobType
H0 : JobTask Job Task
============================
reflexive_priorities
----------------------------------------------------------------------------- *)
Proof. by move⇒ ?; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFP.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
Task : TaskType
H : TaskPriority Task
Job : JobType
H0 : JobTask Job Task
============================
reflexive_priorities
----------------------------------------------------------------------------- *)
Proof. by move⇒ ?; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFP.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
The resulting priority policy is transitive.
Lemma NFP_is_transitive : transitive_priorities.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 51)
Task : TaskType
H : TaskPriority Task
Job : JobType
H0 : JobTask Job Task
============================
transitive_priorities
----------------------------------------------------------------------------- *)
Proof.
move⇒ t y x z.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 57)
Task : TaskType
H : TaskPriority Task
Job : JobType
H0 : JobTask Job Task
t : instant
y, x, z : Job
============================
hep_job_at t x y -> hep_job_at t y z -> hep_job_at t x z
----------------------------------------------------------------------------- *)
rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
Task : TaskType
H : TaskPriority Task
Job : JobType
H0 : JobTask Job Task
t : instant
y, x, z : Job
============================
task_priority (job_task y) <= task_priority (job_task x) ->
task_priority (job_task z) <= task_priority (job_task y) ->
task_priority (job_task z) <= task_priority (job_task x)
----------------------------------------------------------------------------- *)
by move⇒ PRIO_yx PRIO_zy; apply leq_trans with (n := task_priority (job_task y)).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 51)
Task : TaskType
H : TaskPriority Task
Job : JobType
H0 : JobTask Job Task
============================
transitive_priorities
----------------------------------------------------------------------------- *)
Proof.
move⇒ t y x z.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 57)
Task : TaskType
H : TaskPriority Task
Job : JobType
H0 : JobTask Job Task
t : instant
y, x, z : Job
============================
hep_job_at t x y -> hep_job_at t y z -> hep_job_at t x z
----------------------------------------------------------------------------- *)
rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
Task : TaskType
H : TaskPriority Task
Job : JobType
H0 : JobTask Job Task
t : instant
y, x, z : Job
============================
task_priority (job_task y) <= task_priority (job_task x) ->
task_priority (job_task z) <= task_priority (job_task y) ->
task_priority (job_task z) <= task_priority (job_task x)
----------------------------------------------------------------------------- *)
by move⇒ PRIO_yx PRIO_zy; apply leq_trans with (n := task_priority (job_task y)).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
The resulting priority policy is total.
Lemma NFP_is_total : total_priorities.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
Task : TaskType
H : TaskPriority Task
Job : JobType
H0 : JobTask Job Task
============================
total_priorities
----------------------------------------------------------------------------- *)
Proof. by move⇒ t j1 j2; apply leq_total.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End Properties.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
Task : TaskType
H : TaskPriority Task
Job : JobType
H0 : JobTask Job Task
============================
total_priorities
----------------------------------------------------------------------------- *)
Proof. by move⇒ t j1 j2; apply leq_total.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End Properties.
We add the above lemmas into a "Hint Database" basic_facts, so Coq
will be able to apply them automatically.
Hint Resolve
NFP_is_reflexive
NFP_is_transitive
NFP_is_total
: basic_facts.
NFP_is_reflexive
NFP_is_transitive
NFP_is_total
: basic_facts.