Built with
Alectryon , running Coq+SerAPI v8.20.0+0.20.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.model.readiness.suspension.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted. [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
(** In this file, we establish some basic facts related to self-suspensions. *)
Section Suspensions .
(** Consider any kind of jobs. *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Suppose that the jobs can exhibit self-suspensions. *)
Context `{JobSuspension Job}.
(** Consider any valid arrival sequence of jobs ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and assume the notion of readiness for self-suspending jobs. *)
#[local] Existing Instance suspension_ready_instance .
(** Consider any kind of processor model. *)
Context `{PState : ProcessorState Job}.
(** Consider any valid schedule. *)
Variable sched : schedule PState.
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
(** First, we establish some basic lemmas regarding self-suspending jobs. *)
Section BasicLemmas .
(** We show that a self-suspended job cannot be ready, ... *)
Lemma suspended_implies_job_not_ready :
forall j t ,
suspended sched j t ->
~~ job_ready sched j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq
forall (j : Job) (t : instant),
suspended sched j t -> ~~ job_ready sched j t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq
forall (j : Job) (t : instant),
suspended sched j t -> ~~ job_ready sched j t
move => j t /andP[SUS PEND].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t : instant SUS : ~~ suspension_has_passed sched j t PEND : pending sched j t
~~ job_ready sched j t
rewrite /job_ready /suspension_ready_instance.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t : instant SUS : ~~ suspension_has_passed sched j t PEND : pending sched j t
~~
(suspension_has_passed sched j t &&
~~ completed_by sched j t)
by rewrite negb_and; apply /orP; left .
Qed .
(** ... which trivially implies that the job cannot be scheduled. *)
Lemma suspended_implies_not_scheduled :
forall j t ,
suspended sched j t ->
~~ scheduled_at sched j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq
forall (j : Job) (t : instant),
suspended sched j t -> ~~ scheduled_at sched j t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq
forall (j : Job) (t : instant),
suspended sched j t -> ~~ scheduled_at sched j t
move => j t /suspended_implies_job_not_ready SUS.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t : instant SUS : ~~ job_ready sched j t
~~ scheduled_at sched j t
by move : SUS; apply contra.
Qed .
(** Next, we observe that a self-suspended job has already arrived. *)
Lemma suspended_implies_arrived :
forall j t ,
suspended sched j t ->
has_arrived j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq
forall (j : Job) (t : instant),
suspended sched j t -> has_arrived j t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq
forall (j : Job) (t : instant),
suspended sched j t -> has_arrived j t
by move => j t /andP [? /andP [? ?]].
Qed .
(** By definition, only pending jobs can be self-suspended. *)
Lemma suspended_implies_pending :
forall j t ,
suspended sched j t ->
pending sched j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq
forall (j : Job) (t : instant),
suspended sched j t -> pending sched j t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq
forall (j : Job) (t : instant),
suspended sched j t -> pending sched j t
by move => j t /andP [? ?].
Qed .
(** Next, we note that self-suspended jobs are not backlogged. *)
Lemma suspended_implies_not_backlogged :
forall j t ,
suspended sched j t ->
~~ backlogged sched j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq
forall (j : Job) (t : instant),
suspended sched j t -> ~~ backlogged sched j t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq
forall (j : Job) (t : instant),
suspended sched j t -> ~~ backlogged sched j t
move => j t /suspended_implies_job_not_ready SUS.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t : instant SUS : ~~ job_ready sched j t
~~ backlogged sched j t
by rewrite /backlogged negb_and; apply /orP; left .
Qed .
(** Further, we prove that if a job is pending and not self-suspended then
it is ready. *)
Lemma pending_and_not_suspended_implies_ready :
forall j t ,
pending sched j t ->
~~ suspended sched j t ->
job_ready sched j t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq
forall (j : Job) (t : instant),
pending sched j t ->
~~ suspended sched j t -> job_ready sched j t
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq
forall (j : Job) (t : instant),
pending sched j t ->
~~ suspended sched j t -> job_ready sched j t
move => j t; rewrite /suspended => PEND NOTSUS.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t : instant PEND : pending sched j t NOTSUS : ~~
(~~ suspension_has_passed sched j t &&
pending sched j t)
job_ready sched j t
rewrite PEND andbT negbK in NOTSUS.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t : instant PEND : pending sched j t NOTSUS : suspension_has_passed sched j t
job_ready sched j t
move : PEND => /andP [ARR NOTCOMP].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t : instant NOTSUS : suspension_has_passed sched j t ARR : has_arrived j t NOTCOMP : ~~ completed_by sched j t
job_ready sched j t
by rewrite /job_ready /suspension_ready_instance; apply /andP; split .
Qed .
End BasicLemmas .
(** Next, we focus on bounding the self-suspension period of a job after receiving
some amount of service. *)
Section SuspensionBoundedinInterval .
(** Consider any job [j] ... *)
Variable j : Job.
(** ... and any time interval <<[t1, t2)>>. *)
Variable t1 t2 : instant.
(** Now consider any amount of work [ρ]. *)
Variable ρ : work.
(** Our aim is to prove a bound on the self-suspension period of [j] after receiving
an amount of service [ρ].
Note that it is possible that the job may not self-suspend after receiving [ρ]
amount of service in which case [job_suspension j ρ = 0].
Additionally, it is also important to note that the job may self-suspend multiple
times within an interval, and these self-suspension intervals are separated by an
interval where the job gets serviced. We can refer each such self-suspension interval as
a segment, and each such segment is characterized by the amount of service received by the job.
Essentially here we are establishing a bound on the length of the self-suspension segment of [j]
characterized by [ρ]. *)
(** Note that we can have two cases here, either the job [j] starts a suspension segment within
the interval <<[t1, t2)>>, or the job is already suspended at [t1]. *)
Section Step1 .
(** Consider a point [tf] inside <<[t1, t2)>>. *)
Variable tf : instant.
Hypothesis INtf : t1 <= tf < t2.
(** Let [tf] be the first point in the interval <<[t1, t2)>> that is also inside
the self-suspension segment. *)
Hypothesis H_suspended_tf : suspended sched j tf.
Hypothesis H_service_at_tf : service sched j tf = ρ.
Hypothesis H_before_tf :
forall to ,
t1 <= to < tf ->
~~ (suspended sched j to && (service sched j to == ρ)).
(** First, we prove a trivial result that the total suspension before [tf] is zero. *)
Local Lemma suspension_zero_before :
\sum_(t1 <= t < tf | service sched j t == ρ) suspended sched j t = 0 .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))
\sum_(t1 <= t < tf | service sched j t == ρ)
suspended sched j t = 0
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))
\sum_(t1 <= t < tf | service sched j t == ρ)
suspended sched j t = 0
apply /eqP; rewrite sum_nat_eq0_nat.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))
all
(fun x : Datatypes_nat__canonical__eqtype_Equality
=> suspended sched j x == 0 )
[seq x <- index_iota t1 tf | service sched j x == ρ]
apply /allP => [to /[!mem_filter]/andP[SERVto /[!mem_index_iota]INto]].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))to : Datatypes_nat__canonical__eqtype_Equality SERVto : service sched j to == ρ INto : t1 <= to < tf
suspended sched j to == 0
move : (H_before_tf to INto); rewrite SERVto andbT.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))to : Datatypes_nat__canonical__eqtype_Equality SERVto : service sched j to == ρ INto : t1 <= to < tf
~~ suspended sched j to -> suspended sched j to == 0
by move => /negPf ->.
Qed .
(** Next we consider the trivial case when the suspension period exceeds the interval <<[tf, t2)>>. *)
Section TrivialCase .
Hypothesis H_LEQ : t2 - tf <= job_suspension j ρ.
Lemma suspension_bounded_trivial :
\sum_(tf <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_LEQ : t2 - tf <= job_suspension j ρ
\sum_(tf <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_LEQ : t2 - tf <= job_suspension j ρ
\sum_(tf <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
apply : leq_trans;
first by apply sum_majorant_constant with (c := 1 ) => ? ? ?; lia .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_LEQ : t2 - tf <= job_suspension j ρ
1 *
size
[seq j0 <- index_iota tf t2
| (fun
j1 : Datatypes_nat__canonical__eqtype_Equality
=> service sched j j1 == ρ) j0] <=
job_suspension j ρ
rewrite mul1n -sum1_size big_filter.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_LEQ : t2 - tf <= job_suspension j ρ
\sum_(i <- index_iota tf t2 | service sched j i == ρ)
1 <= job_suspension j ρ
apply leq_trans with (n := \sum_(t0 <- index_iota tf t2) 1 ); first by apply leq_sum_seq_pred.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_LEQ : t2 - tf <= job_suspension j ρ
\sum_(tf <= t0 < t2) 1 <= job_suspension j ρ
by rewrite sum1_size size_iota.
Qed .
End TrivialCase .
(** Next, we consider the case when the suspension period is within the interval <<[tf, t2)>>. *)
Section IntervalLengthLonger .
Hypothesis H_GT : t2 - tf > job_suspension j ρ.
Lemma suspension_bounded_longer_interval :
\sum_(tf <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf
\sum_(tf <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf
\sum_(tf <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
have ARRj : job_arrival j <= tf by apply suspended_implies_arrived.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf
\sum_(tf <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
have PENDj : pending sched j tf by apply suspended_implies_pending.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf
\sum_(tf <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
erewrite big_cat_nat with (n := tf + job_suspension j ρ); rewrite //=; try by lia .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf
\sum_(tf <= i < tf + job_suspension j ρ | service
sched j i ==
ρ)
suspended sched j i +
\sum_(tf + job_suspension j ρ <= i < t2 | service
sched j i ==
ρ)
suspended sched j i <= job_suspension j ρ
have ->: \sum_(tf + job_suspension j ρ <= t < t2 | service sched j t == ρ) suspended sched j t = 0 .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf
\sum_(tf + job_suspension j ρ <= t < t2 | service
sched j t ==
ρ)
suspended sched j t = 0
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf
\sum_(tf + job_suspension j ρ <= t < t2 | service
sched j t ==
ρ)
suspended sched j t = 0
apply /eqP; rewrite sum_nat_eq0_nat //=.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf
all (fun x : nat => suspended sched j x == 0 )
[seq x <- index_iota (tf + job_suspension j ρ) t2
| service sched j x == ρ]
apply /negP => /negP /allPn[to INto NOTSUSto].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf to : Datatypes_nat__canonical__eqtype_Equality INto : to
\in [seq x <- index_iota
(tf + job_suspension j ρ) t2
| service sched j x == ρ] NOTSUSto : suspended sched j to != 0
False
have A : forall b : bool, b > 0 -> b by lia .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf to : Datatypes_nat__canonical__eqtype_Equality INto : to
\in [seq x <- index_iota
(tf + job_suspension j ρ) t2
| service sched j x == ρ] NOTSUSto : suspended sched j to != 0 A : forall b : bool, 0 < b -> b
False
move : NOTSUSto; rewrite -lt0n => /A NOTSUSto.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf to : Datatypes_nat__canonical__eqtype_Equality INto : to
\in [seq x <- index_iota
(tf + job_suspension j ρ) t2
| service sched j x == ρ] A : forall b : bool, 0 < b -> bNOTSUSto : suspended sched j to
False
move : INto; rewrite mem_filter mem_index_iota => /andP[/eqP SERVto /andP[INgt INlt]].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf to : Datatypes_nat__canonical__eqtype_Equality A : forall b : bool, 0 < b -> bNOTSUSto : suspended sched j to SERVto : service sched j to = ρ INgt : tf + job_suspension j ρ <= to INlt : to < t2
False
move : NOTSUSto; rewrite /suspended.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf to : Datatypes_nat__canonical__eqtype_Equality A : forall b : bool, 0 < b -> bSERVto : service sched j to = ρ INgt : tf + job_suspension j ρ <= to INlt : to < t2
~~ suspension_has_passed sched j to &&
pending sched j to -> False
have ->//=: suspension_has_passed sched j to.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf to : Datatypes_nat__canonical__eqtype_Equality A : forall b : bool, 0 < b -> bSERVto : service sched j to = ρ INgt : tf + job_suspension j ρ <= to INlt : to < t2
suspension_has_passed sched j to
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf to : Datatypes_nat__canonical__eqtype_Equality A : forall b : bool, 0 < b -> bSERVto : service sched j to = ρ INgt : tf + job_suspension j ρ <= to INlt : to < t2
suspension_has_passed sched j to
rewrite /suspension_has_passed SERVto; apply /andP; split .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf to : Datatypes_nat__canonical__eqtype_Equality A : forall b : bool, 0 < b -> bSERVto : service sched j to = ρ INgt : tf + job_suspension j ρ <= to INlt : to < t2
job_arrival j + job_suspension j ρ <= to
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf to : Datatypes_nat__canonical__eqtype_Equality A : forall b : bool, 0 < b -> bSERVto : service sched j to = ρ INgt : tf + job_suspension j ρ <= to INlt : to < t2
job_arrival j + job_suspension j ρ <= to
have LT : job_suspension j ρ <= to - tf by apply leq_subRL_impl.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf to : Datatypes_nat__canonical__eqtype_Equality A : forall b : bool, 0 < b -> bSERVto : service sched j to = ρ INgt : tf + job_suspension j ρ <= to INlt : to < t2 LT : job_suspension j ρ <= to - tf
job_arrival j + job_suspension j ρ <= to
by move : (leq_add ARRj LT); rewrite subnKC //=; lia . } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf to : Datatypes_nat__canonical__eqtype_Equality A : forall b : bool, 0 < b -> bSERVto : service sched j to = ρ INgt : tf + job_suspension j ρ <= to INlt : to < t2
no_progress_for sched j to (job_suspension j ρ)
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf to : Datatypes_nat__canonical__eqtype_Equality A : forall b : bool, 0 < b -> bSERVto : service sched j to = ρ INgt : tf + job_suspension j ρ <= to INlt : to < t2
no_progress_for sched j to (job_suspension j ρ)
rewrite /no_progress_for /no_progress.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf to : Datatypes_nat__canonical__eqtype_Equality A : forall b : bool, 0 < b -> bSERVto : service sched j to = ρ INgt : tf + job_suspension j ρ <= to INlt : to < t2
service sched j (to - job_suspension j ρ) ==
service sched j to
have SERVGT : service sched j (to - job_suspension j ρ) >= ρ
by rewrite -[in leqLHS]H_service_at_tf; apply service_monotonic; lia .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf to : Datatypes_nat__canonical__eqtype_Equality A : forall b : bool, 0 < b -> bSERVto : service sched j to = ρ INgt : tf + job_suspension j ρ <= to INlt : to < t2 SERVGT : ρ <=
service sched j (to - job_suspension j ρ)
service sched j (to - job_suspension j ρ) ==
service sched j to
have SERVLT : ρ >= service sched j (to - job_suspension j ρ)
by rewrite -[in leqRHS]SERVto; apply service_monotonic; lia .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf to : Datatypes_nat__canonical__eqtype_Equality A : forall b : bool, 0 < b -> bSERVto : service sched j to = ρ INgt : tf + job_suspension j ρ <= to INlt : to < t2 SERVGT : ρ <=
service sched j (to - job_suspension j ρ) SERVLT : service sched j (to - job_suspension j ρ) <=
ρ
service sched j (to - job_suspension j ρ) ==
service sched j to
by apply /eqP; lia . } } } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf
\sum_(tf <= i < tf + job_suspension j ρ | service
sched j i ==
ρ)
suspended sched j i + 0 <= job_suspension j ρ
rewrite addn0.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf
\sum_(tf <= i < tf + job_suspension j ρ | service
sched j i ==
ρ)
suspended sched j i <= job_suspension j ρ
apply : leq_trans; first by apply sum_majorant_constant with (c := 1 ) => ? ? ?; lia .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf
1 *
size
[seq j0 <- index_iota tf (tf + job_suspension j ρ)
| (fun
j1 : Datatypes_nat__canonical__eqtype_Equality
=> service sched j j1 == ρ) j0] <=
job_suspension j ρ
rewrite mul1n -sum1_size big_filter.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf
\sum_(i <- index_iota tf (tf + job_suspension j ρ) |
service sched j i == ρ) 1 <= job_suspension j ρ
apply leq_trans with (n := \sum_(t0 <- index_iota tf (tf + job_suspension j ρ)) 1 );
first by apply leq_sum_seq_pred.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))H_GT : job_suspension j ρ < t2 - tf ARRj : job_arrival j <= tf PENDj : pending sched j tf
\sum_(tf <= t0 < tf + job_suspension j ρ) 1 <=
job_suspension j ρ
by rewrite sum1_size size_iota; lia .
Qed .
End IntervalLengthLonger .
(** Now we prove the required bound in case a point like [tf] exists. This helps to simplify
our final proof. *)
Lemma suspension_bounded_in_interval_aux :
\sum_(t1 <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))
\sum_(t1 <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))
\sum_(t1 <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
have ARRj : job_arrival j <= tf by apply suspended_implies_arrived.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))ARRj : job_arrival j <= tf
\sum_(t1 <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
have PENDj : pending sched j tf by apply suspended_implies_pending.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))ARRj : job_arrival j <= tf PENDj : pending sched j tf
\sum_(t1 <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
erewrite big_cat_nat with (n := tf) => //=; try by lia .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))ARRj : job_arrival j <= tf PENDj : pending sched j tf
\sum_(t1 <= i < tf | service sched j i == ρ)
suspended sched j i +
\sum_(tf <= i < t2 | service sched j i == ρ)
suspended sched j i <= job_suspension j ρ
rewrite suspension_zero_before add0n.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))ARRj : job_arrival j <= tf PENDj : pending sched j tf
\sum_(tf <= i < t2 | service sched j i == ρ)
suspended sched j i <= job_suspension j ρ
have [LEQ | GT] := boolP(t2 - tf <= job_suspension j ρ).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))ARRj : job_arrival j <= tf PENDj : pending sched j tf LEQ : t2 - tf <= job_suspension j ρ
\sum_(tf <= i < t2 | service sched j i == ρ)
suspended sched j i <= job_suspension j ρ
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))ARRj : job_arrival j <= tf PENDj : pending sched j tf LEQ : t2 - tf <= job_suspension j ρ
\sum_(tf <= i < t2 | service sched j i == ρ)
suspended sched j i <= job_suspension j ρ
by apply suspension_bounded_trivial.
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work tf : instant INtf : t1 <= tf < t2 H_suspended_tf : suspended sched j tf H_service_at_tf : service sched j tf = ρ H_before_tf : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))ARRj : job_arrival j <= tf PENDj : pending sched j tf GT : ~~ (t2 - tf <= job_suspension j ρ)
\sum_(tf <= i < t2 | service sched j i == ρ)
suspended sched j i <= job_suspension j ρ
by apply suspension_bounded_longer_interval; lia .
Qed .
End Step1 .
Section Step2 .
(** Now we prove that the point [tf], as used in the above lemmas, always exists if [suspended]
is true at some point inside <<[t1, t2)>>. *)
Hypothesis H_exists : (exists2 t, t \in index_iota t1 t2 & (suspended sched j t && (service sched j t == ρ))).
Lemma exists_some_point :
exists t' ,
t1 <= t' < t2 /\
suspended sched j t' /\
service sched j t' = ρ /\
forall to ,
t1 <= to < t' ->
~~ (suspended sched j to && (service sched j to == ρ)).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)
exists t' : nat,
t1 <= t' < t2 /\
suspended sched j t' /\
service sched j t' = ρ /\
(forall to : nat,
t1 <= to < t' ->
~~
(suspended sched j to && (service sched j to == ρ)))
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)
exists t' : nat,
t1 <= t' < t2 /\
suspended sched j t' /\
service sched j t' = ρ /\
(forall to : nat,
t1 <= to < t' ->
~~
(suspended sched j to && (service sched j to == ρ)))
set P := (fun t => suspended sched j t && (service sched j t == ρ)).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool
exists t' : nat,
t1 <= t' < t2 /\
suspended sched j t' /\
service sched j t' = ρ /\
(forall to : nat,
t1 <= to < t' ->
~~
(suspended sched j to && (service sched j to == ρ)))
set ind := find P (index_iota t1 t2).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat
exists t' : nat,
t1 <= t' < t2 /\
suspended sched j t' /\
service sched j t' = ρ /\
(forall to : nat,
t1 <= to < t' ->
~~
(suspended sched j to && (service sched j to == ρ)))
set t' := nth 0 (index_iota t1 t2) ind.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat
exists t' : nat,
t1 <= t' < t2 /\
suspended sched j t' /\
service sched j t' = ρ /\
(forall to : nat,
t1 <= to < t' ->
~~
(suspended sched j to && (service sched j to == ρ)))
move /hasP: H_exists; rewrite has_find //= => indLT.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2)
exists t' : nat,
t1 <= t' < t2 /\
suspended sched j t' /\
service sched j t' = ρ /\
(forall to : nat,
t1 <= to < t' ->
~~
(suspended sched j to && (service sched j to == ρ)))
have INt' : t1 <= t' < t2 by rewrite -mem_index_iota mem_nth.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2
exists t' : nat,
t1 <= t' < t2 /\
suspended sched j t' /\
service sched j t' = ρ /\
(forall to : nat,
t1 <= to < t' ->
~~
(suspended sched j to && (service sched j to == ρ)))
have /andP[SUSt' /eqP SERVt'] : P t' by apply (@nth_find _ 0 P (index_iota t1 t2)); apply /hasP.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ
exists t' : nat,
t1 <= t' < t2 /\
suspended sched j t' /\
service sched j t' = ρ /\
(forall to : nat,
t1 <= to < t' ->
~~
(suspended sched j to && (service sched j to == ρ)))
exists t' ; do 3 ![split ; eauto ].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ
forall to : nat,
t1 <= to < t' ->
~~ (suspended sched j to && (service sched j to == ρ))
move => to; rewrite -mem_index_iota => INto.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t'
~~ (suspended sched j to && (service sched j to == ρ))
have LT : index to (iota t1 (t' - t1)) < size (iota t1 (t' - t1)) by rewrite index_mem.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1))
~~ (suspended sched j to && (service sched j to == ρ))
have indexLT: index to (index_iota t1 t2) < ind.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1))
index to (index_iota t1 t2) < ind
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1))
index to (index_iota t1 t2) < ind
rewrite /index_iota.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1))
index to (iota t1 (t2 - t1)) < ind
have SPLIT: t2 - t1 = (t' - t1) + (t2 - t') by rewrite addBnAC; lia .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1)) SPLIT : t2 - t1 = t' - t1 + (t2 - t')
index to (iota t1 (t2 - t1)) < ind
rewrite SPLIT iotaD index_cat.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1)) SPLIT : t2 - t1 = t' - t1 + (t2 - t')
(if to \in iota t1 (t' - t1)
then index to (iota t1 (t' - t1))
else
size (iota t1 (t' - t1)) +
index to (iota (t1 + (t' - t1)) (t2 - t'))) < ind
have ->: to \in iota t1 (t' - t1) by [].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1)) SPLIT : t2 - t1 = t' - t1 + (t2 - t')
index to (iota t1 (t' - t1)) < ind
have NOTINt': t' \notin iota t1 (t' - t1) by apply /negP; rewrite mem_index_iota; lia .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1)) SPLIT : t2 - t1 = t' - t1 + (t2 - t') NOTINt' : t' \notin iota t1 (t' - t1)
index to (iota t1 (t' - t1)) < ind
have GT: index t' (index_iota t1 t2) >= size (iota t1 (t' - t1)).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1)) SPLIT : t2 - t1 = t' - t1 + (t2 - t') NOTINt' : t' \notin iota t1 (t' - t1)
size (iota t1 (t' - t1)) <=
index t' (index_iota t1 t2)
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1)) SPLIT : t2 - t1 = t' - t1 + (t2 - t') NOTINt' : t' \notin iota t1 (t' - t1)
size (iota t1 (t' - t1)) <=
index t' (index_iota t1 t2)
rewrite /index_iota SPLIT iotaD index_cat.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1)) SPLIT : t2 - t1 = t' - t1 + (t2 - t') NOTINt' : t' \notin iota t1 (t' - t1)
size (iota t1 (t' - t1)) <=
(if t' \in iota t1 (t' - t1)
then index t' (iota t1 (t' - t1))
else
size (iota t1 (t' - t1)) +
index t' (iota (t1 + (t' - t1)) (t2 - t')))
have ->: t' \in iota t1 (t' - t1) = false; try by lia .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1)) SPLIT : t2 - t1 = t' - t1 + (t2 - t') NOTINt' : t' \notin iota t1 (t' - t1)
size (iota t1 (t' - t1)) <=
size (iota t1 (t' - t1)) +
index t' (iota (t1 + (t' - t1)) (t2 - t'))
rewrite size_iota; by lia . } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1)) SPLIT : t2 - t1 = t' - t1 + (t2 - t') NOTINt' : t' \notin iota t1 (t' - t1) GT : size (iota t1 (t' - t1)) <=
index t' (index_iota t1 t2)
index to (iota t1 (t' - t1)) < ind
move : LT; rewrite size_iota => LT.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' SPLIT : t2 - t1 = t' - t1 + (t2 - t') NOTINt' : t' \notin iota t1 (t' - t1) GT : size (iota t1 (t' - t1)) <=
index t' (index_iota t1 t2) LT : index to (iota t1 (t' - t1)) < t' - t1
index to (iota t1 (t' - t1)) < ind
move : GT; rewrite size_iota {2 }/t' index_uniq; try by lia .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' SPLIT : t2 - t1 = t' - t1 + (t2 - t') NOTINt' : t' \notin iota t1 (t' - t1) LT : index to (iota t1 (t' - t1)) < t' - t1
ind < size (index_iota t1 t2)
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' SPLIT : t2 - t1 = t' - t1 + (t2 - t') NOTINt' : t' \notin iota t1 (t' - t1) LT : index to (iota t1 (t' - t1)) < t' - t1
ind < size (index_iota t1 t2)
by rewrite /ind /P. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' SPLIT : t2 - t1 = t' - t1 + (t2 - t') NOTINt' : t' \notin iota t1 (t' - t1) LT : index to (iota t1 (t' - t1)) < t' - t1
uniq (index_iota t1 t2)
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' SPLIT : t2 - t1 = t' - t1 + (t2 - t') NOTINt' : t' \notin iota t1 (t' - t1) LT : index to (iota t1 (t' - t1)) < t' - t1
uniq (index_iota t1 t2)
by apply iota_uniq. } } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1)) indexLT : index to (index_iota t1 t2) < ind
~~ (suspended sched j to && (service sched j to == ρ))
have : P to = false.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1)) indexLT : index to (index_iota t1 t2) < ind
P to = false
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1)) indexLT : index to (index_iota t1 t2) < ind
P to = false
apply (@before_find _ 0 P (index_iota t1 t2) _) in indexLT.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1)) indexLT : P
(nth 0 (index_iota t1 t2)
(index to (index_iota t1 t2))) = false
P to = false
rewrite nth_index in indexLT => //=.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1))
to \in index_iota t1 t2
move : INto; rewrite mem_index_iota => INto.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1)) INto : t1 <= to < t'
to \in index_iota t1 t2
rewrite mem_index_iota; lia . } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work H_exists : exists2
t : Datatypes_nat__canonical__eqtype_Equality,
t \in index_iota t1 t2 &
suspended sched j t &&
(service sched j t == ρ)P := fun t : instant =>
suspended sched j t && (service sched j t == ρ): instant -> bool ind := find P (index_iota t1 t2) : nat t' := nth 0 (index_iota t1 t2) ind : nat indLT : find
(fun t : nat =>
suspended sched j t &&
(service sched j t == ρ))
(index_iota t1 t2) <
size (index_iota t1 t2) INt' : t1 <= t' < t2 SUSt' : suspended sched j t' SERVt' : service sched j t' = ρ to : nat INto : to \in index_iota t1 t' LT : index to (iota t1 (t' - t1)) <
size (iota t1 (t' - t1)) indexLT : index to (index_iota t1 t2) < ind
P to = false ->
~~ (suspended sched j to && (service sched j to == ρ))
by rewrite /P => ->.
Qed .
End Step2 .
(** Finally we prove the required result. *)
Lemma suspension_bounded_in_interval :
\sum_(t1 <= t < t2 | service sched j t == ρ) suspended sched j t <= job_suspension j ρ.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work
\sum_(t1 <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work
\sum_(t1 <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
have [/hasP HAS|/hasPn NOTHAS] := boolP(has (fun t => (suspended sched j t && (service sched j t == ρ))) (index_iota t1 t2)).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work HAS : exists2
x : Datatypes_nat__canonical__eqtype_Equality,
x \in index_iota t1 t2 &
suspended sched j x &&
(service sched j x == ρ)
\sum_(t1 <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work HAS : exists2
x : Datatypes_nat__canonical__eqtype_Equality,
x \in index_iota t1 t2 &
suspended sched j x &&
(service sched j x == ρ)
\sum_(t1 <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
move : (exists_some_point HAS) => [tf [INtf [SUStf [SERVtf tfFirst]]]].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work HAS : exists2
x : Datatypes_nat__canonical__eqtype_Equality,
x \in index_iota t1 t2 &
suspended sched j x &&
(service sched j x == ρ)tf : nat INtf : t1 <= tf < t2 SUStf : suspended sched j tf SERVtf : service sched j tf = ρ tfFirst : forall to : nat,
t1 <= to < tf ->
~~
(suspended sched j to &&
(service sched j to == ρ))
\sum_(t1 <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
by apply : suspension_bounded_in_interval_aux. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work NOTHAS : {in index_iota t1 t2,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
~~
(suspended sched j x &&
(service sched j x == ρ))}
\sum_(t1 <= t < t2 | service sched j t == ρ)
suspended sched j t <= job_suspension j ρ
have ->: \sum_(t1 <= t < t2 | service sched j t == ρ) suspended sched j t = 0 => //=.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work NOTHAS : {in index_iota t1 t2,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
~~
(suspended sched j x &&
(service sched j x == ρ))}
\sum_(t1 <= t < t2 | service sched j t == ρ)
suspended sched j t = 0
apply /eqP; rewrite sum_nat_eq0_nat.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work NOTHAS : {in index_iota t1 t2,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
~~
(suspended sched j x &&
(service sched j x == ρ))}
all
(fun x : Datatypes_nat__canonical__eqtype_Equality
=> suspended sched j x == 0 )
[seq x <- index_iota t1 t2 | service sched j x == ρ]
apply /allP => [to INto].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work NOTHAS : {in index_iota t1 t2,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
~~
(suspended sched j x &&
(service sched j x == ρ))} to : Datatypes_nat__canonical__eqtype_Equality INto : to
\in [seq x <- index_iota t1 t2
| service sched j x == ρ]
suspended sched j to == 0
move : INto; rewrite mem_filter => /andP[SERVto INto].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work NOTHAS : {in index_iota t1 t2,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
~~
(suspended sched j x &&
(service sched j x == ρ))} to : Datatypes_nat__canonical__eqtype_Equality SERVto : service sched j to == ρ INto : to \in index_iota t1 t2
suspended sched j to == 0
move : (NOTHAS to INto); rewrite SERVto andbT.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobSuspension Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq j : Job t1, t2 : instant ρ : work NOTHAS : {in index_iota t1 t2,
forall
x : Datatypes_nat__canonical__eqtype_Equality,
~~
(suspended sched j x &&
(service sched j x == ρ))} to : Datatypes_nat__canonical__eqtype_Equality SERVto : service sched j to == ρ INto : to \in index_iota t1 t2
~~ suspended sched j to -> suspended sched j to == 0
by move => /negPf ->.
Qed .
End SuspensionBoundedinInterval .
End Suspensions .