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)

In the following section, we define a notion of "job progress", and conversely a notion of a lack of progress.

Section Progress.

Consider any type of jobs with a known cost...
  Context {Job : JobType}.
  Context `{JobCost Job}.

... and any kind of schedule.
  Context {PState : Type}.
  Context `{ProcessorState Job PState}.

For a given job and a given schedule...
  Variable sched : schedule PState.
  Variable j : Job.

  Section NotionsOfProgress.

...and two ordered points in time...
    Variable t1 t2 : nat.
    Hypothesis H_t1_before_t2: t1 t2.

... we say that the job has progressed between the two points iff its total received service has increased.
    Definition job_has_progressed := service sched j t1 < service sched j t2.

Conversely, if the accumulated service does not change, there is no progress.
    Definition no_progress := service sched j t1 == service sched j t2.

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.

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.