add alternate interpretation of numeric priorities

To complement the existing interpretation, add one more instance of
numeric fixed priority that assigns higher priority to lower numeric
values.

model/priority/numeric_fixed_priority.v

@@ -11,14 +11,62 @@ Require Export prosa.model.priority.classes.
     to a numeric priority value. *)
 Class TaskPriority (Task : TaskType) := task_priority : Task -> nat.
 
-(** 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
-}.
+(** Based on this parameter, we define two corresponding FP policies. In one
+    instance, a lower numeric value indicates lower priority, while in the other
+    instance, a lower numeric value indicates higher priority. Both these
+    interpretations can be found in practice and in the literature. For example,
+    Linux uses "higher numeric value <-> higher priority", whereas many papers
+    assume "lower numeric value <-> higher priority". *)
 
-(** In this section, we prove a few basic properties of numeric fixed priorities. *)
-Section Properties.
+(** 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 [NumericFPAscending] assigns higher priority to tasks with
+      higher numeric [task_priority] value. *)
+  #[local] Instance NumericFPAscending (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}.
+  Context `{TaskPriority Task}.
+
+  (** ...and jobs stemming from these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+
+  (** The resulting priority policy is reflexive. *)
+  Lemma NFPA_is_reflexive : reflexive_priorities.
+  Proof.  by move=> ?; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFPAscending. Qed.
+
+  (** The resulting priority policy is transitive. *)
+  Lemma NFPA_is_transitive : transitive_priorities.
+  Proof.
+    move=> t y x z.
+    rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFPAscending.
+    by move=> PRIO_yx PRIO_zy; apply leq_trans with (n := task_priority (job_task y)).
+  Qed.
+
+  (** The resulting priority policy is total. *)
+  Lemma NFPA_is_total : total_priorities.
+  Proof. by move=> t 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 [NumericFPDescending] assigns lower priority to tasks with
+      higher numeric [task_priority] value. *)
+  #[local] Instance NumericFPDescending (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}.
@@ -29,28 +77,31 @@ Section Properties.
   Context `{JobTask Job Task}.
 
   (** The resulting priority policy is reflexive. *)
-  Lemma NFP_is_reflexive : reflexive_priorities.
-  Proof. by move=> ?; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFP. Qed.
+  Lemma NFPD_is_reflexive : reflexive_priorities.
+  Proof.  by  move=> ?; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFPDescending. Qed.
 
   (** The resulting priority policy is transitive. *)
-  Lemma NFP_is_transitive : transitive_priorities.
+  Lemma NFPD_is_transitive : transitive_priorities.
   Proof.
     move=> t y x z.
-    rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFP.
+    rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFPDescending.
     by move=> PRIO_yx PRIO_zy; apply leq_trans with (n := task_priority (job_task y)).
   Qed.
 
   (** The resulting priority policy is total. *)
-  Lemma NFP_is_total : total_priorities.
+  Lemma NFPD_is_total : total_priorities.
   Proof. by move=> t j1 j2; apply leq_total. Qed.
 
-End Properties.
+End PropertiesNFPD.
 
 (** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
     will be able to apply them automatically. *)
 Global Hint Resolve
-     NFP_is_reflexive
-     NFP_is_transitive
-     NFP_is_total
+     NFPA_is_reflexive
+     NFPA_is_transitive
+     NFPA_is_total
+     NFPD_is_reflexive
+     NFPD_is_transitive
+     NFPD_is_total
   : basic_rt_facts.