Library rt.restructuring.behavior.facts.arrivals

(* In this section, we relate job readiness to [has_arrived]. *)
Section Arrived.
  (* Consider any kinds of jobs and any kind of processor state. *)
  Context {Job : JobType} {PState : Type}.
  Context `{ProcessorState Job PState}.

  (* Consider any schedule... *)
  Variable sched : schedule PState.

  (* ...and suppose that jobs have a cost, an arrival time, and a notion of
     readiness. *)
  Context `{JobCost Job}.
  Context `{JobArrival Job}.
  Context `{JobReady Job PState}.

  (* We observe that a given job must have arrived to be ready... *)
  Lemma ready_implies_arrived:
    ∀ j t, job_ready sched j t → has_arrived j t.

  (* ...and lift this observation also to the level of whole schedules. *)
  Lemma jobs_must_arrive_to_be_ready:
    jobs_must_be_ready_to_execute sched →
    jobs_must_arrive_to_execute sched.

End Arrived.

(* 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.