add lemmas about job relations

analysis/facts/priority/classes.v

+Require Export prosa.model.priority.classes.
+
+(** In this section, we prove some basic properties about priority relations. *)
+Section BasicLemmas.
+  
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  
+  (** 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 :
+    forall j, ~ another_hep_job j j.
+  Proof.
+    by move => j /andP [_ /negP NEQ]; apply: NEQ.
+  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. *) 
+  Lemma another_task_hep_job_taskwise_antireflexive :
+    forall tsk j j',
+      job_of_task tsk j ->
+      job_of_task tsk j' ->
+      ~ another_task_hep_job j' j.
+  Proof.
+    move=> tsko j j' /eqP TSK1 /eqP TSK2 /andP [_ AA].
+    by move: AA; rewrite TSK1 TSK2 => /negP A; apply: A.
+  Qed.
+
+End BasicLemmas.

model/priority/classes.v

@@ -177,13 +177,13 @@ Section DerivedPriorityRleations.
   (** First, we introduce a relation that defines whether job [j1] has
       a higher-than-or-equal-priority than job [j2] and [j1] is not
       equal to [j2]. *)
-  Definition another_hep_job : JLFP_policy Job :=
+  Definition another_hep_job :=
     fun j1 j2 => hep_job j1 j2 && (j1 != j2).
 
   (** Next, we introduce a relation that defines whether a job [j1]
       has a higher-or-equal-priority than job [j2] and the task of
       [j1] is not equal to task of [j2]. *)
-  Definition another_task_hep_job : JLFP_policy Job :=
+  Definition another_task_hep_job :=
     fun j1 j2 => hep_job j1 j2 && (job_task j1 != job_task j2).
 
 End DerivedPriorityRleations.