Library prosa.classic.model.arrival.jitter.arrival_sequence

Require Import prosa.classic.util.all prosa.classic.model.arrival.basic.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.

(* In this file we provide extra definitions for job arrival sequences with jitter. *)
Module ArrivalSequenceWithJitter.

  Export ArrivalSequence.

  (* First, we identify the actual arrival time of a job. *)
  Section ActualArrival.

    Context {Job: eqType}.
    Variable job_arrival: Job time.
    Variable job_jitter: Job time.

    (* Let j be any job. *)
    Variable j: Job.

    (* We define the actual arrival of job j as the time when the jitter ends. *)
    Definition actual_arrival := job_arrival j + job_jitter j.

    (* Next, we state whether the actual arrival of job j occurs in some interval 0, t, ... *)
    Definition jitter_has_passed (t: time) := actual_arrival t.

    (* ...along with the variants for interval 0, t), ... *)
    Definition actual_arrival_before (t: time) := actual_arrival < t.

    (* ...and interval t1, t2). *)
    Definition actual_arrival_between (t1 t2: time) :=
      t1 actual_arrival < t2.

  End ActualArrival.

  (* In this section, we show how to compute the list of arriving jobs. *)
  Section ArrivingJobs.

    Context {Job: eqType}.
    Variable job_arrival: Job time.
    Variable job_jitter: Job time.
    Variable arr_seq: arrival_sequence Job.

    (* For simplicity, let's define some local names. *)
    Let actual_job_arrival := actual_arrival job_arrival job_jitter.
    Let actual_job_arrival_between := actual_arrival_between job_arrival job_jitter.
    Let actual_job_arrival_before := actual_arrival_before job_arrival job_jitter.
    Let arrivals_before := jobs_arrived_before arr_seq.

    (* First, we define the actual job arrivals in the interval t1, t2). *)
    Definition actual_arrivals_between (t1 t2: time) :=
      [seq j <- arrivals_before t2 | t1 actual_job_arrival j < t2].

    (* Similarly, we define the actual job arrivals up to time t... *)
    Definition actual_arrivals_up_to (t: time) := actual_arrivals_between 0 t.+1.

    (* ...and the actual job arrivals strictly before time t. *)
    Definition actual_arrivals_before (t: time) := actual_arrivals_between 0 t.

    (* In this section, we prove some lemmas about the arrival sequence prefixes. *)
    Section Lemmas.

      (* Assume that job arrival times are consistent. *)
      Hypothesis H_arrival_times_are_consistent:
        arrival_times_are_consistent job_arrival arr_seq.

      (* We begin with basic lemmas for manipulating the sequences. *)
      Section Basic.

        (* First, we show that the set of arriving jobs can be split
           into disjoint intervals. *)

        Lemma actual_arrivals_between_mem_cat:
           j t1 t t2,
            t1 t
            t t2
            j \in actual_arrivals_between t1 t2 =
            (j \in actual_arrivals_between t1 t ++ actual_arrivals_between t t2).

        Lemma actual_arrivals_between_sub:
           j t1 t1' t2 t2',
            t1' t1
            t2 t2'
            j \in actual_arrivals_between t1 t2
            j \in actual_arrivals_between t1' t2'.

      End Basic.

      (* Next, we relate the arrival prefixes with job arrival times. *)
      Section ArrivalTimes.

        (* First, we prove that if a job belongs to the prefix (actual_arrivals_before t),
         then it arrives in the arrival sequence. *)

        Lemma in_actual_arrivals_between_implies_arrived:
           j t1 t2,
            j \in actual_arrivals_between t1 t2
            arrives_in arr_seq j.

        Lemma in_actual_arrivals_before_implies_arrived:
           j t,
            j \in actual_arrivals_before t
            arrives_in arr_seq j.

        (* Next, we prove that if a job belongs to the prefix (actual_arrivals_before t),
         then its actual job arrival occured before t. *)

        Lemma in_actual_arrivals_implies_arrived_before:
           j t,
            j \in actual_arrivals_before t
            actual_job_arrival_before j t.

        (* We also prove that if a job belongs to the prefix (actual_arrivals_between t1 t2),
           then its actual job arrival occured between t1 and t2. *)

        Lemma in_actual_arrivals_implies_arrived_between:
           j t1 t2,
            j \in actual_arrivals_between t1 t2
            actual_job_arrival_between j t1 t2.

        (* Similarly, we prove that if a job from the arrival sequence has actual arrival
         before time t, then it belongs to the sequence (actual_arrivals_before t). *)

        Lemma arrived_between_implies_in_actual_arrivals:
           j t1 t2,
            arrives_in arr_seq j
            actual_job_arrival_between j t1 t2
            j \in actual_arrivals_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 actual_arrivals_uniq :
          arrival_sequence_is_a_set arr_seq
           t1 t2, uniq (actual_arrivals_between t1 t2).

      End ArrivalTimes.

    End Lemmas.

  End ArrivingJobs.

End ArrivalSequenceWithJitter.