# Library prosa.analysis.facts.priority.fp

Require Export prosa.model.priority.fp.
In this section, we state and prove some basic facts about job-level policies that behave as fixed-priority policies.
Section FPPolicyFacts.
Consider any type of tasks ...
Context {Task : TaskType}.
... and jobs of these tasks.
Context {Job : JobType} `{JobTask Job Task}.
Consider any arbitrary FP policy ...
Context {FP : FP_policy Task}.
... and a JLFP policy that behaves like it.
Context {JLFP : JLFP_policy Job}.
Hypothesis H_policy_is_FP : policy_is_FP FP JLFP.
Under such a policy, higher-or-equal job priority implies higher-or-equal priority of the corresponding tasks.
Fact FP_policy_task_priority_order :
∀ j j',
@hep_job _ JLFP j j' → hep_task (job_task j) (job_task j').
Conversely, strict task priority implies higher-or-equal job priority.
Fact FP_policy_higher_priority_task :
∀ j j',
hp_task (job_task j) (job_task j') → @hep_job _ JLFP j j'.
FP-like job priorities are reflexive by definition.
Fact FP_policy_is_reflexive : reflexive_job_priorities JLFP.
FP-like job priorities are transitive by definition.
Fact FP_policy_is_transitive : transitive_job_priorities JLFP.
FP-like job priorities are total by definition.
Fact FP_policy_is_total : total_job_priorities JLFP.
End FPPolicyFacts.
We add the generally useful FP-policy facts into the basic_rt_facts hint database, so Coq can apply them automatically where needed.
Global Hint Resolve
FP_policy_is_reflexive
FP_policy_is_transitive
FP_policy_is_total
: basic_rt_facts.