schedule.v

Require Export prosa.util.all.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.model.processor.platform_properties.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.facts.behavior.service.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Import prosa.model.processor.ideal.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]

(** Note: we do not re-export the basic definitions to avoid littering the global
   namespace with type class instances. *)

(** In this section we establish the classes to which an ideal schedule belongs. *)
Section ScheduleClass.

  (** We assume ideal uni-processor schedules. *)
  #[local] Existing Instance ideal.processor_state.

  Local Transparent scheduled_in scheduled_on.
  (** Consider any job type and the ideal processor model. *)
  Context {Job: JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

  (** We note that the ideal processor model is indeed a uni-processor
     model. *)
  Lemma ideal_proc_model_is_a_uniprocessor_model:
    uniprocessor_model (processor_state Job).Job: JobType
H: JobArrival Job
H0: JobCost Job
uniprocessor_model (processor_state Job)
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
uniprocessor_model (processor_state Job)
    move=> j1 j2 sched t /existsP[[]/eqP E1] /existsP[[]/eqP E2].Job: JobType
H: JobArrival Job
H0: JobCost Job
j1, j2: Job
sched: schedule (processor_state Job)
t: instant
E1: sched t = Some j1
E2: sched t = Some j2
j1 = j2
    by move: E1 E2 =>->[].
  Qed.

  (** By definition, [service_in] is the sum of the service received
      in total across all cores.  In the ideal uniprocessor model,
      however, there is only one "core," which is expressed by using
      [unit] as the type of cores. The type [unit] only has a single
      member [tt], which serves as a placeholder. Consequently, the
      definition of [service_in] simplifies to a single term of the
      sum, the service on the one core, which we note with the
      following lemma that relates [service_in] to [service_on]. *)
  Lemma service_in_service_on (j : Job) s :
    service_in j s = service_on j s tt.Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
service_in j s = service_on j s tt
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
service_in j s = service_on j s tt
    by rewrite /service_in /index_enum Finite.EnumDef.enumDef /= big_seq1.
  Qed.

  (** Furthermore, since the ideal uniprocessor state is represented
      by the [option Job] type, [service_in] further simplifies to a
      simple equality comparison, which we note next. *)
  Lemma service_in_def (j : Job) (s : processor_state Job) :
    service_in j s = (s == Some j).Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
service_in j s = (s == Some j)
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
service_in j s = (s == Some j)
    by rewrite service_in_service_on.
  Qed.

  (** We observe that the ideal processor model falls into the category
     of ideal-progress models, i.e., a scheduled job always receives
     service. *)
  Lemma ideal_proc_model_ensures_ideal_progress:
    ideal_progress_proc_model (processor_state Job).Job: JobType
H: JobArrival Job
H0: JobCost Job
ideal_progress_proc_model (processor_state Job)
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
ideal_progress_proc_model (processor_state Job)
    move=> j s /existsP[[]/eqP->] /=.Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
0 < service_in j (Some j)
    by rewrite service_in_def /= eqxx /nat_of_bool.
  Qed.

  (** The ideal processor model is a unit-service model. *)
  Lemma ideal_proc_model_provides_unit_service:
    unit_service_proc_model (processor_state Job).Job: JobType
H: JobArrival Job
H0: JobCost Job
unit_service_proc_model (processor_state Job)
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
unit_service_proc_model (processor_state Job)
    move=> j s.Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
service_in j s <= 1
    rewrite service_in_def /= /nat_of_bool.Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
(if s == Some j then 1 else 0) <= 1
    by case:ifP.
  Qed.

  Lemma scheduled_in_def (j : Job) s :
    scheduled_in j s = (s == Some j).Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
scheduled_in j s = (s == Some j)
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
scheduled_in j s = (s == Some j)
    rewrite /scheduled_in/scheduled_on/=.Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
[exists c, s == Some j] = (s == Some j)
    case: existsP=>[[_->]//|].Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
~ (exists _ : unit_finType, s == Some j) ->
false = (s == Some j)
    case: (s == Some j)=>//=[[]].Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
exists _ : unit, true
    by exists.
  Qed.

  Lemma scheduled_at_def sched (j : Job) t :
    scheduled_at sched j t = (sched t == Some j).Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant
scheduled_at sched j t = (sched t == Some j)
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant
scheduled_at sched j t = (sched t == Some j)
      by rewrite /scheduled_at scheduled_in_def.
  Qed.

  Lemma service_in_is_scheduled_in (j : Job) s :
    service_in j s = scheduled_in j s.Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
service_in j s = scheduled_in j s
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
service_in j s = scheduled_in j s
    by rewrite service_in_def scheduled_in_def.
  Qed.

  Lemma service_at_is_scheduled_at sched (j : Job) t :
    service_at sched j t = scheduled_at sched j t.Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant
service_at sched j t = scheduled_at sched j t
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant
service_at sched j t = scheduled_at sched j t
      by rewrite /service_at service_in_is_scheduled_in.
  Qed.

  Lemma service_on_def (j : Job) (s : processor_state Job) c :
    service_on j s c = (s == Some j).Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
c: Core
service_on j s c = (s == Some j)
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
j: Job
s: processor_state Job
c: Core
service_on j s c = (s == Some j)
    done.
  Qed.

  Lemma service_at_def sched (j : Job) t :
    service_at sched j t = (sched t == Some j).Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant
service_at sched j t = (sched t == Some j)
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant
service_at sched j t = (sched t == Some j)
    by rewrite /service_at service_in_def.
  Qed.

  (** Next we prove a lemma which helps us to do a case analysis on
      the state of an ideal schedule. *)
  Lemma ideal_proc_model_sched_case_analysis:
    forall (sched : schedule (ideal.processor_state Job)) (t : instant),
      is_idle sched t \/ exists j, scheduled_at sched j t.Job: JobType
H: JobArrival Job
H0: JobCost Job
forall (sched : schedule (processor_state Job))
  (t : instant),
is_idle sched t \/
(exists j : Job, scheduled_at sched j t)
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
forall (sched : schedule (processor_state Job))
  (t : instant),
is_idle sched t \/
(exists j : Job, scheduled_at sched j t)
    intros.Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
t: instant
is_idle sched t \/
(exists j : Job, scheduled_at sched j t)
    unfold is_idle; simpl; destruct (sched t) eqn:EQ.Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
t: instant
s: Job
EQ: sched t = Some s
Some s == None \/
(exists j : Job, scheduled_at sched j t)
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
t: instant
EQ: sched t = None
None == None \/
(exists j : Job, scheduled_at sched j t)
    -Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
t: instant
s: Job
EQ: sched t = Some s
Some s == None \/
(exists j : Job, scheduled_at sched j t)
Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
t: instant
EQ: sched t = None
None == None \/
(exists j : Job, scheduled_at sched j t) by right; exists s; auto; rewrite scheduled_at_def EQ.Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
t: instant
EQ: sched t = None
None == None \/
(exists j : Job, scheduled_at sched j t)
    -Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
t: instant
EQ: sched t = None
None == None \/
(exists j : Job, scheduled_at sched j t) by left; auto.
  Qed.

  (** We prove that if a job [j] is scheduled at a time instant [t],
      then the scheduler is not idle at [t]. *) 
  Lemma ideal_sched_implies_not_idle sched (j : Job) t :
    scheduled_at sched j t ->
    ~ is_idle sched t.Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant
scheduled_at sched j t -> ~ is_idle sched t
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant
scheduled_at sched j t -> ~ is_idle sched t
    rewrite scheduled_at_def => /eqP SCHED /eqP IDLE.Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant
SCHED: sched t = Some j
IDLE: sched t = None
False
    by rewrite IDLE in SCHED; inversion SCHED.
  Qed.
  
  (** On a similar note, if a scheduler is idle at a time instant [t],
      then no job can receive service at [t]. *)
  Lemma ideal_not_idle_implies_sched sched (j : Job) t :
    is_idle sched t ->
    service_at sched j t = 0.Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant
is_idle sched t -> service_at sched j t = 0
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
sched: schedule (processor_state Job)
j: Job
t: instant
is_idle sched t -> service_at sched j t = 0 by rewrite service_at_is_scheduled_at scheduled_at_def => /eqP ->. Qed.
  
End ScheduleClass.

(** * Incremental Service in Ideal Schedule *)
(** In the following section we prove a few facts about service in ideal schedule. *)
(* Note that these lemmas can be generalized to an arbitrary scheduler. *)
Section IncrementalService.

  (** Consider any job type, ... *)
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

  (** ... any arrival sequence, ... *)
  Variable arr_seq : arrival_sequence Job.

  (** ... and any ideal uni-processor schedule of this arrival sequence. *)
  Variable sched : schedule (ideal.processor_state Job).

  (** As a base case, we prove that if a job [j] receives service in
      some time interval <<[t1,t2)>>, then there exists a time instant
      <<t ∈ [t1,t2)>> such that [j] is scheduled at time [t] and [t] is
      the first instant where [j] receives service. *)
  Lemma positive_service_during:
    forall j t1 t2,
      0 < service_during sched j t1 t2 ->
      exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
forall (j : Job) (t1 t2 : instant),
0 < service_during sched j t1 t2 ->
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = 0
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
forall (j : Job) (t1 t2 : instant),
0 < service_during sched j t1 t2 ->
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = 0
    intros j t1 t2 SERV.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = 0
    have LE: t1 <= t2.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
t1 <= t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = 0
    {Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
t1 <= t2 rewrite leqNgt; apply/negP; intros CONTR.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
CONTR: t2 < t1
False
        by apply ltnW in CONTR;  move: SERV; rewrite /service_during big_geq.
    }Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = 0
    destruct (scheduled_at sched j t1) eqn:SCHED.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = false
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = 0
    {Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = 0 exists t1; repeat split; try done.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
t1 <= t1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
service_during sched j t1 t1 = 0
      -Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
t1 <= t1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
service_during sched j t1 t1 = 0 apply/andP; split; first by done.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
t1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
service_during sched j t1 t1 = 0
        rewrite ltnNge; apply/negP; intros CONTR.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
CONTR: t2 <= t1
False
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
service_during sched j t1 t1 = 0
          by move: SERV; rewrite/service_during big_geq.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
service_during sched j t1 t1 = 0
      -Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = true
service_during sched j t1 t1 = 0 by rewrite /service_during big_geq.
    }Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = false
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = 0
    {Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: scheduled_at sched j t1 = false
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = 0 apply negbT in SCHED.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
SERV: 0 < service_during sched j t1 t2
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = 0
      move: SERV.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
0 < service_during sched j t1 t2 ->
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = 0
      rewrite /service_during sum_nat_gt0 filter_predT => /hasP[t IN SCHEDt].Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
IN: t \in index_iota t1 t2
SCHEDt: 0 < service_at sched j t
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  \sum_(t1 <= t0 < t) service_at sched j t0 = 0
      rewrite service_at_def /= lt0b in SCHEDt.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
IN: t \in index_iota t1 t2
SCHEDt: sched t == Some j
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  \sum_(t1 <= t0 < t) service_at sched j t0 = 0
      rewrite mem_iota subnKC in IN; last by done.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN: t1 <= t < t2
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  \sum_(t1 <= t0 < t) service_at sched j t0 = 0
      move: IN => /andP [IN1 IN2].Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  \sum_(t1 <= t0 < t) service_at sched j t0 = 0
      move: (exists_first_intermediate_point
               ((fun t => scheduled_at sched j t)) t1 t IN1 SCHED) => A.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
A: scheduled_at sched j t ->
exists t0 : nat,
  t1 < t0 <= t /\
  (forall x : nat,
   t1 <= x < t0 -> ~~ scheduled_at sched j x) /\
  scheduled_at sched j t0
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  \sum_(t1 <= t0 < t) service_at sched j t0 = 0
      feed A; first by rewrite scheduled_at_def/=.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
A: exists t0 : nat,
  t1 < t0 <= t /\
  (forall x : nat,
   t1 <= x < t0 -> ~~ scheduled_at sched j x) /\
  scheduled_at sched j t0
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  \sum_(t1 <= t0 < t) service_at sched j t0 = 0
      move: A => [x [/andP [T1 T4] [T2 T3]]].Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  \sum_(t1 <= t0 < t) service_at sched j t0 = 0
      exists x; repeat split; try done.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
t1 <= x < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
\sum_(t1 <= t < x) service_at sched j t = 0
      -Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
t1 <= x < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
\sum_(t1 <= t < x) service_at sched j t = 0 apply/andP; split; first by apply ltnW.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
x < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
\sum_(t1 <= t < x) service_at sched j t = 0
          by apply leq_ltn_trans with t.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
\sum_(t1 <= t < x) service_at sched j t = 0
      -Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
\sum_(t1 <= t < x) service_at sched j t = 0 apply/eqP; rewrite big_nat_cond big1 //.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
forall i : nat,
(t1 <= i < x) && true -> service_at sched j i = 0
        move => y /andP [T5 _].Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
y: nat
T5: t1 <= y < x
service_at sched j y = 0
        apply/eqP.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
y: nat
T5: t1 <= y < x
service_at sched j y == 0
        rewrite service_at_def /= eqb0.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
LE: t1 <= t2
SCHED: ~~ scheduled_at sched j t1
t: nat_eqType
SCHEDt: sched t == Some j
IN1: t1 <= t
IN2: t < t2
x: nat
T1: t1 < x
T4: x <= t
T2: forall x0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0
T3: scheduled_at sched j x
y: nat
T5: t1 <= y < x
sched y != Some j
        by specialize (T2 y); rewrite scheduled_at_def/= in T2; apply T2.
    }
  Qed.

  (** Furthermore, we observe that, if a job receives some positive
      amount of service during an interval <<[t1, t2)>>, then the
      interval can't be empty and hence [t1 < t2]. *)
  Lemma service_during_ge :
    forall j t1 t2 k,
      service_during sched j t1 t2 > k ->
      t1 < t2.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
forall (j : Job) (t1 t2 : instant) (k : nat),
k < service_during sched j t1 t2 -> t1 < t2
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
forall (j : Job) (t1 t2 : instant) (k : nat),
k < service_during sched j t1 t2 -> t1 < t2
    move=> j t1 t2 k SERV.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k < service_during sched j t1 t2
t1 < t2
    rewrite leqNgt.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k < service_during sched j t1 t2
~~ (t2 < t1.+1)
    apply/negP => CONTR.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k < service_during sched j t1 t2
CONTR: t2 < t1.+1
False
    move: SERV.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
CONTR: t2 < t1.+1
k < service_during sched j t1 t2 -> False
    by rewrite /service_during big_geq.
  Qed.

  (** Next, we prove that if in some time interval <<[t1,t2)>> a job [j]
     receives [k] units of service, then there exists a time instant
     <<t ∈ [t1,t2)>> such that [j] is scheduled at time [t] and service
     of job [j] within interval <<[t1,t)>> is equal to [k]. *)
  Lemma incremental_service_during:
    forall j t1 t2 k,
      service_during sched j t1 t2 > k ->
      exists t, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
forall (j : Job) (t1 t2 : instant) (k : nat),
k < service_during sched j t1 t2 ->
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k
  Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
forall (j : Job) (t1 t2 : instant) (k : nat),
k < service_during sched j t1 t2 ->
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k
    move=> j t1 t2 k SERV.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k < service_during sched j t1 t2
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k
    have LE: t1 < t2 by move: (service_during_ge _ _ _ _ SERV).Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k < service_during sched j t1 t2
LE: t1 < t2
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k
    induction k; first by apply positive_service_during in SERV.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
IHk: k < service_during sched j t1 t2 ->
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
    feed IHk; first by apply ltn_trans with k.+1.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
IHk: exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
    move: IHk => [t [/andP [NEQ1 NEQ2] [SCHEDt SERVk]]].Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
    have SERVk1: service_during sched j t1 t.+1 = k.+1.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
service_during sched j t1 t.+1 = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
    {Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
service_during sched j t1 t.+1 = k.+1 rewrite -(service_during_cat _ _ _ t); last by apply/andP; split.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
service_during sched j t1 t +
service_during sched j t t.+1 = k.+1
      rewrite  SERVk -[X in _ = X]addn1; apply/eqP; rewrite eqn_add2l.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
service_during sched j t t.+1 == 1
      rewrite /service_during big_nat1 service_at_def /=.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
(sched t == Some j) == 1
      by rewrite eqb1 -scheduled_at_def /=.
    }Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
SERV: k.+1 < service_during sched j t1 t2
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
    move: SERV; rewrite -(service_during_cat _ _ _ t.+1); last first.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
t1 <= t.+1 <= t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
k.+1 <
service_during sched j t1 t.+1 +
service_during sched j t.+1 t2 ->
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
    {Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
t1 <= t.+1 <= t2 by apply/andP; split; first apply leq_trans with t. }Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
k.+1 <
service_during sched j t1 t.+1 +
service_during sched j t.+1 t2 ->
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
    rewrite SERVk1 -addn1 leq_add2l; move => SERV.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
    destruct (scheduled_at sched j t.+1) eqn:SCHED.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
    -Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1 exists t.+1; repeat split; try done.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true
t1 <= t.+1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1 apply/andP; split.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true
t1 <= t.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true
t.+1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
      +Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true
t1 <= t.+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true
t.+1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1 apply leq_trans with t; by done.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true
t.+1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
      +Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true
t.+1 < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1 rewrite ltnNge; apply/negP; intros CONTR.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = true
CONTR: t2 <= t.+1
False
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
          by move: SERV; rewrite /service_during big_geq.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
    -Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: scheduled_at sched j t.+1 = false
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1  apply negbT in SCHED.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SERV: 0 < service_during sched j t.+1 t2
SCHED: ~~ scheduled_at sched j t.+1
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  service_during sched j t1 t = k.+1
       move: SERV; rewrite /service /service_during sum_nat_gt0 filter_predT; move => /hasP[x INx SCHEDx].Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
INx: x \in index_iota t.+1 t2
SCHEDx: 0 < service_at sched j x
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  \sum_(t1 <= t0 < t) service_at sched j t0 = k.+1
       rewrite service_at_def lt0b in SCHEDx.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
INx: x \in index_iota t.+1 t2
SCHEDx: sched x == Some j
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  \sum_(t1 <= t0 < t) service_at sched j t0 = k.+1
       rewrite mem_iota subnKC in INx; last by done.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx: t < x < t2
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  \sum_(t1 <= t0 < t) service_at sched j t0 = k.+1
       move: INx => /andP [INx1 INx2].Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  \sum_(t1 <= t0 < t) service_at sched j t0 = k.+1
       move: (exists_first_intermediate_point _ _ _ INx1 SCHED) => A.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
A: scheduled_at sched j x ->
exists t0 : nat,
  t.+1 < t0 <= x /\
  (forall x : nat,
   t < x < t0 -> ~~ scheduled_at sched j x) /\
  scheduled_at sched j t0
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  \sum_(t1 <= t0 < t) service_at sched j t0 = k.+1
       feed A; first by rewrite scheduled_at_def/=.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
A: exists t0 : nat,
  t.+1 < t0 <= x /\
  (forall x : nat,
   t < x < t0 -> ~~ scheduled_at sched j x) /\
  scheduled_at sched j t0
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  \sum_(t1 <= t0 < t) service_at sched j t0 = k.+1
       move: A => [y [/andP [T1 T4] [T2 T3]]].Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
exists t : nat,
  t1 <= t < t2 /\
  scheduled_at sched j t /\
  \sum_(t1 <= t0 < t) service_at sched j t0 = k.+1
       exists y; repeat split => //.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
t1 <= y < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
       +Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
t1 <= y < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1 apply/andP; split.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
t1 <= y
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
y < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
         apply leq_trans with t; first by done.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
t <= y
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
y < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
         apply ltnW, ltn_trans with t.+1; by done.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
y < t2
Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
           by apply leq_ltn_trans with x.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
       +Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1 rewrite (@big_cat_nat _ _ _ t.+1) //=; [ | by apply leq_trans with t | by apply ltn_trans with t.+1].Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: service_during sched j t1 t.+1 = k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
\sum_(t1 <= i < t.+1) service_at sched j i +
\sum_(t.+1 <= i < y) service_at sched j i = k.+1
         unfold service_during in SERVk1; rewrite SERVk1; apply/eqP.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: \sum_(t1 <= t < t.+1) service_at sched j t =
k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
k.+1 + \sum_(t.+1 <= i < y) service_at sched j i ==
k.+1
         rewrite -{2}[k.+1]addn0 eqn_add2l.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: \sum_(t1 <= t < t.+1) service_at sched j t =
k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
\sum_(t.+1 <= i < y) service_at sched j i == 0
         rewrite big_nat_cond big1 //; move => z /andP [H5 _].Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: \sum_(t1 <= t < t.+1) service_at sched j t =
k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
z: nat
H5: t < z < y
service_at sched j z = 0
         apply/eqP.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: \sum_(t1 <= t < t.+1) service_at sched j t =
k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
z: nat
H5: t < z < y
service_at sched j z == 0
         rewrite service_at_def eqb0.Job: JobType
H: JobArrival Job
H0: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (processor_state Job)
j: Job
t1, t2: instant
k: nat
LE: t1 < t2
t: nat
NEQ1: t1 <= t
NEQ2: t < t2
SCHEDt: scheduled_at sched j t
SERVk: service_during sched j t1 t = k
SERVk1: \sum_(t1 <= t < t.+1) service_at sched j t =
k.+1
SCHED: ~~ scheduled_at sched j t.+1
x: nat_eqType
SCHEDx: sched x == Some j
INx1: t < x
INx2: x < t2
y: nat
T1: t.+1 < y
T4: y <= x
T2: forall x : nat,
t < x < y -> ~~ scheduled_at sched j x
T3: scheduled_at sched j y
z: nat
H5: t < z < y
sched z != Some j
         by specialize (T2 z); rewrite scheduled_at_def/= in T2; apply T2.
  Qed.

End IncrementalService.

(** * Automation *)
(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
    will be able to apply them automatically. *)
Global Hint Resolve ideal_proc_model_is_a_uniprocessor_model
     ideal_proc_model_ensures_ideal_progress
     ideal_proc_model_provides_unit_service : basic_rt_facts.

(** We also provide tactics for case analysis on ideal processor state. *)

(** The first tactic generates two sub-goals: one with idle processor and
    the other with processor executing a job named [JobName]. *)
Ltac ideal_proc_model_sched_case_analysis sched t JobName :=
  let Idle := fresh "Idle" in
  let Sched := fresh "Sched_" JobName in
  destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]].

(** The second tactic is similar to the first, but it additionally generates
    two equalities: [sched t = None] and [sched t = Some j]. *)
Ltac ideal_proc_model_sched_case_analysis_eq sched t JobName :=
  let Idle := fresh "Idle" in
  let IdleEq := fresh "Eq" Idle in
  let Sched := fresh "Sched_" JobName in
  let SchedEq := fresh "Eq" Sched in
  destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]];
  [move: (Idle) => /eqP IdleEq; rewrite ?IdleEq
  | move: (Sched); simpl; move => /eqP SchedEq; rewrite ?SchedEq].