# Library prosa.analysis.facts.priority.classes

In this section, we prove some basic properties about priority relations.
Section BasicLemmas.

Consider any type of tasks ...

... and any type of jobs associated with these tasks.
Context {Job : JobType}.

Consider a JLFP policy that indicates a higher-or-equal priority relation.
Context `{JLFP_policy Job}.

First, we prove that another_hep_job relation is anti-reflexive.
Lemma another_hep_job_antireflexive :
j, ¬ another_hep_job j j.
Proof.
by movej /andP [_ /negP NEQ]; apply: NEQ.
Qed.

Second, we relate another_hep_job to same_task.
j j',
another_hep_job j j' = hep_job j j'.
Proof.
movej j' DIFF; rewrite /another_hep_job.
case: (hep_job j j'); [rewrite andTb|rewrite andFb //].
apply: (contra _ DIFF) ⇒ /eqP → {DIFF}.
by apply/eqP.
Qed.

We show that another_task_hep_job is "task-wise" anti-reflexive; that is, given two jobs j and j' from the same task, another_task_hep_job j' j is false.
tsk j j',
Proof.
movetsko j j' /eqP TSK1 /eqP TSK2 /andP [_ AA].
by move: AA; rewrite TSK1 TSK2 ⇒ /negP A; apply: A.
Qed.

j1 j2,
Proof.
movej1 j2.
by rewrite -andbA [X in _ && X]andb_idl//; apply: contraNN ⇒ /eqP→.
Qed.

another_hep_job can either come from another or the same task...
...but not both.
Lemma another_hep_job_exclusive :
j1 j2,
Proof.
by movej1 j2; rewrite !negb_and negbK; case: eqP; rewrite /= !orbT.
Qed.

End BasicLemmas.

In the following section, we establish properties of hp_task and ep_task auxiliary priority relations defined for FP policies. They are useful in proving properties of the ELF scheduling policy.
Consider any type of tasks and an FP policy that indicates a higher-or-equal priority relation on the tasks.

Section BasicProperties.

tsk1 tsk2,
Proof. by move⇒ ? ? /andP[]. Qed.

tsk1 tsk2,
Proof. by move⇒ ? ? /andP[]. Qed.

If a task has higher priority than another task, then the two do not have equal priority.
tsk1 tsk2,
Proof.
move⇒ ? ? /andP[_ ?].
by rewrite negb_and; apply/orP; right; apply/negPn.
Qed.

tsk1 tsk2,
Proof. by movex y; rewrite /ep_task andbC. Qed.

If a task tsk1 has higher-or-equal priority than a task tsk2, then tsk1 either has strictly higher priority than tsk2 or the two have equal priority.
tsk1 tsk2,
Proof. by move⇒ ? ?; rewrite /hp_task /ep_task -andb_orr orNb andbT. Qed.

End BasicProperties.

In the following section, we establish a useful property about the equal priority relation, which follows when the FP policy is reflexive.
Section ReflexiveProperties.

Assuming that the FP policy is reflexive ...

... it follows that the equal priority relation is reflexive.
Proof. by move⇒ ?; apply /andP; split. Qed.

End ReflexiveProperties.

Now we establish useful properties about the higher priority relation, which follow when the FP policy is transitive.
Section TransitiveProperties.

Assuming that the FP policy is transitive ...

... it follows that the higher priority relation is also transitive.
Proof.
movey x z /andP[hepxy Nhepyx] /andP[hepyz Nhepyz]; apply/andP; split.
{ exact: H_transitive hepyz. }
{ by apply: contraNN Nhepyx; exact: H_transitive. }
Qed.

Lemma hp_hep_trans :
tsk1 tsk2 tsk3,
Proof.
movex y z /andP[hepxy Nhepyx] hepyz; apply/andP; split.
{ exact: H_transitive hepyz. }
{ by apply: contraNN Nhepyx; exact: H_transitive. }
Qed.

Lemma hep_hp_trans :
tsk1 tsk2 tsk3,
Proof.
movex y z hepxy /andP[hepyz Nhepzy]; apply/andP; split.
{ exact: H_transitive hepyz. }
{ apply: contraNN Nhepzyhepzy; exact: H_transitive hepxy. }
Qed.

End TransitiveProperties.

Finally, we establish a useful property about the higher priority relation, which follows when the FP policy is total.
Section TotalProperties.

We assume that the FP policy is total.

Proof.
movex y; apply /idP/idP ⇒ [| /andP[//]].
moveNhepxy; apply /andP; split⇒ [|//].
have /orP[h | //] := H_total x y.
by exfalso; move/negP: Nhepxy.
Qed.

The converse also holds.
Proof. by movex y; rewrite -not_hep_hp_task negbK. Qed.

If a task tsk1 does not have higher priority than a task tsk2, then tsk1 either has lesser priority than tsk2 or the two have equal priority.
tsk1 tsk2,
Proof.
Qed.

End TotalProperties.

End FPRelationsProperties.

In the following section, we show that FP policies respect the sequential tasks hypothesis. It means that later-arrived jobs of a task don't have higher priority than earlier-arrived jobs of the same task (assuming that task priorities are reflexive).
Section FPRemarks.

Consider any type of tasks ...

... and any type of jobs associated with these tasks, ...
Context {Job : JobType}.

.. and assume that jobs have a cost and an arrival time.
Context `{JobArrival Job}.
Context `{JobCost Job}.

Consider any FP policy.

Proof.
moveREFL j1 j2 /eqP EQ LT.
by rewrite /hep_job /FP_to_JLFP EQ.
Qed.

End FPRemarks.

Section JLFPFP.
Consider any type of tasks ...

... and any type of jobs associated with these tasks.
Context {Job : JobType}.

Consider any pair of JLFP and FP policies that are compatible.
Context (JLFP : JLFP_policy Job) (FP : FP_policy Task).
Hypothesis H_compatible : JLFP_FP_compatible JLFP FP.

We restate JLFP_FP_compatible to make it easier to discover with Search. Here is the first part...
j1 j2,
hep_job j1 j2