Built with Alectryon, running Coq+SerAPI v8.14.0+0.14.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.
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** Throughout this file, we assume ideal uni-processor schedules. *)
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** Note: we do not re-export the basic definitions to avoid littering the global namespace with type class instances. *)(** In this section we establish the classes to which an ideal schedule belongs. *)SectionScheduleClass.LocalTransparent service_in scheduled_in scheduled_on.(** Consider any job type and the ideal processor model. *)Context {Job: JobType}.Context `{JobArrival Job}.Context `{JobCost Job}.(** We note that the ideal processor model is indeed a uni-processor model. *)
Job: JobType H: JobArrival Job H0: JobCost Job
uniprocessor_model (processor_state Job)
Job: JobType H: JobArrival Job H0: JobCost Job
uniprocessor_model (processor_state Job)
Job: JobType H: JobArrival Job H0: JobCost Job j1, j2: Job sched: schedule (processor_state Job) t: instant E1: sched t = Some j1 E2: sched t = Some j2
j1 = j2
bymove: E1 E2=>->[].Qed.(** We observe that the ideal processor model falls into the category of ideal-progress models, i.e., a scheduled job always receives service. *)
byrewrite /service_at service_in_is_scheduled_in.Qed.(** Next we prove a lemma which helps us to do a case analysis on the state of an ideal schedule. *)
byleft; auto.Qed.EndScheduleClass.(** * Incremental Service in Ideal Schedule *)(** In the following section we prove a few facts about service in ideal schedule. *)(* Note that these lemmas can be generalized to an arbitrary scheduler. *)SectionIncrementalService.(** Consider any job type, ... *)Context {Job : JobType}.Context `{JobArrival Job}.Context `{JobCost Job}.(** ... any arrival sequence, ... *)Variablearr_seq : arrival_sequence Job.(** ... and any ideal uni-processor schedule of this arrival sequence. *)Variablesched : schedule (ideal.processor_state Job).(** As a base case, we prove that if a job j receives service in some time interval <<[t1,t2)>>, then there exists a time instant t ∈ [t1,t2) such that j is scheduled at time t and t is the first instant where j receives service. *)
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant LE: t1 <= t2 SCHED: ~~ scheduled_at sched j t1 t: nat_eqType SCHEDt: sched t == Some j IN1: t1 <= t IN2: t < t2 x: nat T1: t1 < x T4: x <= t T2: forallx0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0 T3: scheduled_at sched j x
t1 <= x < t2
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant LE: t1 <= t2 SCHED: ~~ scheduled_at sched j t1 t: nat_eqType SCHEDt: sched t == Some j IN1: t1 <= t IN2: t < t2 x: nat T1: t1 < x T4: x <= t T2: forallx0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0 T3: scheduled_at sched j x
\sum_(t1 <= t < x) service_at sched j t = 0
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant LE: t1 <= t2 SCHED: ~~ scheduled_at sched j t1 t: nat_eqType SCHEDt: sched t == Some j IN1: t1 <= t IN2: t < t2 x: nat T1: t1 < x T4: x <= t T2: forallx0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0 T3: scheduled_at sched j x
t1 <= x < t2
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant LE: t1 <= t2 SCHED: ~~ scheduled_at sched j t1 t: nat_eqType SCHEDt: sched t == Some j IN1: t1 <= t IN2: t < t2 x: nat T1: t1 < x T4: x <= t T2: forallx0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0 T3: scheduled_at sched j x
\sum_(t1 <= t < x) service_at sched j t = 0
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant LE: t1 <= t2 SCHED: ~~ scheduled_at sched j t1 t: nat_eqType SCHEDt: sched t == Some j IN1: t1 <= t IN2: t < t2 x: nat T1: t1 < x T4: x <= t T2: forallx0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0 T3: scheduled_at sched j x
x < t2
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant LE: t1 <= t2 SCHED: ~~ scheduled_at sched j t1 t: nat_eqType SCHEDt: sched t == Some j IN1: t1 <= t IN2: t < t2 x: nat T1: t1 < x T4: x <= t T2: forallx0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0 T3: scheduled_at sched j x
\sum_(t1 <= t < x) service_at sched j t = 0
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant LE: t1 <= t2 SCHED: ~~ scheduled_at sched j t1 t: nat_eqType SCHEDt: sched t == Some j IN1: t1 <= t IN2: t < t2 x: nat T1: t1 < x T4: x <= t T2: forallx0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0 T3: scheduled_at sched j x
\sum_(t1 <= t < x) service_at sched j t = 0
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant LE: t1 <= t2 SCHED: ~~ scheduled_at sched j t1 t: nat_eqType SCHEDt: sched t == Some j IN1: t1 <= t IN2: t < t2 x: nat T1: t1 < x T4: x <= t T2: forallx0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0 T3: scheduled_at sched j x
\sum_(t1 <= t < x) service_at sched j t = 0
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant LE: t1 <= t2 SCHED: ~~ scheduled_at sched j t1 t: nat_eqType SCHEDt: sched t == Some j IN1: t1 <= t IN2: t < t2 x: nat T1: t1 < x T4: x <= t T2: forallx0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0 T3: scheduled_at sched j x
foralli : nat,
(t1 <= i < x) && true -> service_at sched j i = 0
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant LE: t1 <= t2 SCHED: ~~ scheduled_at sched j t1 t: nat_eqType SCHEDt: sched t == Some j IN1: t1 <= t IN2: t < t2 x: nat T1: t1 < x T4: x <= t T2: forallx0 : nat,
t1 <= x0 < x -> ~~ scheduled_at sched j x0 T3: scheduled_at sched j x y: nat T5: t1 <= y < x
service_at sched j y = 0
byapply/eqP; rewrite eqb0; specialize (T2 y); rewrite scheduled_at_def/= in T2; apply T2.}Qed.(** Next, we prove that if in some time interval <<[t1,t2)>> a job j receives k units of service, then there exists a time instant t ∈ [t1,t2) such that j is scheduled at time t and service of job j within interval [t1,t) is equal to k. *)
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: service_during sched j t1 t.+1 = k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
t1 <= y < t2
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: service_during sched j t1 t.+1 = k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: service_during sched j t1 t.+1 = k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
t1 <= y < t2
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: service_during sched j t1 t.+1 = k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: service_during sched j t1 t.+1 = k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
t1 <= y
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: service_during sched j t1 t.+1 = k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
y < t2
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: service_during sched j t1 t.+1 = k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: service_during sched j t1 t.+1 = k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
t <= y
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: service_during sched j t1 t.+1 = k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
y < t2
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: service_during sched j t1 t.+1 = k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: service_during sched j t1 t.+1 = k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
y < t2
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: service_during sched j t1 t.+1 = k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: service_during sched j t1 t.+1 = k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: service_during sched j t1 t.+1 = k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
\sum_(t1 <= t < y) service_at sched j t = k.+1
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: service_during sched j t1 t.+1 = k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
\sum_(t1 <= i < t.+1) (sched i == Some j) +
\sum_(t.+1 <= i < y) (sched i == Some j) = k.+1
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: \sum_(t1 <= t < t.+1) service_at sched j t =
k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
k.+1 + \sum_(t.+1 <= i < y) (sched i == Some j) ==
k.+1
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: \sum_(t1 <= t < t.+1) service_at sched j t =
k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y
\sum_(t.+1 <= i < y) (sched i == Some j) == 0
Job: JobType H: JobArrival Job H0: JobCost Job arr_seq: arrival_sequence Job sched: schedule (processor_state Job) j: Job t1, t2: instant k: nat LE: t1 <= t2 t: nat NEQ1: t1 <= t NEQ2: t < t2 SCHEDt: scheduled_at sched j t SERVk: service_during sched j t1 t = k SERVk1: \sum_(t1 <= t < t.+1) service_at sched j t =
k.+1 SCHED: ~~ scheduled_at sched j t.+1 x: nat_eqType SCHEDx: sched x == Some j INx1: t < x INx2: x < t2 y: nat T1: t.+1 < y T4: y <= x T2: forallx : nat,
t < x < y -> ~~ scheduled_at sched j x T3: scheduled_at sched j y z: nat H5: t < z < y
(sched z == Some j) = 0
byapply/eqP; rewrite eqb0; specialize (T2 z); rewrite scheduled_at_def/= in T2; apply T2.Qed.EndIncrementalService.(** * Automation *)(** We add the above lemmas into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)GlobalHint Resolve ideal_proc_model_is_a_uniprocessor_model
ideal_proc_model_ensures_ideal_progress
ideal_proc_model_provides_unit_service : basic_facts.(** We also provide tactics for case analysis on ideal processor state. *)(** The first tactic generates two sub-goals: one with idle processor and the other with processor executing a job named [JobName]. *)Ltacideal_proc_model_sched_case_analysis sched t JobName :=
letIdle := fresh"Idle"inletSched := fresh"Sched_" JobName indestruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]].(** The second tactic is similar to the first, but it additionally generates two equalities: [sched t = None] and [sched t = Some j]. *)Ltacideal_proc_model_sched_case_analysis_eq sched t JobName :=
letIdle := fresh"Idle"inletIdleEq := fresh"Eq" Idle inletSched := fresh"Sched_" JobName inletSchedEq := fresh"Eq" Sched indestruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]];
[move: (Idle) => /eqP IdleEq; rewrite?IdleEq
| move: (Sched); simpl; move => /eqP SchedEq; rewrite?SchedEq].