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.analysis.facts.model.task_arrivals.[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]
Require Export prosa.implementation.definitions.maximal_arrival_sequence.
(** Recall that, given an arrival curve [max_arrivals] and a
job-generating function [generate_jobs_at], the function
[concrete_arrival_sequence] generates an arrival sequence. In this
section, we prove a few properties of this function. *)
Section MaximalArrivalSequence .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider a task set [ts] with non-duplicate tasks. *)
Variable ts : seq Task.
Hypothesis H_ts_uniq : uniq ts.
(** Let [max_arrivals] be a family of valid arrival curves, i.e.,
for any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival
bound of [tsk], and (2) it is a monotonic function that equals [0]
for the empty interval [delta = 0]. *)
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
(** Further assume we are given a function that generates the required number of
jobs of a given task at a given instant of time. *)
Variable generate_jobs_at : Task -> nat -> instant -> seq Job.
(** First, we assume that [generate_jobs_at tsk n t] generates [n] jobs. *)
Hypothesis H_job_generation_valid_number :
forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n.
(** Second, we assume that [generate_jobs_at tsk n t] generates jobs of task
[tsk] that arrive at time [t]. *)
Hypothesis H_job_generation_valid_jobs :
forall (tsk : Task) (n : nat) (t : instant) (j : Job),
(j \in generate_jobs_at tsk n t) ->
job_task j = tsk
/\ job_arrival j = t
/\ job_cost j <= task_cost tsk.
(** Finally, we assume that all jobs generated by [generate_jobs_at] are unique. *)
Hypothesis H_jobs_unique :
forall (t1 t2 : instant),
uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2).
(** Assuming such a well-behaved "constructor" [generate_jobs_at], we prove a
few validity claims about an arrival sequence generated by
[concrete_arrival_sequence]. *)
Section ValidityClaims .
(** We start by showing that the obtained arrival sequence is a set. *)
Lemma arr_seq_is_a_set :
arrival_sequence_uniq (concrete_arrival_sequence generate_jobs_at ts).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)
arrival_sequence_uniq
(concrete_arrival_sequence generate_jobs_at ts)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)
arrival_sequence_uniq
(concrete_arrival_sequence generate_jobs_at ts)
move => t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)t : instant
uniq
(arrivals_at
(concrete_arrival_sequence generate_jobs_at ts) t)
move : (H_jobs_unique t t.+1 ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)t : instant
uniq
(arrivals_between
(concrete_arrival_sequence generate_jobs_at ts) t
t.+1 ) ->
uniq
(arrivals_at
(concrete_arrival_sequence generate_jobs_at ts) t)
by rewrite /arrivals_between big_nat1.
Qed .
(** Next, we show that all jobs in the arrival sequence come from [ts]. *)
Lemma concrete_all_jobs_from_taskset :
all_jobs_from_taskset (concrete_arrival_sequence generate_jobs_at ts) ts.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)
all_jobs_from_taskset
(concrete_arrival_sequence generate_jobs_at ts) ts
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)
all_jobs_from_taskset
(concrete_arrival_sequence generate_jobs_at ts) ts
move => j [t /mem_bigcat_exists [tsk [TSK_IN IN]]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)j : Job t : instant tsk : Task TSK_IN : tsk \in ts IN : j
\in generate_jobs_at tsk
(max_arrivals_at tsk t) t
job_task j \in ts
move : (H_job_generation_valid_jobs tsk _ _ _ IN) => [JOB_TASK _].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)j : Job t : instant tsk : Task TSK_IN : tsk \in ts IN : j
\in generate_jobs_at tsk
(max_arrivals_at tsk t) t JOB_TASK : job_task j = tsk
job_task j \in ts
by rewrite JOB_TASK.
Qed .
(** Further, we note that the jobs in the arrival sequence have consistent
arrival times. *)
Lemma arrival_times_are_consistent :
consistent_arrival_times (concrete_arrival_sequence generate_jobs_at ts).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)
consistent_arrival_times
(concrete_arrival_sequence generate_jobs_at ts)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)
consistent_arrival_times
(concrete_arrival_sequence generate_jobs_at ts)
move => j t /mem_bigcat_exists [tsk [TSK_IN IN]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)j : Job t : instant tsk : Task TSK_IN : tsk \in ts IN : j
\in generate_jobs_at tsk
(max_arrivals_at tsk t) t
job_arrival j = t
by move : (H_job_generation_valid_jobs tsk _ _ _ IN) => [_ [JOB_ARR _]].
Qed .
(** Lastly, we observe that the jobs in the arrival sequence have valid job
costs. *)
Lemma concrete_valid_job_cost :
arrivals_have_valid_job_costs (concrete_arrival_sequence generate_jobs_at ts).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)
arrivals_have_valid_job_costs
(concrete_arrival_sequence generate_jobs_at ts)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)
arrivals_have_valid_job_costs
(concrete_arrival_sequence generate_jobs_at ts)
move => j [t /mem_bigcat_exists [tsk [TSK_IN IN]]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)j : Job t : instant tsk : Task TSK_IN : tsk \in ts IN : j
\in generate_jobs_at tsk
(max_arrivals_at tsk t) t
valid_job_cost j
move : (H_job_generation_valid_jobs tsk _ _ _ IN) => [JOB_TASK [_ JOB_COST]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)j : Job t : instant tsk : Task TSK_IN : tsk \in ts IN : j
\in generate_jobs_at tsk
(max_arrivals_at tsk t) t JOB_TASK : job_task j = tsk JOB_COST : job_cost j <= task_cost tsk
valid_job_cost j
by rewrite /valid_job_cost JOB_TASK.
Qed .
End ValidityClaims .
(** In this section, we prove a series of facts regarding the maximal arrival
sequence, leading up to the main theorem that all arrival-curve
constraints are respected. *)
Section Facts .
(** Let [tsk] be any task in [ts] that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** First, we show that the arrivals at time [t] are indeed generated by
[generate_jobs_at] applied at time [t]. *)
Lemma task_arrivals_at_eq_generate_jobs_at :
forall t ,
task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t
= generate_jobs_at tsk (max_arrivals_at tsk t) t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t : instant,
task_arrivals_at
(concrete_arrival_sequence generate_jobs_at ts) tsk
t = generate_jobs_at tsk (max_arrivals_at tsk t) t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t : instant,
task_arrivals_at
(concrete_arrival_sequence generate_jobs_at ts) tsk
t = generate_jobs_at tsk (max_arrivals_at tsk t) t
move => t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t : instant
task_arrivals_at
(concrete_arrival_sequence generate_jobs_at ts) tsk
t = generate_jobs_at tsk (max_arrivals_at tsk t) t
rewrite /task_arrivals_at bigcat_filter_eq_filter_bigcat bigcat_seq_uniqK // => tsk0 j INj.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t : instant tsk0 : Task j : Job INj : j
\in generate_jobs_at tsk0
(max_arrivals_at tsk0 t) t
job_task j = tsk0
apply H_job_generation_valid_jobs in INj.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t : instant tsk0 : Task j : Job INj : job_task j = tsk0 /\
job_arrival j = t /\
job_cost j <= task_cost tsk0
job_task j = tsk0
by destruct INj.
Qed .
(** Next, we show that the number of arrivals at time [t] always matches
[max_arrivals_at] applied at time [t]. *)
Lemma task_arrivals_at_eq :
forall t ,
size (task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t)
= max_arrivals_at tsk t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t : instant,
size
(task_arrivals_at
(concrete_arrival_sequence generate_jobs_at ts)
tsk t) = max_arrivals_at tsk t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t : instant,
size
(task_arrivals_at
(concrete_arrival_sequence generate_jobs_at ts)
tsk t) = max_arrivals_at tsk t
by move => t; rewrite task_arrivals_at_eq_generate_jobs_at. Qed .
(** We then generalize the previous result to an arbitrary interval
<<[t1,t2)>>. *)
Lemma number_of_task_arrivals_eq :
forall t1 t2 ,
number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk t1 t2
= \sum_(t1 <= t < t2) max_arrivals_at tsk t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t1 t2 : instant,
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts) tsk
t1 t2 = \sum_(t1 <= t < t2) max_arrivals_at tsk t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t1 t2 : instant,
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts) tsk
t1 t2 = \sum_(t1 <= t < t2) max_arrivals_at tsk t
move => t1 t2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t1, t2 : instant
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts) tsk
t1 t2 = \sum_(t1 <= t < t2) max_arrivals_at tsk t
rewrite /number_of_task_arrivals task_arrivals_between_is_cat_of_task_arrivals_at -size_big_nat.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t1, t2 : instant
\sum_(t1 <= t < t2)
size
(task_arrivals_at
(concrete_arrival_sequence generate_jobs_at ts)
tsk t) =
\sum_(t1 <= t < t2) max_arrivals_at tsk t
apply eq_big_nat => t RANGE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t1, t2 : instant t : nat RANGE : t1 <= t < t2
size
(task_arrivals_at
(concrete_arrival_sequence generate_jobs_at ts)
tsk t) = max_arrivals_at tsk t
by apply task_arrivals_at_eq.
Qed .
(** We further show that, starting from an empty prefix and applying
[extend_arrival_prefix] [t] times, we end up with a prefix of size
[t]... *)
Lemma extend_horizon_size :
forall t ,
size (iter t (extend_arrival_prefix tsk) [::]) = t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t : nat,
size (iter t (extend_arrival_prefix tsk) [::]) = t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t : nat,
size (iter t (extend_arrival_prefix tsk) [::]) = t
by elim => // t IHt; rewrite size_cat IHt //=; lia . Qed .
(** ...and that the arrival sequence prefix up to an arbitrary horizon
[t] is a sequence of [t+1] elements. *)
Lemma prefix_up_to_size :
forall t ,
size (maximal_arrival_prefix tsk t) = t.+1 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t : nat,
size (maximal_arrival_prefix tsk t) = t.+1
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t : nat,
size (maximal_arrival_prefix tsk t) = t.+1
by elim => // t IHt; rewrite /maximal_arrival_prefix /extend_arrival_prefix size_cat IHt //=; lia .
Qed .
(** Next, we prove prefix inclusion for [maximal_arrival_prefix] when the
horizon is expanded by one... *)
Lemma n_arrivals_at_prefix_inclusion1 :
forall t h ,
t <= h ->
nth 0 (maximal_arrival_prefix tsk h) t
= nth 0 (maximal_arrival_prefix tsk h.+1 ) t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t h : nat,
t <= h ->
nth 0 (maximal_arrival_prefix tsk h) t =
nth 0 (maximal_arrival_prefix tsk h.+1 ) t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t h : nat,
t <= h ->
nth 0 (maximal_arrival_prefix tsk h) t =
nth 0 (maximal_arrival_prefix tsk h.+1 ) t
move => t h LEQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, h : nat LEQ : t <= h
nth 0 (maximal_arrival_prefix tsk h) t =
nth 0 (maximal_arrival_prefix tsk h.+1 ) t
rewrite /maximal_arrival_prefix //= {3 }/extend_arrival_prefix nth_cat prefix_up_to_size.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, h : nat LEQ : t <= h
nth 0
(extend_arrival_prefix tsk
(iter h (extend_arrival_prefix tsk) [::])) t =
(if t < h.+1
then
nth 0
(extend_arrival_prefix tsk
(iter h (extend_arrival_prefix tsk) [::])) t
else
nth 0
[:: next_max_arrival tsk
(extend_arrival_prefix tsk
(iter h (extend_arrival_prefix tsk) [::]))]
(t - h.+1 ))
by case : (ltnP t h.+1 ); lia .
Qed .
(** ...and we generalize the previous result to two arbitrary horizons [h1 <= h2]. *)
Lemma n_arrivals_at_prefix_inclusion :
forall t h1 h2 ,
t <= h1 <= h2 ->
nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t h1 h2 : nat,
t <= h1 <= h2 ->
nth 0 (maximal_arrival_prefix tsk h1) t =
nth 0 (maximal_arrival_prefix tsk h2) t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t h1 h2 : nat,
t <= h1 <= h2 ->
nth 0 (maximal_arrival_prefix tsk h1) t =
nth 0 (maximal_arrival_prefix tsk h2) t
move => t h1 h2 /andP[LEQh1 LEQh2].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, h1, h2 : nat LEQh1 : t <= h1 LEQh2 : h1 <= h2
nth 0 (maximal_arrival_prefix tsk h1) t =
nth 0 (maximal_arrival_prefix tsk h2) t
elim : h2 LEQh2 => [|h2 IHh2] LEQh2; [by have -> : h1 = 0 ; lia |].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, h1 : nat LEQh1 : t <= h1 h2 : nat IHh2 : h1 <= h2 ->
nth 0 (maximal_arrival_prefix tsk h1) t =
nth 0 (maximal_arrival_prefix tsk h2) t LEQh2 : h1 <= h2.+1
nth 0 (maximal_arrival_prefix tsk h1) t =
nth 0 (maximal_arrival_prefix tsk h2.+1 ) t
rewrite leq_eqVlt in LEQh2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, h1 : nat LEQh1 : t <= h1 h2 : nat IHh2 : h1 <= h2 ->
nth 0 (maximal_arrival_prefix tsk h1) t =
nth 0 (maximal_arrival_prefix tsk h2) t LEQh2 : (h1 == h2.+1 ) || (h1 < h2.+1 )
nth 0 (maximal_arrival_prefix tsk h1) t =
nth 0 (maximal_arrival_prefix tsk h2.+1 ) t
move : LEQh2 => /orP [/eqP EQ | LT]; first by rewrite EQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, h1 : nat LEQh1 : t <= h1 h2 : nat IHh2 : h1 <= h2 ->
nth 0 (maximal_arrival_prefix tsk h1) t =
nth 0 (maximal_arrival_prefix tsk h2) t LT : h1 < h2.+1
nth 0 (maximal_arrival_prefix tsk h1) t =
nth 0 (maximal_arrival_prefix tsk h2.+1 ) t
feed IHh2; first by lia . Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, h1 : nat LEQh1 : t <= h1 h2 : nat IHh2 : nth 0 (maximal_arrival_prefix tsk h1) t =
nth 0 (maximal_arrival_prefix tsk h2) t LT : h1 < h2.+1
nth 0 (maximal_arrival_prefix tsk h1) t =
nth 0 (maximal_arrival_prefix tsk h2.+1 ) t
rewrite -n_arrivals_at_prefix_inclusion1 //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, h1 : nat LEQh1 : t <= h1 h2 : nat IHh2 : nth 0 (maximal_arrival_prefix tsk h1) t =
nth 0 (maximal_arrival_prefix tsk h2) t LT : h1 < h2.+1
t <= h2
by lia .
Qed .
(** Next, we prove that, for any positive time instant [t], [max_arrivals_at] indeed
matches the arrivals of [next_max_arrival] applied at [t-1]. *)
Lemma max_arrivals_at_next_max_arrivals_eq :
forall t ,
0 < t ->
max_arrivals_at tsk t
= next_max_arrival tsk (maximal_arrival_prefix tsk t.-1 ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t : nat,
0 < t ->
max_arrivals_at tsk t =
next_max_arrival tsk (maximal_arrival_prefix tsk t.-1 )
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t : nat,
0 < t ->
max_arrivals_at tsk t =
next_max_arrival tsk (maximal_arrival_prefix tsk t.-1 )
move => t GT0.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t : nat GT0 : 0 < t
max_arrivals_at tsk t =
next_max_arrival tsk (maximal_arrival_prefix tsk t.-1 )
move : prefix_up_to_size; rewrite /maximal_arrival_prefix => PUS.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t : nat GT0 : 0 < tPUS : forall t : nat,
size
(iter t.+1 (extend_arrival_prefix tsk) [::]) =
t.+1
max_arrivals_at tsk t =
next_max_arrival tsk
(iter t.-1 .+1 (extend_arrival_prefix tsk) [::])
rewrite /max_arrivals_at /maximal_arrival_prefix {1 }/extend_arrival_prefix nth_cat extend_horizon_size //= ltnn //= subnn //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t : nat GT0 : 0 < tPUS : forall t : nat,
size
(iter t.+1 (extend_arrival_prefix tsk) [::]) =
t.+1
next_max_arrival tsk
((fix loop (m : nat) : seq nat :=
match m with
| 0 => [::]
| i.+1 =>
loop i ++ [:: next_max_arrival tsk (loop i)]
end ) t) =
next_max_arrival tsk
(extend_arrival_prefix tsk
(iter t.-1 (extend_arrival_prefix tsk) [::]))
by destruct t.
Qed .
(** Given a time instant [t] and and interval [Δ], we show that
[max_arrivals_at] applied at time [t] is always less-or-equal to
[max_arrivals] applied to [Δ+1], even when each value of
[max_arrivals_at] in the interval <<[t-Δ, t)>> is subtracted from it. *)
Lemma n_arrivals_at_leq :
forall t Δ ,
Δ <= t ->
max_arrivals_at tsk t
<= max_arrivals tsk Δ.+1 - \sum_(t - Δ <= i < t) max_arrivals_at tsk i.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t Δ : nat,
Δ <= t ->
max_arrivals_at tsk t <=
max_arrivals tsk Δ.+1 -
\sum_(t - Δ <= i < t) max_arrivals_at tsk i
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts
forall t Δ : nat,
Δ <= t ->
max_arrivals_at tsk t <=
max_arrivals tsk Δ.+1 -
\sum_(t - Δ <= i < t) max_arrivals_at tsk i
move => t Δ LEQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t
max_arrivals_at tsk t <=
max_arrivals tsk Δ.+1 -
\sum_(t - Δ <= i < t) max_arrivals_at tsk i
move : (H_valid_arrival_curve tsk H_tsk_in_ts) => [ZERO MONO].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk)
max_arrivals_at tsk t <=
max_arrivals tsk Δ.+1 -
\sum_(t - Δ <= i < t) max_arrivals_at tsk i
destruct t as [|t].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts Δ : nat LEQ : Δ <= 0 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk)
max_arrivals_at tsk 0 <=
max_arrivals tsk Δ.+1 -
\sum_(0 - Δ <= i < 0 ) max_arrivals_at tsk i
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts Δ : nat LEQ : Δ <= 0 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk)
max_arrivals_at tsk 0 <=
max_arrivals tsk Δ.+1 -
\sum_(0 - Δ <= i < 0 ) max_arrivals_at tsk i
rewrite unlock //= subn0.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts Δ : nat LEQ : Δ <= 0 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk)
max_arrivals_at tsk 0 <= max_arrivals tsk Δ.+1
rewrite /max_arrivals_at /maximal_arrival_prefix /extend_arrival_prefix
/next_max_arrival //= /suffix_sum subn0 unlock subn0.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts Δ : nat LEQ : Δ <= 0 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk)
max_arrivals tsk 1 <= max_arrivals tsk Δ.+1
by apply MONO. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t.+1 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk)
max_arrivals_at tsk t.+1 <=
max_arrivals tsk Δ.+1 -
\sum_(t.+1 - Δ <= i < t.+1 ) max_arrivals_at tsk i
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t.+1 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk)
max_arrivals_at tsk t.+1 <=
max_arrivals tsk Δ.+1 -
\sum_(t.+1 - Δ <= i < t.+1 ) max_arrivals_at tsk i
rewrite max_arrivals_at_next_max_arrivals_eq; last by done .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t.+1 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk)
next_max_arrival tsk
(maximal_arrival_prefix tsk t.+1 .-1 ) <=
max_arrivals tsk Δ.+1 -
\sum_(t.+1 - Δ <= i < t.+1 ) max_arrivals_at tsk i
rewrite /next_max_arrival /jobs_remaining prefix_up_to_size.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t.+1 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk)
match
supremum leq
[seq max_arrivals tsk Δ.+1 -
suffix_sum
(maximal_arrival_prefix tsk t.+1 .-1 ) Δ
| Δ <- iota 0 t.+1 .-1 .+2 ]
with
| Some n => n
| None => max_arrivals tsk 1
end <=
max_arrivals tsk Δ.+1 -
\sum_(t.+1 - Δ <= i < t.+1 ) max_arrivals_at tsk i
simpl (t.+1 .-1 ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t.+1 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk)
match
supremum leq
[seq max_arrivals tsk Δ.+1 -
suffix_sum (maximal_arrival_prefix tsk t) Δ
| Δ <- iota 0 t.+2 ]
with
| Some n => n
| None => max_arrivals tsk 1
end <=
max_arrivals tsk Δ.+1 -
\sum_(t.+1 - Δ <= i < t.+1 ) max_arrivals_at tsk i
destruct supremum eqn :SUP; last by move :(supremum_none _ _ SUP); rewrite map_cons.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t.+1 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk) s : Datatypes_nat__canonical__eqtype_Equality SUP : supremum leq
[seq max_arrivals tsk Δ.+1 -
suffix_sum
(maximal_arrival_prefix tsk t) Δ
| Δ <-
iota 0 t.+2 ] =
Some s
s <=
max_arrivals tsk Δ.+1 -
\sum_(t.+1 - Δ <= i < t.+1 ) max_arrivals_at tsk i
eapply (supremum_spec _ leqnn leq_total leq_trans _ _ SUP).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t.+1 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk) s : Datatypes_nat__canonical__eqtype_Equality SUP : supremum leq
[seq max_arrivals tsk Δ.+1 -
suffix_sum
(maximal_arrival_prefix tsk t) Δ
| Δ <-
iota 0 t.+2 ] =
Some s
max_arrivals tsk Δ.+1 -
\sum_(t.+1 - Δ <= i < t.+1 ) max_arrivals_at tsk i
\in [seq max_arrivals tsk Δ.+1 -
suffix_sum (maximal_arrival_prefix tsk t) Δ
| Δ <- iota 0 t.+2 ]
rewrite /suffix_sum prefix_up_to_size /max_arrivals_at.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t.+1 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk) s : Datatypes_nat__canonical__eqtype_Equality SUP : supremum leq
[seq max_arrivals tsk Δ.+1 -
suffix_sum
(maximal_arrival_prefix tsk t) Δ
| Δ <-
iota 0 t.+2 ] =
Some s
max_arrivals tsk Δ.+1 -
\sum_(t.+1 - Δ <= i < t.+1 )
nth 0 (maximal_arrival_prefix tsk i) i
\in [seq max_arrivals tsk Δ.+1 -
\sum_(t.+1 - Δ <= t0 < t.+1 )
nth 0 (maximal_arrival_prefix tsk t) t0
| Δ <- iota 0 t.+2 ]
have -> : \sum_(t.+1 - Δ <= i < t.+1 ) nth 0 (maximal_arrival_prefix tsk i) i =
\sum_(t.+1 - Δ <= i < t.+1 ) nth 0 (maximal_arrival_prefix tsk t) i.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t.+1 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk) s : Datatypes_nat__canonical__eqtype_Equality SUP : supremum leq
[seq max_arrivals tsk Δ.+1 -
suffix_sum
(maximal_arrival_prefix tsk t) Δ
| Δ <-
iota 0 t.+2 ] =
Some s
\sum_(t.+1 - Δ <= i < t.+1 )
nth 0 (maximal_arrival_prefix tsk i) i =
\sum_(t.+1 - Δ <= i < t.+1 )
nth 0 (maximal_arrival_prefix tsk t) i
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t.+1 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk) s : Datatypes_nat__canonical__eqtype_Equality SUP : supremum leq
[seq max_arrivals tsk Δ.+1 -
suffix_sum
(maximal_arrival_prefix tsk t) Δ
| Δ <-
iota 0 t.+2 ] =
Some s
\sum_(t.+1 - Δ <= i < t.+1 )
nth 0 (maximal_arrival_prefix tsk i) i =
\sum_(t.+1 - Δ <= i < t.+1 )
nth 0 (maximal_arrival_prefix tsk t) i
apply eq_big_nat => i RANGE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t.+1 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk) s : Datatypes_nat__canonical__eqtype_Equality SUP : supremum leq
[seq max_arrivals tsk Δ.+1 -
suffix_sum
(maximal_arrival_prefix tsk t) Δ
| Δ <-
iota 0 t.+2 ] =
Some s i : nat RANGE : t.+1 - Δ <= i < t.+1
nth 0 (maximal_arrival_prefix tsk i) i =
nth 0 (maximal_arrival_prefix tsk t) i
by apply n_arrivals_at_prefix_inclusion; lia . } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t.+1 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk) s : Datatypes_nat__canonical__eqtype_Equality SUP : supremum leq
[seq max_arrivals tsk Δ.+1 -
suffix_sum
(maximal_arrival_prefix tsk t) Δ
| Δ <-
iota 0 t.+2 ] =
Some s
max_arrivals tsk Δ.+1 -
\sum_(t.+1 - Δ <= i < t.+1 )
nth 0 (maximal_arrival_prefix tsk t) i
\in [seq max_arrivals tsk Δ.+1 -
\sum_(t.+1 - Δ <= t0 < t.+1 )
nth 0 (maximal_arrival_prefix tsk t) t0
| Δ <- iota 0 t.+2 ]
set f := fun x => max_arrivals _ x.+1 - \sum_(t.+1 -x <= i < t.+1 ) nth 0 (maximal_arrival_prefix _ t) i.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t.+1 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk) s : Datatypes_nat__canonical__eqtype_Equality SUP : supremum leq
[seq max_arrivals tsk Δ.+1 -
suffix_sum
(maximal_arrival_prefix tsk t) Δ
| Δ <-
iota 0 t.+2 ] =
Some s f := fun x : nat =>
max_arrivals tsk x.+1 -
\sum_(t.+1 - x <= i < t.+1 )
nth 0 (maximal_arrival_prefix tsk t) i: nat -> nat
max_arrivals tsk Δ.+1 -
\sum_(t.+1 - Δ <= i < t.+1 )
nth 0 (maximal_arrival_prefix tsk t) i
\in [seq f i | i <- iota 0 t.+2 ]
have -> : max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= i < t.+1 ) nth 0 (maximal_arrival_prefix tsk t) i = f Δ by done .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t.+1 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk) s : Datatypes_nat__canonical__eqtype_Equality SUP : supremum leq
[seq max_arrivals tsk Δ.+1 -
suffix_sum
(maximal_arrival_prefix tsk t) Δ
| Δ <-
iota 0 t.+2 ] =
Some s f := fun x : nat =>
max_arrivals tsk x.+1 -
\sum_(t.+1 - x <= i < t.+1 )
nth 0 (maximal_arrival_prefix tsk t) i: nat -> nat
f Δ \in [seq f i | i <- iota 0 t.+2 ]
apply map_f.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task H_tsk_in_ts : tsk \in ts t, Δ : nat LEQ : Δ <= t.+1 ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk) s : Datatypes_nat__canonical__eqtype_Equality SUP : supremum leq
[seq max_arrivals tsk Δ.+1 -
suffix_sum
(maximal_arrival_prefix tsk t) Δ
| Δ <-
iota 0 t.+2 ] =
Some s f := fun x : nat =>
max_arrivals tsk x.+1 -
\sum_(t.+1 - x <= i < t.+1 )
nth 0 (maximal_arrival_prefix tsk t) i: nat -> nat
Δ \in iota 0 t.+2
by rewrite mem_iota; lia . }
Qed .
End Facts .
(** Finally, we prove our main result, that is, the proposed maximal arrival
sequence instantiation indeed respects all arrival-curve constraints. *)
Theorem concrete_is_arrival_curve :
taskset_respects_max_arrivals (concrete_arrival_sequence generate_jobs_at ts) ts.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)
taskset_respects_max_arrivals
(concrete_arrival_sequence generate_jobs_at ts) ts
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)
taskset_respects_max_arrivals
(concrete_arrival_sequence generate_jobs_at ts) ts
move => tsk IN t1 t LEQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1, t : instant LEQ : t1 <= t
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts) tsk
t1 t <= max_arrivals tsk (t - t1)
set Δ := t - t1.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1, t : instant LEQ : t1 <= t Δ := t - t1 : nat
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts) tsk
t1 t <= max_arrivals tsk Δ
replace t1 with (t-Δ); last by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1, t : instant LEQ : t1 <= t Δ := t - t1 : nat
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts) tsk
(t - Δ) t <= max_arrivals tsk Δ
have LEQd: Δ <= t by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1, t : instant LEQ : t1 <= t Δ := t - t1 : nat LEQd : Δ <= t
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts) tsk
(t - Δ) t <= max_arrivals tsk Δ
generalize Δ LEQd; clear LEQ Δ LEQd.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1, t : instant
forall Δ : nat,
Δ <= t ->
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts) tsk
(t - Δ) t <= max_arrivals tsk Δ
elim : t => [|t IHt] Δ LEQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant Δ : nat LEQ : Δ <= 0
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts) tsk
(0 - Δ) 0 <= max_arrivals tsk Δ
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant Δ : nat LEQ : Δ <= 0
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts) tsk
(0 - Δ) 0 <= max_arrivals tsk Δ
rewrite sub0n.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant Δ : nat LEQ : Δ <= 0
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts) tsk
0 0 <= max_arrivals tsk Δ
rewrite number_of_task_arrivals_eq //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant Δ : nat LEQ : Δ <= 0
\sum_(0 <= t < 0 ) max_arrivals_at tsk t <=
max_arrivals tsk Δ
by vm_compute ; rewrite unlock . } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant t : nat IHt : forall Δ : nat,
Δ <= t ->
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts)
tsk (t - Δ) t <=
max_arrivals tsk ΔΔ : nat LEQ : Δ <= t.+1
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts) tsk
(t.+1 - Δ) t.+1 <= max_arrivals tsk Δ
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant t : nat IHt : forall Δ : nat,
Δ <= t ->
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts)
tsk (t - Δ) t <=
max_arrivals tsk ΔΔ : nat LEQ : Δ <= t.+1
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts) tsk
(t.+1 - Δ) t.+1 <= max_arrivals tsk Δ
rewrite number_of_task_arrivals_eq //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant t : nat IHt : forall Δ : nat,
Δ <= t ->
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts)
tsk (t - Δ) t <=
max_arrivals tsk ΔΔ : nat LEQ : Δ <= t.+1
\sum_(t.+1 - Δ <= t < t.+1 ) max_arrivals_at tsk t <=
max_arrivals tsk Δ
destruct Δ as [|Δ]; first by rewrite /index_iota subnn; vm_compute ; rewrite unlock .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant t : nat IHt : forall Δ : nat,
Δ <= t ->
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts)
tsk (t - Δ) t <=
max_arrivals tsk ΔΔ : nat LEQ : Δ < t.+1
\sum_(t.+1 - Δ.+1 <= t < t.+1 ) max_arrivals_at tsk t <=
max_arrivals tsk Δ.+1
rewrite subSS.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant t : nat IHt : forall Δ : nat,
Δ <= t ->
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts)
tsk (t - Δ) t <=
max_arrivals tsk ΔΔ : nat LEQ : Δ < t.+1
\sum_(t - Δ <= t < t.+1 ) max_arrivals_at tsk t <=
max_arrivals tsk Δ.+1
specialize (IHt Δ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant t, Δ : nat IHt : Δ <= t ->
number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts)
tsk (t - Δ) t <=
max_arrivals tsk Δ LEQ : Δ < t.+1
\sum_(t - Δ <= t < t.+1 ) max_arrivals_at tsk t <=
max_arrivals tsk Δ.+1
feed IHt; first by lia . Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant t, Δ : nat IHt : number_of_task_arrivals
(concrete_arrival_sequence generate_jobs_at ts)
tsk (t - Δ) t <=
max_arrivals tsk Δ LEQ : Δ < t.+1
\sum_(t - Δ <= t < t.+1 ) max_arrivals_at tsk t <=
max_arrivals tsk Δ.+1
rewrite number_of_task_arrivals_eq // in IHt.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant t, Δ : nat LEQ : Δ < t.+1 IHt : \sum_(t - Δ <= t < t) max_arrivals_at tsk t <=
max_arrivals tsk Δ
\sum_(t - Δ <= t < t.+1 ) max_arrivals_at tsk t <=
max_arrivals tsk Δ.+1
rewrite big_nat_recr //=; last by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant t, Δ : nat LEQ : Δ < t.+1 IHt : \sum_(t - Δ <= t < t) max_arrivals_at tsk t <=
max_arrivals tsk Δ
\sum_(t - Δ <= i < t) max_arrivals_at tsk i +
max_arrivals_at tsk t <= max_arrivals tsk Δ.+1
rewrite -leq_subRL; first apply n_arrivals_at_leq; try lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant t, Δ : nat LEQ : Δ < t.+1 IHt : \sum_(t - Δ <= t < t) max_arrivals_at tsk t <=
max_arrivals tsk Δ
\sum_(t - Δ <= i < t) max_arrivals_at tsk i <=
max_arrivals tsk Δ.+1
move : (H_valid_arrival_curve tsk IN) => [ZERO MONO].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant t, Δ : nat LEQ : Δ < t.+1 IHt : \sum_(t - Δ <= t < t) max_arrivals_at tsk t <=
max_arrivals tsk Δ ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk)
\sum_(t - Δ <= i < t) max_arrivals_at tsk i <=
max_arrivals tsk Δ.+1
apply (leq_trans IHt).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job ts : seq Task H_ts_uniq : uniq ts H3 : MaxArrivals Task H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals generate_jobs_at : Task -> nat -> instant -> seq Job H_job_generation_valid_number : forall (tsk : Task)
(n : nat)
(t : instant),
tsk \in ts ->
size
(generate_jobs_at
tsk n t) = nH_job_generation_valid_jobs : forall (tsk : Task)
(n : nat)
(t : instant)
(j : Job),
j
\in generate_jobs_at
tsk n t ->
job_task j = tsk /\
job_arrival j = t /\
job_cost j <=
task_cost tskH_jobs_unique : forall t1 t2 : instant,
uniq
(arrivals_between
(concrete_arrival_sequence
generate_jobs_at ts) t1 t2)tsk : Task IN : tsk \in ts t1 : instant t, Δ : nat LEQ : Δ < t.+1 IHt : \sum_(t - Δ <= t < t) max_arrivals_at tsk t <=
max_arrivals tsk Δ ZERO : max_arrivals tsk 0 = 0 MONO : monotone leq (max_arrivals tsk)
max_arrivals tsk Δ <= max_arrivals tsk Δ.+1
by apply MONO. }
Qed .
End MaximalArrivalSequence .