Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.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.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
(** In this section, we prove some properties related to [job_index]. *)
Section JobIndexLemmas .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
(** ... and any jobs associated with the tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
(** Consider any arrival sequence with consistent and non-duplicate arrivals, ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and any two jobs [j1] and [j2] from this arrival sequence
that stem from the same task. *)
Variable j1 j2 : Job.
Hypothesis H_j1_from_arrival_sequence : arrives_in arr_seq j1.
Hypothesis H_j2_from_arrival_sequence : arrives_in arr_seq j2.
Hypothesis H_same_task : job_task j1 = job_task j2.
(** In the next section, we prove some basic properties about jobs with equal indices. *)
Section EqualJobIndex .
(** Assume that the jobs [j1] and [j2] have the same [job_index]
in the arrival sequence. *)
Hypothesis H_equal_index : job_index arr_seq j1 = job_index arr_seq j2.
(** To show that jobs [j1] and [j2] are equal, we'll perform case
analysis on the relation between their arrival times. *)
(** Jobs with equal indices have to be equal regardless of their
arrival times because of the way [job_index] is defined (i.e.,
jobs are first ordered according to their arrival times and ties are
broken arbitrarily due to which no two unequal jobs have the same
[job_index]). *)
(** In case job [j2] arrives after or at the same time as [j1] arrives, we
show that the jobs are equal. *)
Lemma case_arrival_lte_implies_equal_job :
job_arrival j1 <= job_arrival j2 -> j1 = j2.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2
job_arrival j1 <= job_arrival j2 -> j1 = j2
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2
job_arrival j1 <= job_arrival j2 -> j1 = j2
move => ARR_LT.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2 ARR_LT : job_arrival j1 <= job_arrival j2
j1 = j2
move : H_equal_index => IND.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2 ARR_LT : job_arrival j1 <= job_arrival j2 IND : job_index arr_seq j1 = job_index arr_seq j2
j1 = j2
try ( apply task_arrivals_up_to_prefix_cat with (arr_seq0 := arr_seq) in ARR_LT => // ) ||
apply task_arrivals_up_to_prefix_cat with (arr_seq := arr_seq) in ARR_LT => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2 ARR_LT : prefix_of
(task_arrivals_up_to_job_arrival arr_seq j1)
(task_arrivals_up_to_job_arrival arr_seq j2) IND : job_index arr_seq j1 = job_index arr_seq j2
j1 = j2
move : ARR_LT => [xs ARR_CAT].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j1 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j2
j1 = j2
try ( apply eq_ind_in_seq with (xs0 := task_arrivals_up_to_job_arrival arr_seq j2) => // ) ||
apply eq_ind_in_seq with (xs := task_arrivals_up_to_job_arrival arr_seq j2) => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j1 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j2
index j1 (task_arrivals_up_to_job_arrival arr_seq j2) =
index j2 (task_arrivals_up_to_job_arrival arr_seq j2)
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j1 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j2
index j1 (task_arrivals_up_to_job_arrival arr_seq j2) =
index j2 (task_arrivals_up_to_job_arrival arr_seq j2)
by rewrite -/(job_index _ _) -IND -ARR_CAT index_cat ifT;
try apply arrives_in_task_arrivals_up_to; rt_eauto.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j1 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j2
j1 \in task_arrivals_up_to_job_arrival arr_seq j2
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j1 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j2
j1 \in task_arrivals_up_to_job_arrival arr_seq j2
rewrite -ARR_CAT mem_cat; apply /orP.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j1 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j2
j1 \in task_arrivals_up_to_job_arrival arr_seq j1 \/
j1 \in xs
by left ; apply arrives_in_task_arrivals_up_to; rt_eauto.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j1 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j2
j2 \in task_arrivals_up_to_job_arrival arr_seq j2
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j1 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j2
j2 \in task_arrivals_up_to_job_arrival arr_seq j2
by apply arrives_in_task_arrivals_up_to; rt_eauto.
Qed .
(** And similarly if [j1] arrives after [j2], we show that
the jobs are equal. *)
Lemma case_arrival_gt_implies_equal_job :
job_arrival j1 > job_arrival j2 -> j1 = j2.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2
job_arrival j2 < job_arrival j1 -> j1 = j2
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2
job_arrival j2 < job_arrival j1 -> j1 = j2
move => LT.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2 LT : job_arrival j2 < job_arrival j1
j1 = j2
move : H_equal_index => IND.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2 LT : job_arrival j2 < job_arrival j1 IND : job_index arr_seq j1 = job_index arr_seq j2
j1 = j2
apply ltnW, (task_arrivals_up_to_prefix_cat arr_seq) in LT => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2 LT : prefix_of
(task_arrivals_up_to_job_arrival arr_seq j2)
(task_arrivals_up_to_job_arrival arr_seq j1) IND : job_index arr_seq j1 = job_index arr_seq j2
j1 = j2
move : LT => [xs ARR_CAT].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j2 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j1
j1 = j2
apply (eq_ind_in_seq _ _ (task_arrivals_up_to_job_arrival arr_seq j1)) => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j2 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j1
index j1 (task_arrivals_up_to_job_arrival arr_seq j1) =
index j2 (task_arrivals_up_to_job_arrival arr_seq j1)
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j2 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j1
index j1 (task_arrivals_up_to_job_arrival arr_seq j1) =
index j2 (task_arrivals_up_to_job_arrival arr_seq j1)
by rewrite -/(job_index _ _) IND -ARR_CAT index_cat ifT;
try apply arrives_in_task_arrivals_up_to; rt_eauto.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j2 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j1
j1 \in task_arrivals_up_to_job_arrival arr_seq j1
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j2 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j1
j1 \in task_arrivals_up_to_job_arrival arr_seq j1
by apply arrives_in_task_arrivals_up_to; rt_eauto.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j2 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j1
j2 \in task_arrivals_up_to_job_arrival arr_seq j1
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j2 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j1
j2 \in task_arrivals_up_to_job_arrival arr_seq j1
rewrite -ARR_CAT mem_cat; apply /orP.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index, IND : job_index arr_seq j1 =
job_index arr_seq j2 xs : seq Job ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j2 ++
xs =
task_arrivals_up_to_job_arrival arr_seq j1
j2 \in task_arrivals_up_to_job_arrival arr_seq j2 \/
j2 \in xs
by left ; apply arrives_in_task_arrivals_up_to => //; rt_eauto.
Qed .
(** And finally we show that irrespective of the relation between the arrival
of job [j1] and [j2], [j1] must be equal to [j2]. *)
Lemma equal_index_implies_equal_jobs :
j1 = j2.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2
j1 = j2
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2
j1 = j2
case : (ltngtP (job_arrival j1) (job_arrival j2)) => [LT|GT|EQ].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2
j1 = j2
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2 LT : job_arrival j1 < job_arrival j2
j1 = j2
by apply case_arrival_lte_implies_equal_job; lia .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2 GT : job_arrival j2 < job_arrival j1
j1 = j2
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2 GT : job_arrival j2 < job_arrival j1
j1 = j2
by apply case_arrival_gt_implies_equal_job; lia .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2 EQ : job_arrival j1 = job_arrival j2
j1 = j2
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 H_equal_index : job_index arr_seq j1 =
job_index arr_seq j2 EQ : job_arrival j1 = job_arrival j2
j1 = j2
by apply case_arrival_lte_implies_equal_job; lia .
Qed .
End EqualJobIndex .
(** We show that jobs of a task are different if and only if they
have different indices. *)
Lemma diff_jobs_iff_diff_indices :
j1 <> j2 <->
job_index arr_seq j1 <> job_index arr_seq j2.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
j1 <> j2 <->
job_index arr_seq j1 <> job_index arr_seq j2
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
j1 <> j2 <->
job_index arr_seq j1 <> job_index arr_seq j2
split .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
j1 <> j2 ->
job_index arr_seq j1 <> job_index arr_seq j2
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
j1 <> j2 ->
job_index arr_seq j1 <> job_index arr_seq j2
move => NEQJ EQ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 NEQJ : j1 <> j2 EQ : job_index arr_seq j1 = job_index arr_seq j2
False
by apply equal_index_implies_equal_jobs in EQ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
job_index arr_seq j1 <> job_index arr_seq j2 ->
j1 <> j2
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
job_index arr_seq j1 <> job_index arr_seq j2 ->
j1 <> j2
move => NEQ EQ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 NEQ : job_index arr_seq j1 <> job_index arr_seq j2 EQ : j1 = j2
False
by move : EQ NEQ => ->.
Qed .
(** We show that [job_index j] can be written as a sum of [size (task_arrivals_before_job_arrival j)]
and [index j (task_arrivals_at arr_seq (job_task j) (job_arrival j))]. *)
Lemma index_as_sum_size_and_index :
job_index arr_seq j1 =
size (task_arrivals_before_job_arrival arr_seq j1)
+ index j1 (task_arrivals_at_job_arrival arr_seq j1).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
job_index arr_seq j1 =
size (task_arrivals_before_job_arrival arr_seq j1) +
index j1 (task_arrivals_at_job_arrival arr_seq j1)
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
job_index arr_seq j1 =
size (task_arrivals_before_job_arrival arr_seq j1) +
index j1 (task_arrivals_at_job_arrival arr_seq j1)
rewrite /task_arrivals_at_job_arrival /job_index task_arrivals_up_to_cat //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
index j1
(task_arrivals_before_job_arrival arr_seq j1 ++
task_arrivals_at_job_arrival arr_seq j1) =
size (task_arrivals_before_job_arrival arr_seq j1) +
index j1
(task_arrivals_at arr_seq (job_task j1)
(job_arrival j1))
rewrite index_cat ifF; first by reflexivity .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
(j1 \in task_arrivals_before_job_arrival arr_seq j1) =
false
apply Bool.not_true_is_false; intro T.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 T : (j1
\in task_arrivals_before_job_arrival arr_seq j1) =
true
False
move : T; rewrite mem_filter => /andP [/eqP SM_TSK JB_IN_ARR].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 SM_TSK : job_task j1 = job_task j1 JB_IN_ARR : j1
\in arrivals_between arr_seq 0
(job_arrival j1)
False
apply mem_bigcat_nat_exists in JB_IN_ARR; move : JB_IN_ARR => [ind [JB_IN IND_INTR]].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 SM_TSK : job_task j1 = job_task j1 ind : nat JB_IN : j1 \in arrivals_at arr_seq ind IND_INTR : 0 <= ind < job_arrival j1
False
have ARR : job_arrival j1 = ind by rt_eauto.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 SM_TSK : job_task j1 = job_task j1 ind : nat JB_IN : j1 \in arrivals_at arr_seq ind IND_INTR : 0 <= ind < job_arrival j1ARR : job_arrival j1 = ind
False
by lia .
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 (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).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
forall (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 .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
forall (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)
intros * J1_IN J2_IN ARR_LT.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant J1_IN : j1 \in arrivals_between_P arr_seq P t1 t2 J2_IN : j2 \in arrivals_between_P arr_seq P t1 t2 ARR_LT : job_arrival j2 < job_arrival j1
j2
\in arrivals_between_P arr_seq P t1 (job_arrival j1)
rewrite mem_filter in J2_IN; move : J2_IN => /andP [PJ2 J2ARR] => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant J1_IN : j1 \in arrivals_between_P arr_seq P t1 t2 ARR_LT : job_arrival j2 < job_arrival j1 PJ2 : P j2 J2ARR : j2 \in arrivals_between arr_seq t1 t2
j2
\in arrivals_between_P arr_seq P t1 (job_arrival j1)
rewrite mem_filter; apply /andP; split => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant J1_IN : j1 \in arrivals_between_P arr_seq P t1 t2 ARR_LT : job_arrival j2 < job_arrival j1 PJ2 : P j2 J2ARR : j2 \in arrivals_between arr_seq t1 t2
j2 \in arrivals_between arr_seq t1 (job_arrival j1)
apply mem_bigcat_nat_exists in J2ARR; move : J2ARR => [i [J2_IN INEQ]].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant J1_IN : j1 \in arrivals_between_P arr_seq P t1 t2 ARR_LT : job_arrival j2 < job_arrival j1 PJ2 : P j2 i : nat J2_IN : j2 \in arrivals_at arr_seq i INEQ : t1 <= i < t2
j2 \in arrivals_between arr_seq t1 (job_arrival j1)
apply mem_bigcat_nat with (j := i) => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant J1_IN : j1 \in arrivals_between_P arr_seq P t1 t2 ARR_LT : job_arrival j2 < job_arrival j1 PJ2 : P j2 i : nat J2_IN : j2 \in arrivals_at arr_seq i INEQ : t1 <= i < t2
t1 <= i < job_arrival j1
apply job_arrival_at in J2_IN; rt_eauto.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant J1_IN : j1 \in arrivals_between_P arr_seq P t1 t2 ARR_LT : job_arrival j2 < job_arrival j1 PJ2 : P j2 i : nat J2_IN : job_arrival j2 = i INEQ : t1 <= i < t2
t1 <= i < job_arrival j1
by lia .
Qed .
(** We show that jobs in the sequence [arrivals_between_P] are ordered by their arrival times, i.e.,
if index of a job [j2] is greater than or equal to index of any other job [j1] in the sequence,
then [job_arrival j2] must be greater than or equal to [job_arrival j1]. *)
Lemma index_lte_implies_arrival_lte_P :
forall (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) ->
index j1 (arrivals_between_P arr_seq P t1 t2) <= index j2 (arrivals_between_P arr_seq P t1 t2) ->
job_arrival j1 <= job_arrival j2.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
forall (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 ->
index j1 (arrivals_between_P arr_seq P t1 t2) <=
index j2 (arrivals_between_P arr_seq P t1 t2) ->
job_arrival j1 <= job_arrival j2
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
forall (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 ->
index j1 (arrivals_between_P arr_seq P t1 t2) <=
index j2 (arrivals_between_P arr_seq P t1 t2) ->
job_arrival j1 <= job_arrival j2
intros * IN1 IN2 LE.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant IN1 : j1 \in arrivals_between_P arr_seq P t1 t2 IN2 : j2 \in arrivals_between_P arr_seq P t1 t2 LE : index j1 (arrivals_between_P arr_seq P t1 t2) <=
index j2 (arrivals_between_P arr_seq P t1 t2)
job_arrival j1 <= job_arrival j2
move_neq_up LT; move_neq_down LE. Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant IN1 : j1 \in arrivals_between_P arr_seq P t1 t2 IN2 : j2 \in arrivals_between_P arr_seq P t1 t2 LT : job_arrival j2 < job_arrival j1
index j2 (arrivals_between_P arr_seq P t1 t2) <
index j1 (arrivals_between_P arr_seq P t1 t2)
rewrite -> arrivals_P_cat with (t := job_arrival j1); last by apply job_arrival_between_P in IN1; rt_eauto.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant IN1 : j1 \in arrivals_between_P arr_seq P t1 t2 IN2 : j2 \in arrivals_between_P arr_seq P t1 t2 LT : job_arrival j2 < job_arrival j1
index j2
(arrivals_between_P arr_seq P t1 (job_arrival j1) ++
arrivals_between_P arr_seq P (job_arrival j1) t2) <
index j1
(arrivals_between_P arr_seq P t1 (job_arrival j1) ++
arrivals_between_P arr_seq P (job_arrival j1) t2)
rewrite !index_cat ifT; last by eapply arrival_lt_implies_job_in_arrivals_between_P; eauto .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant IN1 : j1 \in arrivals_between_P arr_seq P t1 t2 IN2 : j2 \in arrivals_between_P arr_seq P t1 t2 LT : job_arrival j2 < job_arrival j1
index j2
(arrivals_between_P arr_seq P t1 (job_arrival j1)) <
(if
j1
\in arrivals_between_P arr_seq P t1
(job_arrival j1)
then
index j1
(arrivals_between_P arr_seq P t1 (job_arrival j1))
else
size
(arrivals_between_P arr_seq P t1 (job_arrival j1)) +
index j1
(arrivals_between_P arr_seq P (job_arrival j1) t2))
rewrite ifF.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant IN1 : j1 \in arrivals_between_P arr_seq P t1 t2 IN2 : j2 \in arrivals_between_P arr_seq P t1 t2 LT : job_arrival j2 < job_arrival j1
index j2
(arrivals_between_P arr_seq P t1 (job_arrival j1)) <
size
(arrivals_between_P arr_seq P t1 (job_arrival j1)) +
index j1
(arrivals_between_P arr_seq P (job_arrival j1) t2)
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant IN1 : j1 \in arrivals_between_P arr_seq P t1 t2 IN2 : j2 \in arrivals_between_P arr_seq P t1 t2 LT : job_arrival j2 < job_arrival j1
index j2
(arrivals_between_P arr_seq P t1 (job_arrival j1)) <
size
(arrivals_between_P arr_seq P t1 (job_arrival j1)) +
index j1
(arrivals_between_P arr_seq P (job_arrival j1) t2)
eapply leq_trans; [ | by erewrite leq_addr].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant IN1 : j1 \in arrivals_between_P arr_seq P t1 t2 IN2 : j2 \in arrivals_between_P arr_seq P t1 t2 LT : job_arrival j2 < job_arrival j1
index j2
(arrivals_between_P arr_seq P t1 (job_arrival j1)) <
size
(arrivals_between_P arr_seq P t1 (job_arrival j1))
rewrite index_mem.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant IN1 : j1 \in arrivals_between_P arr_seq P t1 t2 IN2 : j2 \in arrivals_between_P arr_seq P t1 t2 LT : job_arrival j2 < job_arrival j1
j2
\in arrivals_between_P arr_seq P t1 (job_arrival j1)
by eapply arrival_lt_implies_job_in_arrivals_between_P; eauto .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant IN1 : j1 \in arrivals_between_P arr_seq P t1 t2 IN2 : j2 \in arrivals_between_P arr_seq P t1 t2 LT : job_arrival j2 < job_arrival j1
(j1
\in arrivals_between_P arr_seq P t1
(job_arrival j1)) = false
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant IN1 : j1 \in arrivals_between_P arr_seq P t1 t2 IN2 : j2 \in arrivals_between_P arr_seq P t1 t2 LT : job_arrival j2 < job_arrival j1
(j1
\in arrivals_between_P arr_seq P t1
(job_arrival j1)) = false
apply Bool.not_true_is_false; intro T.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 P : Job -> bool t1, t2 : instant IN1 : j1 \in arrivals_between_P arr_seq P t1 t2 IN2 : j2 \in arrivals_between_P arr_seq P t1 t2 LT : job_arrival j2 < job_arrival j1 T : (j1
\in arrivals_between_P arr_seq P t1
(job_arrival j1)) = true
False
by apply job_arrival_between_P in T; try lia ; rt_eauto.
Qed .
(** We observe that index of job [j1] is same in the
sequences [task_arrivals_up_to_job_arrival j1] and [task_arrivals_up_to_job_arrival j2]
provided [j2] arrives after [j1]. *)
Lemma job_index_same_in_task_arrivals :
job_arrival j1 <= job_arrival j2 ->
index j1 (task_arrivals_up_to_job_arrival arr_seq j1) = index j1 (task_arrivals_up_to_job_arrival arr_seq j2).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
job_arrival j1 <= job_arrival j2 ->
index j1 (task_arrivals_up_to_job_arrival arr_seq j1) =
index j1 (task_arrivals_up_to_job_arrival arr_seq j2)
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
job_arrival j1 <= job_arrival j2 ->
index j1 (task_arrivals_up_to_job_arrival arr_seq j1) =
index j1 (task_arrivals_up_to_job_arrival arr_seq j2)
rewrite leq_eqVlt => /orP [/eqP LT|LT]; first by rewrite /task_arrivals_up_to_job_arrival LT H_same_task.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 LT : job_arrival j1 < job_arrival j2
index j1 (task_arrivals_up_to_job_arrival arr_seq j1) =
index j1 (task_arrivals_up_to_job_arrival arr_seq j2)
have CONSISTENT : consistent_arrival_times arr_seq by rt_eauto.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 LT : job_arrival j1 < job_arrival j2 CONSISTENT : consistent_arrival_times arr_seq
index j1 (task_arrivals_up_to_job_arrival arr_seq j1) =
index j1 (task_arrivals_up_to_job_arrival arr_seq j2)
specialize (arrival_lt_implies_strict_prefix arr_seq CONSISTENT (job_task j1) j1 j2) => SUB.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 LT : job_arrival j1 < job_arrival j2 CONSISTENT : consistent_arrival_times arr_seq SUB : job_task j1 = job_task j1 ->
job_task j2 = job_task j1 ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
strict_prefix_of
(task_arrivals_up_to_job_arrival arr_seq j1)
(task_arrivals_up_to_job_arrival arr_seq j2)
index j1 (task_arrivals_up_to_job_arrival arr_seq j1) =
index j1 (task_arrivals_up_to_job_arrival arr_seq j2)
feed_n 5 SUB => //; move : SUB => [xs2 [NEMPT2 CAT2]]. Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 LT : job_arrival j1 < job_arrival j2 CONSISTENT : consistent_arrival_times arr_seq xs2 : seq Job NEMPT2 : xs2 <> [::] CAT2 : task_arrivals_up_to_job_arrival arr_seq j1 ++
xs2 =
task_arrivals_up_to_job_arrival arr_seq j2
index j1 (task_arrivals_up_to_job_arrival arr_seq j1) =
index j1 (task_arrivals_up_to_job_arrival arr_seq j2)
rewrite -CAT2 index_cat ifT //=.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 LT : job_arrival j1 < job_arrival j2 CONSISTENT : consistent_arrival_times arr_seq xs2 : seq Job NEMPT2 : xs2 <> [::] CAT2 : task_arrivals_up_to_job_arrival arr_seq j1 ++
xs2 =
task_arrivals_up_to_job_arrival arr_seq j2
j1 \in task_arrivals_up_to_job_arrival arr_seq j1
by apply arrives_in_task_arrivals_up_to => //.
Qed .
(** We show that the [job_index] of a job [j1] is strictly less than
the size of [task_arrivals_up_to_job_arrival arr_seq j1]. *)
Lemma index_job_lt_size_task_arrivals_up_to_job :
job_index arr_seq j1 < size (task_arrivals_up_to_job_arrival arr_seq j1).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
job_index arr_seq j1 <
size (task_arrivals_up_to_job_arrival arr_seq j1)
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
job_index arr_seq j1 <
size (task_arrivals_up_to_job_arrival arr_seq j1)
rewrite /job_index index_mem.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
j1 \in task_arrivals_up_to_job_arrival arr_seq j1
by apply arrives_in_task_arrivals_up_to; rt_eauto.
Qed .
(** Finally, we show that a lower job index implies an earlier arrival time. *)
Lemma index_lte_implies_arrival_lte :
job_index arr_seq j2 <= job_index arr_seq j1 ->
job_arrival j2 <= job_arrival j1.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
job_index arr_seq j2 <= job_index arr_seq j1 ->
job_arrival j2 <= job_arrival j1
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
job_index arr_seq j2 <= job_index arr_seq j1 ->
job_arrival j2 <= job_arrival j1
intros IND_LT.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 IND_LT : job_index arr_seq j2 <= job_index arr_seq j1
job_arrival j2 <= job_arrival j1
rewrite /job_index in IND_LT.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 IND_LT : index j2
(task_arrivals_up_to_job_arrival arr_seq j2) <=
index j1
(task_arrivals_up_to_job_arrival arr_seq j1)
job_arrival j2 <= job_arrival j1
move_neq_up ARR_GT; move_neq_down IND_LT. Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 ARR_GT : job_arrival j1 < job_arrival j2
index j1 (task_arrivals_up_to_job_arrival arr_seq j1) <
index j2 (task_arrivals_up_to_job_arrival arr_seq j2)
rewrite job_index_same_in_task_arrivals /task_arrivals_up_to_job_arrival; try by lia .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 ARR_GT : job_arrival j1 < job_arrival j2
index j1
(task_arrivals_up_to arr_seq (job_task j2)
(job_arrival j2)) <
index j2
(task_arrivals_up_to arr_seq (job_task j2)
(job_arrival j2))
rewrite -> task_arrivals_cat with (t_m := job_arrival j1); try by lia .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 ARR_GT : job_arrival j1 < job_arrival j2
index j1
(task_arrivals_up_to arr_seq (job_task j2)
(job_arrival j1) ++
task_arrivals_between arr_seq (job_task j2)
(job_arrival j1).+1 (job_arrival j2).+1 ) <
index j2
(task_arrivals_up_to arr_seq (job_task j2)
(job_arrival j1) ++
task_arrivals_between arr_seq (job_task j2)
(job_arrival j1).+1 (job_arrival j2).+1 )
rewrite -H_same_task !index_cat ifT; try by apply arrives_in_task_arrivals_up_to; rt_eauto.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 ARR_GT : job_arrival j1 < job_arrival j2
index j1
(task_arrivals_up_to arr_seq (job_task j1)
(job_arrival j1)) <
(if
j2
\in task_arrivals_up_to arr_seq (job_task j1)
(job_arrival j1)
then
index j2
(task_arrivals_up_to arr_seq (job_task j1)
(job_arrival j1))
else
size
(task_arrivals_up_to arr_seq (job_task j1)
(job_arrival j1)) +
index j2
(task_arrivals_between arr_seq (job_task j1)
(job_arrival j1).+1 (job_arrival j2).+1 ))
rewrite ifF.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 ARR_GT : job_arrival j1 < job_arrival j2
index j1
(task_arrivals_up_to arr_seq (job_task j1)
(job_arrival j1)) <
size
(task_arrivals_up_to arr_seq (job_task j1)
(job_arrival j1)) +
index j2
(task_arrivals_between arr_seq (job_task j1)
(job_arrival j1).+1 (job_arrival j2).+1 )
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 ARR_GT : job_arrival j1 < job_arrival j2
index j1
(task_arrivals_up_to arr_seq (job_task j1)
(job_arrival j1)) <
size
(task_arrivals_up_to arr_seq (job_task j1)
(job_arrival j1)) +
index j2
(task_arrivals_between arr_seq (job_task j1)
(job_arrival j1).+1 (job_arrival j2).+1 )
by eapply leq_trans;
[apply index_job_lt_size_task_arrivals_up_to_job | rewrite leq_addr].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 ARR_GT : job_arrival j1 < job_arrival j2
(j2
\in task_arrivals_up_to arr_seq (job_task j1)
(job_arrival j1)) = false
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 ARR_GT : job_arrival j1 < job_arrival j2
(j2
\in task_arrivals_up_to arr_seq (job_task j1)
(job_arrival j1)) = false
apply Bool.not_true_is_false; intro T.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 ARR_GT : job_arrival j1 < job_arrival j2 T : (j2
\in task_arrivals_up_to arr_seq
(job_task j1) (job_arrival j1)) = true
False
by apply job_arrival_between_P in T; try lia ; rt_eauto.
Qed .
(** We show that if job [j1] arrives earlier than job [j2]
then [job_index arr_seq j1] is strictly less than [job_index arr_seq j2]. *)
Lemma earlier_arrival_implies_lower_index :
job_arrival j1 < job_arrival j2 ->
job_index arr_seq j1 < job_index arr_seq j2.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
job_arrival j1 < job_arrival j2 ->
job_index arr_seq j1 < job_index arr_seq j2
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
job_arrival j1 < job_arrival j2 ->
job_index arr_seq j1 < job_index arr_seq j2
intros ARR_LT.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 ARR_LT : job_arrival j1 < job_arrival j2
job_index arr_seq j1 < job_index arr_seq j2
move_neq_up IND_LT; move_neq_down ARR_LT. Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 IND_LT : job_index arr_seq j2 <= job_index arr_seq j1
job_arrival j2 <= job_arrival j1
by apply index_lte_implies_arrival_lte.
Qed .
(** We prove a weaker version of the lemma [index_job_lt_size_task_arrivals_up_to_job],
given that the [job_index] of [j] is positive. *)
Lemma job_index_minus_one_lt_size_task_arrivals_up_to :
job_index arr_seq j1 - 1 < size (task_arrivals_up_to_job_arrival arr_seq j1).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
job_index arr_seq j1 - 1 <
size (task_arrivals_up_to_job_arrival arr_seq j1)
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
job_index arr_seq j1 - 1 <
size (task_arrivals_up_to_job_arrival arr_seq j1)
apply leq_ltn_trans with (n := job_index arr_seq j1); try by lia .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
job_index arr_seq j1 <
size (task_arrivals_up_to_job_arrival arr_seq j1)
by apply index_job_lt_size_task_arrivals_up_to_job.
Qed .
(** Since [task_arrivals_up_to_job_arrival arr_seq j] has at least the job
[j] in it, its size has to be positive. *)
Lemma positive_job_index_implies_positive_size_of_task_arrivals :
size (task_arrivals_up_to_job_arrival arr_seq j1) > 0 .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
0 < size (task_arrivals_up_to_job_arrival arr_seq j1)
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2
0 < size (task_arrivals_up_to_job_arrival arr_seq j1)
rewrite lt0n; apply /eqP; intro Z.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 Z : size (task_arrivals_up_to_job_arrival arr_seq j1) =
0
False
apply size0nil in Z.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 Z : task_arrivals_up_to_job_arrival arr_seq j1 = [::]
False
have J_IN : (j1 \in task_arrivals_up_to_job_arrival arr_seq j1)
by apply arrives_in_task_arrivals_up_to => //; rt_eauto.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j1, j2 : Job H_j1_from_arrival_sequence : arrives_in arr_seq j1 H_j2_from_arrival_sequence : arrives_in arr_seq j2 H_same_task : job_task j1 = job_task j2 Z : task_arrivals_up_to_job_arrival arr_seq j1 = [::] J_IN : j1
\in task_arrivals_up_to_job_arrival arr_seq
j1
False
by rewrite Z in J_IN.
Qed .
End JobIndexLemmas .
(** In this section, we prove a few basic properties of
function [prev_job]. *)
Section PreviousJob .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
(** ... and any jobs associated with the tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
(** Consider any unique arrival sequence with consistent arrivals ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and an arbitrary job with a positive [job_index]. *)
Variable j : Job.
Hypothesis H_arrives_in_arr_seq : arrives_in arr_seq j.
Hypothesis H_positive_job_index : job_index arr_seq j > 0 .
(** We observe that the fact that job [j] is in the arrival sequence
implies that job [prev_job j] is in the arrival sequence. *)
Lemma prev_job_arr :
arrives_in arr_seq (prev_job arr_seq j).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
arrives_in arr_seq (prev_job arr_seq j)
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
arrives_in arr_seq (prev_job arr_seq j)
destruct (default_or_in (job_index arr_seq j - 1 ) j (task_arrivals_up_to_job_arrival arr_seq j)) as [EQ|IN].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq jEQ : nth j (task_arrivals_up_to_job_arrival arr_seq j)
(job_index arr_seq j - 1 ) = j
arrives_in arr_seq (prev_job arr_seq j)
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq jEQ : nth j (task_arrivals_up_to_job_arrival arr_seq j)
(job_index arr_seq j - 1 ) = j
arrives_in arr_seq (prev_job arr_seq j)
by rewrite /prev_job EQ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq jIN : nth j (task_arrivals_up_to_job_arrival arr_seq j)
(job_index arr_seq j - 1 )
\in task_arrivals_up_to_job_arrival arr_seq j
arrives_in arr_seq (prev_job arr_seq j)
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq jIN : nth j (task_arrivals_up_to_job_arrival arr_seq j)
(job_index arr_seq j - 1 )
\in task_arrivals_up_to_job_arrival arr_seq j
arrives_in arr_seq (prev_job arr_seq j)
apply in_arrivals_implies_arrived with (t1 := 0 ) (t2 := (job_arrival j).+1 ).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq jIN : nth j (task_arrivals_up_to_job_arrival arr_seq j)
(job_index arr_seq j - 1 )
\in task_arrivals_up_to_job_arrival arr_seq j
prev_job arr_seq j
\in arrivals_between arr_seq 0 (job_arrival j).+1
by move : IN; rewrite mem_filter => /andP [_ IN].
Qed .
(** We show that the index of [prev_job j] in task arrivals up to [j] is one less
than [job_index arr_seq j]. *)
Lemma prev_job_index :
index (prev_job arr_seq j) (task_arrivals_up_to_job_arrival arr_seq j) = job_index arr_seq j - 1 .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
index (prev_job arr_seq j)
(task_arrivals_up_to_job_arrival arr_seq j) =
job_index arr_seq j - 1
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
index (prev_job arr_seq j)
(task_arrivals_up_to_job_arrival arr_seq j) =
job_index arr_seq j - 1
apply index_uniq; last by apply uniq_task_arrivals; rt_eauto.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
job_index arr_seq j - 1 <
size (task_arrivals_up_to_job_arrival arr_seq j)
apply leq_ltn_trans with (n := job_index arr_seq j); try by lia .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
job_index arr_seq j <
size (task_arrivals_up_to_job_arrival arr_seq j)
by apply index_job_lt_size_task_arrivals_up_to_job.
Qed .
(** Observe that job [j] and [prev_job j] stem from the same task. *)
Lemma prev_job_task :
job_task (prev_job arr_seq j) = job_task j.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
job_task (prev_job arr_seq j) = job_task j
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
job_task (prev_job arr_seq j) = job_task j
specialize (job_index_minus_one_lt_size_task_arrivals_up_to arr_seq H_valid_arrival_sequence j H_arrives_in_arr_seq) => SIZEL.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq jSIZEL : job_index arr_seq j - 1 <
size
(task_arrivals_up_to_job_arrival arr_seq j)
job_task (prev_job arr_seq j) = job_task j
rewrite -prev_job_index index_mem mem_filter in SIZEL.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq jSIZEL : job_of_task (job_task j) (prev_job arr_seq j) &&
(prev_job arr_seq j
\in arrivals_between arr_seq 0
(job_arrival j).+1 )
job_task (prev_job arr_seq j) = job_task j
by move : SIZEL => /andP [/eqP TSK PREV_IN].
Qed .
(** We show that [prev_job arr_seq j] belongs in [task_arrivals_up_to_job_arrival arr_seq j]. *)
Lemma prev_job_in_task_arrivals_up_to_j :
prev_job arr_seq j \in task_arrivals_up_to_job_arrival arr_seq j.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
prev_job arr_seq j
\in task_arrivals_up_to_job_arrival arr_seq j
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
prev_job arr_seq j
\in task_arrivals_up_to_job_arrival arr_seq j
rewrite /prev_job -index_mem index_uniq;
try by apply job_index_minus_one_lt_size_task_arrivals_up_to.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
uniq (task_arrivals_up_to_job_arrival arr_seq j)
by apply uniq_task_arrivals; rt_eauto.
Qed .
(** We observe that for any job [j] the arrival time of [prev_job j] is
strictly less than the arrival time of [j] in context of periodic tasks. *)
Lemma prev_job_arr_lte :
job_arrival (prev_job arr_seq j) <= job_arrival j.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
job_arrival (prev_job arr_seq j) <= job_arrival j
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
job_arrival (prev_job arr_seq j) <= job_arrival j
move : (prev_job_in_task_arrivals_up_to_j) => PREV_JOB_IN.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq jPREV_JOB_IN : prev_job arr_seq j
\in task_arrivals_up_to_job_arrival
arr_seq j
job_arrival (prev_job arr_seq j) <= job_arrival j
rewrite mem_filter in PREV_JOB_IN; move : PREV_JOB_IN => /andP [TSK PREV_IN].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq jTSK : job_of_task (job_task j) (prev_job arr_seq j) PREV_IN : prev_job arr_seq j
\in arrivals_between arr_seq 0
(job_arrival j).+1
job_arrival (prev_job arr_seq j) <= job_arrival j
apply mem_bigcat_nat_exists in PREV_IN; move : PREV_IN => [i [PREV_IN INEQ]].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq jTSK : job_of_task (job_task j) (prev_job arr_seq j) i : nat PREV_IN : prev_job arr_seq j \in arrivals_at arr_seq i INEQ : 0 <= i < (job_arrival j).+1
job_arrival (prev_job arr_seq j) <= job_arrival j
move : H_valid_arrival_sequence => [CONSISTENT UNIQ].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq jTSK : job_of_task (job_task j) (prev_job arr_seq j) i : nat PREV_IN : prev_job arr_seq j \in arrivals_at arr_seq i INEQ : 0 <= i < (job_arrival j).+1 CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq
job_arrival (prev_job arr_seq j) <= job_arrival j
apply CONSISTENT in PREV_IN; rewrite -PREV_IN in INEQ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq jTSK : job_of_task (job_task j) (prev_job arr_seq j) i : nat PREV_IN : job_arrival (prev_job arr_seq j) = i CONSISTENT : consistent_arrival_times arr_seq UNIQ : arrival_sequence_uniq arr_seq INEQ : 0 <= job_arrival (prev_job arr_seq j) <
(job_arrival j).+1
job_arrival (prev_job arr_seq j) <= job_arrival j
by lia .
Qed .
(** We show that for any job [j] the job index of [prev_job j] is one less
than the job index of [j]. *)
Lemma prev_job_index_j :
job_index arr_seq j > 0 ->
job_index arr_seq (prev_job arr_seq j) = job_index arr_seq j - 1 .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
0 < job_index arr_seq j ->
job_index arr_seq (prev_job arr_seq j) =
job_index arr_seq j - 1
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
0 < job_index arr_seq j ->
job_index arr_seq (prev_job arr_seq j) =
job_index arr_seq j - 1
intros NZ_IND.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, NZ_IND : 0 < job_index arr_seq j
job_index arr_seq (prev_job arr_seq j) =
job_index arr_seq j - 1
rewrite -prev_job_index.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, NZ_IND : 0 < job_index arr_seq j
job_index arr_seq (prev_job arr_seq j) =
index (prev_job arr_seq j)
(task_arrivals_up_to_job_arrival arr_seq j)
apply job_index_same_in_task_arrivals => //; rt_eauto.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, NZ_IND : 0 < job_index arr_seq j
arrives_in arr_seq (prev_job arr_seq j)
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, NZ_IND : 0 < job_index arr_seq j
arrives_in arr_seq (prev_job arr_seq j)
by apply prev_job_arr.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, NZ_IND : 0 < job_index arr_seq j
job_task (prev_job arr_seq j) = job_task j
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, NZ_IND : 0 < job_index arr_seq j
job_task (prev_job arr_seq j) = job_task j
by apply prev_job_task.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, NZ_IND : 0 < job_index arr_seq j
job_arrival (prev_job arr_seq j) <= job_arrival j
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, NZ_IND : 0 < job_index arr_seq j
job_arrival (prev_job arr_seq j) <= job_arrival j
by apply prev_job_arr_lte.
Qed .
(** We also show that for any job [j] there are no task arrivals
between [prev_job j] and [j].*)
Lemma no_jobs_between_consecutive_jobs :
job_index arr_seq j > 0 ->
task_arrivals_between arr_seq (job_task j)
(job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
0 < job_index arr_seq j ->
task_arrivals_between arr_seq (job_task j)
(job_arrival (prev_job arr_seq j)).+1
(job_arrival j) = [::]
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
0 < job_index arr_seq j ->
task_arrivals_between arr_seq (job_task j)
(job_arrival (prev_job arr_seq j)).+1
(job_arrival j) = [::]
move => POS_IND.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq j
task_arrivals_between arr_seq (job_task j)
(job_arrival (prev_job arr_seq j)).+1
(job_arrival j) = [::]
move : (prev_job_arr_lte); rewrite leq_eqVlt; move => /orP [/eqP EQ | LT].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jEQ : job_arrival (prev_job arr_seq j) = job_arrival j
task_arrivals_between arr_seq (job_task j)
(job_arrival (prev_job arr_seq j)).+1
(job_arrival j) = [::]
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jEQ : job_arrival (prev_job arr_seq j) = job_arrival j
task_arrivals_between arr_seq (job_task j)
(job_arrival (prev_job arr_seq j)).+1
(job_arrival j) = [::]
rewrite EQ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jEQ : job_arrival (prev_job arr_seq j) = job_arrival j
task_arrivals_between arr_seq (job_task j)
(job_arrival j).+1 (job_arrival j) = [::]
apply /eqP/negPn/negP; rewrite -has_filter => /hasP [j' IN /eqP TASK].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jEQ : job_arrival (prev_job arr_seq j) = job_arrival j j' : Job IN : j'
\in arrivals_between arr_seq
(job_arrival j).+1
(job_arrival j) TASK : job_task j' = job_task j
False
apply mem_bigcat_nat_exists in IN; move : IN => [i [J'_IN ARR_INEQ]].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jEQ : job_arrival (prev_job arr_seq j) = job_arrival j j' : Job TASK : job_task j' = job_task j i : nat J'_IN : j' \in arrivals_at arr_seq i ARR_INEQ : job_arrival j < i < job_arrival j
False
by lia .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jLT : job_arrival (prev_job arr_seq j) < job_arrival j
task_arrivals_between arr_seq (job_task j)
(job_arrival (prev_job arr_seq j)).+1
(job_arrival j) = [::]
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jLT : job_arrival (prev_job arr_seq j) < job_arrival j
task_arrivals_between arr_seq (job_task j)
(job_arrival (prev_job arr_seq j)).+1
(job_arrival j) = [::]
apply /eqP/negPn/negP; rewrite -has_filter => /hasP [j3 IN /eqP TASK].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jLT : job_arrival (prev_job arr_seq j) < job_arrival j j3 : Job IN : j3
\in arrivals_between arr_seq
(job_arrival (prev_job arr_seq j)).+1
(job_arrival j) TASK : job_task j3 = job_task j
False
apply mem_bigcat_nat_exists in IN; move : IN => [i [J3_IN ARR_INEQ]].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jLT : job_arrival (prev_job arr_seq j) < job_arrival j j3 : Job TASK : job_task j3 = job_task j i : nat J3_IN : j3 \in arrivals_at arr_seq i ARR_INEQ : job_arrival (prev_job arr_seq j) < i <
job_arrival j
False
have J3_ARR : (arrives_in arr_seq j3) by apply in_arrseq_implies_arrives with (t := i).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jLT : job_arrival (prev_job arr_seq j) < job_arrival j j3 : Job TASK : job_task j3 = job_task j i : nat J3_IN : j3 \in arrivals_at arr_seq i ARR_INEQ : job_arrival (prev_job arr_seq j) < i <
job_arrival j J3_ARR : arrives_in arr_seq j3
False
apply job_arrival_at in J3_IN; rt_eauto; rewrite -J3_IN in ARR_INEQ.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jLT : job_arrival (prev_job arr_seq j) < job_arrival j j3 : Job TASK : job_task j3 = job_task j i : nat J3_IN : job_arrival j3 = i J3_ARR : arrives_in arr_seq j3 ARR_INEQ : job_arrival (prev_job arr_seq j) <
job_arrival j3 < job_arrival j
False
move : ARR_INEQ => /andP [PJ_L_J3 J3_L_J].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jLT : job_arrival (prev_job arr_seq j) < job_arrival j j3 : Job TASK : job_task j3 = job_task j i : nat J3_IN : job_arrival j3 = i J3_ARR : arrives_in arr_seq j3 PJ_L_J3 : job_arrival (prev_job arr_seq j) <
job_arrival j3 J3_L_J : job_arrival j3 < job_arrival j
False
apply (earlier_arrival_implies_lower_index arr_seq H_valid_arrival_sequence _ _) in PJ_L_J3 => //; try by
rewrite prev_job_task.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jLT : job_arrival (prev_job arr_seq j) < job_arrival j j3 : Job TASK : job_task j3 = job_task j i : nat J3_IN : job_arrival j3 = i J3_ARR : arrives_in arr_seq j3 PJ_L_J3 : job_index arr_seq (prev_job arr_seq j) <
job_index arr_seq j3 J3_L_J : job_arrival j3 < job_arrival j
False
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jLT : job_arrival (prev_job arr_seq j) < job_arrival j j3 : Job TASK : job_task j3 = job_task j i : nat J3_IN : job_arrival j3 = i J3_ARR : arrives_in arr_seq j3 PJ_L_J3 : job_index arr_seq (prev_job arr_seq j) <
job_index arr_seq j3 J3_L_J : job_arrival j3 < job_arrival j
False
apply (earlier_arrival_implies_lower_index arr_seq H_valid_arrival_sequence _ _) in J3_L_J => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jLT : job_arrival (prev_job arr_seq j) < job_arrival j j3 : Job TASK : job_task j3 = job_task j i : nat J3_IN : job_arrival j3 = i J3_ARR : arrives_in arr_seq j3 PJ_L_J3 : job_index arr_seq (prev_job arr_seq j) <
job_index arr_seq j3 J3_L_J : job_index arr_seq j3 < job_index arr_seq j
False
by rewrite prev_job_index_j in PJ_L_J3; try by lia .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jLT : job_arrival (prev_job arr_seq j) < job_arrival j j3 : Job TASK : job_task j3 = job_task j i : nat J3_IN : job_arrival j3 = i J3_ARR : arrives_in arr_seq j3 PJ_L_J3 : job_arrival (prev_job arr_seq j) <
job_arrival j3 J3_L_J : job_arrival j3 < job_arrival j
arrives_in arr_seq (prev_job arr_seq j)
+ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index, POS_IND : 0 < job_index arr_seq jLT : job_arrival (prev_job arr_seq j) < job_arrival j j3 : Job TASK : job_task j3 = job_task j i : nat J3_IN : job_arrival j3 = i J3_ARR : arrives_in arr_seq j3 PJ_L_J3 : job_arrival (prev_job arr_seq j) <
job_arrival j3 J3_L_J : job_arrival j3 < job_arrival j
arrives_in arr_seq (prev_job arr_seq j)
by apply prev_job_arr.
Qed .
(** We show that there always exists a job of lesser [job_index] than a
job with a positive [job_index] that arrives in the arrival sequence. *)
Lemma exists_jobs_before_j :
forall k ,
k < job_index arr_seq j ->
exists j' ,
j <> j' /\
job_task j' = job_task j /\
arrives_in arr_seq j' /\
job_index arr_seq j' = k.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
forall k : nat,
k < job_index arr_seq j ->
exists j' : Job,
j <> j' /\
job_task j' = job_task j /\
arrives_in arr_seq j' /\ job_index arr_seq j' = k
Proof .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j H_positive_job_index : 0 < job_index arr_seq j
forall k : nat,
k < job_index arr_seq j ->
exists j' : Job,
j <> j' /\
job_task j' = job_task j /\
arrives_in arr_seq j' /\ job_index arr_seq j' = k
clear H_positive_job_index.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j
forall k : nat,
k < job_index arr_seq j ->
exists j' : Job,
j <> j' /\
job_task j' = job_task j /\
arrives_in arr_seq j' /\ job_index arr_seq j' = k
intros k K_LT.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j
exists j' : Job,
j <> j' /\
job_task j' = job_task j /\
arrives_in arr_seq j' /\ job_index arr_seq j' = k
exists (nth j (task_arrivals_up_to_job_arrival arr_seq j) k).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j
j <>
nth j (task_arrivals_up_to_job_arrival arr_seq j) k /\
job_task
(nth j (task_arrivals_up_to_job_arrival arr_seq j) k) =
job_task j /\
arrives_in arr_seq
(nth j (task_arrivals_up_to_job_arrival arr_seq j) k) /\
job_index arr_seq
(nth j (task_arrivals_up_to_job_arrival arr_seq j) k) =
k
set (jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job
j <> jk /\
job_task jk = job_task j /\
arrives_in arr_seq jk /\ job_index arr_seq jk = k
have K_LT_SIZE : (k < size (task_arrivals_up_to_job_arrival arr_seq j)) by
apply leq_trans with (n := job_index arr_seq j) => //; first by apply index_size.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j)
j <> jk /\
job_task jk = job_task j /\
arrives_in arr_seq jk /\ job_index arr_seq jk = k
have JK_IN : (jk \in task_arrivals_up_to_job_arrival arr_seq j) by rewrite /jk; apply mem_nth => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) JK_IN : jk
\in task_arrivals_up_to_job_arrival arr_seq
j
j <> jk /\
job_task jk = job_task j /\
arrives_in arr_seq jk /\ job_index arr_seq jk = k
rewrite mem_filter in JK_IN; move : JK_IN => /andP [/eqP TSK JK_IN].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j JK_IN : jk
\in arrivals_between arr_seq 0
(job_arrival j).+1
j <> jk /\
job_task jk = job_task j /\
arrives_in arr_seq jk /\ job_index arr_seq jk = k
apply mem_bigcat_nat_exists in JK_IN; move : JK_IN => [i [JK_IN I_INEQ]].Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1
j <> jk /\
job_task jk = job_task j /\
arrives_in arr_seq jk /\ job_index arr_seq jk = k
have JK_ARR : (arrives_in arr_seq jk) by apply in_arrseq_implies_arrives with (t := i) => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk
j <> jk /\
job_task jk = job_task j /\
arrives_in arr_seq jk /\ job_index arr_seq jk = k
have INDJK : (index jk (task_arrivals_up_to_job_arrival arr_seq j) = k).Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk
index jk (task_arrivals_up_to_job_arrival arr_seq j) =
k
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk
index jk (task_arrivals_up_to_job_arrival arr_seq j) =
k
apply index_uniq => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk
uniq (task_arrivals_up_to_job_arrival arr_seq j)
by apply uniq_task_arrivals => //; rt_eauto. } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk INDJK : index jk
(task_arrivals_up_to_job_arrival arr_seq j) =
k
j <> jk /\
job_task jk = job_task j /\
arrives_in arr_seq jk /\ job_index arr_seq jk = k
repeat split => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk INDJK : index jk
(task_arrivals_up_to_job_arrival arr_seq j) =
k
j <> jk
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk INDJK : index jk
(task_arrivals_up_to_job_arrival arr_seq j) =
k
j <> jk
rewrite -> diff_jobs_iff_diff_indices => //; eauto .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk INDJK : index jk
(task_arrivals_up_to_job_arrival arr_seq j) =
k
job_index arr_seq j <> job_index arr_seq jk
rewrite /job_index; rewrite [in X in _ <> X] (job_index_same_in_task_arrivals _ _ jk j) => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk INDJK : index jk
(task_arrivals_up_to_job_arrival arr_seq j) =
k
index j (task_arrivals_up_to_job_arrival arr_seq j) <>
index jk (task_arrivals_up_to_job_arrival arr_seq j)
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk INDJK : index jk
(task_arrivals_up_to_job_arrival arr_seq j) =
k
index j (task_arrivals_up_to_job_arrival arr_seq j) <>
index jk (task_arrivals_up_to_job_arrival arr_seq j)
rewrite index_uniq -/(job_index arr_seq j)=> //; last by apply uniq_task_arrivals; rt_eauto.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk INDJK : index jk
(task_arrivals_up_to_job_arrival arr_seq j) =
k
job_index arr_seq j <> k
by lia .Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk INDJK : index jk
(task_arrivals_up_to_job_arrival arr_seq j) =
k
job_arrival jk <= job_arrival j
- Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk INDJK : index jk
(task_arrivals_up_to_job_arrival arr_seq j) =
k
job_arrival jk <= job_arrival j
by apply job_arrival_at in JK_IN; rt_eauto; rewrite -JK_IN in I_INEQ. } Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk INDJK : index jk
(task_arrivals_up_to_job_arrival arr_seq j) =
k
job_index arr_seq jk = k
{ Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk INDJK : index jk
(task_arrivals_up_to_job_arrival arr_seq j) =
k
job_index arr_seq jk = k
rewrite /job_index; rewrite [in X in X = _] (job_index_same_in_task_arrivals _ _ jk j) => //.Task : TaskType Job : JobType H : JobTask Job Task H0 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq j : Job H_arrives_in_arr_seq : arrives_in arr_seq j k : nat K_LT : k < job_index arr_seq j jk := nth j (task_arrivals_up_to_job_arrival arr_seq j)
k : Job K_LT_SIZE : k <
size
(task_arrivals_up_to_job_arrival arr_seq
j) TSK : job_task jk = job_task j i : nat JK_IN : jk \in arrivals_at arr_seq i I_INEQ : 0 <= i < (job_arrival j).+1 JK_ARR : arrives_in arr_seq jk INDJK : index jk
(task_arrivals_up_to_job_arrival arr_seq j) =
k
job_arrival jk <= job_arrival j
by apply job_arrival_at in JK_IN; rt_eauto; rewrite -JK_IN in I_INEQ. }
Qed .
End PreviousJob .