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.
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.

We show that the number of arrivals of task can be split into disjoint intervals.
  Lemma num_arrivals_of_task_cat:
    ∀ tsk t t1 t2,
      t1 ≤ t ≤ t2 →
      number_of_task_arrivals arr_seq tsk t1 t2 =
      number_of_task_arrivals arr_seq tsk t1 t + number_of_task_arrivals arr_seq tsk t t2.

To simplify subsequent proofs, we further lift arrivals_between_cat to the filtered version task_arrivals_between.
  Lemma task_arrivals_between_cat:
    ∀ tsk t1 t t2,
      t1 ≤ t →
      t ≤ t2 →
      task_arrivals_between arr_seq tsk t1 t2
      = task_arrivals_between arr_seq tsk t1 t ++ task_arrivals_between arr_seq tsk t t2.

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.
  Lemma task_arrivals_up_to_prefix_cat:
    ∀ j1 j2,
      arrives_in arr_seq j1 →
      arrives_in arr_seq j2 →
      job_task j1 = job_task j2 →
      job_arrival j1 ≤ job_arrival j2 →
      prefix_of (task_arrivals_up_to_job_arrival arr_seq j1) (task_arrivals_up_to_job_arrival arr_seq j2).

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.
  Lemma arrives_in_task_arrivals_up_to:
    ∀ j,
      arrives_in arr_seq j →
      j \in task_arrivals_up_to_job_arrival arr_seq 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.
  Lemma task_arrivals_cat:
    ∀ t_m t,
      t_m ≤ t →
      task_arrivals_up_to arr_seq tsk t =
      task_arrivals_up_to arr_seq tsk t_m ++ task_arrivals_between arr_seq tsk t_m.+1 t.+1.

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.
  Lemma task_arrivals_up_to_cat:
    ∀ j,
      arrives_in arr_seq j →
      task_arrivals_up_to_job_arrival arr_seq j =
      task_arrivals_before_job_arrival arr_seq j ++ task_arrivals_at_job_arrival arr_seq 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.
  Lemma task_arrivals_between_subset:
    ∀ t1 t2 j,
      j \in task_arrivals_between arr_seq tsk t1 t2 →
      j \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.
  Corollary arrives_in_task_arrivals_implies_arrived:
    ∀ t1 t2 j,
      j \in task_arrivals_between arr_seq tsk t1 t2 →
      arrives_in arr_seq j.

Any job j in task_arrivals_before arr_seq tsk t has an arrival time earlier than t.
  Lemma arrives_in_task_arrivals_before_implies_arrives_before :
    ∀ j t,
      j \in task_arrivals_before arr_seq tsk t →
      job_arrival j < 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.
  Lemma in_task_arrivals_between_implies_job_of_task :
    ∀ t1 t2 j,
      j \in task_arrivals_between arr_seq tsk t1 t2 →
      job_task j = tsk.

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.
  Lemma task_arrivals_between_uniq :
    ∀ t1 t2,
      arrival_sequence_uniq arr_seq →
      uniq (task_arrivals_between arr_seq tsk t1 t2).

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.
  Lemma arrival_lt_implies_strict_prefix:
    ∀ j1 j2,
      job_task j1 = tsk →
      job_task j2 = tsk →
      arrives_in arr_seq j1 →
      arrives_in arr_seq j2 →
      job_arrival j1 < job_arrival j2 →
      strict_prefix_of (task_arrivals_up_to_job_arrival arr_seq j1) (task_arrivals_up_to_job_arrival arr_seq 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).
  Lemma task_arrivals_between_is_cat_of_task_arrivals_at:
    ∀ t1 t2,
      task_arrivals_between arr_seq tsk t1 t2 = \cat_(t1 ≤ t < t2) task_arrivals_at arr_seq tsk t.

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).
  Lemma size_of_task_arrivals_between:
    ∀ t1 t2,
      size (task_arrivals_between arr_seq tsk t1 t2)
      = \sum_(t1 ≤ t < t2) size (task_arrivals_at arr_seq tsk t).

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.
  Corollary task_arrivals_between_sorted :
    ∀ t1 t2,
      sorted by_arrival_times (task_arrivals_between arr_seq tsk t1 t2).

End TaskArrivals.