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.behavior.all .[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.util.all .
Require Export prosa.model.task.arrivals.
(** * Arrival Sequence *)
(** First, we relate the stronger to the weaker arrival predicates. *)
Section ArrivalPredicates .
(** Consider any kinds of jobs with arrival times. *)
Context {Job : JobType} `{JobArrival Job}.
(** A job that arrives in some interval <<[t1, t2)>> certainly arrives before
time [t2]. *)
Lemma arrived_between_before :
forall j t1 t2 ,
arrived_between j t1 t2 ->
arrived_before j t2.Job : JobType H : JobArrival Job
forall (j : Job) (t1 t2 : instant),
arrived_between j t1 t2 -> arrived_before j t2
Proof .Job : JobType H : JobArrival Job
forall (j : Job) (t1 t2 : instant),
arrived_between j t1 t2 -> arrived_before j t2
by move => ? ? ? /andP[]. Qed .
(** A job that arrives before a time [t] certainly has arrived by time
[t]. *)
Lemma arrived_before_has_arrived :
forall j t ,
arrived_before j t ->
has_arrived j t.Job : JobType H : JobArrival Job
forall (j : Job) (t : instant),
arrived_before j t -> has_arrived j t
Proof .Job : JobType H : JobArrival Job
forall (j : Job) (t : instant),
arrived_before j t -> has_arrived j t
move => ? ?; exact : ltnW. Qed .
(** Furthermore, we restate a common hypothesis to make its
implication easier to discover. *)
Lemma consistent_times_valid_arrival :
forall arr_seq ,
valid_arrival_sequence arr_seq -> consistent_arrival_times arr_seq.Job : JobType H : JobArrival Job
forall arr_seq : arrival_sequence Job,
valid_arrival_sequence arr_seq ->
consistent_arrival_times arr_seq
Proof .Job : JobType H : JobArrival Job
forall arr_seq : arrival_sequence Job,
valid_arrival_sequence arr_seq ->
consistent_arrival_times arr_seq
by move => ? []. Qed .
(** We restate another common hypothesis to make its implication
easier to discover. *)
Lemma uniq_valid_arrival :
forall arr_seq ,
valid_arrival_sequence arr_seq -> arrival_sequence_uniq arr_seq.Job : JobType H : JobArrival Job
forall arr_seq : arrival_sequence Job,
valid_arrival_sequence arr_seq ->
arrival_sequence_uniq arr_seq
Proof .Job : JobType H : JobArrival Job
forall arr_seq : arrival_sequence Job,
valid_arrival_sequence arr_seq ->
arrival_sequence_uniq arr_seq
by move => ? []. Qed .
End ArrivalPredicates .
(** In this section, we relate job readiness to [has_arrived]. *)
Section Arrived .
(** Consider any kinds of jobs and any kind of processor state. *)
Context {Job : JobType} {PState : ProcessorState Job}.
(** Consider any schedule... *)
Variable sched : schedule PState.
(** ...and suppose that jobs have a cost, an arrival time, and a
notion of readiness. *)
Context `{JobCost Job}.
Context `{JobArrival Job}.
Context {jr : JobReady Job PState}.
(** First, we note that readiness models are by definition consistent
w.r.t. [pending]. *)
Lemma any_ready_job_is_pending :
forall j t ,
job_ready sched j t -> pending sched j t.Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
forall (j : Job) (t : instant),
job_ready sched j t -> pending sched j t
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
forall (j : Job) (t : instant),
job_ready sched j t -> pending sched j t
move : jr => [? +] /= ?; exact . Qed .
(** Next, we observe that a given job must have arrived to be ready... *)
Lemma ready_implies_arrived :
forall j t , job_ready sched j t -> has_arrived j t.Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
forall (j : Job) (t : instant),
job_ready sched j t -> has_arrived j t
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
forall (j : Job) (t : instant),
job_ready sched j t -> has_arrived j t
by move => ? ? /any_ready_job_is_pending => /andP[]. Qed .
(** ...and lift this observation also to the level of whole schedules. *)
Lemma jobs_must_arrive_to_be_ready :
jobs_must_be_ready_to_execute sched -> jobs_must_arrive_to_execute sched.Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
jobs_must_be_ready_to_execute sched ->
jobs_must_arrive_to_execute sched
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
jobs_must_be_ready_to_execute sched ->
jobs_must_arrive_to_execute sched
move => READY ? ? ?; exact /ready_implies_arrived/READY. Qed .
(** Furthermore, in a valid schedule, jobs must arrive to execute. *)
Corollary valid_schedule_implies_jobs_must_arrive_to_execute :
forall arr_seq ,
valid_schedule sched arr_seq -> jobs_must_arrive_to_execute sched.Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
forall arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
jobs_must_arrive_to_execute sched
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
forall arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
jobs_must_arrive_to_execute sched
move => ? [? ?]; exact : jobs_must_arrive_to_be_ready. Qed .
(** Since backlogged jobs are by definition ready, any backlogged job must have arrived. *)
Corollary backlogged_implies_arrived :
forall j t ,
backlogged sched j t -> has_arrived j t.Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
forall (j : Job) (t : instant),
backlogged sched j t -> has_arrived j t
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
forall (j : Job) (t : instant),
backlogged sched j t -> has_arrived j t
move => ? ? /andP[? ?]; exact : ready_implies_arrived. Qed .
(** Similarly, since backlogged jobs are by definition pending, any
backlogged job must be incomplete. *)
Lemma backlogged_implies_incomplete :
forall j t ,
backlogged sched j t -> ~~ completed_by sched j t.Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
forall (j : Job) (t : instant),
backlogged sched j t -> ~~ completed_by sched j t
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
forall (j : Job) (t : instant),
backlogged sched j t -> ~~ completed_by sched j t
by move => ? ? /andP[/any_ready_job_is_pending /andP[]]. Qed .
(** Finally, we restate common hypotheses on the well-formedness of
schedules to make their implications more easily
discoverable. First, on the readiness of scheduled jobs, ... *)
Lemma job_scheduled_implies_ready :
jobs_must_be_ready_to_execute sched ->
forall j t ,
scheduled_at sched j t -> job_ready sched j t.Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
jobs_must_be_ready_to_execute sched ->
forall (j : Job) (t : instant),
scheduled_at sched j t -> job_ready sched j t
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
jobs_must_be_ready_to_execute sched ->
forall (j : Job) (t : instant),
scheduled_at sched j t -> job_ready sched j t
exact . Qed .
(** ... second, on the origin of scheduled jobs, and ... *)
Lemma valid_schedule_jobs_come_from_arrival_sequence :
forall arr_seq ,
valid_schedule sched arr_seq ->
jobs_come_from_arrival_sequence sched arr_seq.Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
forall arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
jobs_come_from_arrival_sequence sched arr_seq
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
forall arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
jobs_come_from_arrival_sequence sched arr_seq
by move => ? []. Qed .
(** ... third, on the readiness of jobs in valid schedules. *)
Lemma valid_schedule_jobs_must_be_ready_to_execute :
forall arr_seq ,
valid_schedule sched arr_seq -> jobs_must_be_ready_to_execute sched.Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
forall arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
jobs_must_be_ready_to_execute sched
Proof .Job : JobType PState : ProcessorState Job sched : schedule PState H : JobCost Job H0 : JobArrival Job jr : JobReady Job PState
forall arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
jobs_must_be_ready_to_execute sched
by move => ? []. Qed .
End Arrived .
(** In this section, we establish useful facts about arrival sequence prefixes. *)
Section ArrivalSequencePrefix .
(** Consider any kind of tasks and jobs. *)
Context {Job : JobType}.
Context {Task : TaskType}.
Context `{JobArrival Job}.
Context `{JobTask Job Task}.
(** Consider any job arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** We begin with basic lemmas for manipulating the sequences. *)
Section Composition .
(** We show that the set of arriving jobs can be split
into disjoint intervals. *)
Lemma arrivals_between_cat :
forall t1 t t2 ,
t1 <= t ->
t <= t2 ->
arrivals_between arr_seq t1 t2 =
arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall t1 t t2 : nat,
t1 <= t ->
t <= t2 ->
arrivals_between arr_seq t1 t2 =
arrivals_between arr_seq t1 t ++
arrivals_between arr_seq t t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall t1 t t2 : nat,
t1 <= t ->
t <= t2 ->
arrivals_between arr_seq t1 t2 =
arrivals_between arr_seq t1 t ++
arrivals_between arr_seq t t2
by move => ? ? ? ? ?; rewrite -big_cat_nat. Qed .
(** We also prove a stronger version of the above lemma
in the case of arrivals that satisfy a predicate [P]. *)
Lemma arrivals_P_cat :
forall P t t1 t2 ,
t1 <= t < t2 ->
arrivals_between_P arr_seq P t1 t2 =
arrivals_between_P arr_seq P t1 t ++ arrivals_between_P arr_seq P t t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall (P : Job -> bool) (t t1 t2 : nat),
t1 <= t < t2 ->
arrivals_between_P arr_seq P t1 t2 =
arrivals_between_P arr_seq P t1 t ++
arrivals_between_P arr_seq P t t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall (P : Job -> bool) (t t1 t2 : nat),
t1 <= t < t2 ->
arrivals_between_P arr_seq P t1 t2 =
arrivals_between_P arr_seq P t1 t ++
arrivals_between_P arr_seq P t t2
move => P t t1 t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job P : Job -> bool t, t1, t2 : nat
t1 <= t < t2 ->
arrivals_between_P arr_seq P t1 t2 =
arrivals_between_P arr_seq P t1 t ++
arrivals_between_P arr_seq P t t2
by move => /andP[? ?]; rewrite -filter_cat -arrivals_between_cat// ltnW.
Qed .
(** The same observation applies to membership in the set of
arrived jobs. *)
Lemma arrivals_between_mem_cat :
forall j t1 t t2 ,
t1 <= t ->
t <= t2 ->
j \in arrivals_between arr_seq t1 t2 =
(j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall (j : Job) (t1 t t2 : nat),
t1 <= t ->
t <= t2 ->
(j \in arrivals_between arr_seq t1 t2) =
(j
\in arrivals_between arr_seq t1 t ++
arrivals_between arr_seq t t2)
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall (j : Job) (t1 t t2 : nat),
t1 <= t ->
t <= t2 ->
(j \in arrivals_between arr_seq t1 t2) =
(j
\in arrivals_between arr_seq t1 t ++
arrivals_between arr_seq t t2)
by move => ? ? ? ? ? ?; rewrite -arrivals_between_cat. Qed .
(** We observe that we can grow the considered interval without
"losing" any arrived jobs, i.e., membership in the set of arrived jobs
is monotonic. *)
Lemma arrivals_between_sub :
forall j t1 t1' t2 t2' ,
t1' <= t1 ->
t2 <= t2' ->
j \in arrivals_between arr_seq t1 t2 ->
j \in arrivals_between arr_seq t1' t2'.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall (j : Job) (t1 t1' t2 t2' : nat),
t1' <= t1 ->
t2 <= t2' ->
j \in arrivals_between arr_seq t1 t2 ->
j \in arrivals_between arr_seq t1' t2'
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall (j : Job) (t1 t1' t2 t2' : nat),
t1' <= t1 ->
t2 <= t2' ->
j \in arrivals_between arr_seq t1 t2 ->
j \in arrivals_between arr_seq t1' t2'
move => j t1 t1' t2 t2' t1'_le_t1 t2_le_t2' j_in.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job j : Job t1, t1', t2, t2' : nat t1'_le_t1 : t1' <= t1 t2_le_t2' : t2 <= t2' j_in : j \in arrivals_between arr_seq t1 t2
j \in arrivals_between arr_seq t1' t2'
have /orP[t2_le_t1|t1_le_t2] := leq_total t2 t1.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job j : Job t1, t1', t2, t2' : nat t1'_le_t1 : t1' <= t1 t2_le_t2' : t2 <= t2' j_in : j \in arrivals_between arr_seq t1 t2 t2_le_t1 : t2 <= t1
j \in arrivals_between arr_seq t1' t2'
{ Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job j : Job t1, t1', t2, t2' : nat t1'_le_t1 : t1' <= t1 t2_le_t2' : t2 <= t2' j_in : j \in arrivals_between arr_seq t1 t2 t2_le_t1 : t2 <= t1
j \in arrivals_between arr_seq t1' t2'
by move : j_in; rewrite /arrivals_between big_geq. } Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job j : Job t1, t1', t2, t2' : nat t1'_le_t1 : t1' <= t1 t2_le_t2' : t2 <= t2' j_in : j \in arrivals_between arr_seq t1 t2 t1_le_t2 : t1 <= t2
j \in arrivals_between arr_seq t1' t2'
rewrite (arrivals_between_mem_cat _ _ t1)// ?mem_cat .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job j : Job t1, t1', t2, t2' : nat t1'_le_t1 : t1' <= t1 t2_le_t2' : t2 <= t2' j_in : j \in arrivals_between arr_seq t1 t2 t1_le_t2 : t1 <= t2
(j \in arrivals_between arr_seq t1' t1)
|| (j \in arrivals_between arr_seq t1 t2')
2 :{Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job j : Job t1, t1', t2, t2' : nat t1'_le_t1 : t1' <= t1 t2_le_t2' : t2 <= t2' j_in : j \in arrivals_between arr_seq t1 t2 t1_le_t2 : t1 <= t2
t1 <= t2'
exact : leq_trans t2_le_t2'. } Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job j : Job t1, t1', t2, t2' : nat t1'_le_t1 : t1' <= t1 t2_le_t2' : t2 <= t2' j_in : j \in arrivals_between arr_seq t1 t2 t1_le_t2 : t1 <= t2
(j \in arrivals_between arr_seq t1' t1)
|| (j \in arrivals_between arr_seq t1 t2')
rewrite [X in _ || X](arrivals_between_mem_cat _ _ t2)// mem_cat.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job j : Job t1, t1', t2, t2' : nat t1'_le_t1 : t1' <= t1 t2_le_t2' : t2 <= t2' j_in : j \in arrivals_between arr_seq t1 t2 t1_le_t2 : t1 <= t2
[|| j \in arrivals_between arr_seq t1' t1,
j \in arrivals_between arr_seq t1 t2
| j \in arrivals_between arr_seq t2 t2']
by rewrite j_in orbT.
Qed .
End Composition .
(** Next, we relate the arrival prefixes with job arrival times. *)
Section ArrivalTimes .
(** Assume that job arrival times are consistent. *)
Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
(** To make the hypothesis and its implication easier to discover,
we restate it as a trivial lemma. *)
Lemma job_arrival_arrives_at :
forall {j t },
arrives_at arr_seq j t -> job_arrival j = t.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t : instant),
arrives_at arr_seq j t -> job_arrival j = t
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t : instant),
arrives_at arr_seq j t -> job_arrival j = t
exact : H_consistent_arrival_times. Qed .
(** Similarly, to simplify subsequent proofs, we restate the
[H_consistent_arrival_times] assumption as a trivial
corollary. *)
Lemma job_arrival_at :
forall {j t },
j \in arrivals_at arr_seq t -> job_arrival j = t.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t : instant),
j \in arrivals_at arr_seq t -> job_arrival j = t
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t : instant),
j \in arrivals_at arr_seq t -> job_arrival j = t
exact : H_consistent_arrival_times. Qed .
(** Next, we prove that if [j] is a part of the arrival sequence,
then the converse of the above also holds. *)
Lemma job_in_arrivals_at :
forall j t ,
arrives_in arr_seq j ->
job_arrival j = t ->
j \in arrivals_at arr_seq t.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t : instant),
arrives_in arr_seq j ->
job_arrival j = t -> j \in arrivals_at arr_seq t
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t : instant),
arrives_in arr_seq j ->
job_arrival j = t -> j \in arrivals_at arr_seq t
move => j t [t' IN] => /eqP.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t, t' : instant IN : j \in arrivals_at arr_seq t'
job_arrival j == t -> j \in arrivals_at arr_seq t
apply contraTT => /negP NOTIN.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t, t' : instant IN : j \in arrivals_at arr_seq t' NOTIN : ~ j \in arrivals_at arr_seq t
job_arrival j != t
apply /neqP => ARR.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t, t' : instant IN : j \in arrivals_at arr_seq t' NOTIN : ~ j \in arrivals_at arr_seq t ARR : job_arrival j = t
False
have ARR' := (H_consistent_arrival_times _ t' IN).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t, t' : instant IN : j \in arrivals_at arr_seq t' NOTIN : ~ j \in arrivals_at arr_seq t ARR : job_arrival j = t ARR' : job_arrival j = t'
False
by move : IN; rewrite -ARR' ARR.
Qed .
(** To begin with actual properties, we observe that any job in
the set of all arrivals between time instants [t1] and [t2]
must arrive in the interval <<[t1,t2)>>. *)
Lemma job_arrival_between :
forall {j t1 t2 },
j \in arrivals_between arr_seq t1 t2 -> t1 <= job_arrival j < t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
t1 <= job_arrival j < t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
t1 <= job_arrival j < t2
by move => ? ? ? /mem_bigcat_nat_exists[i [/job_arrival_at <-]]. Qed .
(** For convenience, we restate the left bound of the above lemma... *)
Corollary job_arrival_between_ge :
forall {j t1 t2 },
j \in arrivals_between arr_seq t1 t2 -> t1 <= job_arrival j.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
t1 <= job_arrival j
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
t1 <= job_arrival j
by move => ? ? ? /job_arrival_between/andP[]. Qed .
(** ... as well as the right bound separately as corollaries. *)
Corollary job_arrival_between_lt :
forall {j t1 t2 },
j \in arrivals_between arr_seq t1 t2 -> job_arrival j < t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
job_arrival j < t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
job_arrival j < t2
by move => ? ? ? /job_arrival_between/andP[]. Qed .
(** Consequently, if we filter the list of arrivals in an interval
<<[t1,t2)>> with an arrival-time threshold less than [t1], we are
left with an empty list. *)
Lemma arrivals_between_filter_nil :
forall t1 t2 t ,
t < t1 ->
[seq j <- arrivals_between arr_seq t1 t2 | job_arrival j < t] = [::].Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (t1 : nat) (t2 : instant) (t : nat),
t < t1 ->
[seq j <- arrivals_between arr_seq t1 t2
| job_arrival j < t] = [::]
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (t1 : nat) (t2 : instant) (t : nat),
t < t1 ->
[seq j <- arrivals_between arr_seq t1 t2
| job_arrival j < t] = [::]
move => t1 t2 t LT.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : nat t2 : instant t : nat LT : t < t1
[seq j <- arrivals_between arr_seq t1 t2
| job_arrival j < t] = [::]
case : (leqP t1 t2) => RANGE;
last by rewrite /arrivals_between big_geq //=; lia .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : nat t2 : instant t : nat LT : t < t1 RANGE : t1 <= t2
[seq j <- arrivals_between arr_seq t1 t2
| job_arrival j < t] = [::]
rewrite filter_in_pred0 // => j IN.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : nat t2 : instant t : nat LT : t < t1 RANGE : t1 <= t2 j : Job IN : j \in arrivals_between arr_seq t1 t2
~~ (job_arrival j < t)
rewrite -ltnNge.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : nat t2 : instant t : nat LT : t < t1 RANGE : t1 <= t2 j : Job IN : j \in arrivals_between arr_seq t1 t2
t < (job_arrival j).+1
apply : (ltn_trans LT).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : nat t2 : instant t : nat LT : t < t1 RANGE : t1 <= t2 j : Job IN : j \in arrivals_between arr_seq t1 t2
t1 < (job_arrival j).+1
rewrite ltnS.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : nat t2 : instant t : nat LT : t < t1 RANGE : t1 <= t2 j : Job IN : j \in arrivals_between arr_seq t1 t2
t1 <= job_arrival j
by apply : job_arrival_between_ge; eauto .
Qed .
(** Furthermore, if we filter the list of arrivals in an interval
<<[t1,t2)>> with an arrival-time threshold less than [t2],
we can simply discard the tail past the threshold. *)
Lemma arrivals_between_filter :
forall t1 t2 t ,
t <= t2 ->
arrivals_between arr_seq t1 t
= [seq j <- arrivals_between arr_seq t1 t2 | job_arrival j < t].Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (t1 : instant) (t2 t : nat),
t <= t2 ->
arrivals_between arr_seq t1 t =
[seq j <- arrivals_between arr_seq t1 t2
| job_arrival j < t]
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (t1 : instant) (t2 t : nat),
t <= t2 ->
arrivals_between arr_seq t1 t =
[seq j <- arrivals_between arr_seq t1 t2
| job_arrival j < t]
move => t1 t2 t LE2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2
arrivals_between arr_seq t1 t =
[seq j <- arrivals_between arr_seq t1 t2
| job_arrival j < t]
case : (leqP t1 t2) => RANGE;
last by rewrite /arrivals_between !big_geq //=; lia .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2
arrivals_between arr_seq t1 t =
[seq j <- arrivals_between arr_seq t1 t2
| job_arrival j < t]
case : (leqP t1 t) => LE1;
last by rewrite [LHS]/arrivals_between big_geq; try lia ; rewrite arrivals_between_filter_nil.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t
arrivals_between arr_seq t1 t =
[seq j <- arrivals_between arr_seq t1 t2
| job_arrival j < t]
rewrite /arrivals_between bigcat_nat_filter_eq_filter_bigcat_nat.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t
\cat_(t1<=t<t)arrivals_at arr_seq t =
\cat_(t1<=t0<t2)
[seq x <- arrivals_at arr_seq t0 | job_arrival x < t]
rewrite (big_cat_nat _ _ _ LE1 LE2) //=.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t
\cat_(t1<=t<t)arrivals_at arr_seq t =
\cat_(t1<=i<t)
[seq x <- arrivals_at arr_seq i | job_arrival x < t] ++
\cat_(t<=i<t2)
[seq x <- arrivals_at arr_seq i | job_arrival x < t]
rewrite !big_nat [X in _ ++ X]big1; last first .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t
forall i : nat,
t <= i < t2 ->
[seq x <- arrivals_at arr_seq i | job_arrival x < t] =
[::]
{ Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t
forall i : nat,
t <= i < t2 ->
[seq x <- arrivals_at arr_seq i | job_arrival x < t] =
[::]
move => t' /andP[LO HI].Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t t' : nat LO : t <= t' HI : t' < t2
[seq x <- arrivals_at arr_seq t' | job_arrival x < t] =
[::]
rewrite filter_in_pred0 // => j IN.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t t' : nat LO : t <= t' HI : t' < t2 j : Job IN : j \in arrivals_at arr_seq t'
~~ (job_arrival j < t)
have -> : job_arrival j = t' by apply : job_arrival_at; eauto .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t t' : nat LO : t <= t' HI : t' < t2 j : Job IN : j \in arrivals_at arr_seq t'
~~ (t' < t)
rewrite -leqNgt.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t t' : nat LO : t <= t' HI : t' < t2 j : Job IN : j \in arrivals_at arr_seq t'
t <= t'
exact : LO. } Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t
\cat_(t1<=i<t|(t1 <= i < t))arrivals_at arr_seq i =
\cat_(t1<=i<t|(t1 <= i < t))
[seq x <- arrivals_at arr_seq i | job_arrival x < t] ++
[::]
{ Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t
\cat_(t1<=i<t|(t1 <= i < t))arrivals_at arr_seq i =
\cat_(t1<=i<t|(t1 <= i < t))
[seq x <- arrivals_at arr_seq i | job_arrival x < t] ++
[::]
rewrite cats0.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t
\cat_(t1<=i<t|(t1 <= i < t))arrivals_at arr_seq i =
\cat_(t1<=i<t|(t1 <= i < t))
[seq x <- arrivals_at arr_seq i | job_arrival x < t]
apply : eq_bigr => t' /andP[LO HI].Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t t' : nat LO : t1 <= t' HI : t' < t
arrivals_at arr_seq t' =
[seq x <- arrivals_at arr_seq t' | job_arrival x < t]
apply esym.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t t' : nat LO : t1 <= t' HI : t' < t
[seq x <- arrivals_at arr_seq t' | job_arrival x < t] =
arrivals_at arr_seq t'
apply /all_filterP/allP => j IN.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t t' : nat LO : t1 <= t' HI : t' < t j : Job IN : j \in arrivals_at arr_seq t'
job_arrival j < t
have -> : job_arrival j = t' by apply : job_arrival_at; eauto .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2, t : nat LE2 : t <= t2 RANGE : t1 <= t2 LE1 : t1 <= t t' : nat LO : t1 <= t' HI : t' < t j : Job IN : j \in arrivals_at arr_seq t'
t' < t
exact : HI. }
Qed .
(** Next, we prove that if a job belongs to the prefix
(jobs_arrived_before t), then it arrives in the arrival
sequence. *)
Lemma in_arrivals_implies_arrived :
forall j t1 t2 ,
j \in arrivals_between arr_seq t1 t2 ->
arrives_in arr_seq j.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
arrives_in arr_seq j
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
arrives_in arr_seq j
by move => ? ? ? /mem_bigcat_nat_exists[arr [? _]]; exists arr . Qed .
(** We also prove a weaker version of the above lemma. *)
Lemma in_arrseq_implies_arrives :
forall t j ,
j \in arr_seq t ->
arrives_in arr_seq j.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (t : instant) (j : Job),
j \in arr_seq t -> arrives_in arr_seq j
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (t : instant) (j : Job),
j \in arr_seq t -> arrives_in arr_seq j
by move => t ? ?; exists t . Qed .
(** Next, we prove that if a job belongs to the prefix
(jobs_arrived_between t1 t2), then it indeed arrives between t1 and
t2. *)
Lemma in_arrivals_implies_arrived_between :
forall j t1 t2 ,
j \in arrivals_between arr_seq t1 t2 ->
arrived_between j t1 t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
arrived_between j t1 t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
arrived_between j t1 t2
by move => ? ? ? /mem_bigcat_nat_exists[t0 [/job_arrival_at <-]]. Qed .
(** Similarly, if a job belongs to the prefix (jobs_arrived_before t),
then it indeed arrives before time t. *)
Lemma in_arrivals_implies_arrived_before :
forall j t ,
j \in arrivals_before arr_seq t ->
arrived_before j t.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t : instant),
j \in arrivals_before arr_seq t -> arrived_before j t
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t : instant),
j \in arrivals_before arr_seq t -> arrived_before j t
by move => ? ? /in_arrivals_implies_arrived_between. Qed .
(** Similarly, we prove that if a job from the arrival sequence arrives
before t, then it belongs to the sequence (jobs_arrived_before t). *)
Lemma arrived_between_implies_in_arrivals :
forall j t1 t2 ,
arrives_in arr_seq j ->
arrived_between j t1 t2 ->
j \in arrivals_between arr_seq t1 t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
arrives_in arr_seq j ->
arrived_between j t1 t2 ->
j \in arrivals_between arr_seq t1 t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
arrives_in arr_seq j ->
arrived_between j t1 t2 ->
j \in arrivals_between arr_seq t1 t2
move => j t1 t2 [a_j arrj] before ; apply : mem_bigcat_nat (arrj).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t1, t2, a_j : instant arrj : j \in arrivals_at arr_seq a_j before : arrived_between j t1 t2
t1 <= a_j < t2
by rewrite -(job_arrival_at arrj).
Qed .
(** Any job in arrivals between time instants [t1] and [t2] must arrive
in the interval <<[t1,t2)>>. *)
Lemma job_arrival_between_P :
forall j P t1 t2 ,
j \in arrivals_between_P arr_seq P t1 t2 ->
t1 <= job_arrival j < t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (P : Job -> bool) (t1 t2 : instant),
j \in arrivals_between_P arr_seq P t1 t2 ->
t1 <= job_arrival j < t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (P : Job -> bool) (t1 t2 : instant),
j \in arrivals_between_P arr_seq P t1 t2 ->
t1 <= job_arrival j < t2
move => j P t1 t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job P : Job -> bool t1, t2 : instant
j \in arrivals_between_P arr_seq P t1 t2 ->
t1 <= job_arrival j < t2
rewrite mem_filter => /andP[Pj /mem_bigcat_nat_exists[i [+ iitv]]].Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job P : Job -> bool t1, t2 : instant Pj : P j i : nat iitv : t1 <= i < t2
j \in arrivals_at arr_seq i ->
t1 <= job_arrival j < t2
by move => /job_arrival_at ->.
Qed .
(** Any job [j] is in the sequence [arrivals_between t1 t2] given
that [j] arrives in the interval <<[t1,t2)>>. *)
Lemma job_in_arrivals_between :
forall j t1 t2 ,
arrives_in arr_seq j ->
t1 <= job_arrival j ->
job_arrival j < t2 ->
j \in arrivals_between arr_seq t1 t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : nat),
arrives_in arr_seq j ->
t1 <= job_arrival j ->
job_arrival j < t2 ->
j \in arrivals_between arr_seq t1 t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : nat),
arrives_in arr_seq j ->
t1 <= job_arrival j ->
job_arrival j < t2 ->
j \in arrivals_between arr_seq t1 t2
move => j t1 t2 ARRSEQ ARR1 ARR2; apply : mem_bigcat_nat.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t1, t2 : nat ARRSEQ : arrives_in arr_seq j ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
t1 <= ?Goal < t2
- Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t1, t2 : nat ARRSEQ : arrives_in arr_seq j ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
t1 <= ?Goal < t2
by apply /andP; split ; [exact ARR1| exact ARR2].
- Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t1, t2 : nat ARRSEQ : arrives_in arr_seq j ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
j \in arrivals_at arr_seq (job_arrival j)
by apply job_in_arrivals_at => //=.
Qed .
(** Next, we prove that if the arrival sequence doesn't contain duplicate
jobs, the same applies for any of its prefixes. *)
Lemma arrivals_uniq :
arrival_sequence_uniq arr_seq ->
forall t1 t2 , uniq (arrivals_between arr_seq t1 t2).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
arrival_sequence_uniq arr_seq ->
forall t1 t2 : instant,
uniq (arrivals_between arr_seq t1 t2)
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
arrival_sequence_uniq arr_seq ->
forall t1 t2 : instant,
uniq (arrivals_between arr_seq t1 t2)
move => SET t1 t2; apply : bigcat_nat_uniq => // j t1' t2'.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq SET : arrival_sequence_uniq arr_seq t1, t2 : instant j : Job t1', t2' : nat
j \in arrivals_at arr_seq t1' ->
j \in arrivals_at arr_seq t2' -> t1' = t2'
by move => /job_arrival_at <- /job_arrival_at <-.
Qed .
(** Also note that there can't by any arrivals in an empty time interval. *)
Lemma arrivals_between_geq :
forall t1 t2 ,
t1 >= t2 ->
arrivals_between arr_seq t1 t2 = [::].Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall t1 t2 : nat,
t2 <= t1 -> arrivals_between arr_seq t1 t2 = [::]
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall t1 t2 : nat,
t2 <= t1 -> arrivals_between arr_seq t1 t2 = [::]
by move => ? ? ?; rewrite /arrivals_between big_geq. Qed .
(** Conversely, if a job arrives, the considered interval is non-empty. *)
Corollary arrivals_between_nonempty :
forall t1 t2 j ,
j \in arrivals_between arr_seq t1 t2 -> t1 < t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (t1 t2 : instant) (j : Job),
j \in arrivals_between arr_seq t1 t2 -> t1 < t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (t1 t2 : instant) (j : Job),
j \in arrivals_between arr_seq t1 t2 -> t1 < t2
by move => j1 j2 t; apply : contraPltn=> LEQ; rewrite arrivals_between_geq. Qed .
(** Given jobs [j1] and [j2] in [arrivals_between_P arr_seq P t1 t2], the fact that
[j2] arrives strictly before [j1] implies that [j2] also belongs in the sequence
[arrivals_between_P arr_seq P t1 (job_arrival j1)]. *)
Lemma arrival_lt_implies_job_in_arrivals_between_P :
forall (j1 j2 : Job) (P : Job -> bool) (t1 t2 : instant),
j1 \in arrivals_between_P arr_seq P t1 t2 ->
j2 \in arrivals_between_P arr_seq P t1 t2 ->
job_arrival j2 < job_arrival j1 ->
j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j1 j2 : Job) (P : Job -> bool)
(t1 t2 : instant),
j1 \in arrivals_between_P arr_seq P t1 t2 ->
j2 \in arrivals_between_P arr_seq P t1 t2 ->
job_arrival j2 < job_arrival j1 ->
j2
\in arrivals_between_P arr_seq P t1 (job_arrival j1)
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j1 j2 : Job) (P : Job -> bool)
(t1 t2 : instant),
j1 \in arrivals_between_P arr_seq P t1 t2 ->
j2 \in arrivals_between_P arr_seq P t1 t2 ->
job_arrival j2 < job_arrival j1 ->
j2
\in arrivals_between_P arr_seq P t1 (job_arrival j1)
move => j1 j2 P t1 t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j1, j2 : Job P : Job -> bool t1, t2 : instant
j1 \in arrivals_between_P arr_seq P t1 t2 ->
j2 \in arrivals_between_P arr_seq P t1 t2 ->
job_arrival j2 < job_arrival j1 ->
j2
\in arrivals_between_P arr_seq P t1 (job_arrival j1)
rewrite !mem_filter => /andP[_ j1arr] /andP[Pj2 j2arr] arr_lt.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j1, j2 : Job P : Job -> bool t1, t2 : instant j1arr : j1 \in arrivals_between arr_seq t1 t2 Pj2 : P j2 j2arr : j2 \in arrivals_between arr_seq t1 t2 arr_lt : job_arrival j2 < job_arrival j1
P j2 &&
(j2 \in arrivals_between arr_seq t1 (job_arrival j1))
rewrite Pj2/=; apply : job_in_arrivals_between => //=.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j1, j2 : Job P : Job -> bool t1, t2 : instant j1arr : j1 \in arrivals_between arr_seq t1 t2 Pj2 : P j2 j2arr : j2 \in arrivals_between arr_seq t1 t2 arr_lt : job_arrival j2 < job_arrival j1
arrives_in arr_seq j2
- Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j1, j2 : Job P : Job -> bool t1, t2 : instant j1arr : j1 \in arrivals_between arr_seq t1 t2 Pj2 : P j2 j2arr : j2 \in arrivals_between arr_seq t1 t2 arr_lt : job_arrival j2 < job_arrival j1
arrives_in arr_seq j2
exact : in_arrivals_implies_arrived j2arr.
- Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j1, j2 : Job P : Job -> bool t1, t2 : instant j1arr : j1 \in arrivals_between arr_seq t1 t2 Pj2 : P j2 j2arr : j2 \in arrivals_between arr_seq t1 t2 arr_lt : job_arrival j2 < job_arrival j1
t1 <= job_arrival j2
by rewrite (job_arrival_between_ge j2arr).
Qed .
(** For ease of rewriting, we establish the equivalence between a job's membership in
[arrivals_between] and its membership in [arrives_in], subject to constraints on
the job's arrival time. *)
Lemma job_arrival_in_bounds :
forall (j : Job) (t1 t2 : instant),
(j \in arrivals_between arr_seq t1 t2)
<-> (arrives_in arr_seq j /\ t1 <= job_arrival j < t2).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 <->
arrives_in arr_seq j /\ t1 <= job_arrival j < t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 <->
arrives_in arr_seq j /\ t1 <= job_arrival j < t2
move => j t1 t2; split .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t1, t2 : instant
j \in arrivals_between arr_seq t1 t2 ->
arrives_in arr_seq j /\ t1 <= job_arrival j < t2
- Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t1, t2 : instant
j \in arrivals_between arr_seq t1 t2 ->
arrives_in arr_seq j /\ t1 <= job_arrival j < t2
move => IN; split .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t1, t2 : instant IN : j \in arrivals_between arr_seq t1 t2
arrives_in arr_seq j
+ Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t1, t2 : instant IN : j \in arrivals_between arr_seq t1 t2
arrives_in arr_seq j
by eapply in_arrivals_implies_arrived => //=.
+ Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t1, t2 : instant IN : j \in arrivals_between arr_seq t1 t2
t1 <= job_arrival j < t2
by apply in_arrivals_implies_arrived_between in IN => //=.
- Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t1, t2 : instant
arrives_in arr_seq j /\ t1 <= job_arrival j < t2 ->
j \in arrivals_between arr_seq t1 t2
move => [IN ARR].Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t1, t2 : instant IN : arrives_in arr_seq j ARR : t1 <= job_arrival j < t2
j \in arrivals_between arr_seq t1 t2
by apply arrived_between_implies_in_arrivals => //=.
Qed .
(** We observe that, by construction, the sequence of arrivals is
sorted by arrival times. To this end, we first define the
order relation. *)
Definition by_arrival_times (j1 j2 : Job) : bool := job_arrival j1 <= job_arrival j2.
(** Trivially, the arrivals at any one point in time are ordered
w.r.t. arrival times. *)
Lemma arrivals_at_sorted :
forall t ,
sorted by_arrival_times (arrivals_at arr_seq t).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall t : instant,
sorted by_arrival_times (arrivals_at arr_seq t)
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall t : instant,
sorted by_arrival_times (arrivals_at arr_seq t)
move => t.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t : instant
sorted by_arrival_times (arrivals_at arr_seq t)
have AT_t : forall j , j \in (arrivals_at arr_seq t) -> job_arrival j = t
by move => j; apply job_arrival_at.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t : instant AT_t : forall j : Job,
j \in arrivals_at arr_seq t ->
job_arrival j = t
sorted by_arrival_times (arrivals_at arr_seq t)
case : (arrivals_at arr_seq t) AT_t => // j' js AT_t.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t : instant j' : Job js : seq Job AT_t : forall j : Job,
j \in j' :: js -> job_arrival j = t
sorted by_arrival_times (j' :: js)
apply /(pathP j') => i LT.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t : instant j' : Job js : seq Job AT_t : forall j : Job,
j \in j' :: js -> job_arrival j = ti : nat LT : i < size js
by_arrival_times (nth j' (j' :: js) i) (nth j' js i)
rewrite /by_arrival_times !AT_t //;
last by apply mem_nth; auto .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t : instant j' : Job js : seq Job AT_t : forall j : Job,
j \in j' :: js -> job_arrival j = ti : nat LT : i < size js
nth j' js i \in j' :: js
rewrite in_cons; apply /orP; right .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t : instant j' : Job js : seq Job AT_t : forall j : Job,
j \in j' :: js -> job_arrival j = ti : nat LT : i < size js
nth j' js i \in js
by exact : mem_nth.
Qed .
(** By design, the list of arrivals in any interval is sorted. *)
Lemma arrivals_between_sorted :
forall t1 t2 ,
sorted by_arrival_times (arrivals_between arr_seq t1 t2).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall t1 t2 : instant,
sorted by_arrival_times
(arrivals_between arr_seq t1 t2)
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall t1 t2 : instant,
sorted by_arrival_times
(arrivals_between arr_seq t1 t2)
move => t1 t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1, t2 : instant
sorted by_arrival_times
(arrivals_between arr_seq t1 t2)
rewrite /arrivals_between.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1, t2 : instant
sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t)
elim : t2 => [|t2 SORTED];
first by rewrite big_nil.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t)
sorted by_arrival_times
(\cat_(t1<=t<t2.+1 )arrivals_at arr_seq t)
case : (leqP t1 t2) => T1T2;
last by rewrite big_geq.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2
sorted by_arrival_times
(\cat_(t1<=t<t2.+1 )arrivals_at arr_seq t)
rewrite (big_cat_nat _ _ _ T1T2 _) //=.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2
sorted by_arrival_times
(\cat_(t1<=i<t2)arrivals_at arr_seq i ++
\cat_(t2<=i<t2.+1 )arrivals_at arr_seq i)
case A1: (\cat_(t1<=t<t2)arrivals_at arr_seq t) => [|j js];
first by rewrite cat0s big_nat1; exact : arrivals_at_sorted.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
sorted by_arrival_times
((j :: js) ++
\cat_(t2<=i<t2.+1 )arrivals_at arr_seq i)
have CAT : path by_arrival_times j (\cat_(t1<=t<t2)arrivals_at arr_seq t ++ \cat_(t2<=i<t2.+1 )arrivals_at arr_seq i).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times j
(\cat_(t1<=t<t2)arrivals_at arr_seq t ++
\cat_(t2<=i<t2.+1 )arrivals_at arr_seq i)
{ Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times j
(\cat_(t1<=t<t2)arrivals_at arr_seq t ++
\cat_(t2<=i<t2.+1 )arrivals_at arr_seq i)
rewrite cat_path; apply /andP; split .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times j
(\cat_(t1<=t<t2)arrivals_at arr_seq t)
{ Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times j
(\cat_(t1<=t<t2)arrivals_at arr_seq t)
move : SORTED.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) ->
path by_arrival_times j
(\cat_(t1<=t<t2)arrivals_at arr_seq t)
rewrite /sorted A1 => PATH_js.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js PATH_js : path by_arrival_times j js
path by_arrival_times j (j :: js)
by rewrite /path -/(path _ _ js) /by_arrival_times; apply /andP; split . } Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times
(last j (\cat_(t1<=t<t2)arrivals_at arr_seq t))
(\cat_(t2<=i<t2.+1 )arrivals_at arr_seq i)
{ Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times
(last j (\cat_(t1<=t<t2)arrivals_at arr_seq t))
(\cat_(t2<=i<t2.+1 )arrivals_at arr_seq i)
rewrite big_nat1.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times
(last j (\cat_(t1<=t<t2)arrivals_at arr_seq t))
(arrivals_at arr_seq t2)
case A2: (arrivals_at arr_seq t2) => // [j' js'].Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js j' : Job js' : seq Job A2 : arrivals_at arr_seq t2 = j' :: js'
path by_arrival_times
(last j (\cat_(t1<=t<t2)arrivals_at arr_seq t))
(j' :: js')
apply path_le with (x' := j').Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js j' : Job js' : seq Job A2 : arrivals_at arr_seq t2 = j' :: js'
transitive (T:=Job) by_arrival_times
{ Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js j' : Job js' : seq Job A2 : arrivals_at arr_seq t2 = j' :: js'
transitive (T:=Job) by_arrival_times
by rewrite /transitive/by_arrival_times; lia . } Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js j' : Job js' : seq Job A2 : arrivals_at arr_seq t2 = j' :: js'
by_arrival_times
(last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) j'
{ Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js j' : Job js' : seq Job A2 : arrivals_at arr_seq t2 = j' :: js'
by_arrival_times
(last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) j'
rewrite /by_arrival_times.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js j' : Job js' : seq Job A2 : arrivals_at arr_seq t2 = j' :: js'
job_arrival
(last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) <=
job_arrival j'
have -> : job_arrival j' = t2
by apply job_arrival_at; rewrite A2; apply mem_head.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js j' : Job js' : seq Job A2 : arrivals_at arr_seq t2 = j' :: js'
job_arrival
(last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) <=
t2
set L := (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js j' : Job js' : seq Job A2 : arrivals_at arr_seq t2 = j' :: js' L := last j (\cat_(t1<=t<t2)arrivals_at arr_seq t): Job
job_arrival L <= t2
have EX : exists t' , L \in arrivals_at arr_seq t' /\ t1 <= t' < t2
by apply mem_bigcat_nat_exists; rewrite /L A1 last_cons; exact : mem_last.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js j' : Job js' : seq Job A2 : arrivals_at arr_seq t2 = j' :: js' L := last j (\cat_(t1<=t<t2)arrivals_at arr_seq t): Job EX : exists t' : instant,
L \in arrivals_at arr_seq t' /\ t1 <= t' < t2
job_arrival L <= t2
move : EX => [t' [IN /andP [t1t' t't2]]].Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js j' : Job js' : seq Job A2 : arrivals_at arr_seq t2 = j' :: js' L := last j (\cat_(t1<=t<t2)arrivals_at arr_seq t): Job t' : instant IN : L \in arrivals_at arr_seq t' t1t' : t1 <= t' t't2 : t' < t2
job_arrival L <= t2
have -> : job_arrival L = t' by apply job_arrival_at.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js j' : Job js' : seq Job A2 : arrivals_at arr_seq t2 = j' :: js' L := last j (\cat_(t1<=t<t2)arrivals_at arr_seq t): Job t' : instant IN : L \in arrivals_at arr_seq t' t1t' : t1 <= t' t't2 : t' < t2
t' <= t2
by lia . } Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js j' : Job js' : seq Job A2 : arrivals_at arr_seq t2 = j' :: js'
path by_arrival_times j' (j' :: js')
{ Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js j' : Job js' : seq Job A2 : arrivals_at arr_seq t2 = j' :: js'
path by_arrival_times j' (j' :: js')
move : (arrivals_at_sorted t2); rewrite /sorted A2 => PATH'.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js j' : Job js' : seq Job A2 : arrivals_at arr_seq t2 = j' :: js' PATH' : path by_arrival_times j' js'
path by_arrival_times j' (j' :: js')
rewrite /path -/(path _ _ js') {1 }/by_arrival_times.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js j' : Job js' : seq Job A2 : arrivals_at arr_seq t2 = j' :: js' PATH' : path by_arrival_times j' js'
(job_arrival j' <= job_arrival j') &&
path by_arrival_times j' js'
by apply /andP; split => //. } } } Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t1 : instant t2 : nat SORTED : sorted by_arrival_times
(\cat_(t1<=t<t2)arrivals_at arr_seq t) T1T2 : t1 <= t2 j : Job js : seq Job A1 : \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js CAT : path by_arrival_times j
(\cat_(t1<=t<t2)arrivals_at arr_seq t ++
\cat_(t2<=i<t2.+1 )arrivals_at arr_seq i)
sorted by_arrival_times
((j :: js) ++
\cat_(t2<=i<t2.+1 )arrivals_at arr_seq i)
by move : CAT; rewrite /sorted A1 cat_cons {1 }/path -/(path _ _ (js ++ _)) => /andP [_ CAT].
Qed .
End ArrivalTimes .
(** In the following section, we establish a lemma that allows splitting the arrival sequence by task. *)
Section ArrivalPartition .
(** If all jobs stem from tasks in a given task set [ts]... *)
Variable ts : seq Task.
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** ... then we can partition the arrival sequence by task. *)
Lemma arrivals_between_partitioned_by_task :
forall t1 t2 j ,
(j \in arrivals_between arr_seq t1 t2)
= (j \in \cat_(tsk <- ts) task_arrivals_between arr_seq tsk t1 t2).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts
forall (t1 t2 : instant) (j : Job),
(j \in arrivals_between arr_seq t1 t2) =
(j
\in \cat_(tsk<-ts)
task_arrivals_between arr_seq tsk t1 t2)
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts
forall (t1 t2 : instant) (j : Job),
(j \in arrivals_between arr_seq t1 t2) =
(j
\in \cat_(tsk<-ts)
task_arrivals_between arr_seq tsk t1 t2)
move => t1 t2 j.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t1, t2 : instant j : Job
(j \in arrivals_between arr_seq t1 t2) =
(j
\in \cat_(tsk<-ts)
task_arrivals_between arr_seq tsk t1 t2)
rewrite /task_arrivals_between.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t1, t2 : instant j : Job
(j \in arrivals_between arr_seq t1 t2) =
(j
\in \cat_(tsk<-ts)
[seq j <- arrivals_between arr_seq t1 t2
| job_of_task tsk j])
set l:= arrivals_between arr_seq t1 t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t1, t2 : instant j : Job l := arrivals_between arr_seq t1 t2 : seq Job
(j \in l) =
(j \in \cat_(tsk<-ts)[seq j <- l | job_of_task tsk j])
rewrite -{1 }(@filter_predT _ l).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t1, t2 : instant j : Job l := arrivals_between arr_seq t1 t2 : seq Job
(j \in [seq x <- l | predT x]) =
(j \in \cat_(tsk<-ts)[seq j <- l | job_of_task tsk j])
under eq_big_seq.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t1, t2 : instant j : Job l := arrivals_between arr_seq t1 t2 : seq Job
forall x : Task,
x \in ts -> 'Under[ [seq j <- l | job_of_task x j] ]
{ Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t1, t2 : instant j : Job l := arrivals_between arr_seq t1 t2 : seq Job
forall x : Task,
x \in ts -> 'Under[ [seq j <- l | job_of_task x j] ]
move => tsk tsk_IN.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t1, t2 : instant j : Job l := arrivals_between arr_seq t1 t2 : seq Job tsk : Task tsk_IN : tsk \in ts
'Under[ [seq j <- l | job_of_task tsk j] ]
rewrite (@eq_in_filter _ _ (fun j => (predT j) && (job_of_task tsk j))) => //.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t1, t2 : instant j : Job l := arrivals_between arr_seq t1 t2 : seq Job tsk : Task tsk_IN : tsk \in ts
'Under[ [seq j <- l | predT j & job_of_task tsk j] ]
over . } Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t1, t2 : instant j : Job l := arrivals_between arr_seq t1 t2 : seq Job
(j \in [seq x <- l | predT x]) =
(j
\in \cat_(i<-ts)
(fun tsk : Task =>
[seq j <- l | predT j & job_of_task tsk j]) i)
apply bigcat_partitions => j' IN' pred_true.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t1, t2 : instant j : Job l := arrivals_between arr_seq t1 t2 : seq Job j' : Job IN' : j' \in l pred_true : predT j'
job_task j' \in ts
apply H_all_jobs_from_taskset.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts t1, t2 : instant j : Job l := arrivals_between arr_seq t1 t2 : seq Job j' : Job IN' : j' \in l pred_true : predT j'
arrives_in arr_seq j'
by apply in_arrivals_implies_arrived in IN'.
Qed .
End ArrivalPartition .
End ArrivalSequencePrefix .
(** In this section, we establish a few auxiliary facts about the
relation between the property of being scheduled and arrival
predicates to facilitate automation. *)
Section ScheduledImpliesArrives .
(** Consider any type of jobs. *)
Context {Job : JobType}.
Context `{JobArrival Job}.
(** Consider any kind of processor state model, ... *)
Context {PState : ProcessorState Job}.
(** ... any job arrival sequence with consistent arrivals, .... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(** ... and any schedule of this arrival sequence ... *)
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
(** ... where jobs do not execute before their arrival. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
(** Next, consider a job [j] ... *)
Variable j : Job.
(** ... which is scheduled at a time instant [t]. *)
Variable t : instant.
Hypothesis H_scheduled_at : scheduled_at sched j t.
(** Then we show that [j] arrives in [arr_seq]. *)
Lemma arrives_in_jobs_come_from_arrival_sequence :
arrives_in arr_seq j.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job t : instant H_scheduled_at : scheduled_at sched j t
arrives_in arr_seq j
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job t : instant H_scheduled_at : scheduled_at sched j t
arrives_in arr_seq j
by apply : H_jobs_come_from_arrival_sequence H_scheduled_at.
Qed .
(** Job [j] has arrived by time instant [t]. *)
Lemma arrived_between_jobs_must_arrive_to_execute :
has_arrived j t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job t : instant H_scheduled_at : scheduled_at sched j t
has_arrived j t
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job t : instant H_scheduled_at : scheduled_at sched j t
has_arrived j t
by apply : H_jobs_must_arrive_to_execute H_scheduled_at.
Qed .
(** For any future time [t'], job [j] arrives before [t']. *)
Lemma arrivals_before_scheduled_at :
forall t' ,
t < t' ->
j \in arrivals_before arr_seq t'.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job t : instant H_scheduled_at : scheduled_at sched j t
forall t' : nat,
t < t' -> j \in arrivals_before arr_seq t'
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job t : instant H_scheduled_at : scheduled_at sched j t
forall t' : nat,
t < t' -> j \in arrivals_before arr_seq t'
move => t' LTtt'.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job t : instant H_scheduled_at : scheduled_at sched j t t' : nat LTtt' : t < t'
j \in arrivals_before arr_seq t'
apply : arrived_between_implies_in_arrivals => //.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job t : instant H_scheduled_at : scheduled_at sched j t t' : nat LTtt' : t < t'
arrived_between j 0 t'
apply : leq_ltn_trans LTtt'.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job t : instant H_scheduled_at : scheduled_at sched j t t' : nat
job_arrival j <= t
by apply : arrived_between_jobs_must_arrive_to_execute.
Qed .
(** Similarly, job [j] arrives up to time [t'] for any [t'] such that [t <= t']. *)
Lemma arrivals_up_to_scheduled_at :
forall t' ,
t <= t' ->
j \in arrivals_up_to arr_seq t'.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job t : instant H_scheduled_at : scheduled_at sched j t
forall t' : nat,
t <= t' -> j \in arrivals_up_to arr_seq t'
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job t : instant H_scheduled_at : scheduled_at sched j t
forall t' : nat,
t <= t' -> j \in arrivals_up_to arr_seq t'
by move => t' LEtt'; apply arrivals_before_scheduled_at; lia .
Qed .
End ScheduledImpliesArrives .
(** We add some of the above lemmas to the "Hint Database"
[basic_rt_facts], so the [auto] tactic will be able to use them. *)
Global Hint Resolve
any_ready_job_is_pending
arrivals_before_scheduled_at
arrivals_uniq
arrived_between_implies_in_arrivals
arrived_between_jobs_must_arrive_to_execute
arrives_in_jobs_come_from_arrival_sequence
backlogged_implies_arrived
job_scheduled_implies_ready
jobs_must_arrive_to_be_ready
jobs_must_arrive_to_be_ready
ready_implies_arrived
valid_schedule_implies_jobs_must_arrive_to_execute
valid_schedule_jobs_come_from_arrival_sequence
valid_schedule_jobs_must_be_ready_to_execute
uniq_valid_arrival
consistent_times_valid_arrival
job_arrival_arrives_at
job_in_arrivals_between
: basic_rt_facts.