Shortened, restructured, polished proofs

implementation/facts/ideal_uni/preemption_aware.v

@@ -123,11 +123,24 @@ Section NPUniprocessorScheduler.
     Hypothesis H_valid_preemption_behavior:
       valid_nonpreemptive_readiness RM.
 
-    (** Under this natural assumption, the generated schedule is valid. *)
+    (** First, we show that if a job is chosen from the list of backlogged jobs, then it must be ready. *)
+    Lemma choose_job_implies_job_ready:
+      forall t j,
+      choose_job t.+1 (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state t) t.+1) = Some j
+      -> job_ready schedule j t.+1.
+    Proof.
+      move=> t j IN.
+      move: (H_chooses_from_set _ _ _ IN).
+      rewrite mem_filter /backlogged => /andP [/andP [READY _]  _].
+      rewrite -(H_nonclairvoyant_job_readiness (schedule_up_to policy idle_state t) schedule j t.+1) //.
+      by apply schedule_up_to_identical_prefix.
+    Qed.
+
+    (** Next, we show that, under these natural assumptions, the generated schedule is valid. *)
     Theorem np_schedule_valid:
       valid_schedule schedule arr_seq.
     Proof.
-      rewrite /valid_schedule; split; move=> j t; rewrite scheduled_at_def /schedule /np_uni_schedule /generic_schedule.
+      split; move=> j t; rewrite scheduled_at_def /schedule /np_uni_schedule /generic_schedule.
       { elim: t => [/eqP | t'  IH /eqP].
         - rewrite schedule_up_to_def  /allocation_at  /prev_job_nonpreemptive => IN.
           move: (H_chooses_from_set _ _ _ IN).
@@ -143,16 +156,8 @@ Section NPUniprocessorScheduler.
           rewrite mem_filter /backlogged => /andP [/andP [READY _]  _].
           by rewrite -(H_nonclairvoyant_job_readiness (empty_schedule idle_state) schedule j 0).
         - rewrite schedule_up_to_def  /allocation_at /prev_job_nonpreemptive.
-          have JOB: choose_job t'.+1 (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state  t') t'.+1)
-                    = Some j
-                    -> job_ready schedule j t'.+1.
-          { move=> IN.
-            move: (H_chooses_from_set _ _ _ IN).
-            rewrite mem_filter /backlogged => /andP [/andP [READY _]  _].
-            rewrite -(H_nonclairvoyant_job_readiness (schedule_up_to policy idle_state t') schedule j t'.+1) //.
-            by apply schedule_up_to_identical_prefix. }
-          case: (schedule_up_to _ _ t' t') => [j' | IN]; last by apply JOB.
-          destruct (~~ job_preemptable j' _) eqn:NP => [EQ|IN]; last by apply JOB.
+          case: (schedule_up_to _ _ t' t') => [j' | IN]; last by apply choose_job_implies_job_ready.
+          destruct (~~ job_preemptable j' _) eqn:NP => [EQ|IN]; last by apply choose_job_implies_job_ready.
           apply H_valid_preemption_behavior.
           injection EQ => <-.
           move: NP.
@@ -196,13 +201,13 @@ Section NPUniprocessorScheduler.
         ~~ preemption_time schedule t.
     Proof.
       elim => [|t _]; first by rewrite /prev_job_nonpreemptive.
-      rewrite /schedule /np_uni_schedule /generic_schedule /preemption_time schedule_up_to_def /prefix /allocation_at => NP.
-      rewrite ifT //.
-      rewrite -pred_Sn.
-      move: NP. rewrite /prev_job_nonpreemptive.
+      rewrite /schedule /np_uni_schedule /generic_schedule /preemption_time
+              schedule_up_to_def /prefix /allocation_at => NP.
+      rewrite ifT // -pred_Sn.
+      move: NP; rewrite /prev_job_nonpreemptive.
       elim: (schedule_up_to policy idle_state t t) => // j.
-      have <-: service (schedule_up_to policy idle_state t) j t.+1
-               = service (fun t0 : instant => schedule_up_to policy idle_state t0 t0) j t.+1 => //.
+      have ->: (service (fun t0 : instant => schedule_up_to policy idle_state t0 t0) j t.+1 =
+                service (schedule_up_to policy idle_state t) j t.+1) => //.
       rewrite /service.
       apply equal_prefix_implies_same_service_during => t' /andP [_ BOUND].
       by rewrite (schedule_up_to_prefix_inclusion _ _ t' t).
@@ -227,8 +232,8 @@ Section NPUniprocessorScheduler.
     Lemma np_respects_preemption_model :
       schedule_respects_preemption_model arr_seq schedule.
     Proof.
-      move=> j; elim => [| t' IH];
-        first by rewrite service0 => ARR /negP NP; move: (H_valid_preemption_function j ARR) => P; exfalso.
+      move=> j.
+      elim => [| t' IH]; first by rewrite service0 => ARR /negP NP; move: (H_valid_preemption_function j ARR).
       move=> ARR NP.
       have: scheduled_at schedule j t'.
       { apply contraT => NOT_SCHED.