Library prosa.analysis.definitions.progress
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.behavior.service.
Job Progress (or Lack Thereof)
Consider any type of jobs with a known cost...
... and any kind of schedule.
For a given job and a given schedule...
...and two ordered points in time...
... we say that the job has progressed between the two points iff its
total received service has increased.
Conversely, if the accumulated service does not change, there is no
progress.
We note that the negation of the former is equivalent to the latter
definition.
Lemma no_progress_equiv: ~~ job_has_progressed ↔ no_progress.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
~~ job_has_progressed <-> no_progress
----------------------------------------------------------------------------- *)
Proof.
rewrite /job_has_progressed /no_progress.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 47)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
~~ (service sched j t1 < service sched j t2) <->
service sched j t1 == service sched j t2
----------------------------------------------------------------------------- *)
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 49)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
~~ (service sched j t1 < service sched j t2) ->
service sched j t1 == service sched j t2
subgoal 2 (ID 50) is:
service sched j t1 == service sched j t2 ->
~~ (service sched j t1 < service sched j t2)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 49)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
~~ (service sched j t1 < service sched j t2) ->
service sched j t1 == service sched j t2
----------------------------------------------------------------------------- *)
rewrite -leqNgt leq_eqVlt ⇒ /orP [EQ|LT]; first by rewrite eq_sym.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 102)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
LT : service sched j t2 < service sched j t1
============================
service sched j t1 == service sched j t2
----------------------------------------------------------------------------- *)
exfalso.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 108)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
LT : service sched j t2 < service sched j t1
============================
False
----------------------------------------------------------------------------- *)
have MONO: service sched j t1 ≤ service sched j t2
by apply service_monotonic.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 121)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
LT : service sched j t2 < service sched j t1
MONO : service sched j t1 <= service sched j t2
============================
False
----------------------------------------------------------------------------- *)
have NOT_MONO: ~~ (service sched j t1 ≤ service sched j t2)
by apply /negPf; apply ltn_geF.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 151)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
LT : service sched j t2 < service sched j t1
MONO : service sched j t1 <= service sched j t2
NOT_MONO : ~~ (service sched j t1 <= service sched j t2)
============================
False
----------------------------------------------------------------------------- *)
move: NOT_MONO ⇒ /negP NOT_MONO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 179)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
LT : service sched j t2 < service sched j t1
MONO : service sched j t1 <= service sched j t2
NOT_MONO : ~ service sched j t1 <= service sched j t2
============================
False
----------------------------------------------------------------------------- *)
contradiction.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
subgoal 1 (ID 50) is:
service sched j t1 == service sched j t2 ->
~~ (service sched j t1 < service sched j t2)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
service sched j t1 == service sched j t2 ->
~~ (service sched j t1 < service sched j t2)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
service sched j t1 == service sched j t2 ->
~~ (service sched j t1 < service sched j t2)
----------------------------------------------------------------------------- *)
move ⇒ /eqP →.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 216)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
~~ (service sched j t2 < service sched j t2)
----------------------------------------------------------------------------- *)
rewrite -leqNgt.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 220)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
service sched j t2 <= service sched j t2
----------------------------------------------------------------------------- *)
by apply service_monotonic.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End NotionsOfProgress.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
~~ job_has_progressed <-> no_progress
----------------------------------------------------------------------------- *)
Proof.
rewrite /job_has_progressed /no_progress.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 47)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
~~ (service sched j t1 < service sched j t2) <->
service sched j t1 == service sched j t2
----------------------------------------------------------------------------- *)
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 49)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
~~ (service sched j t1 < service sched j t2) ->
service sched j t1 == service sched j t2
subgoal 2 (ID 50) is:
service sched j t1 == service sched j t2 ->
~~ (service sched j t1 < service sched j t2)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 49)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
~~ (service sched j t1 < service sched j t2) ->
service sched j t1 == service sched j t2
----------------------------------------------------------------------------- *)
rewrite -leqNgt leq_eqVlt ⇒ /orP [EQ|LT]; first by rewrite eq_sym.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 102)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
LT : service sched j t2 < service sched j t1
============================
service sched j t1 == service sched j t2
----------------------------------------------------------------------------- *)
exfalso.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 108)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
LT : service sched j t2 < service sched j t1
============================
False
----------------------------------------------------------------------------- *)
have MONO: service sched j t1 ≤ service sched j t2
by apply service_monotonic.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 121)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
LT : service sched j t2 < service sched j t1
MONO : service sched j t1 <= service sched j t2
============================
False
----------------------------------------------------------------------------- *)
have NOT_MONO: ~~ (service sched j t1 ≤ service sched j t2)
by apply /negPf; apply ltn_geF.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 151)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
LT : service sched j t2 < service sched j t1
MONO : service sched j t1 <= service sched j t2
NOT_MONO : ~~ (service sched j t1 <= service sched j t2)
============================
False
----------------------------------------------------------------------------- *)
move: NOT_MONO ⇒ /negP NOT_MONO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 179)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
LT : service sched j t2 < service sched j t1
MONO : service sched j t1 <= service sched j t2
NOT_MONO : ~ service sched j t1 <= service sched j t2
============================
False
----------------------------------------------------------------------------- *)
contradiction.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
subgoal 1 (ID 50) is:
service sched j t1 == service sched j t2 ->
~~ (service sched j t1 < service sched j t2)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
service sched j t1 == service sched j t2 ->
~~ (service sched j t1 < service sched j t2)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
service sched j t1 == service sched j t2 ->
~~ (service sched j t1 < service sched j t2)
----------------------------------------------------------------------------- *)
move ⇒ /eqP →.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 216)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
~~ (service sched j t2 < service sched j t2)
----------------------------------------------------------------------------- *)
rewrite -leqNgt.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 220)
Job : JobType
H : JobCost Job
PState : Type
H0 : ProcessorState Job PState
sched : schedule PState
j : Job
t1, t2 : nat
H_t1_before_t2 : t1 <= t2
============================
service sched j t2 <= service sched j t2
----------------------------------------------------------------------------- *)
by apply service_monotonic.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End NotionsOfProgress.
For convenience, we define a lack of progress also in terms of given
reference point [t] and the length of the preceding interval of
inactivity [delta], meaning that no progress has been made for at least
[delta] time units.
Definition no_progress_for (t : instant) (delta : duration) := no_progress (t - delta) t.
End Progress.
End Progress.