Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]


(** In this module, we provide basic definitions concerning the job
    arrivals of a given task. *)

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}.
  Context `{JobCost Job}.

  (** Consider any job arrival sequence ...  *)
  Variable arr_seq : arrival_sequence Job.

  (** ... and any task. *)
  Variable tsk : Task.

  (** First, we construct the list of jobs of task [tsk] that arrive
      in a given half-open interval <<[t1, t2)>>. *)
  Definition task_arrivals_between (t1 t2 : instant) :=
    [seq j <- arrivals_between arr_seq t1 t2 | job_of_task tsk j].

  (** Based on that, we define the list of jobs of task [tsk] that
      arrive up to and including time [t], ... *)
  Definition task_arrivals_up_to (t : instant) :=
    task_arrivals_between 0 t.+1.

  (** ... the list of jobs of task [tsk] that arrive strictly
      before time [t], ... *)
  Definition task_arrivals_before (t : instant) :=
    task_arrivals_between 0 t.

  (** ... the list of jobs of task [tsk] that arrive exactly at an instant [t], ... *)
  Definition task_arrivals_at (tsk : Task) (t : instant) :=
    [seq j <- arrivals_at arr_seq t | job_of_task tsk j].
  
  (** ... and finally count the number of job arrivals. *)
  Definition number_of_task_arrivals (t1 t2 : instant) :=
    size (task_arrivals_between t1 t2).

  (** ... and also count the cost of job arrivals. *)
  Definition cost_of_task_arrivals (t1 t2 : instant) :=
    \sum_(j <- task_arrivals_between t1 t2) job_cost j.

  (** In the following, suppose there is a deadline associated with each job. *)
  Context `{JobDeadline Job}.

  (** We define the list of jobs of task [tsk] that arrive in
      a given half-open interval <<[t1, t2)>> and that also have a deadline
      within the closed interval <<[t1, t2]>>, ... *)
  Definition task_arrivals_with_deadline_within (t1 t2 : instant) :=
    [seq j <- arrivals_between arr_seq t1 t2 | job_of_task tsk j & job_deadline j <= t2].

  (** ... and similarly define the count of such jobs. *)
  Definition number_of_task_arrivals_with_deadline_within (t1 t2 : instant) :=
    size (task_arrivals_with_deadline_within t1 t2).

End TaskArrivals.

(** In this section we introduce a few definitions
    regarding arrivals of a particular task prior to a job. *)
Section PriorArrivals.

  (** Consider any type of jobs associated with any type of tasks. *)
  Context {Job : JobType}.
  Context {Task : TaskType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  
  (** Consider any arrival sequence of jobs ... *)
  Variable arr_seq : arrival_sequence Job.

  (** ... and any job [j]. *)
  Variable j : Job.
  
  (** We first define a sequence of jobs of a task 
   that arrive before or at [job_arrival j]. *)
  Definition task_arrivals_up_to_job_arrival :=
    task_arrivals_up_to arr_seq (job_task j) (job_arrival j).

  (** Next, we define a sequence of jobs of a task
   that arrive strictly before [job_arrival j]. *)
  Definition task_arrivals_before_job_arrival :=
    task_arrivals_before arr_seq (job_task j) (job_arrival j).

  (** Finally, we define a sequence of jobs of a task 
   that arrive at [job_arrival j]. *)
  Definition task_arrivals_at_job_arrival :=
    task_arrivals_at arr_seq (job_task j) (job_arrival j).
  
End PriorArrivals.

(** In this section, we define the notion of a job's index. *)
Section JobIndex.

  (** Consider any type of tasks, ... *)
  Context {Task : TaskType}.

  (** ... any type of jobs associated with the tasks, ... *)
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobTask Job Task}.

  (** ... and any arrival sequence. *)
  Variable arr_seq : arrival_sequence Job.  
  
  (** Given a job [j], we define a concept of job index as the number
      of jobs of the same task as [j] that arrived before or at the 
      same instant as [j]. Please note that job indices start from zero. *)
  Definition job_index (j : Job) :=
    index j (task_arrivals_up_to_job_arrival arr_seq j).

End JobIndex.

(** In this section we define the notion of a previous job 
    for any job with a positive [job_index]. *)
Section PreviousJob.

  (** Consider any type of jobs associated with any type of tasks. *)
  Context {Job : JobType}.
  Context {Task : TaskType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  
  (** Consider any job arrival sequence.  *)
  Variable arr_seq : arrival_sequence Job.

  Let task_arrivals_up_to_job_arrival j := task_arrivals_up_to_job_arrival arr_seq j.
  Let prev_index j := job_index arr_seq j - 1.
    
  (** For any job [j] with a positive [job_index] we define the notion 
     of a previous job. *)  
  Definition prev_job (j : Job) := nth j (task_arrivals_up_to_job_arrival j) (prev_index j).

End PreviousJob.