Library rt.restructuring.behavior.facts.arrivals
(* In this section, we establish useful facts about arrival sequence prefixes. *)
Section ArrivalSequencePrefix.
(* Assume that job arrival times are known. *)
Context {Job: JobType}.
Context `{JobArrival Job}.
(* Consider any job arrival sequence. *)
Variable arr_seq: arrival_sequence Job.
(* In this section, we prove some lemmas about arrival sequence prefixes. *)
Section Lemmas.
(* We begin with basic lemmas for manipulating the sequences. *)
Section Composition.
(* First, we show that the set of arriving jobs can be split
into disjoint intervals. *)
Lemma arrivals_between_cat:
∀ t1 t t2,
t1 ≤ t →
t ≤ t2 →
arrivals_between arr_seq t1 t2 = arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.
(* Second, the same observation applies to membership in the set of
arrived jobs. *)
Lemma arrivals_between_mem_cat:
∀ j t1 t t2,
t1 ≤ t →
t ≤ t2 →
j \in arrivals_between arr_seq t1 t2 =
(j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).
(* Third, we observe that we can grow the considered interval without
"losing" any arrived jobs, i.e., membership in the set of arrived jobs
is monotonic. *)
Lemma arrivals_between_sub:
∀ j t1 t1' t2 t2',
t1' ≤ t1 →
t2 ≤ t2' →
j \in arrivals_between arr_seq t1 t2 →
j \in arrivals_between arr_seq t1' t2'.
End Composition.
(* Next, we relate the arrival prefixes with job arrival times. *)
Section ArrivalTimes.
(* Assume that job arrival times are consistent. *)
Hypothesis H_consistent_arrival_times:
consistent_arrival_times arr_seq.
(* First, we prove that if a job belongs to the prefix
(jobs_arrived_before t), then it arrives in the arrival sequence. *)
Lemma in_arrivals_implies_arrived:
∀ j t1 t2,
j \in arrivals_between arr_seq t1 t2 →
arrives_in arr_seq j.
(* Next, we prove that if a job belongs to the prefix
(jobs_arrived_between t1 t2), then it indeed arrives between t1 and
t2. *)
Lemma in_arrivals_implies_arrived_between:
∀ j t1 t2,
j \in arrivals_between arr_seq t1 t2 →
arrived_between j t1 t2.
(* Similarly, if a job belongs to the prefix (jobs_arrived_before t),
then it indeed arrives before time t. *)
Lemma in_arrivals_implies_arrived_before:
∀ j t,
j \in arrivals_before arr_seq t →
arrived_before j t.
(* Similarly, we prove that if a job from the arrival sequence arrives
before t, then it belongs to the sequence (jobs_arrived_before t). *)
Lemma arrived_between_implies_in_arrivals:
∀ j t1 t2,
arrives_in arr_seq j →
arrived_between j t1 t2 →
j \in arrivals_between arr_seq t1 t2.
(* Next, we prove that if the arrival sequence doesn't contain duplicate
jobs, the same applies for any of its prefixes. *)
Lemma arrivals_uniq :
arrival_sequence_uniq arr_seq →
∀ t1 t2, uniq (arrivals_between arr_seq t1 t2).
End ArrivalTimes.
End Lemmas.
End ArrivalSequencePrefix.