EDF optimality argument

As a Coq/sslreflect/Prosa exercise, and to get a feel for the restructured foundation, I've been working on a proof of the classic EDF optimality argument that proceeds by swapping pairs of jobs that violate EDF. While this is not particularly useful (i.e., it's not essential for anything else on our radar at the moment), it's a nice classic result that I'd like to integrate anyway.

As part of this work, I've also cleaned up a few things in the foundation and added some utility lemmas.

Review and feedback would be much appreciated, both on the proof itself and the organization/naming of the files/lemmas/defs. I'm still learning, so if I'm doing something "wrong" or strangely in some proof, please point it out.

As a starting point, the main optimality claim may be found in: rt.restructuring.analysis.edf.optimality.

CC: @sbozhko @mlesourd @sophie @proux

restructuring/analysis/edf/optimality.v

+From rt.restructuring.model Require Export schedule.edf.
+From rt.restructuring.analysis Require Import schedulability transform.facts.edf_opt.
+
+(** This file contains the theorem that states the famous EDF
+    optimality result: if there is any way to meet all deadlines
+    (assuming an ideal uniprocessor), then there is also an EDF
+    schedule in which all deadlines are met. *)
+
+Section Optimality.
+  (* For any given type of jobs... *)
+  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
+  
+  (* ... and any valid job arrival sequence. *)
+  Variable arr_seq: arrival_sequence Job.
+  Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.
+
+  (* We observe that EDF is optimal in the sense that, if there exists
+     any schedule in which all jobs of arr_seq meet their deadline,
+     then there also exists an EDF schedule in which all deadlines are
+     met. *)
+  Theorem EDF_optimality:
+    (exists any_sched : schedule (ideal.processor_state Job),
+        valid_schedule any_sched arr_seq /\
+        all_deadlines_of_arrivals_met arr_seq any_sched) ->
+    exists edf_sched : schedule (ideal.processor_state Job),
+        valid_schedule edf_sched arr_seq /\
+        all_deadlines_of_arrivals_met arr_seq edf_sched /\
+        is_EDF_schedule edf_sched.
+  Proof.
+    move=> [sched [[COME [ARR COMP]] DL_ARR_MET]].
+    move: (all_deadlines_met_in_valid_schedule _ _ COME DL_ARR_MET) => DL_MET.
+    set sched' := edf_transform sched.
+    exists sched'. split; last split.
+    - by apply edf_schedule_is_valid.
+    - by apply edf_schedule_meets_all_deadlines_wrt_arrivals.
+    - by apply edf_transform_ensures_edf.
+  Qed.
+
+End Optimality.
+
+(** We further state a weaker notion of the above optimality claim
+    that avoids a dependency on a given arrival sequence. *)
+Section WeakOptimality.
+
+  (* For any given type of jobs,... *)
+  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
+
+  (* ...if we have a well-behaved schedule in which no deadlines are missed,... *)
+  Variable any_sched: schedule (ideal.processor_state Job).
+  Hypothesis H_must_arrive: jobs_must_arrive_to_execute any_sched.
+  Hypothesis H_completed_dont_execute: completed_jobs_dont_execute any_sched.
+  Hypothesis H_all_deadlines_met: all_deadlines_met any_sched.
+
+  (* ...then there also exists a corresponding EDF schedule in which
+     no deadlines are missed (and in which exactly the same set of
+     jobs is scheduled, as ensured by the last clause). *)
+  Theorem weak_EDF_optimality:
+    exists edf_sched : schedule (ideal.processor_state Job),
+      jobs_must_arrive_to_execute edf_sched /\
+      completed_jobs_dont_execute edf_sched /\
+      all_deadlines_met edf_sched /\
+      is_EDF_schedule edf_sched /\
+      forall j,
+          (exists t,  scheduled_at any_sched j t) <->
+          (exists t', scheduled_at edf_sched j t').
+  Proof.
+    set sched' := edf_transform any_sched.
+    exists sched'. repeat split.
+    - by apply edf_transform_jobs_must_arrive.
+    - by apply edf_transform_completed_jobs_dont_execute.
+    - by apply edf_transform_deadlines_met.
+    - by apply edf_transform_ensures_edf.
+    - by move=> [t SCHED_j]; apply edf_transform_job_scheduled' with (t0 := t).
+    - by move=> [t SCHED_j]; apply edf_transform_job_scheduled with (t0 := t).
+  Qed.
+
+End WeakOptimality.