task_arrivals.v

Require Export prosa.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 "_ + _" 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.util.all.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]
Require Export prosa.analysis.facts.behavior.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]

(** 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}.
  Context `{JobArrival Job}.

  (** Consider any job arrival sequence with consistent arrivals. *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.

  (** We show that the number of arrivals of task can be split into disjoint intervals. *)
  Lemma num_arrivals_of_task_cat:
    forall tsk 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.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
forall (tsk : Task) (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.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
forall (tsk : Task) (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
    move => tsk t t1 t2 /andP [GE LE].Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
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.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t, t1, t2: nat
GE: t1 <= t
LE: t <= t2
size
  [seq j <- \cat_(t1<=t<t2)arrivals_at arr_seq t
     | job_of_task tsk j] =
size
  [seq j <- \cat_(t1<=t<t)arrivals_at arr_seq t
     | job_of_task tsk j] +
size
  [seq j <- \cat_(t<=t<t2)arrivals_at arr_seq t
     | job_of_task tsk j]
    now rewrite (@big_cat_nat _ _ _ t) //= filter_cat size_cat.
  Qed.

  (** To simplify subsequent proofs, we further lift [arrivals_between_cat] to
      the filtered version [task_arrivals_between]. *)
  Lemma task_arrivals_between_cat:
    forall tsk t1 t t2,
      t1 <= t ->
      t <= t2 ->
      task_arrivals_between arr_seq tsk t1 t2
      = task_arrivals_between arr_seq tsk t1 t ++ task_arrivals_between arr_seq tsk t t2.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
forall (tsk : Task) (t1 t t2 : nat),
t1 <= t ->
t <= t2 ->
task_arrivals_between arr_seq tsk t1 t2 =
task_arrivals_between arr_seq tsk t1 t ++
task_arrivals_between arr_seq tsk t t2
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
forall (tsk : Task) (t1 t t2 : nat),
t1 <= t ->
t <= t2 ->
task_arrivals_between arr_seq tsk t1 t2 =
task_arrivals_between arr_seq tsk t1 t ++
task_arrivals_between arr_seq tsk t t2
    move=> tsk t1 t t2 LEQ_t1 LEQ_t2.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t1, t, t2: nat
LEQ_t1: t1 <= t
LEQ_t2: t <= t2
task_arrivals_between arr_seq tsk t1 t2 =
task_arrivals_between arr_seq tsk t1 t ++
task_arrivals_between arr_seq tsk t t2
    now rewrite /task_arrivals_between -filter_cat -arrivals_between_cat.
  Qed.
  
  (** We show that [task_arrivals_up_to_job_arrival j1] is a prefix 
   of [task_arrivals_up_to_job_arrival j2] if [j2] arrives at the same time 
   or after [j1]. *)
  Lemma task_arrivals_up_to_prefix_cat: 
    forall j1 j2,
      arrives_in arr_seq j1 ->
      arrives_in arr_seq j2 ->
      job_task j1 = job_task j2 ->
      job_arrival j1 <= job_arrival j2 ->
      prefix_of (task_arrivals_up_to_job_arrival arr_seq j1) (task_arrivals_up_to_job_arrival arr_seq j2).Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
forall j1 j2 : Job,
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = job_task j2 ->
job_arrival j1 <= job_arrival j2 ->
prefix_of (task_arrivals_up_to_job_arrival arr_seq j1)
  (task_arrivals_up_to_job_arrival arr_seq j2)
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
forall j1 j2 : Job,
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = job_task j2 ->
job_arrival j1 <= job_arrival j2 ->
prefix_of (task_arrivals_up_to_job_arrival arr_seq j1)
  (task_arrivals_up_to_job_arrival arr_seq j2)
    intros j1 j2 ARR1 ARR2 TSK ARR_LT.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
j1, j2: Job
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
TSK: job_task j1 = job_task j2
ARR_LT: job_arrival j1 <= job_arrival j2
prefix_of (task_arrivals_up_to_job_arrival arr_seq j1)
  (task_arrivals_up_to_job_arrival arr_seq j2)
    exists (task_arrivals_between arr_seq (job_task j1) (job_arrival j1 + 1) (job_arrival j2 + 1)).Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
j1, j2: Job
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
TSK: job_task j1 = job_task j2
ARR_LT: job_arrival j1 <= job_arrival j2
task_arrivals_up_to_job_arrival arr_seq j1 ++
task_arrivals_between arr_seq (job_task j1)
  (job_arrival j1 + 1) (job_arrival j2 + 1) =
task_arrivals_up_to_job_arrival arr_seq j2
    now rewrite /task_arrivals_up_to_job_arrival !addn1 TSK -task_arrivals_between_cat.
  Qed.    

  (** Let [tsk] be any task. *)
  Variable tsk : Task.
  
  (** Any job [j] from the arrival sequence is contained in 
   [task_arrivals_up_to_job_arrival j]. *)
  Lemma arrives_in_task_arrivals_up_to:
    forall j,
      arrives_in arr_seq j ->
      j \in task_arrivals_up_to_job_arrival arr_seq j.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall j : Job,
arrives_in arr_seq j ->
j \in task_arrivals_up_to_job_arrival arr_seq j
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall j : Job,
arrives_in arr_seq j ->
j \in task_arrivals_up_to_job_arrival arr_seq j
    intros j ARR.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j
j \in task_arrivals_up_to_job_arrival arr_seq j
    rewrite mem_filter; apply /andP.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j
job_of_task (job_task j) j /\
j \in arrivals_between arr_seq 0 (job_arrival j).+1
    split; first by apply /eqP => //.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j
j \in arrivals_between arr_seq 0 (job_arrival j).+1 
    move : ARR => [t ARR]; move : (ARR) => EQ.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t: instant
ARR, EQ: j \in arrivals_at arr_seq t
j \in arrivals_between arr_seq 0 (job_arrival j).+1
    apply H_consistent_arrivals in EQ.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t: instant
ARR: j \in arrivals_at arr_seq t
EQ: job_arrival j = t
j \in arrivals_between arr_seq 0 (job_arrival j).+1
    rewrite (mem_bigcat_nat _ (fun t => arrivals_at arr_seq t) j 0 _ (job_arrival j)) // EQ //.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t: instant
ARR: j \in arrivals_at arr_seq t
EQ: job_arrival j = t
0 <= t < t.+1
    now lia.
  Qed.

  (** Also, any job [j] from the arrival sequence is contained in 
   [task_arrivals_at_job_arrival j]. *)
  Lemma arrives_in_task_arrivals_at:
    forall j,
      arrives_in arr_seq j ->
      j \in task_arrivals_at_job_arrival arr_seq j.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall j : Job,
arrives_in arr_seq j ->
j \in task_arrivals_at_job_arrival arr_seq j
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall j : Job,
arrives_in arr_seq j ->
j \in task_arrivals_at_job_arrival arr_seq j
    intros j ARR.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j
j \in task_arrivals_at_job_arrival arr_seq j
    rewrite mem_filter; apply /andP.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j
job_of_task (job_task j) j /\
j \in arrivals_at arr_seq (job_arrival j)
    split; first by apply /eqP => //.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j
j \in arrivals_at arr_seq (job_arrival j) 
    rewrite /arrivals_at.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j
j \in arr_seq (job_arrival j)
    move : ARR => [t ARR].Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t: instant
ARR: j \in arrivals_at arr_seq t
j \in arr_seq (job_arrival j)
    now rewrite (H_consistent_arrivals j t ARR).
  Qed.

  (** We show that for any time [t_m] less than or equal to [t], 
      task arrivals up to [t_m] forms a prefix of task arrivals up to [t]. *)
  Lemma task_arrivals_cat:
    forall t_m t,
      t_m <= t ->
      task_arrivals_up_to arr_seq tsk t =
      task_arrivals_up_to arr_seq tsk t_m ++ task_arrivals_between arr_seq tsk t_m.+1 t.+1.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall t_m t : nat,
t_m <= t ->
task_arrivals_up_to arr_seq tsk t =
task_arrivals_up_to arr_seq tsk t_m ++
task_arrivals_between arr_seq tsk t_m.+1 t.+1
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall t_m t : nat,
t_m <= t ->
task_arrivals_up_to arr_seq tsk t =
task_arrivals_up_to arr_seq tsk t_m ++
task_arrivals_between arr_seq tsk t_m.+1 t.+1
    intros t1 t2 INEQ.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t1, t2: nat
INEQ: t1 <= t2
task_arrivals_up_to arr_seq tsk t2 =
task_arrivals_up_to arr_seq tsk t1 ++
task_arrivals_between arr_seq tsk t1.+1 t2.+1
    now rewrite -filter_cat -arrivals_between_cat. 
  Qed.

  (** We observe that for any job [j], task arrivals up to [job_arrival j] is a 
      concatenation of task arrivals before [job_arrival j] and task arrivals 
      at [job_arrival j]. *)
  Lemma task_arrivals_up_to_cat:
    forall j,
      arrives_in arr_seq j ->
      task_arrivals_up_to_job_arrival arr_seq j =
      task_arrivals_before_job_arrival arr_seq j ++ task_arrivals_at_job_arrival arr_seq j.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall j : Job,
arrives_in arr_seq j ->
task_arrivals_up_to_job_arrival arr_seq j =
task_arrivals_before_job_arrival arr_seq j ++
task_arrivals_at_job_arrival arr_seq j
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall j : Job,
arrives_in arr_seq j ->
task_arrivals_up_to_job_arrival arr_seq j =
task_arrivals_before_job_arrival arr_seq j ++
task_arrivals_at_job_arrival arr_seq j
    intros j ARR.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j
task_arrivals_up_to_job_arrival arr_seq j =
task_arrivals_before_job_arrival arr_seq j ++
task_arrivals_at_job_arrival arr_seq j
    rewrite /task_arrivals_up_to_job_arrival /task_arrivals_up_to
            /task_arrivals_before /task_arrivals_between.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j
[seq j0 <- arrivals_between arr_seq 0
             (job_arrival j).+1
   | job_of_task (job_task j) j0] =
task_arrivals_before_job_arrival arr_seq j ++
task_arrivals_at_job_arrival arr_seq j 
    rewrite -filter_cat (arrivals_between_cat _ 0 (job_arrival j) (job_arrival j).+1) //.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
ARR: arrives_in arr_seq j
[seq j0 <- arrivals_between arr_seq 0 (job_arrival j) ++
           arrivals_between arr_seq (job_arrival j)
             (job_arrival j).+1
   | job_of_task (job_task j) j0] =
[seq j0 <- arrivals_between arr_seq 0 (job_arrival j) ++
           arrivals_at arr_seq (job_arrival j)
   | job_of_task (job_task j) j0]
    now rewrite /arrivals_between big_nat1.
  Qed.

  (** We show that any job [j] in the arrival sequence is also contained in task arrivals 
      between time instants [t1] and [t2], if [job_arrival j] lies in the interval <<[t1,t2)>>. *)
  Lemma job_in_task_arrivals_between:
    forall j t1 t2,
      arrives_in arr_seq j ->
      job_task j = tsk ->
      t1 <= job_arrival j < t2 -> 
      j \in task_arrivals_between arr_seq tsk t1 t2.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (j : Job) (t1 t2 : nat),
arrives_in arr_seq j ->
job_task j = tsk ->
t1 <= job_arrival j < t2 ->
j \in task_arrivals_between arr_seq tsk t1 t2
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (j : Job) (t1 t2 : nat),
arrives_in arr_seq j ->
job_task j = tsk ->
t1 <= job_arrival j < t2 ->
j \in task_arrivals_between arr_seq tsk t1 t2
    intros * ARR TSK INEQ.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t1, t2: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
INEQ: t1 <= job_arrival j < t2
j \in task_arrivals_between arr_seq tsk t1 t2
    rewrite mem_filter; apply/andP.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t1, t2: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
INEQ: t1 <= job_arrival j < t2
job_of_task tsk j /\
j \in arrivals_between arr_seq t1 t2
    split; first by apply /eqP => //.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t1, t2: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
INEQ: t1 <= job_arrival j < t2
j \in arrivals_between arr_seq t1 t2
    now apply arrived_between_implies_in_arrivals.
  Qed.

  (** Any job [j] in [task_arrivals_between arr_seq tsk t1 t2] is also
      contained in [arrivals_between arr_seq t1 t2]. *)
  Lemma task_arrivals_between_subset:
    forall t1 t2 j,
      j \in task_arrivals_between arr_seq tsk t1 t2 ->
      j \in arrivals_between arr_seq t1 t2.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (t1 t2 : instant) (j : Job),
j \in task_arrivals_between arr_seq tsk t1 t2 ->
j \in arrivals_between arr_seq t1 t2
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (t1 t2 : instant) (j : Job),
j \in task_arrivals_between arr_seq tsk t1 t2 ->
j \in arrivals_between arr_seq t1 t2 move=> t1 t2 j.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t1, t2: instant
j: Job
j \in task_arrivals_between arr_seq tsk t1 t2 ->
j \in arrivals_between arr_seq t1 t2 by rewrite mem_filter; move => /andP [/eqP TSK JB_IN]. Qed.

  (** Any job [j] in [task_arrivals_between arr_seq tsk t1 t2] arrives 
      in the arrival sequence [arr_seq]. *)
  Corollary arrives_in_task_arrivals_implies_arrived:
    forall t1 t2 j,
      j \in task_arrivals_between arr_seq tsk t1 t2 ->
      arrives_in arr_seq j.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (t1 t2 : instant) (j : Job),
j \in task_arrivals_between arr_seq tsk t1 t2 ->
arrives_in arr_seq j
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (t1 t2 : instant) (j : Job),
j \in task_arrivals_between arr_seq tsk t1 t2 ->
arrives_in arr_seq j move=> t1 t2 j IN; apply/in_arrivals_implies_arrived/task_arrivals_between_subset; exact IN. Qed.

  (** Any job [j] in [task_arrivals_before arr_seq tsk t] has an arrival
      time earlier than [t]. *)
  Lemma arrives_in_task_arrivals_before_implies_arrives_before :
    forall j t,
      j \in task_arrivals_before arr_seq tsk t ->
      job_arrival j < t.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (j : Job) (t : instant),
j \in task_arrivals_before arr_seq tsk t ->
job_arrival j < t
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (j : Job) (t : instant),
j \in task_arrivals_before arr_seq tsk t ->
job_arrival j < t
    intros * IN.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t: instant
IN: j \in task_arrivals_before arr_seq tsk t
job_arrival j < t
    unfold task_arrivals_before, task_arrivals_between in *.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t: instant
IN: j
  \in [seq j <- arrivals_between arr_seq 0 t
         | job_of_task tsk j]
job_arrival j < t
    move: IN; rewrite mem_filter => /andP [_ IN].Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t: instant
IN: j \in arrivals_between arr_seq 0 t
job_arrival j < t
    by apply in_arrivals_implies_arrived_between in IN => //.
  Qed.

  (** Any job [j] in [task_arrivals_before arr_seq tsk t] is a job of task [tsk]. *)
  Lemma arrives_in_task_arrivals_implies_job_task :
    forall j t,
      j \in task_arrivals_before arr_seq tsk t ->
      job_task j == tsk.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (j : Job) (t : instant),
j \in task_arrivals_before arr_seq tsk t ->
job_task j == tsk
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (j : Job) (t : instant),
j \in task_arrivals_before arr_seq tsk t ->
job_task j == tsk
    intros * IN.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t: instant
IN: j \in task_arrivals_before arr_seq tsk t
job_task j == tsk
    unfold task_arrivals_before, task_arrivals_between in *.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t: instant
IN: j
  \in [seq j <- arrivals_between arr_seq 0 t
         | job_of_task tsk j]
job_task j == tsk
    by move: IN; rewrite mem_filter => /andP [TSK _].
  Qed.

  (** We repeat the observation for [task_arrivals_between]. *)
  Lemma in_task_arrivals_between_implies_job_of_task :
    forall t1 t2 j,
      j \in task_arrivals_between arr_seq tsk t1 t2 ->
      job_task j = tsk.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (t1 t2 : instant) (j : Job),
j \in task_arrivals_between arr_seq tsk t1 t2 ->
job_task j = tsk
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (t1 t2 : instant) (j : Job),
j \in task_arrivals_between arr_seq tsk t1 t2 ->
job_task j = tsk
    move=> t1 t2 j.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t1, t2: instant
j: Job
j \in task_arrivals_between arr_seq tsk t1 t2 ->
job_task j = tsk
    rewrite mem_filter => /andP [JT _].Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t1, t2: instant
j: Job
JT: job_of_task tsk j
job_task j = tsk
    by move: JT; rewrite /job_of_task => /eqP.
  Qed.

  (** If a job arrives between to points in time, then the corresponding interval is nonempty... *)
  Lemma task_arrivals_nonempty :
    forall t1 t2 j,
      j \in task_arrivals_between arr_seq tsk t1 t2 ->
      t1 < t2.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (t1 t2 : instant) (j : Job),
j \in task_arrivals_between arr_seq tsk t1 t2 ->
t1 < t2
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (t1 t2 : instant) (j : Job),
j \in task_arrivals_between arr_seq tsk t1 t2 ->
t1 < t2 move=> t1 t2 j IN.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t1, t2: instant
j: Job
IN: j \in task_arrivals_between arr_seq tsk t1 t2
t1 < t2 by apply /(arrivals_between_nonempty arr_seq _ _ j)/task_arrivals_between_subset. Qed.

  (** ... which we can also express in terms of [number_of_task_arrivals] being nonzero. *)
  Corollary number_of_task_arrivals_nonzero :
    forall t1 t2,
      number_of_task_arrivals arr_seq tsk t1 t2 > 0 ->
      t1 < t2.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall t1 t2 : instant,
0 < number_of_task_arrivals arr_seq tsk t1 t2 ->
t1 < t2
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall t1 t2 : instant,
0 < number_of_task_arrivals arr_seq tsk t1 t2 ->
t1 < t2 by move=> t1 t2; rewrite -has_predT => /hasP [j IN] _; eapply task_arrivals_nonempty; eauto. Qed.

  (** An arrival sequence with non-duplicate arrivals implies that the 
      task arrivals also contain non-duplicate arrivals. *)
  Lemma uniq_task_arrivals:
    forall t,
      arrival_sequence_uniq arr_seq ->
      uniq (task_arrivals_up_to arr_seq tsk t).Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall t : instant,
arrival_sequence_uniq arr_seq ->
uniq (task_arrivals_up_to arr_seq tsk t)
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall t : instant,
arrival_sequence_uniq arr_seq ->
uniq (task_arrivals_up_to arr_seq tsk t)
    intros * UNQ_SEQ.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t: instant
UNQ_SEQ: arrival_sequence_uniq arr_seq
uniq (task_arrivals_up_to arr_seq tsk t)
    apply filter_uniq.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t: instant
UNQ_SEQ: arrival_sequence_uniq arr_seq
uniq (arrivals_between arr_seq 0 t.+1)
    now apply arrivals_uniq.
  Qed.

  (** The same observation applies to [task_arrivals_between]. *)
  Lemma task_arrivals_between_uniq :
    forall t1 t2,
      arrival_sequence_uniq arr_seq ->
      uniq (task_arrivals_between arr_seq tsk t1 t2).Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall t1 t2 : instant,
arrival_sequence_uniq arr_seq ->
uniq (task_arrivals_between arr_seq tsk t1 t2)
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall t1 t2 : instant,
arrival_sequence_uniq arr_seq ->
uniq (task_arrivals_between arr_seq tsk t1 t2) move=> t1 t2 UNIQ.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t1, t2: instant
UNIQ: arrival_sequence_uniq arr_seq
uniq (task_arrivals_between arr_seq tsk t1 t2) by apply/filter_uniq/arrivals_uniq. Qed.
  
  (** A job cannot arrive before it's arrival time. *) 
  Lemma job_notin_task_arrivals_before :
    forall j t, 
      arrives_in arr_seq j ->
      job_arrival j > t ->
      j \notin task_arrivals_up_to arr_seq (job_task j) t.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (j : Job) (t : nat),
arrives_in arr_seq j ->
t < job_arrival j ->
j \notin task_arrivals_up_to arr_seq (job_task j) t
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (j : Job) (t : nat),
arrives_in arr_seq j ->
t < job_arrival j ->
j \notin task_arrivals_up_to arr_seq (job_task j) t
    intros j t ARR INEQ.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t: nat
ARR: arrives_in arr_seq j
INEQ: t < job_arrival j
j \notin task_arrivals_up_to arr_seq (job_task j) t
    apply /negP; rewrite mem_filter => /andP [_ IN].Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t: nat
ARR: arrives_in arr_seq j
INEQ: t < job_arrival j
IN: j \in arrivals_between arr_seq 0 t.+1
False
    apply mem_bigcat_nat_exists in IN; move : IN => [t' [IN NEQt']].Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t: nat
ARR: arrives_in arr_seq j
INEQ: t < job_arrival j
t': nat
IN: j \in arrivals_at arr_seq t'
NEQt': 0 <= t' < t.+1
False
    rewrite -(H_consistent_arrivals j t') in NEQt' => //.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j: Job
t: nat
ARR: arrives_in arr_seq j
INEQ: t < job_arrival j
t': nat
IN: j \in arrivals_at arr_seq t'
NEQt': 0 <= job_arrival j < t.+1
False
    now lia.
  Qed.

  (** We show that for any two jobs [j1] and [j2], task arrivals up to arrival of job [j1] form a 
      strict prefix of task arrivals up to arrival of job [j2]. *)
  Lemma arrival_lt_implies_strict_prefix:
    forall j1 j2,
      job_task j1 = tsk ->
      job_task j2 = tsk ->
      arrives_in arr_seq j1 ->
      arrives_in arr_seq j2 -> 
      job_arrival j1 < job_arrival j2 ->
      strict_prefix_of (task_arrivals_up_to_job_arrival arr_seq j1) (task_arrivals_up_to_job_arrival arr_seq j2).Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
strict_prefix_of
  (task_arrivals_up_to_job_arrival arr_seq j1)
  (task_arrivals_up_to_job_arrival arr_seq j2)
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
strict_prefix_of
  (task_arrivals_up_to_job_arrival arr_seq j1)
  (task_arrivals_up_to_job_arrival arr_seq j2)
    intros j1 j2 TSK1 TSK2 ARR_1 ARR_2 ARR_INEQ.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
strict_prefix_of
  (task_arrivals_up_to_job_arrival arr_seq j1)
  (task_arrivals_up_to_job_arrival arr_seq j2)
    exists (task_arrivals_between arr_seq tsk ((job_arrival j1).+1) ((job_arrival j2).+1)).Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
task_arrivals_between arr_seq tsk (job_arrival j1).+1
  (job_arrival j2).+1 <> [::] /\
task_arrivals_up_to_job_arrival arr_seq j1 ++
task_arrivals_between arr_seq tsk (job_arrival j1).+1
  (job_arrival j2).+1 =
task_arrivals_up_to_job_arrival arr_seq j2
    split.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
task_arrivals_between arr_seq tsk (job_arrival j1).+1
  (job_arrival j2).+1 <> [::]
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
task_arrivals_up_to_job_arrival arr_seq j1 ++
task_arrivals_between arr_seq tsk 
  (job_arrival j1).+1 (job_arrival j2).+1 =
task_arrivals_up_to_job_arrival arr_seq j2
    -Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
task_arrivals_between arr_seq tsk (job_arrival j1).+1
  (job_arrival j2).+1 <> [::]
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
task_arrivals_up_to_job_arrival arr_seq j1 ++
task_arrivals_between arr_seq tsk 
  (job_arrival j1).+1 (job_arrival j2).+1 =
task_arrivals_up_to_job_arrival arr_seq j2 move: (in_nil j2) => /negP => JIN NIL.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
JIN: ~ j2 \in [::]
NIL: task_arrivals_between arr_seq tsk
  (job_arrival j1).+1 (job_arrival j2).+1 = [::]
False
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
task_arrivals_up_to_job_arrival arr_seq j1 ++
task_arrivals_between arr_seq tsk 
  (job_arrival j1).+1 (job_arrival j2).+1 =
task_arrivals_up_to_job_arrival arr_seq j2
      rewrite -NIL in JIN; contradict JIN.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
NIL: task_arrivals_between arr_seq tsk
  (job_arrival j1).+1 (job_arrival j2).+1 = [::]
j2
  \in task_arrivals_between arr_seq tsk
        (job_arrival j1).+1 (job_arrival j2).+1
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
task_arrivals_up_to_job_arrival arr_seq j1 ++
task_arrivals_between arr_seq tsk 
  (job_arrival j1).+1 (job_arrival j2).+1 =
task_arrivals_up_to_job_arrival arr_seq j2
      now apply job_in_task_arrivals_between => //; lia.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
task_arrivals_up_to_job_arrival arr_seq j1 ++
task_arrivals_between arr_seq tsk (job_arrival j1).+1
  (job_arrival j2).+1 =
task_arrivals_up_to_job_arrival arr_seq j2
    -Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
task_arrivals_up_to_job_arrival arr_seq j1 ++
task_arrivals_between arr_seq tsk (job_arrival j1).+1
  (job_arrival j2).+1 =
task_arrivals_up_to_job_arrival arr_seq j2 rewrite /task_arrivals_up_to_job_arrival TSK1 TSK2.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
j1, j2: Job
TSK1: job_task j1 = tsk
TSK2: job_task j2 = tsk
ARR_1: arrives_in arr_seq j1
ARR_2: arrives_in arr_seq j2
ARR_INEQ: job_arrival j1 < job_arrival j2
task_arrivals_up_to arr_seq tsk (job_arrival j1) ++
task_arrivals_between arr_seq tsk (job_arrival j1).+1
  (job_arrival j2).+1 =
task_arrivals_up_to arr_seq tsk (job_arrival j2)
      now rewrite -task_arrivals_cat; try by lia.
  Qed.

  (** For any job [j2] with [job_index] equal to [n], the nth job 
   in the sequence [task_arrivals_up_to arr_seq tsk t] is [j2], given that
   [t] is not less than [job_arrival j2]. *)
  (** Note that [j_def] is used as a default job for the access function and
   has nothing to do with the lemma. *)
  Lemma nth_job_of_task_arrivals:
    forall n j_def j t,
      arrives_in arr_seq j ->
      job_task j = tsk ->
      job_index arr_seq j = n ->
      t >= job_arrival j ->
      nth j_def (task_arrivals_up_to arr_seq tsk t) n = j.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (n : nat) (j_def j : Job) (t : nat),
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = n ->
job_arrival j <= t ->
nth j_def (task_arrivals_up_to arr_seq tsk t) n = j
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall (n : nat) (j_def j : Job) (t : nat),
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = n ->
job_arrival j <= t ->
nth j_def (task_arrivals_up_to arr_seq tsk t) n = j
    intros * ARR TSK IND T_G.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
nth j_def (task_arrivals_up_to arr_seq tsk t) n = j
    rewrite -IND.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
nth j_def (task_arrivals_up_to arr_seq tsk t)
  (job_index arr_seq j) = j
    have EQ_IND : index j (task_arrivals_up_to_job_arrival arr_seq j) = index j (task_arrivals_up_to arr_seq tsk t).Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
index j (task_arrivals_up_to_job_arrival arr_seq j) =
index j (task_arrivals_up_to arr_seq tsk t)
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
EQ_IND: index j
  (task_arrivals_up_to_job_arrival arr_seq j) =
index j (task_arrivals_up_to arr_seq tsk t)
nth j_def (task_arrivals_up_to arr_seq tsk t)
  (job_index arr_seq j) = j
    {Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
index j (task_arrivals_up_to_job_arrival arr_seq j) =
index j (task_arrivals_up_to arr_seq tsk t) have CAT : exists xs, task_arrivals_up_to_job_arrival arr_seq j ++ xs = task_arrivals_up_to arr_seq tsk t.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
exists xs : seq Job,
  task_arrivals_up_to_job_arrival arr_seq j ++ xs =
  task_arrivals_up_to arr_seq tsk t
Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
CAT: exists xs : seq Job,
  task_arrivals_up_to_job_arrival arr_seq j ++
  xs = task_arrivals_up_to arr_seq tsk t
index j (task_arrivals_up_to_job_arrival arr_seq j) =
index j (task_arrivals_up_to arr_seq tsk t)
      {Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
exists xs : seq Job,
  task_arrivals_up_to_job_arrival arr_seq j ++ xs =
  task_arrivals_up_to arr_seq tsk t rewrite /task_arrivals_up_to_job_arrival TSK.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
exists xs : seq Job,
  task_arrivals_up_to arr_seq tsk (job_arrival j) ++
  xs = task_arrivals_up_to arr_seq tsk t
        exists (task_arrivals_between arr_seq tsk ((job_arrival j).+1) t.+1).Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
task_arrivals_up_to arr_seq tsk (job_arrival j) ++
task_arrivals_between arr_seq tsk (job_arrival j).+1
  t.+1 = task_arrivals_up_to arr_seq tsk t
        now rewrite -task_arrivals_cat.
      }Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
CAT: exists xs : seq Job,
  task_arrivals_up_to_job_arrival arr_seq j ++
  xs = task_arrivals_up_to arr_seq tsk t
index j (task_arrivals_up_to_job_arrival arr_seq j) =
index j (task_arrivals_up_to arr_seq tsk t)
      move : CAT => [xs ARR_CAT].Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
xs: seq Job
ARR_CAT: task_arrivals_up_to_job_arrival arr_seq j ++
xs = task_arrivals_up_to arr_seq tsk t
index j (task_arrivals_up_to_job_arrival arr_seq j) =
index j (task_arrivals_up_to arr_seq tsk t)
      now rewrite -ARR_CAT index_cat ifT; last by apply arrives_in_task_arrivals_up_to.
    }Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
EQ_IND: index j
  (task_arrivals_up_to_job_arrival arr_seq j) =
index j (task_arrivals_up_to arr_seq tsk t)
nth j_def (task_arrivals_up_to arr_seq tsk t)
  (job_index arr_seq j) = j
    rewrite /job_index EQ_IND nth_index => //.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
EQ_IND: index j
  (task_arrivals_up_to_job_arrival arr_seq j) =
index j (task_arrivals_up_to arr_seq tsk t)
j \in task_arrivals_up_to arr_seq tsk t
    rewrite mem_filter; apply /andP.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
EQ_IND: index j
  (task_arrivals_up_to_job_arrival arr_seq j) =
index j (task_arrivals_up_to arr_seq tsk t)
job_of_task tsk j /\
j \in arrivals_between arr_seq 0 t.+1
    split; first by apply /eqP.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
n: nat
j_def, j: Job
t: nat
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: job_index arr_seq j = n
T_G: job_arrival j <= t
EQ_IND: index j
  (task_arrivals_up_to_job_arrival arr_seq j) =
index j (task_arrivals_up_to arr_seq tsk t)
j \in arrivals_between arr_seq 0 t.+1
    now apply job_in_arrivals_between => //.
  Qed.

  (** We show that task arrivals in the interval <<[t1, t2)>> 
   is the same as concatenation of task arrivals at each instant in <<[t1, t2)>>. *)
  Lemma task_arrivals_between_is_cat_of_task_arrivals_at:
    forall t1 t2,
      task_arrivals_between arr_seq tsk t1 t2 = \cat_(t1 <= t < t2) task_arrivals_at arr_seq tsk t.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall t1 t2 : instant,
task_arrivals_between arr_seq tsk t1 t2 =
\cat_(t1<=t<t2)task_arrivals_at arr_seq tsk t
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall t1 t2 : instant,
task_arrivals_between arr_seq tsk t1 t2 =
\cat_(t1<=t<t2)task_arrivals_at arr_seq tsk t
    intros *.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t1, t2: instant
task_arrivals_between arr_seq tsk t1 t2 =
\cat_(t1<=t<t2)task_arrivals_at arr_seq tsk t
    rewrite /task_arrivals_between /task_arrivals_at /arrivals_between.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t1, t2: instant
[seq j <- \cat_(t1<=t<t2)arrivals_at arr_seq t
   | job_of_task tsk j] =
\cat_(t1<=t<t2)
 [seq j <- arrivals_at arr_seq t | job_of_task tsk j]
    now apply bigcat_nat_filter_eq_filter_bigcat_nat.
  Qed.

  (** The number of jobs of a task [tsk] in the interval <<[t1, t2)>> is the same 
   as sum of the number of jobs of the task [tsk] at each instant in <<[t1, t2)>>. *)
  Lemma size_of_task_arrivals_between:
    forall t1 t2,
      size (task_arrivals_between arr_seq tsk t1 t2)
      = \sum_(t1 <= t < t2) size (task_arrivals_at arr_seq tsk t).Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall t1 t2 : instant,
size (task_arrivals_between arr_seq tsk t1 t2) =
\sum_(t1 <= t < t2)
   size (task_arrivals_at arr_seq tsk t) 
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall t1 t2 : instant,
size (task_arrivals_between arr_seq tsk t1 t2) =
\sum_(t1 <= t < t2)
   size (task_arrivals_at arr_seq tsk t)
    intros *.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t1, t2: instant
size (task_arrivals_between arr_seq tsk t1 t2) =
\sum_(t1 <= t < t2)
   size (task_arrivals_at arr_seq tsk t)
    rewrite /task_arrivals_between /task_arrivals_at /arrivals_between.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t1, t2: instant
size
  [seq j <- \cat_(t1<=t<t2)arrivals_at arr_seq t
     | job_of_task tsk j] =
\sum_(t1 <= t < t2)
   size
     [seq j <- arrivals_at arr_seq t
        | job_of_task tsk j]
    now rewrite size_big_nat bigcat_nat_filter_eq_filter_bigcat_nat.
  Qed.

  (** We note that, trivially, the list of task arrivals
      [task_arrivals_between] is sorted by arrival times because the
      underlying [arrivals_between] is sorted, as established by the
      lemma [arrivals_between_sorted]. *)
  Corollary task_arrivals_between_sorted :
    forall t1 t2,
      sorted by_arrival_times (task_arrivals_between arr_seq tsk t1 t2).Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall t1 t2 : instant,
sorted by_arrival_times
  (task_arrivals_between arr_seq tsk t1 t2)
  Proof.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
forall t1 t2 : instant,
sorted by_arrival_times
  (task_arrivals_between arr_seq tsk t1 t2)
    move=> t1 t2.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t1, t2: instant
sorted by_arrival_times
  (task_arrivals_between arr_seq tsk t1 t2) apply sorted_filter;
      first by rewrite /by_arrival_times /transitive; lia.Job: JobType
Task: TaskType
H: JobTask Job Task
H0: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times
  arr_seq
tsk: Task
t1, t2: instant
sorted by_arrival_times
  (arrivals_between arr_seq t1 t2)
    exact: arrivals_between_sorted.
  Qed.

End TaskArrivals.