task_arrivals.v 1010 Bytes
Newer Older
1
From rt.restructuring.model.aggregate Require Export task_arrivals.
2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30

(* 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:
    forall 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.
  Proof.
    move => t t1 t2 /andP [GE LE].
    rewrite /number_of_task_arrivals /task_arrivals_between /arrivals_between. 
    rewrite (@big_cat_nat _ _ _ t) //=.
      by rewrite filter_cat size_cat.
  Qed.

End TaskArrivals.