From 6b15dbb0087ad1fffc1ae9fed1dbbd2f26f3c4ad Mon Sep 17 00:00:00 2001
From: Marco Maida <mmaida@mpi-sws.org>
Date: Fri, 12 Mar 2021 10:18:45 +0100
Subject: [PATCH] Now -> by
---
.../facts/ideal_uni/preemption_aware.v | 20 +++++++++----------
1 file changed, 10 insertions(+), 10 deletions(-)
diff --git a/implementation/facts/ideal_uni/preemption_aware.v b/implementation/facts/ideal_uni/preemption_aware.v
index de4b6ca15..d1373f7a6 100644
--- a/implementation/facts/ideal_uni/preemption_aware.v
+++ b/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) //.
--
GitLab