Require Export prosa.util.epsilon.
Require Export prosa.model.task.arrival.curves.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.analysis.facts.model.task_arrivals.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]

(** * 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 ε
  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 ε
    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 ε
    move: (H_curve_is_valid t t.+1) => 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: t <= t.+1 ->
number_of_task_arrivals arr_seq tsk t t.+1 <=
max_arrivals tsk (t.+1 - t)
0 < max_arrivals tsk ε
    have -> : ε = t.+1 - t by rewrite /ε; lia.
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: t <= t.+1 ->
number_of_task_arrivals arr_seq tsk t t.+1 <=
max_arrivals tsk (t.+1 - t)
0 < max_arrivals tsk (t.+1 - t)
    apply: leq_trans; last by apply 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: t <= t.+1 ->
number_of_task_arrivals arr_seq tsk t t.+1 <=
max_arrivals tsk (t.+1 - t)
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: t <= t.+1 ->
number_of_task_arrivals arr_seq tsk t t.+1 <=
max_arrivals tsk (t.+1 - t)
0 <
\sum_(t <= t < t.+1)
   size (task_arrivals_at arr_seq tsk t)
    rewrite big_ltn // 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: t <= t.+1 ->
number_of_task_arrivals arr_seq tsk t t.+1 <=
max_arrivals tsk (t.+1 - t)
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: t <= t.+1 ->
number_of_task_arrivals arr_seq tsk t t.+1 <=
max_arrivals tsk (t.+1 - t)
has [eta job_of_task tsk] (arrivals_at arr_seq t)
    by apply /hasP; exists j.
  Qed.

End NonPathologicalCurve.