Library rt.restructuring.analysis.transform.facts.replace_at
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.restructuring.analysis.transform Require Export swap.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.util Require Import nat.
In this file, we make a few simple observations about schedules with
replacements.
For any given type of jobs...
... and any given type of processor states, ...
...consider any given reference schedule.
Suppose we are given a specific time [t'] ...
...and a replacement state [state].
In the following, let sched' denote the schedule with replacement at time
t'.
We begin with the trivial observation that the schedule doesn't change at
other times.
Lemma rest_of_schedule_invariant:
∀ t, t ≠ t' → sched' t = sched t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 39)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
============================
forall t : instant, t <> t' -> sched' t = sched t
----------------------------------------------------------------------------- *)
Proof.
move ⇒ t DIFF.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 41)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t : instant
DIFF : t <> t'
============================
sched' t = sched t
----------------------------------------------------------------------------- *)
rewrite /sched' /replace_at.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t : instant
DIFF : t <> t'
============================
(if t' == t then nstate else sched t) = sched t
----------------------------------------------------------------------------- *)
case (t' == t) eqn:TT; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t : instant
DIFF : t <> t'
TT : (t' == t) = true
============================
nstate = sched t
----------------------------------------------------------------------------- *)
by move/eqP in TT; rewrite TT in DIFF; contradiction.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t, t ≠ t' → sched' t = sched t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 39)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
============================
forall t : instant, t <> t' -> sched' t = sched t
----------------------------------------------------------------------------- *)
Proof.
move ⇒ t DIFF.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 41)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t : instant
DIFF : t <> t'
============================
sched' t = sched t
----------------------------------------------------------------------------- *)
rewrite /sched' /replace_at.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t : instant
DIFF : t <> t'
============================
(if t' == t then nstate else sched t) = sched t
----------------------------------------------------------------------------- *)
case (t' == t) eqn:TT; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t : instant
DIFF : t <> t'
TT : (t' == t) = true
============================
nstate = sched t
----------------------------------------------------------------------------- *)
by move/eqP in TT; rewrite TT in DIFF; contradiction.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
As a result, the service in intervals that do not intersect with t' is
invariant, too.
Lemma service_at_other_times_invariant:
∀ t1 t2,
t2 ≤ t' ∨ t' < t1 →
∀ j,
service_during sched j t1 t2
=
service_during sched' j t1 t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 53)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
============================
forall t1 t2 : nat,
t2 <= t' \/ t' < t1 ->
forall j : Job,
service_during sched j t1 t2 = service_during sched' j t1 t2
----------------------------------------------------------------------------- *)
Proof.
move ⇒ t1 t2 SWAP_EXCLUDED j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 57)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
SWAP_EXCLUDED : t2 <= t' \/ t' < t1
j : Job
============================
service_during sched j t1 t2 = service_during sched' j t1 t2
----------------------------------------------------------------------------- *)
rewrite /service_during /service_at.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 71)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
SWAP_EXCLUDED : t2 <= t' \/ t' < t1
j : Job
============================
\sum_(t1 <= t < t2) service_in j (sched t) =
\sum_(t1 <= t < t2) service_in j (sched' t)
----------------------------------------------------------------------------- *)
apply eq_big_nat ⇒ t /andP [le_t1t lt_tt2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 113)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
SWAP_EXCLUDED : t2 <= t' \/ t' < t1
j : Job
t : nat
le_t1t : t1 <= t
lt_tt2 : t < t2
============================
service_in j (sched t) = service_in j (sched' t)
----------------------------------------------------------------------------- *)
rewrite rest_of_schedule_invariant//.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 118)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
SWAP_EXCLUDED : t2 <= t' \/ t' < t1
j : Job
t : nat
le_t1t : t1 <= t
lt_tt2 : t < t2
============================
t <> t'
----------------------------------------------------------------------------- *)
eapply point_not_in_interval; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 149)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
SWAP_EXCLUDED : t2 <= t' \/ t' < t1
j : Job
t : nat
le_t1t : t1 <= t
lt_tt2 : t < t2
============================
t1 <= t < t2
----------------------------------------------------------------------------- *)
apply /andP; by split.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t1 t2,
t2 ≤ t' ∨ t' < t1 →
∀ j,
service_during sched j t1 t2
=
service_during sched' j t1 t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 53)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
============================
forall t1 t2 : nat,
t2 <= t' \/ t' < t1 ->
forall j : Job,
service_during sched j t1 t2 = service_during sched' j t1 t2
----------------------------------------------------------------------------- *)
Proof.
move ⇒ t1 t2 SWAP_EXCLUDED j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 57)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
SWAP_EXCLUDED : t2 <= t' \/ t' < t1
j : Job
============================
service_during sched j t1 t2 = service_during sched' j t1 t2
----------------------------------------------------------------------------- *)
rewrite /service_during /service_at.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 71)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
SWAP_EXCLUDED : t2 <= t' \/ t' < t1
j : Job
============================
\sum_(t1 <= t < t2) service_in j (sched t) =
\sum_(t1 <= t < t2) service_in j (sched' t)
----------------------------------------------------------------------------- *)
apply eq_big_nat ⇒ t /andP [le_t1t lt_tt2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 113)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
SWAP_EXCLUDED : t2 <= t' \/ t' < t1
j : Job
t : nat
le_t1t : t1 <= t
lt_tt2 : t < t2
============================
service_in j (sched t) = service_in j (sched' t)
----------------------------------------------------------------------------- *)
rewrite rest_of_schedule_invariant//.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 118)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
SWAP_EXCLUDED : t2 <= t' \/ t' < t1
j : Job
t : nat
le_t1t : t1 <= t
lt_tt2 : t < t2
============================
t <> t'
----------------------------------------------------------------------------- *)
eapply point_not_in_interval; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 149)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
SWAP_EXCLUDED : t2 <= t' \/ t' < t1
j : Job
t : nat
le_t1t : t1 <= t
lt_tt2 : t < t2
============================
t1 <= t < t2
----------------------------------------------------------------------------- *)
apply /andP; by split.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Next, we consider the amount of service received in intervals that do span
across the replacement point. We can relate the service received in the
original and the new schedules by adding the service in the respective
"missing" state...
Lemma service_delta:
∀ t1 t2,
t1 ≤ t' < t2 →
∀ j,
service_during sched j t1 t2 + service_at sched' j t'
=
service_during sched' j t1 t2 + service_at sched j t'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
============================
forall t1 t2 : nat,
t1 <= t' < t2 ->
forall j : Job,
service_during sched j t1 t2 + service_at sched' j t' =
service_during sched' j t1 t2 + service_at sched j t'
----------------------------------------------------------------------------- *)
Proof.
move ⇒ t1 t2 TIMES j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 79)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
TIMES : t1 <= t' < t2
j : Job
============================
service_during sched j t1 t2 + service_at sched' j t' =
service_during sched' j t1 t2 + service_at sched j t'
----------------------------------------------------------------------------- *)
rewrite -(service_split_at_point sched _ _ t' _) //
-(service_split_at_point sched' _ _ t' _) //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 144)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
TIMES : t1 <= t' < t2
j : Job
============================
service_during sched j t1 t' + service_at sched j t' +
service_during sched j t'.+1 t2 + service_at sched' j t' =
service_during sched' j t1 t' + service_at sched' j t' +
service_during sched' j t'.+1 t2 + service_at sched j t'
----------------------------------------------------------------------------- *)
by rewrite !service_at_other_times_invariant -/sched'; [ring | right | left].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t1 t2,
t1 ≤ t' < t2 →
∀ j,
service_during sched j t1 t2 + service_at sched' j t'
=
service_during sched' j t1 t2 + service_at sched j t'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
============================
forall t1 t2 : nat,
t1 <= t' < t2 ->
forall j : Job,
service_during sched j t1 t2 + service_at sched' j t' =
service_during sched' j t1 t2 + service_at sched j t'
----------------------------------------------------------------------------- *)
Proof.
move ⇒ t1 t2 TIMES j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 79)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
TIMES : t1 <= t' < t2
j : Job
============================
service_during sched j t1 t2 + service_at sched' j t' =
service_during sched' j t1 t2 + service_at sched j t'
----------------------------------------------------------------------------- *)
rewrite -(service_split_at_point sched _ _ t' _) //
-(service_split_at_point sched' _ _ t' _) //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 144)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
TIMES : t1 <= t' < t2
j : Job
============================
service_during sched j t1 t' + service_at sched j t' +
service_during sched j t'.+1 t2 + service_at sched' j t' =
service_during sched' j t1 t' + service_at sched' j t' +
service_during sched' j t'.+1 t2 + service_at sched j t'
----------------------------------------------------------------------------- *)
by rewrite !service_at_other_times_invariant -/sched'; [ring | right | left].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
...which we can also rewrite as follows.
Corollary service_in_replaced:
∀ t1 t2,
t1 ≤ t' < t2 →
∀ j,
service_during sched' j t1 t2
=
service_during sched j t1 t2 + service_at sched' j t' - service_at sched j t'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 97)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
============================
forall t1 t2 : nat,
t1 <= t' < t2 ->
forall j : Job,
service_during sched' j t1 t2 =
service_during sched j t1 t2 + service_at sched' j t' -
service_at sched j t'
----------------------------------------------------------------------------- *)
Proof. move ⇒ t1 t2 ORDER j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 101)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
ORDER : t1 <= t' < t2
j : Job
============================
service_during sched' j t1 t2 =
service_during sched j t1 t2 + service_at sched' j t' -
service_at sched j t'
----------------------------------------------------------------------------- *)
by rewrite service_delta// addnK.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t1 t2,
t1 ≤ t' < t2 →
∀ j,
service_during sched' j t1 t2
=
service_during sched j t1 t2 + service_at sched' j t' - service_at sched j t'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 97)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
============================
forall t1 t2 : nat,
t1 <= t' < t2 ->
forall j : Job,
service_during sched' j t1 t2 =
service_during sched j t1 t2 + service_at sched' j t' -
service_at sched j t'
----------------------------------------------------------------------------- *)
Proof. move ⇒ t1 t2 ORDER j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 101)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
t1, t2 : nat
ORDER : t1 <= t' < t2
j : Job
============================
service_during sched' j t1 t2 =
service_during sched j t1 t2 + service_at sched' j t' -
service_at sched j t'
----------------------------------------------------------------------------- *)
by rewrite service_delta// addnK.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
As another simple invariant (useful for case analysis), we observe that if
a job is scheduled neither in the replaced nor in the new state, then at
any time it receives exactly the same amount of service in the new
schedule with replacements as in the original schedule.
Lemma service_at_of_others_invariant (j: Job):
~~ scheduled_in j (sched' t') →
~~ scheduled_in j (sched t') →
∀ t,
service_at sched j t = service_at sched' j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 114)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
============================
~~ scheduled_in j (sched' t') ->
~~ scheduled_in j (sched t') ->
forall t : instant, service_at sched j t = service_at sched' j t
----------------------------------------------------------------------------- *)
Proof.
move⇒ NOT_IN_NEW NOT_IN_OLD t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 117)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
NOT_IN_NEW : ~~ scheduled_in j (sched' t')
NOT_IN_OLD : ~~ scheduled_in j (sched t')
t : instant
============================
service_at sched j t = service_at sched' j t
----------------------------------------------------------------------------- *)
rewrite /service_at.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 124)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
NOT_IN_NEW : ~~ scheduled_in j (sched' t')
NOT_IN_OLD : ~~ scheduled_in j (sched t')
t : instant
============================
service_in j (sched t) = service_in j (sched' t)
----------------------------------------------------------------------------- *)
case: (boolP (t == t')) ⇒ /eqP TT.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 211)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
NOT_IN_NEW : ~~ scheduled_in j (sched' t')
NOT_IN_OLD : ~~ scheduled_in j (sched t')
t : instant
TT : t = t'
============================
service_in j (sched t) = service_in j (sched' t)
subgoal 2 (ID 212) is:
service_in j (sched t) = service_in j (sched' t)
----------------------------------------------------------------------------- *)
- rewrite !TT !service_implies_scheduled //; by apply negbTE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 212)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
NOT_IN_NEW : ~~ scheduled_in j (sched' t')
NOT_IN_OLD : ~~ scheduled_in j (sched t')
t : instant
TT : t <> t'
============================
service_in j (sched t) = service_in j (sched' t)
----------------------------------------------------------------------------- *)
- rewrite rest_of_schedule_invariant//.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
~~ scheduled_in j (sched' t') →
~~ scheduled_in j (sched t') →
∀ t,
service_at sched j t = service_at sched' j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 114)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
============================
~~ scheduled_in j (sched' t') ->
~~ scheduled_in j (sched t') ->
forall t : instant, service_at sched j t = service_at sched' j t
----------------------------------------------------------------------------- *)
Proof.
move⇒ NOT_IN_NEW NOT_IN_OLD t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 117)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
NOT_IN_NEW : ~~ scheduled_in j (sched' t')
NOT_IN_OLD : ~~ scheduled_in j (sched t')
t : instant
============================
service_at sched j t = service_at sched' j t
----------------------------------------------------------------------------- *)
rewrite /service_at.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 124)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
NOT_IN_NEW : ~~ scheduled_in j (sched' t')
NOT_IN_OLD : ~~ scheduled_in j (sched t')
t : instant
============================
service_in j (sched t) = service_in j (sched' t)
----------------------------------------------------------------------------- *)
case: (boolP (t == t')) ⇒ /eqP TT.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 211)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
NOT_IN_NEW : ~~ scheduled_in j (sched' t')
NOT_IN_OLD : ~~ scheduled_in j (sched t')
t : instant
TT : t = t'
============================
service_in j (sched t) = service_in j (sched' t)
subgoal 2 (ID 212) is:
service_in j (sched t) = service_in j (sched' t)
----------------------------------------------------------------------------- *)
- rewrite !TT !service_implies_scheduled //; by apply negbTE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 212)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
NOT_IN_NEW : ~~ scheduled_in j (sched' t')
NOT_IN_OLD : ~~ scheduled_in j (sched t')
t : instant
TT : t <> t'
============================
service_in j (sched t) = service_in j (sched' t)
----------------------------------------------------------------------------- *)
- rewrite rest_of_schedule_invariant//.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Based on the previous observation, we can trivially lift the invariant
that jobs not involved in the replacement receive equal service to the
cumulative service received in any interval.
Corollary service_during_of_others_invariant (j: Job):
~~ scheduled_in j (sched' t') →
~~ scheduled_in j (sched t') →
∀ t1 t2,
service_during sched j t1 t2 = service_during sched' j t1 t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 132)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
============================
~~ scheduled_in j (sched' t') ->
~~ scheduled_in j (sched t') ->
forall t1 t2 : instant,
service_during sched j t1 t2 = service_during sched' j t1 t2
----------------------------------------------------------------------------- *)
Proof.
move⇒ NOT_IN_NEW NOT_IN_OLD t1 t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 136)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
NOT_IN_NEW : ~~ scheduled_in j (sched' t')
NOT_IN_OLD : ~~ scheduled_in j (sched t')
t1, t2 : instant
============================
service_during sched j t1 t2 = service_during sched' j t1 t2
----------------------------------------------------------------------------- *)
rewrite /service_during.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 143)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
NOT_IN_NEW : ~~ scheduled_in j (sched' t')
NOT_IN_OLD : ~~ scheduled_in j (sched t')
t1, t2 : instant
============================
\sum_(t1 <= t < t2) service_at sched j t =
\sum_(t1 <= t < t2) service_at sched' j t
----------------------------------------------------------------------------- *)
apply eq_big_nat ⇒ t /andP [le_t1t lt_tt2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 185)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
NOT_IN_NEW : ~~ scheduled_in j (sched' t')
NOT_IN_OLD : ~~ scheduled_in j (sched t')
t1, t2 : instant
t : nat
le_t1t : t1 <= t
lt_tt2 : t < t2
============================
service_at sched j t = service_at sched' j t
----------------------------------------------------------------------------- *)
rewrite service_at_of_others_invariant //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ReplaceAtFacts.
~~ scheduled_in j (sched' t') →
~~ scheduled_in j (sched t') →
∀ t1 t2,
service_during sched j t1 t2 = service_during sched' j t1 t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 132)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
============================
~~ scheduled_in j (sched' t') ->
~~ scheduled_in j (sched t') ->
forall t1 t2 : instant,
service_during sched j t1 t2 = service_during sched' j t1 t2
----------------------------------------------------------------------------- *)
Proof.
move⇒ NOT_IN_NEW NOT_IN_OLD t1 t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 136)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
NOT_IN_NEW : ~~ scheduled_in j (sched' t')
NOT_IN_OLD : ~~ scheduled_in j (sched t')
t1, t2 : instant
============================
service_during sched j t1 t2 = service_during sched' j t1 t2
----------------------------------------------------------------------------- *)
rewrite /service_during.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 143)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
NOT_IN_NEW : ~~ scheduled_in j (sched' t')
NOT_IN_OLD : ~~ scheduled_in j (sched t')
t1, t2 : instant
============================
\sum_(t1 <= t < t2) service_at sched j t =
\sum_(t1 <= t < t2) service_at sched' j t
----------------------------------------------------------------------------- *)
apply eq_big_nat ⇒ t /andP [le_t1t lt_tt2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 185)
Job : JobType
PState : eqType
H : ProcessorState Job PState
sched : schedule PState
t' : instant
nstate : PState
sched' := replace_at sched t' nstate : instant -> PState
j : Job
NOT_IN_NEW : ~~ scheduled_in j (sched' t')
NOT_IN_OLD : ~~ scheduled_in j (sched t')
t1, t2 : instant
t : nat
le_t1t : t1 <= t
lt_tt2 : t < t2
============================
service_at sched j t = service_at sched' j t
----------------------------------------------------------------------------- *)
rewrite service_at_of_others_invariant //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ReplaceAtFacts.