Equivalence of EDF Predicates

This MR connects the two ways with which one can specify that a schedule is an EDF schedule in PROSA: the EDF_schedule predicate and the respects_policy_at_preemption_point - given the EDF priority policy - predicate. We connect these two predicates by showing that they're equivalent. We then restate the optimality proof of EDF schedules using the proven equivalence.

analysis/facts/behavior/arrivals.v

@@ -93,6 +93,19 @@ Section Arrived.
     now apply ready_implies_arrived.
   Qed.
 
+  (** Similarly, since backlogged jobs are by definition pending, any
+      backlogged job must be incomplete. *)
+  Lemma backlogged_implies_incomplete:
+    forall j t,
+      backlogged sched j t -> ~~ completed_by sched j t.
+  Proof.
+    move=> j t BACK.
+    have suff: pending sched j t.
+    - by move /andP => [_ INCOMP].
+    - apply; move: BACK => /andP [READY _].
+      by apply any_ready_job_is_pending.
+  Qed.
+
 End Arrived.
 
 (** In this section, we establish useful facts about arrival sequence prefixes. *)