Library prosa.analysis.facts.job_index
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.model.task_arrivals.
In this section, we prove some properties related to [job_index].
Consider any type of tasks ...
... and any jobs associated with the tasks.
Consider any arrival sequence with consistent and non-duplicate arrivals, ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq : arrival_sequence_uniq arr_seq.
Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq : arrival_sequence_uniq 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.
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.
Assume that the jobs [j1] and [j2] have the same [job_index]
in the arrival sequence.
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
move ⇒ ARR_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
apply task_arrivals_up_to_prefix_cat with (arr_seq0 := arr_seq) in ARR_LT ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 69)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 Job (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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 108)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
apply eq_ind_in_seq with (xs := task_arrivals_up_to_job_arrival arr_seq j2) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 114)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
subgoal 2 (ID 115) is:
uniq (task_arrivals_up_to_job_arrival arr_seq j2)
subgoal 3 (ID 116) is:
j1 \in task_arrivals_up_to_job_arrival arr_seq j2
subgoal 4 (ID 117) is:
j2 \in task_arrivals_up_to_job_arrival arr_seq j2
----------------------------------------------------------------------------- *)
- now rewrite -/(job_index _ _) -IND -ARR_CAT index_cat ifT;
try apply arrives_in_task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 115)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
============================
uniq (task_arrivals_up_to_job_arrival arr_seq j2)
subgoal 2 (ID 116) is:
j1 \in task_arrivals_up_to_job_arrival arr_seq j2
subgoal 3 (ID 117) is:
j2 \in task_arrivals_up_to_job_arrival arr_seq j2
----------------------------------------------------------------------------- *)
- now apply uniq_task_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 116)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 117) is:
j2 \in task_arrivals_up_to_job_arrival arr_seq j2
----------------------------------------------------------------------------- *)
- rewrite -ARR_CAT mem_cat; apply /orP.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 288)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 117) is:
j2 \in task_arrivals_up_to_job_arrival arr_seq j2
----------------------------------------------------------------------------- *)
now left; apply arrives_in_task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 117)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
- now apply arrives_in_task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_arrival j1 ≤ job_arrival j2 → j1 = j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
move ⇒ ARR_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
apply task_arrivals_up_to_prefix_cat with (arr_seq0 := arr_seq) in ARR_LT ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 69)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 Job (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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 108)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
apply eq_ind_in_seq with (xs := task_arrivals_up_to_job_arrival arr_seq j2) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 114)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
subgoal 2 (ID 115) is:
uniq (task_arrivals_up_to_job_arrival arr_seq j2)
subgoal 3 (ID 116) is:
j1 \in task_arrivals_up_to_job_arrival arr_seq j2
subgoal 4 (ID 117) is:
j2 \in task_arrivals_up_to_job_arrival arr_seq j2
----------------------------------------------------------------------------- *)
- now rewrite -/(job_index _ _) -IND -ARR_CAT index_cat ifT;
try apply arrives_in_task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 115)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
============================
uniq (task_arrivals_up_to_job_arrival arr_seq j2)
subgoal 2 (ID 116) is:
j1 \in task_arrivals_up_to_job_arrival arr_seq j2
subgoal 3 (ID 117) is:
j2 \in task_arrivals_up_to_job_arrival arr_seq j2
----------------------------------------------------------------------------- *)
- now apply uniq_task_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 116)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 117) is:
j2 \in task_arrivals_up_to_job_arrival arr_seq j2
----------------------------------------------------------------------------- *)
- rewrite -ARR_CAT mem_cat; apply /orP.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 288)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 117) is:
j2 \in task_arrivals_up_to_job_arrival arr_seq j2
----------------------------------------------------------------------------- *)
now left; apply arrives_in_task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 117)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
- now apply arrives_in_task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 68)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
move⇒ LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 69)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 71)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 78)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 Job (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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 136)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 147)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
subgoal 2 (ID 148) is:
uniq (task_arrivals_up_to_job_arrival arr_seq j1)
subgoal 3 (ID 149) is:
j1 \in task_arrivals_up_to_job_arrival arr_seq j1
subgoal 4 (ID 150) is:
j2 \in task_arrivals_up_to_job_arrival arr_seq j1
----------------------------------------------------------------------------- *)
- now rewrite -/(job_index _ _) IND -ARR_CAT index_cat ifT;
try apply arrives_in_task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 148)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
============================
uniq (task_arrivals_up_to_job_arrival arr_seq j1)
subgoal 2 (ID 149) is:
j1 \in task_arrivals_up_to_job_arrival arr_seq j1
subgoal 3 (ID 150) is:
j2 \in task_arrivals_up_to_job_arrival arr_seq j1
----------------------------------------------------------------------------- *)
- now apply uniq_task_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 149)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 150) is:
j2 \in task_arrivals_up_to_job_arrival arr_seq j1
----------------------------------------------------------------------------- *)
- now apply arrives_in_task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 150)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 327)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now left; apply arrives_in_task_arrivals_up_to ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_arrival j1 > job_arrival j2 → j1 = j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 68)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
move⇒ LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 69)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 71)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 78)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 Job (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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 136)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 147)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
subgoal 2 (ID 148) is:
uniq (task_arrivals_up_to_job_arrival arr_seq j1)
subgoal 3 (ID 149) is:
j1 \in task_arrivals_up_to_job_arrival arr_seq j1
subgoal 4 (ID 150) is:
j2 \in task_arrivals_up_to_job_arrival arr_seq j1
----------------------------------------------------------------------------- *)
- now rewrite -/(job_index _ _) IND -ARR_CAT index_cat ifT;
try apply arrives_in_task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 148)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
============================
uniq (task_arrivals_up_to_job_arrival arr_seq j1)
subgoal 2 (ID 149) is:
j1 \in task_arrivals_up_to_job_arrival arr_seq j1
subgoal 3 (ID 150) is:
j2 \in task_arrivals_up_to_job_arrival arr_seq j1
----------------------------------------------------------------------------- *)
- now apply uniq_task_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 149)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 150) is:
j2 \in task_arrivals_up_to_job_arrival arr_seq j1
----------------------------------------------------------------------------- *)
- now apply arrives_in_task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 150)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 327)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now left; apply arrives_in_task_arrivals_up_to ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 71)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
case: (ltngtP (job_arrival j1) (job_arrival j2)) ⇒ [LT|GT|EQ].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 137)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 138) is:
j1 = j2
subgoal 3 (ID 139) is:
j1 = j2
----------------------------------------------------------------------------- *)
- now apply case_arrival_lte_implies_equal_job; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 138)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 139) is:
j1 = j2
----------------------------------------------------------------------------- *)
- now apply case_arrival_gt_implies_equal_job; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 139)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
- now apply case_arrival_lte_implies_equal_job; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End EqualJobIndex.
j1 = j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 71)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
case: (ltngtP (job_arrival j1) (job_arrival j2)) ⇒ [LT|GT|EQ].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 137)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 138) is:
j1 = j2
subgoal 3 (ID 139) is:
j1 = j2
----------------------------------------------------------------------------- *)
- now apply case_arrival_lte_implies_equal_job; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 138)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 139) is:
j1 = j2
----------------------------------------------------------------------------- *)
- now apply case_arrival_gt_implies_equal_job; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 139)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
- now apply case_arrival_lte_implies_equal_job; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 57)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 59)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 60) is:
job_index arr_seq j1 <> job_index arr_seq j2 -> j1 <> j2
----------------------------------------------------------------------------- *)
+ move ⇒ NEQJ EQ.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 63)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 60) is:
job_index arr_seq j1 <> job_index arr_seq j2 -> j1 <> j2
----------------------------------------------------------------------------- *)
now apply equal_index_implies_equal_jobs in EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 60)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 68)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now move: EQ NEQ ⇒ →.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
j1 ≠ j2 ↔
job_index arr_seq j1 ≠ job_index arr_seq j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 57)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 59)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 60) is:
job_index arr_seq j1 <> job_index arr_seq j2 -> j1 <> j2
----------------------------------------------------------------------------- *)
+ move ⇒ NEQJ EQ.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 63)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 60) is:
job_index arr_seq j1 <> job_index arr_seq j2 -> j1 <> j2
----------------------------------------------------------------------------- *)
now apply equal_index_implies_equal_jobs in EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 60)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 68)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now move: EQ NEQ ⇒ →.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 74)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
rewrite /task_arrivals_at_job_arrival /job_index task_arrivals_up_to_cat //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 105)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 142)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 146)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 226)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 251)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
erewrite H_consistent_arrivals in IND_INTR; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 423)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 < ind
============================
False
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_index arr_seq j1 =
size (task_arrivals_before_job_arrival arr_seq j1)
+ index j1 (task_arrivals_at_job_arrival arr_seq j1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 74)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
rewrite /task_arrivals_at_job_arrival /job_index task_arrivals_up_to_cat //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 105)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 142)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 146)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 226)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 251)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
erewrite H_consistent_arrivals in IND_INTR; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 423)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 < ind
============================
False
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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:
∀ (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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 96)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
intros × J1_IN J2_IN ARR_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 102)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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] ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 175)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 230)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 277)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 278)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 H_consistent_arrivals in J2_IN; rewrite J2_IN in ARR_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 333)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
PJ2 : P j2
i : nat
J2_IN : job_arrival j2 = i
INEQ : t1 <= i < t2
ARR_LT : i < job_arrival j1
============================
t1 <= i < job_arrival j1
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ (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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 96)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
intros × J1_IN J2_IN ARR_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 102)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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] ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 175)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 230)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 277)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 278)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 H_consistent_arrivals in J2_IN; rewrite J2_IN in ARR_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 333)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
PJ2 : P j2
i : nat
J2_IN : job_arrival j2 = i
INEQ : t1 <= i < t2
ARR_LT : i < job_arrival j1
============================
t1 <= i < job_arrival j1
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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:
∀ (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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 115)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
intros × IN1 IN2 LE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 121)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 192)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 in IN1 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 196)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 231)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 250)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
subgoal 2 (ID 251) is:
(j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false
----------------------------------------------------------------------------- *)
- eapply ltn_leq_trans; [ | now erewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 253)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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))
subgoal 2 (ID 251) is:
(j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false
----------------------------------------------------------------------------- *)
rewrite index_mem.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 466)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
subgoal 2 (ID 251) is:
(j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false
----------------------------------------------------------------------------- *)
now eapply arrival_lt_implies_job_in_arrivals_between_P; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 251)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 480)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now apply job_arrival_between in T; try ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ (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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 115)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
intros × IN1 IN2 LE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 121)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 192)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 in IN1 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 196)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 231)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 250)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
subgoal 2 (ID 251) is:
(j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false
----------------------------------------------------------------------------- *)
- eapply ltn_leq_trans; [ | now erewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 253)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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))
subgoal 2 (ID 251) is:
(j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false
----------------------------------------------------------------------------- *)
rewrite index_mem.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 466)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
subgoal 2 (ID 251) is:
(j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false
----------------------------------------------------------------------------- *)
now eapply arrival_lt_implies_job_in_arrivals_between_P; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 251)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 480)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now apply job_arrival_between in T; try ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 132)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
rewrite leq_eqVlt ⇒ /orP [/eqP LT|LT]; first by rewrite /task_arrivals_up_to_job_arrival LT H_same_task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 212)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
----------------------------------------------------------------------------- *)
specialize (arrival_lt_implies_strict_prefix _ H_consistent_arrivals (job_task j1) j1 j2) ⇒ SUB.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 237)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
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 Job (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]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 331)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
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)
----------------------------------------------------------------------------- *)
now rewrite -CAT2 index_cat ifT; last by apply arrives_in_task_arrivals_up_to ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 132)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
rewrite leq_eqVlt ⇒ /orP [/eqP LT|LT]; first by rewrite /task_arrivals_up_to_job_arrival LT H_same_task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 212)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
----------------------------------------------------------------------------- *)
specialize (arrival_lt_implies_strict_prefix _ H_consistent_arrivals (job_task j1) j1 j2) ⇒ SUB.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 237)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
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 Job (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]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 331)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
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)
----------------------------------------------------------------------------- *)
now rewrite -CAT2 index_cat ifT; last by apply arrives_in_task_arrivals_up_to ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 142)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
rewrite /job_index index_mem.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 156)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now apply arrives_in_task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_index arr_seq j1 < size (task_arrivals_up_to_job_arrival arr_seq j1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 142)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
rewrite /job_index index_mem.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 156)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now apply arrives_in_task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 155)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
intros IND_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 156)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 185)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 256)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 269)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 552)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 856)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 874)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
subgoal 2 (ID 875) is:
(j2 \in task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) = false
----------------------------------------------------------------------------- *)
- now eapply ltn_leq_trans;
[apply index_job_lt_size_task_arrivals_up_to_job | rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 875)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 885)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now apply job_arrival_between in T; try ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_index arr_seq j2 ≤ job_index arr_seq j1 →
job_arrival j2 ≤ job_arrival j1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 155)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
intros IND_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 156)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 185)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 256)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 269)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 552)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 856)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 874)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
subgoal 2 (ID 875) is:
(j2 \in task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) = false
----------------------------------------------------------------------------- *)
- now eapply ltn_leq_trans;
[apply index_job_lt_size_task_arrivals_up_to_job | rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 875)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 885)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now apply job_arrival_between in T; try ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 168)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
intros ARR_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 169)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 234)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now apply index_lte_implies_arrival_lte.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_arrival j1 < job_arrival j2 →
job_index arr_seq j1 < job_index arr_seq j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 168)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
intros ARR_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 169)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 234)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now apply index_lte_implies_arrival_lte.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 178)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
apply leq_ltn_trans with (n := job_index arr_seq j1); try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 184)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
----------------------------------------------------------------------------- *)
now apply index_job_lt_size_task_arrivals_up_to_job.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_index arr_seq j1 - 1 < size (task_arrivals_up_to_job_arrival arr_seq j1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 178)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
apply leq_ltn_trans with (n := job_index arr_seq j1); try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 184)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
----------------------------------------------------------------------------- *)
now apply index_job_lt_size_task_arrivals_up_to_job.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 184)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
rewrite lt0n; apply /eqP; intro Z.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 227)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 228)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 246)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now rewrite Z in J_IN.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End JobIndexLemmas.
size (task_arrivals_up_to_job_arrival arr_seq j1) > 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 184)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
rewrite lt0n; apply /eqP; intro Z.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 227)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 228)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 246)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now rewrite Z in J_IN.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End JobIndexLemmas.
In this section, we prove a few basic properties of
function [prev_job].
Consider any type of tasks ...
... and any jobs associated with the tasks.
Consider any unique arrival sequence with consistent arrivals ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq : arrival_sequence_uniq arr_seq.
Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq : arrival_sequence_uniq 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.
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
destruct (default_or_in _ (job_index arr_seq j - 1) j (task_arrivals_up_to_job_arrival arr_seq j)) as [EQ|IN].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 62)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
EQ : 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)
subgoal 2 (ID 63) is:
arrives_in arr_seq (prev_job arr_seq j)
----------------------------------------------------------------------------- *)
+ now rewrite /prev_job EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 63)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
IN : 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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 78)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
IN : 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
----------------------------------------------------------------------------- *)
now move: IN; rewrite mem_filter ⇒ /andP [_ IN].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
arrives_in arr_seq (prev_job arr_seq j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
destruct (default_or_in _ (job_index arr_seq j - 1) j (task_arrivals_up_to_job_arrival arr_seq j)) as [EQ|IN].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 62)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
EQ : 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)
subgoal 2 (ID 63) is:
arrives_in arr_seq (prev_job arr_seq j)
----------------------------------------------------------------------------- *)
+ now rewrite /prev_job EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 63)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
IN : 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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 78)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
IN : 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
----------------------------------------------------------------------------- *)
now move: IN; rewrite mem_filter ⇒ /andP [_ IN].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
apply index_uniq; last by apply uniq_task_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
----------------------------------------------------------------------------- *)
now apply index_job_lt_size_task_arrivals_up_to_job.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
index (prev_job arr_seq j) (task_arrivals_up_to_job_arrival arr_seq j) = job_index arr_seq j - 1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
apply index_uniq; last by apply uniq_task_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
----------------------------------------------------------------------------- *)
now apply index_job_lt_size_task_arrivals_up_to_job.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 74)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
specialize (job_index_minus_one_lt_size_task_arrivals_up_to arr_seq H_consistent_arrivals j H_arrives_in_arr_seq) ⇒ SIZEL.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 81)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
SIZEL : 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 112)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
SIZEL : (job_task (prev_job arr_seq j) == job_task 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
----------------------------------------------------------------------------- *)
now move : SIZEL ⇒ /andP [/eqP TSK PREV_IN].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_task (prev_job arr_seq j) = job_task j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 74)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
specialize (job_index_minus_one_lt_size_task_arrivals_up_to arr_seq H_consistent_arrivals j H_arrives_in_arr_seq) ⇒ SIZEL.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 81)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
SIZEL : 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 112)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
SIZEL : (job_task (prev_job arr_seq j) == job_task 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
----------------------------------------------------------------------------- *)
now move : SIZEL ⇒ /andP [/eqP TSK PREV_IN].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 87)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
rewrite /prev_job -index_mem index_uniq;
try by apply job_index_minus_one_lt_size_task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 111)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
----------------------------------------------------------------------------- *)
now apply uniq_task_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
prev_job arr_seq j \in task_arrivals_up_to_job_arrival arr_seq j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 87)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
rewrite /prev_job -index_mem index_uniq;
try by apply job_index_minus_one_lt_size_task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 111)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
----------------------------------------------------------------------------- *)
now apply uniq_task_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 96)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
move : (prev_job_in_task_arrivals_up_to_j) ⇒ PREV_JOB_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 98)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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_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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 164)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
TSK : job_task (prev_job arr_seq j) == job_task 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]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 189)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
TSK : job_task (prev_job arr_seq j) == job_task 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
----------------------------------------------------------------------------- *)
apply H_consistent_arrivals in PREV_IN; rewrite -PREV_IN in INEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 214)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
TSK : job_task (prev_job arr_seq j) == job_task j
i : nat
PREV_IN : job_arrival (prev_job arr_seq j) = i
INEQ : 0 <= job_arrival (prev_job arr_seq j) < (job_arrival j).+1
============================
job_arrival (prev_job arr_seq j) <= job_arrival j
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_arrival (prev_job arr_seq j) ≤ job_arrival j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 96)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
move : (prev_job_in_task_arrivals_up_to_j) ⇒ PREV_JOB_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 98)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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_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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 164)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
TSK : job_task (prev_job arr_seq j) == job_task 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]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 189)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
TSK : job_task (prev_job arr_seq j) == job_task 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
----------------------------------------------------------------------------- *)
apply H_consistent_arrivals in PREV_IN; rewrite -PREV_IN in INEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 214)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index arr_seq j
TSK : job_task (prev_job arr_seq j) == job_task j
i : nat
PREV_IN : job_arrival (prev_job arr_seq j) = i
INEQ : 0 <= job_arrival (prev_job arr_seq j) < (job_arrival j).+1
============================
job_arrival (prev_job arr_seq j) <= job_arrival j
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 115)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
intros NZ_IND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 116)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 118)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 124)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
subgoal 2 (ID 126) is:
job_task (prev_job arr_seq j) = job_task j
subgoal 3 (ID 127) is:
job_arrival (prev_job arr_seq j) <= job_arrival j
----------------------------------------------------------------------------- *)
- now apply prev_job_arr.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 126)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 127) is:
job_arrival (prev_job arr_seq j) <= job_arrival j
----------------------------------------------------------------------------- *)
- now apply prev_job_task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 127)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
- now apply prev_job_arr_lte.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_index arr_seq j > 0 →
job_index arr_seq (prev_job arr_seq j) = job_index arr_seq j - 1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 115)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
intros NZ_IND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 116)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 118)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 124)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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)
subgoal 2 (ID 126) is:
job_task (prev_job arr_seq j) = job_task j
subgoal 3 (ID 127) is:
job_arrival (prev_job arr_seq j) <= job_arrival j
----------------------------------------------------------------------------- *)
- now apply prev_job_arr.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 126)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 127) is:
job_arrival (prev_job arr_seq j) <= job_arrival j
----------------------------------------------------------------------------- *)
- now apply prev_job_task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 127)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
- now apply prev_job_arr_lte.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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) = [::].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 137)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
move ⇒ POS_IND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 138)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 218)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
EQ : 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) = [::]
subgoal 2 (ID 219) is:
task_arrivals_between arr_seq (job_task j)
(job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
----------------------------------------------------------------------------- *)
- rewrite EQ.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 221)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
EQ : 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) = [::]
subgoal 2 (ID 219) is:
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 [j' IN /eqP TASK].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 423)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
EQ : 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
subgoal 2 (ID 219) is:
task_arrivals_between arr_seq (job_task j)
(job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
----------------------------------------------------------------------------- *)
apply mem_bigcat_nat_exists in IN; move : IN ⇒ [i [J'_IN ARR_INEQ]].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 448)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
EQ : 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
subgoal 2 (ID 219) is:
task_arrivals_between arr_seq (job_task j)
(job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 219)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 919)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 944)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 950)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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 H_consistent_arrivals in J3_IN; rewrite -J3_IN in ARR_INEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 979)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1021)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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_consistent_arrivals _ _) in PJ_L_J3 ⇒ //; try by
rewrite prev_job_task.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1030)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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
subgoal 2 (ID 1032) is:
arrives_in arr_seq (prev_job arr_seq j)
----------------------------------------------------------------------------- *)
+ apply (earlier_arrival_implies_lower_index arr_seq H_consistent_arrivals _ _) in J3_L_J ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1139)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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
subgoal 2 (ID 1032) is:
arrives_in arr_seq (prev_job arr_seq j)
----------------------------------------------------------------------------- *)
now rewrite prev_job_index_j in PJ_L_J3; try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1032)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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)
----------------------------------------------------------------------------- *)
+ now apply prev_job_arr.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
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) = [::].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 137)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
move ⇒ POS_IND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 138)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 218)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
EQ : 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) = [::]
subgoal 2 (ID 219) is:
task_arrivals_between arr_seq (job_task j)
(job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
----------------------------------------------------------------------------- *)
- rewrite EQ.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 221)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
EQ : 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) = [::]
subgoal 2 (ID 219) is:
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 [j' IN /eqP TASK].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 423)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
EQ : 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
subgoal 2 (ID 219) is:
task_arrivals_between arr_seq (job_task j)
(job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
----------------------------------------------------------------------------- *)
apply mem_bigcat_nat_exists in IN; move : IN ⇒ [i [J'_IN ARR_INEQ]].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 448)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
EQ : 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
subgoal 2 (ID 219) is:
task_arrivals_between arr_seq (job_task j)
(job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 219)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 919)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 944)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 950)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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 H_consistent_arrivals in J3_IN; rewrite -J3_IN in ARR_INEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 979)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1021)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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_consistent_arrivals _ _) in PJ_L_J3 ⇒ //; try by
rewrite prev_job_task.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1030)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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
subgoal 2 (ID 1032) is:
arrives_in arr_seq (prev_job arr_seq j)
----------------------------------------------------------------------------- *)
+ apply (earlier_arrival_implies_lower_index arr_seq H_consistent_arrivals _ _) in J3_L_J ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1139)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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
subgoal 2 (ID 1032) is:
arrives_in arr_seq (prev_job arr_seq j)
----------------------------------------------------------------------------- *)
now rewrite prev_job_index_j in PJ_L_J3; try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1032)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
LT : 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)
----------------------------------------------------------------------------- *)
+ now apply prev_job_arr.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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:
∀ k,
k < job_index arr_seq j →
∃ j',
j ≠ j' ∧
job_task j' = job_task j ∧
arrives_in arr_seq j' ∧
job_index arr_seq j' = k.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 162)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
intros k K_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 164)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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
----------------------------------------------------------------------------- *)
∃ (nth j (task_arrivals_up_to_job_arrival arr_seq j) k).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 171)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 178)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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 ltn_leq_trans with (n := job_index arr_seq j) ⇒ //; first by apply index_size.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 214)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 227)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 329)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 354)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 360)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 368)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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
subgoal 2 (ID 370) is:
j <> jk /\
job_task jk = job_task j /\
arrives_in arr_seq jk /\ job_index arr_seq jk = k
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 368)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 372)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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)
----------------------------------------------------------------------------- *)
now apply uniq_task_arrivals ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 370)
subgoal 1 (ID 370) is:
j <> jk /\
job_task jk = job_task j /\
arrives_in arr_seq jk /\ job_index arr_seq jk = k
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 370)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 402)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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
subgoal 2 (ID 558) is:
job_index arr_seq jk = k
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 402)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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 ⇒ //; last by auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 596)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 739)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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)
subgoal 2 (ID 744) is:
job_arrival jk <= job_arrival j
----------------------------------------------------------------------------- *)
- rewrite index_uniq -/(job_index arr_seq j)=> //; last by apply uniq_task_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 812)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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
subgoal 2 (ID 744) is:
job_arrival jk <= job_arrival j
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 744)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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
----------------------------------------------------------------------------- *)
- apply H_consistent_arrivals in JK_IN; rewrite -JK_IN in I_INEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1227)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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 : job_arrival jk = i
JK_ARR : arrives_in arr_seq jk
INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
I_INEQ : 0 <= job_arrival jk < (job_arrival j).+1
============================
job_arrival jk <= job_arrival j
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 558)
subgoal 1 (ID 558) is:
job_index arr_seq jk = k
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 558)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 558)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1610)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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
----------------------------------------------------------------------------- *)
apply H_consistent_arrivals in JK_IN; rewrite -JK_IN in I_INEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1663)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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 : job_arrival jk = i
JK_ARR : arrives_in arr_seq jk
INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
I_INEQ : 0 <= job_arrival jk < (job_arrival j).+1
============================
job_arrival jk <= job_arrival j
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PreviousJob.
∀ k,
k < job_index arr_seq j →
∃ j',
j ≠ j' ∧
job_task j' = job_task j ∧
arrives_in arr_seq j' ∧
job_index arr_seq j' = k.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 162)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
intros k K_LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 164)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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
----------------------------------------------------------------------------- *)
∃ (nth j (task_arrivals_up_to_job_arrival arr_seq j) k).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 171)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 178)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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 ltn_leq_trans with (n := job_index arr_seq j) ⇒ //; first by apply index_size.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 214)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 227)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 329)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 354)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 360)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 368)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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
subgoal 2 (ID 370) is:
j <> jk /\
job_task jk = job_task j /\
arrives_in arr_seq jk /\ job_index arr_seq jk = k
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 368)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 372)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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)
----------------------------------------------------------------------------- *)
now apply uniq_task_arrivals ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 370)
subgoal 1 (ID 370) is:
j <> jk /\
job_task jk = job_task j /\
arrives_in arr_seq jk /\ job_index arr_seq jk = k
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 370)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 402)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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
subgoal 2 (ID 558) is:
job_index arr_seq jk = k
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 402)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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 ⇒ //; last by auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 596)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 739)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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)
subgoal 2 (ID 744) is:
job_arrival jk <= job_arrival j
----------------------------------------------------------------------------- *)
- rewrite index_uniq -/(job_index arr_seq j)=> //; last by apply uniq_task_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 812)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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
subgoal 2 (ID 744) is:
job_arrival jk <= job_arrival j
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 744)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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
----------------------------------------------------------------------------- *)
- apply H_consistent_arrivals in JK_IN; rewrite -JK_IN in I_INEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1227)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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 : job_arrival jk = i
JK_ARR : arrives_in arr_seq jk
INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
I_INEQ : 0 <= job_arrival jk < (job_arrival j).+1
============================
job_arrival jk <= job_arrival j
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 558)
subgoal 1 (ID 558) is:
job_index arr_seq jk = k
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 558)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 558)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1610)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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
----------------------------------------------------------------------------- *)
apply H_consistent_arrivals in JK_IN; rewrite -JK_IN in I_INEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1663)
Task : TaskType
Job : JobType
H : JobTask Job Task
H0 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
j : Job
H_arrives_in_arr_seq : arrives_in arr_seq j
H_positive_job_index : 0 < job_index 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 : job_arrival jk = i
JK_ARR : arrives_in arr_seq jk
INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
I_INEQ : 0 <= job_arrival jk < (job_arrival j).+1
============================
job_arrival jk <= job_arrival j
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PreviousJob.