Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.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.schedule.scheduled.[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 ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_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]
Require Export prosa.model.aggregate.workload.
Require Export prosa.model.aggregate.service_of_jobs.
Require Export prosa.analysis.facts.model.service_of_jobs.
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.facts.model.scheduled.
(** * Service Received by Sets of Jobs in Uniprocessor Ideal-Progress Schedules *)
(** In this file, we establish a fact about the service received by _sets_ of
jobs in the presence of idle times on a uniprocessor under the
ideal-progress assumption (i.e., that a scheduled job necessarily receives
nonzero service). *)
Section IdealModelLemmas .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** Allow for any uniprocessor model that ensures ideal progress. *)
Context {PState : ProcessorState Job}.
Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
Hypothesis H_uniproc : uniprocessor_model PState.
(** Next, consider any ideal uni-processor schedule of this arrival sequence ... *)
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Let [P] be any predicate over jobs. *)
Variable P : pred Job.
(** We prove that if the total service within some time interval <<[t1,t2)>>
is smaller than <<t2 - t1>>, then there is an idle time instant [t ∈ [t1,t2)]. *)
Lemma low_service_implies_existence_of_idle_time :
forall t1 t2 ,
service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
exists t , t1 <= t < t2 /\ is_idle arr_seq sched t.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job
forall t1 t2 : instant,
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job
forall t1 t2 : instant,
service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
move => t1 t2 SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
destruct (t1 <= t2) eqn :LE; last first .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = false
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = false
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
move : LE => /negP/negP; rewrite -ltnNge.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1
t2 < t1 ->
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
move => LT; apply ltnW in LT; rewrite -subn_eq0 in LT.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LT : t2 - t1 == 0
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
by move : LT => /eqP -> in SERV; rewrite ltn0 in SERV.
} Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = true
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
have EX: exists δ , t2 = t1 + δ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = true
exists δ : nat, t2 = t1 + δ
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = true
exists δ : nat, t2 = t1 + δ
by exists (t2 - t1); rewrite subnKC // ltnW. } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1, t2 : instant SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 t2) t1 t2 <
t2 - t1 LE : (t1 <= t2) = true EX : exists δ : nat, t2 = t1 + δ
exists t : nat,
t1 <= t < t2 /\ is_idle arr_seq sched t
move : EX => [δ EQ]; subst t2; clear LE.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ : nat SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 (t1 + δ)) t1
(t1 + δ) <
t1 + δ - t1
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
rewrite {3 }[t1 + δ]addnC -addnBA // subnn addn0 in SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ : nat SERV : service_of_jobs sched predT
(arrivals_between arr_seq 0 (t1 + δ)) t1
(t1 + δ) < δ
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
rewrite /service_of_jobs exchange_big //= in SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ : nat SERV : \sum_(t1 <= j <
t1 + δ)
\sum_(i <-
arrivals_between arr_seq 0
(t1 + δ))
service_at sched i j < δ
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
apply sum_le_summation_range in SERV.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ : nat SERV : exists x : nat,
t1 <= x < t1 + δ /\
\sum_(i <-
arrivals_between arr_seq 0
(t1 + δ))
service_at sched i x = 0
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
move : SERV => [x [/andP [GEx LEx] L]].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ L : \sum_(i <-
arrivals_between arr_seq 0 (t1 + δ))
service_at sched i x = 0
exists t : nat,
t1 <= t < t1 + δ /\ is_idle arr_seq sched t
exists x ; split ; first by apply /andP; split .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ L : \sum_(i <-
arrivals_between arr_seq 0 (t1 + δ))
service_at sched i x = 0
is_idle arr_seq sched x
apply /negPn/negP; rewrite is_nonidle_iff //= => [[j SCHED]].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ L : \sum_(i <-
arrivals_between arr_seq 0 (t1 + δ))
service_at sched i x = 0 j : Job SCHED : scheduled_at sched j x
False
move : L => /eqP; rewrite sum_nat_eq0_nat filter_predT => /allP L.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ j : Job SCHED : scheduled_at sched j x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 }
False
have /eqP: service_at sched j x == 0 .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ j : Job SCHED : scheduled_at sched j x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 }
service_at sched j x == 0
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ j : Job SCHED : scheduled_at sched j x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 }
service_at sched j x == 0
apply /L/arrived_between_implies_in_arrivals => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ j : Job SCHED : scheduled_at sched j x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 }
arrived_between j 0 (t1 + δ)
rewrite /arrived_between; apply /andP; split => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ j : Job SCHED : scheduled_at sched j x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 }
job_arrival j < t1 + δ
have : job_arrival j <= x by apply : H_jobs_must_arrive_to_execute.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ j : Job SCHED : scheduled_at sched j x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 }
job_arrival j <= x -> job_arrival j < t1 + δ
lia . } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job H1 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_uniproc : uniprocessor_model PState sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched P : pred Job t1 : instant δ, x : nat GEx : t1 <= x LEx : x < t1 + δ j : Job SCHED : scheduled_at sched j x L : {in arrivals_between arr_seq 0 (t1 + δ),
forall x0 : Job, service_at sched x0 x == 0 }
service_at sched j x = 0 -> False
by rewrite -no_service_not_scheduled // => /negP.
Qed .
End IdealModelLemmas .