Library prosa.analysis.facts.model.task_arrivals

Require Export prosa.model.task.arrivals.
Require Export prosa.util.all.
Require Export prosa.analysis.facts.behavior.arrivals.

In this file we provide basic properties related to tasks on arrival sequences.
Section TaskArrivals.

Consider any type of job associated with any type of tasks.
  Context {Job : JobType}.
  Context {Task : TaskType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

Consider any job arrival sequence with consistent arrivals.
We show that the number of arrivals of task can be split into disjoint intervals.
To simplify subsequent proofs, we further lift arrivals_between_cat to the filtered version task_arrivals_between.
We show that task_arrivals_up_to_job_arrival j1 is a prefix of task_arrivals_up_to_job_arrival j2 if j2 arrives at the same time or after j1.
Let tsk be any task.
  Variable tsk : Task.

Any job j from the arrival sequence is contained in task_arrivals_up_to_job_arrival j.
Also, any job j from the arrival sequence is contained in task_arrivals_at_job_arrival j.
  Lemma arrives_in_task_arrivals_at:
     j,
      arrives_in arr_seq j
      j \in task_arrivals_at_job_arrival arr_seq j.

We show that for any time t_m less than or equal to t, task arrivals up to t_m forms a prefix of task arrivals up to t.
We observe that for any job j, task arrivals up to job_arrival j is a concatenation of task arrivals before job_arrival j and task arrivals at job_arrival j.
We show that any job j in the arrival sequence is also contained in task arrivals between time instants t1 and t2, if job_arrival j lies in the interval [t1,t2).
  Lemma job_in_task_arrivals_between:
     j t1 t2,
      arrives_in arr_seq j
      job_task j = tsk
      t1 job_arrival j < t2
      j \in task_arrivals_between arr_seq tsk t1 t2.

Any job j in task_arrivals_between arr_seq tsk t1 t2 is also contained in arrivals_between arr_seq t1 t2.
Any job j in task_arrivals_between arr_seq tsk t1 t2 arrives in the arrival sequence arr_seq.
Any job j in task_arrivals_before arr_seq tsk t has an arrival time earlier than t.
Any job j in task_arrivals_before arr_seq tsk t is a job of task tsk.
  Lemma arrives_in_task_arrivals_implies_job_task :
     j t,
      j \in task_arrivals_before arr_seq tsk t
      job_task j == tsk.

We repeat the observation for task_arrivals_between.
If a job arrives between to points in time, then the corresponding interval is nonempty...
  Lemma task_arrivals_nonempty :
     t1 t2 j,
      j \in task_arrivals_between arr_seq tsk t1 t2
      t1 < t2.

... which we can also express in terms of number_of_task_arrivals being nonzero.
  Corollary number_of_task_arrivals_nonzero :
     t1 t2,
      number_of_task_arrivals arr_seq tsk t1 t2 > 0
      t1 < t2.

An arrival sequence with non-duplicate arrivals implies that the task arrivals also contain non-duplicate arrivals.
  Lemma uniq_task_arrivals:
     t,
      arrival_sequence_uniq arr_seq
      uniq (task_arrivals_up_to arr_seq tsk t).

The same observation applies to task_arrivals_between.
A job cannot arrive before it's arrival time.
  Lemma job_notin_task_arrivals_before :
     j t,
      arrives_in arr_seq j
      job_arrival j > t
      j \notin task_arrivals_up_to arr_seq (job_task j) t.

We show that for any two jobs j1 and j2, task arrivals up to arrival of job j1 form a strict prefix of task arrivals up to arrival of job j2.
For any job j2 with job_index equal to n, the nth job in the sequence task_arrivals_up_to arr_seq tsk t is j2, given that t is not less than job_arrival j2. Note that j_def is used as a default job for the access function and has nothing to do with the lemma.
  Lemma nth_job_of_task_arrivals:
     n j_def j t,
      arrives_in arr_seq j
      job_task j = tsk
      job_index arr_seq j = n
      t job_arrival j
      nth j_def (task_arrivals_up_to arr_seq tsk t) n = j.

We show that task arrivals in the interval [t1, t2) is the same as concatenation of task arrivals at each instant in [t1, t2).
The number of jobs of a task tsk in the interval [t1, t2) is the same as sum of the number of jobs of the task tsk at each instant in [t1, t2).
We note that, trivially, the list of task arrivals task_arrivals_between is sorted by arrival times because the underlying arrivals_between is sorted, as established by the lemma arrivals_between_sorted.