# Library prosa.implementation.priority.numeric_fixed_priority

Require Export prosa.model.priority.numeric_fixed_priority.

# Numeric Fixed Task Priorities

In this section, we define ascending numeric fixed priorities, where a larger numeric value indicates higher priority, and note some trivial facts about this interpretation of priority values.
Section PropertiesNFPA.
The instance numeric_fp_ascending assigns higher priority to tasks with higher numeric task_priority value.
#[local] Instance numeric_fp_ascending (Task : TaskType) `{TaskPriority Task} : FP_policy Task :=
{
hep_task (tsk1 tsk2 : Task) := task_priority tsk1 ≥ task_priority tsk2
}.
Consider any kind of tasks with specified priorities.
Context {Task : TaskType} `{TaskPriority Task}.
The concrete numeric_fp_ascending implementation is indeed an ascending numeric FP policy.
Fact NFPA_is_numeric_FP_ascending_policy :
policy_is_numeric_FP_ascending (numeric_fp_ascending Task).
Proof. by []. Qed.
The resulting priority policy is reflexive.
Fact NFPA_is_reflexive :
reflexive_task_priorities (numeric_fp_ascending Task).
Proof. by move⇒ ?; rewrite /hep_task /numeric_fp_ascending. Qed.
The resulting priority policy is transitive.
Fact NFPA_is_transitive :
transitive_task_priorities (numeric_fp_ascending Task).
Proof.
move⇒ y x z.
by rewrite /hep_task /numeric_fp_ascending ⇒ PRIO_yx PRIO_xy; lia.
Qed.
The resulting priority policy is total.
Fact NFPA_is_total :
total_task_priorities (numeric_fp_ascending Task).
Proof. by move⇒ j1 j2; apply: leq_total. Qed.
End PropertiesNFPA.
Next, we define descending numeric fixed priorities, where a larger numeric value indicates lower priority, and again note some trivial facts about this alternate interpretation of priority values.
Section PropertiesNFPD.
The instance numeric_fp_descending assigns lower priority to tasks with higher numeric task_priority value.
#[local] Instance numeric_fp_descending (Task : TaskType) `{TaskPriority Task} : FP_policy Task :=
{
hep_task (tsk1 tsk2 : Task) := task_priority tsk1 ≤ task_priority tsk2
}.
Consider any kind of tasks with specified priorities.
Context {Task : TaskType} `{TaskPriority Task}.
The concrete numeric_fp_descending implementation is indeed a descending numeric FP policy.
Fact NFPD_is_numeric_FP_descending_policy :
policy_is_numeric_FP_descending (numeric_fp_descending Task).
Proof. by []. Qed.
The resulting priority policy is reflexive.
Fact NFPD_is_reflexive :
reflexive_task_priorities (numeric_fp_descending Task).
Proof. by move⇒ ?; rewrite /hep_task /numeric_fp_descending. Qed.
The resulting priority policy is transitive.
Fact NFPD_is_transitive :
transitive_task_priorities (numeric_fp_descending Task).
Proof.
move⇒ y x z.
by rewrite /hep_task /numeric_fp_descending ⇒ PRIO_yx PRIO_xy; lia.
Qed.
The resulting priority policy is total.
Fact NFPD_is_total :
total_task_priorities (numeric_fp_descending Task).
Proof. by move⇒ j1 j2; apply: leq_total. Qed.
End PropertiesNFPD.
We add the above facts into the basic_rt_facts hint database so Coq can apply them automatically where needed.
Global Hint Resolve
NFPA_is_numeric_FP_ascending_policy
NFPA_is_reflexive
NFPA_is_transitive
NFPA_is_total
NFPD_is_numeric_FP_descending_policy
NFPD_is_reflexive
NFPD_is_transitive
NFPD_is_total
: basic_rt_facts.