make a few cosmetic tweaks in the EDF optimality proof

As discussed in #57.

restructuring/analysis/edf/optimality.v

@@ -6,6 +6,12 @@ From rt.restructuring.analysis Require Import schedulability transform.facts.edf
     (assuming an ideal uniprocessor), then there is also an EDF
     schedule in which all deadlines are met. *)
 
+(** The following results assume ideal uniprocessor schedules... *)
+From rt.restructuring.model.processor Require ideal.
+(** ... and the basic (i.e., Liu & Layland) readiness model under which any
+    pending job is ready. *)
+From rt.restructuring.model.readiness Require basic.
+
 Section Optimality.
   (** For any given type of jobs... *)
   Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
@@ -40,8 +46,10 @@ Section Optimality.
 
 End Optimality.
 
-(** We further state a weaker notion of the above optimality claim
-    that avoids a dependency on a given arrival sequence. *)
+(** We further state a weaker notion of the above optimality claim that avoids
+    a dependency on a given arrival sequence. Specifically, it establishes
+    that, given a reference schedule without deadline misses, there exists an
+    EDF schedule of the same jobs in which no deadlines are missed. *)
 Section WeakOptimality.
 
   (** For any given type of jobs,... *)

restructuring/analysis/transform/edf_trans.v

@@ -45,7 +45,7 @@ Section EDFTransformation.
      t1. *)
   Definition make_edf_at (sched: SchedType) (t1: instant): SchedType :=
     match sched t1 with
-    | None => sched (** leave idle instants alone *)
+    | None => sched (* leave idle instants alone *)
     | Some j =>
       let
         t2 := find_swap_candidate sched t1 j

restructuring/analysis/transform/facts/edf_opt.v

@@ -12,9 +12,9 @@ From rt.util Require Import tactics nat.
     schedule. *)
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
-From rt.restructuring.model.processor Require Export ideal.
+From rt.restructuring.model.processor Require Import ideal.
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-From rt.restructuring.model.readiness Require Export basic.
+From rt.restructuring.model.readiness Require Import basic.
 
 (** We start by analyzing the helper function [find_swap_candidate],
     which is a problem-specific wrapper around [search_arg]. *)