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/edf_definitions.v

@@ -80,14 +80,15 @@ Section Equivalence.
     case (boolP (j == j_hp)); first by move /eqP => EQ; subst.
     move /neqP => NEQ.
     exploit (H_priority_driven j j_hp t) => //.
-    + by apply (H_from_arr_seq _ _ SCHED').
-    + by rewrite /preemption_time/job_preemptable/fully_preemptive_model; destruct (sched t) => //.
-    + apply /andP; split => //.
-      * apply /andP; split => //.
+    { by apply (H_from_arr_seq _ _ SCHED'). }
+    { by rewrite /preemption_time; destruct (sched t). }
+    { apply /andP; split => //.
+      - apply /andP; split => //.
         apply (incompletion_monotonic _ j _ _ LEQ).
-        by apply (scheduled_implies_not_completed _ _ H_completed_jobs_dont_execute ideal_proc_model_ensures_ideal_progress).
-      * apply /negP; move => SCHED''.
-        by exploit (ideal_proc_model_is_a_uniprocessor_model j j_hp sched t) => //.
+        apply scheduled_implies_not_completed => //.
+        by apply ideal_proc_model_ensures_ideal_progress.
+      - apply /negP; move => SCHED''.
+        by exploit (ideal_proc_model_is_a_uniprocessor_model j j_hp sched t). }
   Qed.
 
   (** From the two preceding lemmas, it follows immediately that the two EDF