Preemption model compliance

In this MR, we prove that the ideal uniprocessor schedules that are implemented in prosa.implementation.definitions.ideal_uni_scheduler respect the preemption model.

implementation/facts/ideal_uni/preemption_aware.v

@@ -63,7 +63,7 @@ Section NPUniprocessorScheduler.
       elim: (sched t) => [j'|]; last by apply H_non_idling.
       rewrite if_neg.
       elim: (job_preemptable j' (service sched j' t.+1)); first by apply H_non_idling.
-      now discriminate.
+      by discriminate.
     Qed.
 
     (** As a stepping stone, we observe that the generated schedule is idle at
@@ -83,7 +83,7 @@ Section NPUniprocessorScheduler.
       rewrite /identical_prefix => x.
       rewrite ltnS leq_eqVlt => /orP [/eqP ->|LT]; last first.
       { elim: t LT IDLE NONE => // => h IH LT_x IDLE NONE.
-        now apply schedule_up_to_prefix_inclusion. }
+        by apply schedule_up_to_prefix_inclusion. }
       { elim: t IDLE NONE => [IDLE _| t' _ _ ->]; last by rewrite schedule_up_to_empty.
         rewrite /schedule_up_to replace_at_def.
         rewrite /allocation_at /prev_job_nonpreemptive IDLE H_non_idling //. }
@@ -100,7 +100,7 @@ Section NPUniprocessorScheduler.
       have NON_EMPTY: j \in jobs_backlogged_at arr_seq schedule t by apply mem_backlogged_jobs => //.
       clear BACKLOGGED.
       move: (idle_schedule_no_backlogged_jobs t IDLE) => EMPTY.
-      now rewrite EMPTY in NON_EMPTY.
+      by rewrite EMPTY in NON_EMPTY.
     Qed.
 
   End WorkConservation.
@@ -131,17 +131,17 @@ Section NPUniprocessorScheduler.
       { elim: t => [/eqP | t'  IH /eqP].
         - rewrite schedule_up_to_def  /allocation_at  /prev_job_nonpreemptive => IN.
           move: (H_chooses_from_set _ _ _ IN).
-          now apply backlogged_job_arrives_in.
+          by apply backlogged_job_arrives_in.
         - rewrite schedule_up_to_def  /allocation_at.
           case: (prev_job_nonpreemptive  (schedule_up_to _ _ t') t'.+1) => [|IN];
                 first by rewrite -pred_Sn => SCHED; apply IH; apply /eqP.
           move: (H_chooses_from_set _ _ _ IN).
-          now apply backlogged_job_arrives_in. }
+          by apply backlogged_job_arrives_in. }
       { elim: t => [/eqP |t'  IH /eqP].
         - rewrite schedule_up_to_def  /allocation_at  /prev_job_nonpreemptive => IN.
           move: (H_chooses_from_set _ _ _ IN).
           rewrite mem_filter /backlogged => /andP [/andP [READY _]  _].
-          now rewrite -(H_nonclairvoyant_job_readiness (empty_schedule idle_state) schedule j 0).
+          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
@@ -160,7 +160,7 @@ Section NPUniprocessorScheduler.
                     = service (fun t : instant => schedule_up_to policy idle_state t t) j' t'.+1) => //.
           rewrite /service.
           apply equal_prefix_implies_same_service_during => t /andP [_ BOUND].
-          now rewrite (schedule_up_to_prefix_inclusion _  _ t t'). }
+          by rewrite (schedule_up_to_prefix_inclusion _  _ t t'). }
     Qed.
 
   End Validity.
@@ -183,7 +183,7 @@ Section NPUniprocessorScheduler.
       elim => [|t _] //  NP.
       rewrite schedule_up_to_def /allocation_at /policy /allocation_at.
       rewrite ifT // -pred_Sn.
-      now rewrite schedule_up_to_widen.
+      by rewrite schedule_up_to_widen.
     Qed.
 
     (** From this, we conclude that the predicate used to determine whether the
@@ -205,7 +205,7 @@ Section NPUniprocessorScheduler.
                = service (fun t0 : instant => schedule_up_to policy idle_state t0 t0) j t.+1 => //.
       rewrite /service.
       apply equal_prefix_implies_same_service_during => t' /andP [_ BOUND].
-      now rewrite (schedule_up_to_prefix_inclusion _ _ t' t).
+      by rewrite (schedule_up_to_prefix_inclusion _ _ t' t).
     Qed.
 
   End PreemptionTimes.
@@ -234,7 +234,7 @@ Section NPUniprocessorScheduler.
       { apply contraT => NOT_SCHED.
         move: (not_scheduled_implies_no_service _ _ _ NOT_SCHED) => NO_SERVICE.
         rewrite -(service_last_plus_before) NO_SERVICE addn0 in NP; apply IH in NP => //.
-        now move /negP in NOT_SCHED. }
+        by move /negP in NOT_SCHED. }
       rewrite !scheduled_at_def /schedule/np_uni_schedule/generic_schedule => /eqP SCHED.
       rewrite -SCHED (schedule_up_to_prefix_inclusion _ _ t' t'.+1) // np_job_remains_scheduled //.
       rewrite /prev_job_nonpreemptive SCHED (identical_prefix_service _ schedule) //.