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.

  (* By concatenation, we construct the list of jobs that arrived in the
     interval [t1, t2). *)
  Definition jobs_arrived_between (t1 t2 : instant) :=
    \cat_(t1 ≤ t < t2) jobs_arriving_at arr_seq t.

  (* Based on that, we define the list of jobs that arrived up to time t, ...*)
  Definition jobs_arrived_up_to (t : instant) := jobs_arrived_between 0 t.+1.

  (* ...and the list of jobs that arrived strictly before time t. *)
  Definition jobs_arrived_before (t : instant) := jobs_arrived_between 0 t.

  (* 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 job_arrived_between_cat:
        ∀ t1 t t2,
          t1 ≤ t →
          t ≤ t2 →
          jobs_arrived_between t1 t2 = jobs_arrived_between t1 t ++ jobs_arrived_between t t2.

      (* Second, the same observation applies to membership in the set of
         arrived jobs. *)
      Lemma jobs_arrived_between_mem_cat:
        ∀ j t1 t t2,
          t1 ≤ t →
          t ≤ t2 →
          j \in jobs_arrived_between t1 t2 =
                (j \in jobs_arrived_between t1 t ++ jobs_arrived_between 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 jobs_arrived_between_sub:
        ∀ j t1 t1' t2 t2',
          t1' ≤ t1 →
          t2 ≤ t2' →
          j \in jobs_arrived_between t1 t2 →
                j \in jobs_arrived_between 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 jobs_arrived_between 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 jobs_arrived_between 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 jobs_arrived_before 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 jobs_arrived_between 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 (jobs_arrived_between t1 t2).

    End ArrivalTimes.

  End Lemmas.

End ArrivalSequencePrefix.