Require Export prosa.util.epsilon.
Require Export prosa.model.task.arrival.curves.
[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]
Require Export prosa.analysis.facts.model.task_arrivals.

(** * Facts About Arrival Curves *)


(** We observe that tasks that exhibit job arrivals must have non-pathological
    arrival curves. This allows excluding pathological cases in higher-level
    proofs. *)
Section NonPathologicalCurve.

  (** Consider any kind of tasks characterized by an upper-bounding arrival curve... *)
  Context {Task : TaskType} `{MaxArrivals Task}.
  (** ... and the corresponding type of jobs. *)
  Context {Job : JobType} `{JobTask Job Task}.

  (** Consider an arbitrary task ... *)
  Variable tsk : Task.

  (** ... and an arrival sequence ... *)
  Variable arr_seq : arrival_sequence Job.

  (** ... that is compliant with the upper-bounding arrival curve. *)
  Hypothesis H_curve_is_valid : respects_max_arrivals arr_seq tsk (max_arrivals tsk).

  (** If we have evidence that a job of the task [tsk] ... *)
  Variable j : Job.
  Hypothesis H_job_of_tsk : job_of_task tsk j.

  (** ... arrives at any point in time, ... *)
  Hypothesis H_arrives : arrives_in arr_seq j.

  (** ... then the maximum number of job arrivals in a non-empty interval cannot
      be zero. *)
  Lemma non_pathological_max_arrivals :
    max_arrivals tsk ε > 0.
Task: TaskType
H: MaxArrivals Task
Job: JobType
H0: JobTask Job Task
tsk: Task
arr_seq: arrival_sequence Job
H_curve_is_valid: respects_max_arrivals arr_seq tsk
  (max_arrivals tsk)
j: Job
H_job_of_tsk: job_of_task tsk j
H_arrives: arrives_in arr_seq j
0 < max_arrivals tsk 1
  Proof.
Task: TaskType
H: MaxArrivals Task
Job: JobType
H0: JobTask Job Task
tsk: Task
arr_seq: arrival_sequence Job
H_curve_is_valid: respects_max_arrivals arr_seq tsk
  (max_arrivals tsk)
j: Job
H_job_of_tsk: job_of_task tsk j
H_arrives: arrives_in arr_seq j
0 < max_arrivals tsk 1
    move: (H_arrives) => [t ARR].
Task: TaskType
H: MaxArrivals Task
Job: JobType
H0: JobTask Job Task
tsk: Task
arr_seq: arrival_sequence Job
H_curve_is_valid: respects_max_arrivals arr_seq tsk
  (max_arrivals tsk)
j: Job
H_job_of_tsk: job_of_task tsk j
H_arrives: arrives_in arr_seq j
t: instant
ARR: j \in arrivals_at arr_seq t
0 < max_arrivals tsk 1
    move: (H_curve_is_valid t t.+1 ltac:(by done)).
Task: TaskType
H: MaxArrivals Task
Job: JobType
H0: JobTask Job Task
tsk: Task
arr_seq: arrival_sequence Job
H_curve_is_valid: respects_max_arrivals arr_seq tsk
  (max_arrivals tsk)
j: Job
H_job_of_tsk: job_of_task tsk j
H_arrives: arrives_in arr_seq j
t: instant
ARR: j \in arrivals_at arr_seq t
number_of_task_arrivals arr_seq tsk t t.+1 <=
max_arrivals tsk (t.+1 - t) -> 0 < max_arrivals tsk 1
    rewrite -addn1 -addnBAC // addnBl_leq // => VALID.
Task: TaskType
H: MaxArrivals Task
Job: JobType
H0: JobTask Job Task
tsk: Task
arr_seq: arrival_sequence Job
H_curve_is_valid: respects_max_arrivals arr_seq tsk
  (max_arrivals tsk)
j: Job
H_job_of_tsk: job_of_task tsk j
H_arrives: arrives_in arr_seq j
t: instant
ARR: j \in arrivals_at arr_seq t
VALID: number_of_task_arrivals arr_seq tsk t (t + 1) <=
max_arrivals tsk 1
0 < max_arrivals tsk 1
    apply: (leq_trans _ VALID).
Task: TaskType
H: MaxArrivals Task
Job: JobType
H0: JobTask Job Task
tsk: Task
arr_seq: arrival_sequence Job
H_curve_is_valid: respects_max_arrivals arr_seq tsk
  (max_arrivals tsk)
j: Job
H_job_of_tsk: job_of_task tsk j
H_arrives: arrives_in arr_seq j
t: instant
ARR: j \in arrivals_at arr_seq t
VALID: number_of_task_arrivals arr_seq tsk t (t + 1) <=
max_arrivals tsk 1
0 < number_of_task_arrivals arr_seq tsk t (t + 1)
    rewrite /number_of_task_arrivals size_of_task_arrivals_between.
Task: TaskType
H: MaxArrivals Task
Job: JobType
H0: JobTask Job Task
tsk: Task
arr_seq: arrival_sequence Job
H_curve_is_valid: respects_max_arrivals arr_seq tsk
  (max_arrivals tsk)
j: Job
H_job_of_tsk: job_of_task tsk j
H_arrives: arrives_in arr_seq j
t: instant
ARR: j \in arrivals_at arr_seq t
VALID: number_of_task_arrivals arr_seq tsk t (t + 1) <=
max_arrivals tsk 1
0 <
\sum_(t <= t < t + 1)
   size (task_arrivals_at arr_seq tsk t)
    rewrite big_ltn addn1 // big_geq // addn0.
Task: TaskType
H: MaxArrivals Task
Job: JobType
H0: JobTask Job Task
tsk: Task
arr_seq: arrival_sequence Job
H_curve_is_valid: respects_max_arrivals arr_seq tsk
  (max_arrivals tsk)
j: Job
H_job_of_tsk: job_of_task tsk j
H_arrives: arrives_in arr_seq j
t: instant
ARR: j \in arrivals_at arr_seq t
VALID: number_of_task_arrivals arr_seq tsk t (t + 1) <=
max_arrivals tsk 1
0 < size (task_arrivals_at arr_seq tsk t)
    rewrite /task_arrivals_at size_filter //= -has_count.
Task: TaskType
H: MaxArrivals Task
Job: JobType
H0: JobTask Job Task
tsk: Task
arr_seq: arrival_sequence Job
H_curve_is_valid: respects_max_arrivals arr_seq tsk
  (max_arrivals tsk)
j: Job
H_job_of_tsk: job_of_task tsk j
H_arrives: arrives_in arr_seq j
t: instant
ARR: j \in arrivals_at arr_seq t
VALID: number_of_task_arrivals arr_seq tsk t (t + 1) <=
max_arrivals tsk 1
has [eta job_of_task tsk] (arrivals_at arr_seq t)
    by apply /hasP; exists j.
  Qed.

End NonPathologicalCurve.

(** We add the above lemma to the global hints database. *)
Global Hint Resolve non_pathological_max_arrivals : basic_rt_facts.