Library rt.model.basic.arrival_sequence

Require Import rt.util.all rt.model.basic.job rt.model.basic.task rt.model.basic.time.

(* Definitions and properties of job arrival sequences. *)
Module ArrivalSequence.

  Export Time.

  (* Next, we define a job arrival sequence (can be infinite). *)
  Section ArrivalSequenceDef.

    (* Given any job type with decidable equality, ... *)
    Variable Job: eqType.

    (* ..., an arrival sequence is a mapping from time to a sequence of jobs. *)
    Definition arrival_sequence := time seq Job.

  End ArrivalSequenceDef.

  (* Note that Job denotes the universe of all possible jobs.
     In order to distinguish jobs of different arrival sequences, next we
     define a subtype of Job called JobIn. *)

  Section JobInArrivalSequence.

    Context {Job: eqType}.

    (* Whether a job arrives in a particular sequence at time t *)
    Definition arrives_at (j: Job) (arr_seq: arrival_sequence Job) (t: time) :=
      j arr_seq t.

    (* A job j of type (JobIn arr_seq) is a job that arrives at some particular
       time in arr_seq. It holds the arrival time and a proof of arrival. *)

    Record JobIn (arr_seq: arrival_sequence Job) : Type :=
    {
      _job_in: Job;
      _arrival_time: time; (* arrival time *)
      _: arrives_at _job_in arr_seq _arrival_time (* proof of arrival *)
    }.

    (* Define a coercion that states that every JobIn is a Job. *)
    Coercion JobIn_is_Job {arr_seq: arrival_sequence Job} (j: JobIn arr_seq) :=
      _job_in arr_seq j.

    (* Define job arrival time as that time that the job arrives (only works for JobIn). *)
    Definition job_arrival {arr_seq: arrival_sequence Job} (j: JobIn arr_seq) :=
      _arrival_time arr_seq j.

    (* Finally, we define a decidable equality for JobIn, in order to make
       it compatible with ssreflect (see jobin_eqdec.v). *)

    Load jobin_eqdec.

  End JobInArrivalSequence.

  (* A valid arrival sequence must satisfy some properties. *)
  Section ArrivalSequenceProperties.

    Context {Job: eqType}.
    Variable arr_seq: arrival_sequence Job.

    (* The same job j cannot arrive at two different times. *)
    Definition no_multiple_arrivals :=
       (j: Job) t1 t2,
        arrives_at j arr_seq t1 arrives_at j arr_seq t2 t1 = t2.

    (* The sequence of arrivals at a particular time has no duplicates. *)
    Definition arrival_sequence_is_a_set := t, uniq (arr_seq t).

  End ArrivalSequenceProperties.

  (* Next, we define whether a job has arrived in an interval. *)
  Section ArrivingJobs.

    Context {Job: eqType}.
    Context {arr_seq: arrival_sequence Job}.
    Variable j: JobIn arr_seq.

    (* A job has arrived at time t iff it arrives at some time t_0, with 0 <= t_0 <= t. *)
    Definition has_arrived (t: time) := job_arrival j t.

    (* A job arrived before t iff it arrives at some time t_0, with 0 <= t_0 < t. *)
    Definition arrived_before (t: time) := job_arrival j < t.

    (* A job arrives between t1 and t2 iff it arrives at some time t with t1 <= t < t2. *)
    Definition arrived_between (t1 t2: time) := t1 job_arrival j < t2.

  End ArrivingJobs.

  (* In this section, we define prefixes of arrival sequences based on JobIn.
     This is not required in the main proofs, but important for instantiating
     a concrete schedule. Feel free to skip this section. *)

  Section ArrivalSequencePrefix.

    Context {Job: eqType}.
    Variable arr_seq: arrival_sequence Job.

    (* Let's define a function that takes a job j and converts it to
       Some JobIn (if j arrives at time t), or None otherwise. *)

    Program Definition is_JobIn (t: time) (j: Job) :=
      if (j arr_seq t) is true then
        Some (Build_JobIn arr_seq j t _)
      else None.

    (* Now we define the list of JobIn that arrive at time t as the partial
       map of is_JobIn.  *)

    Definition jobs_arriving_at (t: time) := pmap (is_JobIn t) (arr_seq t).

    (* The list of JobIn that have arrived up to time t follows by concatenation. *)
    Definition jobs_arrived_up_to (t': time) :=
      \cat_(t < t'.+1) jobs_arriving_at t.

    Section Lemmas.

      (* There's an inverse function for recovering the original Job from JobIn. *)
      Lemma is_JobIn_inverse :
         t,
          ocancel (is_JobIn t) (_job_in arr_seq).

      (* Prove that a member of the list indeed satisfies the property. *)
      Lemma JobIn_has_arrived :
         j t,
          j jobs_arrived_up_to t has_arrived j t.

      (* If the arrival sequence doesn't allow duplicates,
         the same applies for the list of JobIn that arrive. *)

      Lemma JobIn_uniq :
        arrival_sequence_is_a_set arr_seq
         t, uniq (jobs_arrived_up_to t).

    End Lemmas.

  End ArrivalSequencePrefix.

End ArrivalSequence.