Library prosa.analysis.facts.model.task_arrivals


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)

Require Export prosa.model.task.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}.

Consider any job arrival sequence.
  Variable arr_seq : arrival_sequence Job.

Let [tsk] be any task.
  Variable tsk : Task.

We show that the number of arrivals of task can be split into disjoint intervals.
  Lemma num_arrivals_of_task_cat:
    ∀ 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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 46)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  arr_seq : arrival_sequence Job
  tsk : Task
  ============================
  forall t t1 t2 : nat,
  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

----------------------------------------------------------------------------- *)

  Proof.
    move ⇒ t t1 t2 /andP [GE LE].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 89)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  arr_seq : arrival_sequence Job
  tsk : Task
  t, t1, t2 : nat
  GE : t1 <= t
  LE : 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

----------------------------------------------------------------------------- *)

    rewrite /number_of_task_arrivals /task_arrivals_between /arrivals_between.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 106)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  arr_seq : arrival_sequence Job
  tsk : Task
  t, t1, t2 : nat
  GE : t1 <= t
  LE : t <= t2
  ============================
  size
    [seq j <- \cat_(t1<=t0<t2|true)arrivals_at arr_seq t0
       | job_task j == tsk] =
  size
    [seq j <- \cat_(t1<=t0<t|true)arrivals_at arr_seq t0 | job_task j == tsk] +
  size
    [seq j <- \cat_(t<=t0<t2|true)arrivals_at arr_seq t0 | job_task j == tsk]

----------------------------------------------------------------------------- *)

    rewrite (@big_cat_nat _ _ _ t) //=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 130)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  arr_seq : arrival_sequence Job
  tsk : Task
  t, t1, t2 : nat
  GE : t1 <= t
  LE : t <= t2
  ============================
  size
    [seq j <- \cat_(t1<=i<t|true)arrivals_at arr_seq i ++
              \cat_(t<=i<t2|true)arrivals_at arr_seq i
       | job_task j == tsk] =
  size
    [seq j <- \cat_(t1<=t0<t|true)arrivals_at arr_seq t0 | job_task j == tsk] +
  size
    [seq j <- \cat_(t<=t0<t2|true)arrivals_at arr_seq t0 | job_task j == tsk]

----------------------------------------------------------------------------- *)

      by rewrite filter_cat size_cat.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End TaskArrivals.