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

(** * Arrival Sequence *)

(** First, we relate the stronger to the weaker arrival predicates. *)
Section ArrivalPredicates.

  (** Consider any kinds of jobs with arrival times. *)
  Context {Job : JobType} `{JobArrival Job}.

  (** A job that arrives in some interval <<[t1, t2)>> certainly arrives before
      time [t2]. *)
  Lemma arrived_between_before:
    forall j t1 t2,
      arrived_between j t1 t2 ->
      arrived_before j t2.
Job: JobType
H: JobArrival Job
forall (j : Job) (t1 t2 : instant),
arrived_between j t1 t2 -> arrived_before j t2
  Proof.
Job: JobType
H: JobArrival Job
forall (j : Job) (t1 t2 : instant),
arrived_between j t1 t2 -> arrived_before j t2 by move=> ? ? ? /andP[]. Qed.

  (** A job that arrives before a time [t] certainly has arrived by time
      [t]. *)
  Lemma arrived_before_has_arrived:
    forall j t,
      arrived_before j t ->
      has_arrived j t.
Job: JobType
H: JobArrival Job
forall (j : Job) (t : instant),
arrived_before j t -> has_arrived j t
  Proof.
Job: JobType
H: JobArrival Job
forall (j : Job) (t : instant),
arrived_before j t -> has_arrived j t move=> ? ?; exact: ltnW. Qed.

  (** Furthermore, we restate a common hypothesis to make its
      implication easier to discover. *)
  Lemma consistent_times_valid_arrival :
    forall arr_seq,
      valid_arrival_sequence arr_seq -> consistent_arrival_times arr_seq.
Job: JobType
H: JobArrival Job
forall arr_seq : arrival_sequence Job,
valid_arrival_sequence arr_seq ->
consistent_arrival_times arr_seq
  Proof.
Job: JobType
H: JobArrival Job
forall arr_seq : arrival_sequence Job,
valid_arrival_sequence arr_seq ->
consistent_arrival_times arr_seq by move=> ? []. Qed.

  (** We restate another common hypothesis to make its implication
      easier to discover. *)
  Lemma uniq_valid_arrival :
    forall arr_seq,
      valid_arrival_sequence arr_seq -> arrival_sequence_uniq arr_seq.
Job: JobType
H: JobArrival Job
forall arr_seq : arrival_sequence Job,
valid_arrival_sequence arr_seq ->
arrival_sequence_uniq arr_seq
  Proof.
Job: JobType
H: JobArrival Job
forall arr_seq : arrival_sequence Job,
valid_arrival_sequence arr_seq ->
arrival_sequence_uniq arr_seq by move=> ? []. Qed.

End ArrivalPredicates.

(** In this section, we relate job readiness to [has_arrived]. *)
Section Arrived.

  (** Consider any kinds of jobs and any kind of processor state. *)
  Context {Job : JobType} {PState : ProcessorState Job}.

  (** Consider any schedule... *)
  Variable sched : schedule PState.

  (** ...and suppose that jobs have a cost, an arrival time, and a
      notion of readiness. *)
  Context `{JobCost Job}.
  Context `{JobArrival Job}.
  Context {jr : JobReady Job PState}.

  (** First, we note that readiness models are by definition consistent
      w.r.t. [pending]. *)
  Lemma any_ready_job_is_pending:
    forall j t,
      job_ready sched j t -> pending sched j t.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
forall (j : Job) (t : instant),
job_ready sched j t -> pending sched j t
  Proof.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
forall (j : Job) (t : instant),
job_ready sched j t -> pending sched j t move: jr => [? +] /= ?; exact. Qed.

  (** Next, we observe that a given job must have arrived to be ready... *)
  Lemma ready_implies_arrived :
    forall j t, job_ready sched j t -> has_arrived j t.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
forall (j : Job) (t : instant),
job_ready sched j t -> has_arrived j t
  Proof.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
forall (j : Job) (t : instant),
job_ready sched j t -> has_arrived j t by move=> ? ? /any_ready_job_is_pending => /andP[]. Qed.

  (** ...and lift this observation also to the level of whole schedules. *)
  Lemma jobs_must_arrive_to_be_ready:
    jobs_must_be_ready_to_execute sched -> jobs_must_arrive_to_execute sched.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
jobs_must_be_ready_to_execute sched ->
jobs_must_arrive_to_execute sched
  Proof.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
jobs_must_be_ready_to_execute sched ->
jobs_must_arrive_to_execute sched move=> READY ? ? ?; exact/ready_implies_arrived/READY. Qed.

  (** Furthermore, in a valid schedule, jobs must arrive to execute. *)
  Corollary valid_schedule_implies_jobs_must_arrive_to_execute :
    forall arr_seq,
      valid_schedule sched arr_seq -> jobs_must_arrive_to_execute sched.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
forall arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
jobs_must_arrive_to_execute sched
  Proof.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
forall arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
jobs_must_arrive_to_execute sched move=> ? [? ?]; exact: jobs_must_arrive_to_be_ready. Qed.

  (** Since backlogged jobs are by definition ready, any backlogged job must have arrived. *)
  Corollary backlogged_implies_arrived:
    forall j t,
      backlogged sched j t -> has_arrived j t.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
forall (j : Job) (t : instant),
backlogged sched j t -> has_arrived j t
  Proof.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
forall (j : Job) (t : instant),
backlogged sched j t -> has_arrived j t move=> ? ? /andP[? ?]; exact: ready_implies_arrived. Qed.

  (** Similarly, since backlogged jobs are by definition pending, any
      backlogged job must be incomplete. *)
  Lemma backlogged_implies_incomplete:
    forall j t,
      backlogged sched j t -> ~~ completed_by sched j t.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
forall (j : Job) (t : instant),
backlogged sched j t -> ~~ completed_by sched j t
  Proof.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
forall (j : Job) (t : instant),
backlogged sched j t -> ~~ completed_by sched j t by move=> ? ? /andP[/any_ready_job_is_pending /andP[]]. Qed.

  (** Finally, we restate common hypotheses on the well-formedness of
      schedules to make their implications more easily
      discoverable. First, on the readiness of scheduled jobs, ... *)
  Lemma job_scheduled_implies_ready :
    jobs_must_be_ready_to_execute sched ->
    forall j t,
      scheduled_at sched j t -> job_ready sched j t.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
jobs_must_be_ready_to_execute sched ->
forall (j : Job) (t : instant),
scheduled_at sched j t -> job_ready sched j t
  Proof.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
jobs_must_be_ready_to_execute sched ->
forall (j : Job) (t : instant),
scheduled_at sched j t -> job_ready sched j t exact. Qed.

  (** ... second, on the origin of scheduled jobs, and ... *)
  Lemma valid_schedule_jobs_come_from_arrival_sequence :
    forall arr_seq,
      valid_schedule sched arr_seq ->
      jobs_come_from_arrival_sequence sched arr_seq.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
forall arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
jobs_come_from_arrival_sequence sched arr_seq
  Proof.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
forall arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
jobs_come_from_arrival_sequence sched arr_seq by move=> ? []. Qed.

  (** ... third, on the readiness of jobs in valid schedules. *)
  Lemma valid_schedule_jobs_must_be_ready_to_execute :
    forall arr_seq,
      valid_schedule sched arr_seq -> jobs_must_be_ready_to_execute sched.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
forall arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
jobs_must_be_ready_to_execute sched
  Proof.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
forall arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
jobs_must_be_ready_to_execute sched by move=> ? []. Qed.

End Arrived.

(** In this section, we establish useful facts about arrival sequence prefixes. *)
Section ArrivalSequencePrefix.

  (** Consider any kind of tasks and jobs. *)
  Context {Job: JobType}.
  Context {Task : TaskType}.
  Context `{JobArrival Job}.
  Context `{JobTask Job Task}.

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

  (** We begin with basic lemmas for manipulating the sequences. *)
  Section Composition.

    (** We show that the set of arriving jobs can be split
         into disjoint intervals. *)
    Lemma arrivals_between_cat:
      forall t1 t t2,
        t1 <= t ->
        t <= t2 ->
        arrivals_between arr_seq t1 t2 =
        arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
forall t1 t t2 : nat,
t1 <= t ->
t <= t2 ->
arrivals_between arr_seq t1 t2 =
arrivals_between arr_seq t1 t ++
arrivals_between arr_seq t t2
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
forall t1 t t2 : nat,
t1 <= t ->
t <= t2 ->
arrivals_between arr_seq t1 t2 =
arrivals_between arr_seq t1 t ++
arrivals_between arr_seq t t2 by move=> ? ? ? ? ?; rewrite -big_cat_nat. Qed.

    (** We also prove a stronger version of the above lemma
     in the case of arrivals that satisfy a predicate [P]. *)
    Lemma arrivals_P_cat:
      forall P t t1 t2,
        t1 <= t < t2 ->
        arrivals_between_P arr_seq P t1 t2 =
        arrivals_between_P arr_seq P t1 t ++ arrivals_between_P arr_seq P t t2.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
forall (P : Job -> bool) (t t1 t2 : nat),
t1 <= t < t2 ->
arrivals_between_P arr_seq P t1 t2 =
arrivals_between_P arr_seq P t1 t ++
arrivals_between_P arr_seq P t t2
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
forall (P : Job -> bool) (t t1 t2 : nat),
t1 <= t < t2 ->
arrivals_between_P arr_seq P t1 t2 =
arrivals_between_P arr_seq P t1 t ++
arrivals_between_P arr_seq P t t2
      move=> P t t1 t2.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
P: Job -> bool
t, t1, t2: nat
t1 <= t < t2 ->
arrivals_between_P arr_seq P t1 t2 =
arrivals_between_P arr_seq P t1 t ++
arrivals_between_P arr_seq P t t2
      by move=> /andP[? ?]; rewrite -filter_cat -arrivals_between_cat// ltnW.
    Qed.

    (** The same observation applies to membership in the set of
         arrived jobs. *)
    Lemma arrivals_between_mem_cat:
      forall j t1 t t2,
        t1 <= t ->
        t <= t2 ->
        j \in arrivals_between arr_seq t1 t2 =
        (j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
forall (j : Job) (t1 t t2 : nat),
t1 <= t ->
t <= t2 ->
(j \in arrivals_between arr_seq t1 t2) =
(j
   \in arrivals_between arr_seq t1 t ++
       arrivals_between arr_seq t t2)
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
forall (j : Job) (t1 t t2 : nat),
t1 <= t ->
t <= t2 ->
(j \in arrivals_between arr_seq t1 t2) =
(j
   \in arrivals_between arr_seq t1 t ++
       arrivals_between arr_seq t t2) by move=> ? ? ? ? ? ?; rewrite -arrivals_between_cat. Qed.

    (** We observe that we can grow the considered interval without
         "losing" any arrived jobs, i.e., membership in the set of arrived jobs
         is monotonic. *)
    Lemma arrivals_between_sub :
      forall j t1 t1' t2 t2',
        t1' <= t1 ->
        t2 <= t2' ->
        j \in arrivals_between arr_seq t1 t2 ->
        j \in arrivals_between arr_seq t1' t2'.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
forall (j : Job) (t1 t1' t2 t2' : nat),
t1' <= t1 ->
t2 <= t2' ->
j \in arrivals_between arr_seq t1 t2 ->
j \in arrivals_between arr_seq t1' t2'
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
forall (j : Job) (t1 t1' t2 t2' : nat),
t1' <= t1 ->
t2 <= t2' ->
j \in arrivals_between arr_seq t1 t2 ->
j \in arrivals_between arr_seq t1' t2'
      move=> j t1 t1' t2 t2' t1'_le_t1 t2_le_t2' j_in.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
j \in arrivals_between arr_seq t1' t2'
      have /orP[t2_le_t1|t1_le_t2] := leq_total t2 t1.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t2_le_t1: t2 <= t1
j \in arrivals_between arr_seq t1' t2'
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t1_le_t2: t1 <= t2
j \in arrivals_between arr_seq t1' t2'
      {
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t2_le_t1: t2 <= t1
j \in arrivals_between arr_seq t1' t2' by move: j_in; rewrite /arrivals_between big_geq. }
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t1_le_t2: t1 <= t2
j \in arrivals_between arr_seq t1' t2'
      rewrite (arrivals_between_mem_cat _ _ t1)// ?mem_cat.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t1_le_t2: t1 <= t2
(j \in arrivals_between arr_seq t1' t1)
|| (j \in arrivals_between arr_seq t1 t2')
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t1_le_t2: t1 <= t2
t1 <= t2'
      2:{
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t1_le_t2: t1 <= t2
t1 <= t2' exact: leq_trans t2_le_t2'. }
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t1_le_t2: t1 <= t2
(j \in arrivals_between arr_seq t1' t1)
|| (j \in arrivals_between arr_seq t1 t2')
      rewrite [X in _ || X](arrivals_between_mem_cat _ _ t2)// mem_cat.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
j: Job
t1, t1', t2, t2': nat
t1'_le_t1: t1' <= t1
t2_le_t2': t2 <= t2'
j_in: j \in arrivals_between arr_seq t1 t2
t1_le_t2: t1 <= t2
[|| j \in arrivals_between arr_seq t1' t1,
    j \in arrivals_between arr_seq t1 t2
  | j \in arrivals_between arr_seq t2 t2']
      by rewrite j_in orbT.
    Qed.

  End Composition.

  (** Next, we relate the arrival prefixes with job arrival times. *)
  Section ArrivalTimes.

    (** Assume that job arrival times are consistent. *)
    Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.

    (** To make the hypothesis and its implication easier to discover,
        we restate it as a trivial lemma. *)
    Lemma job_arrival_arrives_at :
      forall {j t},
        arrives_at arr_seq j t -> job_arrival j = t.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t : instant),
arrives_at arr_seq j t -> job_arrival j = t
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t : instant),
arrives_at arr_seq j t -> job_arrival j = t exact: H_consistent_arrival_times. Qed.

    (** Similarly, to simplify subsequent proofs, we restate the
        [H_consistent_arrival_times] assumption as a trivial
        corollary. *)
    Lemma job_arrival_at :
      forall {j t},
        j \in arrivals_at arr_seq t -> job_arrival j = t.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t : instant),
j \in arrivals_at arr_seq t -> job_arrival j = t
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t : instant),
j \in arrivals_at arr_seq t -> job_arrival j = t exact: H_consistent_arrival_times. Qed.

    (** Next, we  prove that if [j] is a part of the arrival sequence,
        then the converse of the above also holds. *)
    Lemma job_in_arrivals_at :
      forall j t,
        arrives_in arr_seq j ->
        job_arrival j = t ->
        j \in arrivals_at arr_seq t.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t : instant),
arrives_in arr_seq j ->
job_arrival j = t -> j \in arrivals_at arr_seq t
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t : instant),
arrives_in arr_seq j ->
job_arrival j = t -> j \in arrivals_at arr_seq t
      move => j t [t' IN] => /eqP.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t, t': instant
IN: j \in arrivals_at arr_seq t'
job_arrival j == t -> j \in arrivals_at arr_seq t
      apply contraTT => /negP NOTIN.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t, t': instant
IN: j \in arrivals_at arr_seq t'
NOTIN: ~ j \in arrivals_at arr_seq t
job_arrival j != t
      apply /neqP => ARR.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t, t': instant
IN: j \in arrivals_at arr_seq t'
NOTIN: ~ j \in arrivals_at arr_seq t
ARR: job_arrival j = t
False
      have ARR' := (H_consistent_arrival_times _ t' IN).
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t, t': instant
IN: j \in arrivals_at arr_seq t'
NOTIN: ~ j \in arrivals_at arr_seq t
ARR: job_arrival j = t
ARR': job_arrival j = t'
False
      by move: IN; rewrite -ARR' ARR.
    Qed.

    (** To begin with actual properties, we observe that any job in
        the set of all arrivals between time instants [t1] and [t2]
        must arrive in the interval <<[t1,t2)>>. *)
    Lemma job_arrival_between :
      forall {j t1 t2},
        j \in arrivals_between arr_seq t1 t2 -> t1 <= job_arrival j < t2.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
t1 <= job_arrival j < t2
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
t1 <= job_arrival j < t2 by move=> ? ? ? /mem_bigcat_nat_exists[i [/job_arrival_at <-]]. Qed.

    (** For convenience, we restate the left bound of the above lemma... *)
    Corollary job_arrival_between_ge :
      forall {j t1 t2},
        j \in arrivals_between arr_seq t1 t2 -> t1 <= job_arrival j.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
t1 <= job_arrival j
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
t1 <= job_arrival j by move=> ? ? ? /job_arrival_between/andP[]. Qed.

    (** ... as well as the right bound separately as corollaries. *)
    Corollary job_arrival_between_lt :
      forall {j t1 t2},
        j \in arrivals_between arr_seq t1 t2 -> job_arrival j < t2.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
job_arrival j < t2
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
job_arrival j < t2 by move=> ? ? ? /job_arrival_between/andP[]. Qed.

    (** Consequently, if we filter the list of arrivals in an interval
        <<[t1,t2)>> with an arrival-time threshold less than [t1], we are
        left with an empty list. *)
    Lemma arrivals_between_filter_nil :
      forall t1 t2 t,
        t < t1 ->
        [seq j <- arrivals_between arr_seq t1 t2 | job_arrival j < t] = [::].
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (t1 : nat) (t2 : instant) (t : nat),
t < t1 ->
[seq j <- arrivals_between arr_seq t1 t2
   | job_arrival j < t] = [::]
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (t1 : nat) (t2 : instant) (t : nat),
t < t1 ->
[seq j <- arrivals_between arr_seq t1 t2
   | job_arrival j < t] = [::]
      move=> t1 t2 t LT.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: nat
t2: instant
t: nat
LT: t < t1
[seq j <- arrivals_between arr_seq t1 t2
   | job_arrival j < t] = [::]
      case: (leqP t1 t2) => RANGE;
        last by rewrite /arrivals_between big_geq //=; lia.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: nat
t2: instant
t: nat
LT: t < t1
RANGE: t1 <= t2
[seq j <- arrivals_between arr_seq t1 t2
   | job_arrival j < t] = [::]
      rewrite filter_in_pred0 // => j IN.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: nat
t2: instant
t: nat
LT: t < t1
RANGE: t1 <= t2
j: Job
IN: j \in arrivals_between arr_seq t1 t2
~~ (job_arrival j < t)
      rewrite -ltnNge.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: nat
t2: instant
t: nat
LT: t < t1
RANGE: t1 <= t2
j: Job
IN: j \in arrivals_between arr_seq t1 t2
t < (job_arrival j).+1
      apply: (ltn_trans LT).
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: nat
t2: instant
t: nat
LT: t < t1
RANGE: t1 <= t2
j: Job
IN: j \in arrivals_between arr_seq t1 t2
t1 < (job_arrival j).+1
      rewrite ltnS.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: nat
t2: instant
t: nat
LT: t < t1
RANGE: t1 <= t2
j: Job
IN: j \in arrivals_between arr_seq t1 t2
t1 <= job_arrival j
      by apply: job_arrival_between_ge; eauto.
    Qed.

    (** Furthermore, if we filter the list of arrivals in an interval
        <<[t1,t2)>> with an arrival-time threshold less than [t2],
        we can simply discard the tail past the threshold. *)
    Lemma arrivals_between_filter :
      forall t1 t2 t,
        t <= t2 ->
        arrivals_between arr_seq t1 t
        = [seq j <- arrivals_between arr_seq t1 t2 | job_arrival j < t].
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (t1 : instant) (t2 t : nat),
t <= t2 ->
arrivals_between arr_seq t1 t =
[seq j <- arrivals_between arr_seq t1 t2
   | job_arrival j < t]
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (t1 : instant) (t2 t : nat),
t <= t2 ->
arrivals_between arr_seq t1 t =
[seq j <- arrivals_between arr_seq t1 t2
   | job_arrival j < t]
      move=> t1 t2 t LE2.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
arrivals_between arr_seq t1 t =
[seq j <- arrivals_between arr_seq t1 t2
   | job_arrival j < t]
      case: (leqP t1 t2) => RANGE;
        last by rewrite /arrivals_between !big_geq //=; lia.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
arrivals_between arr_seq t1 t =
[seq j <- arrivals_between arr_seq t1 t2
   | job_arrival j < t]
      case: (leqP t1 t) => LE1;
        last by rewrite [LHS]/arrivals_between big_geq; try lia; rewrite arrivals_between_filter_nil.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
arrivals_between arr_seq t1 t =
[seq j <- arrivals_between arr_seq t1 t2
   | job_arrival j < t]
      rewrite /arrivals_between bigcat_nat_filter_eq_filter_bigcat_nat.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
\cat_(t1<=t<t)arrivals_at arr_seq t =
\cat_(t1<=t0<t2)
 [seq x <- arrivals_at arr_seq t0 | job_arrival x < t]
      rewrite (big_cat_nat _ _ _ LE1 LE2) //=.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
\cat_(t1<=t<t)arrivals_at arr_seq t =
\cat_(t1<=i<t)
 [seq x <- arrivals_at arr_seq i | job_arrival x < t] ++
\cat_(t<=i<t2)
 [seq x <- arrivals_at arr_seq i | job_arrival x < t]
      rewrite !big_nat [X in _ ++ X]big1; last first.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
forall i : nat,
t <= i < t2 ->
[seq x <- arrivals_at arr_seq i | job_arrival x < t] =
[::]
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
\cat_(t1<=i<t|(t1 <= i < t))arrivals_at arr_seq i =
\cat_(t1<=i<t|(t1 <= i < t))
 [seq x <- arrivals_at arr_seq i | job_arrival x < t] ++
[::]
      {
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
forall i : nat,
t <= i < t2 ->
[seq x <- arrivals_at arr_seq i | job_arrival x < t] =
[::] move=> t' /andP[LO HI].
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
t': nat
LO: t <= t'
HI: t' < t2
[seq x <- arrivals_at arr_seq t' | job_arrival x < t] =
[::]
        rewrite filter_in_pred0 // => j IN.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
t': nat
LO: t <= t'
HI: t' < t2
j: Job
IN: j \in arrivals_at arr_seq t'
~~ (job_arrival j < t)
        have -> : job_arrival j = t' by apply: job_arrival_at; eauto.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
t': nat
LO: t <= t'
HI: t' < t2
j: Job
IN: j \in arrivals_at arr_seq t'
~~ (t' < t)
        rewrite -leqNgt.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
t': nat
LO: t <= t'
HI: t' < t2
j: Job
IN: j \in arrivals_at arr_seq t'
t <= t'
        exact: LO. }
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
\cat_(t1<=i<t|(t1 <= i < t))arrivals_at arr_seq i =
\cat_(t1<=i<t|(t1 <= i < t))
 [seq x <- arrivals_at arr_seq i | job_arrival x < t] ++
[::]
      {
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
\cat_(t1<=i<t|(t1 <= i < t))arrivals_at arr_seq i =
\cat_(t1<=i<t|(t1 <= i < t))
 [seq x <- arrivals_at arr_seq i | job_arrival x < t] ++
[::] rewrite cats0.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
\cat_(t1<=i<t|(t1 <= i < t))arrivals_at arr_seq i =
\cat_(t1<=i<t|(t1 <= i < t))
 [seq x <- arrivals_at arr_seq i | job_arrival x < t]
        apply: eq_bigr => t' /andP[LO HI].
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
t': nat
LO: t1 <= t'
HI: t' < t
arrivals_at arr_seq t' =
[seq x <- arrivals_at arr_seq t' | job_arrival x < t]
        apply esym.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
t': nat
LO: t1 <= t'
HI: t' < t
[seq x <- arrivals_at arr_seq t' | job_arrival x < t] =
arrivals_at arr_seq t'
        apply /all_filterP/allP => j IN.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
t': nat
LO: t1 <= t'
HI: t' < t
j: Job
IN: j \in arrivals_at arr_seq t'
job_arrival j < t
        have -> : job_arrival j = t' by apply: job_arrival_at; eauto.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2, t: nat
LE2: t <= t2
RANGE: t1 <= t2
LE1: t1 <= t
t': nat
LO: t1 <= t'
HI: t' < t
j: Job
IN: j \in arrivals_at arr_seq t'
t' < t
        exact: HI. }
    Qed.

    (** Next, we prove that if a job belongs to the prefix
        (jobs_arrived_before t), then it arrives in the arrival
        sequence. *)
    Lemma in_arrivals_implies_arrived:
      forall j t1 t2,
        j \in arrivals_between arr_seq t1 t2 ->
        arrives_in arr_seq j.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
arrives_in arr_seq j
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
arrives_in arr_seq j by move=> ? ? ? /mem_bigcat_nat_exists[arr [? _]]; exists arr. Qed.

    (** We also prove a weaker version of the above lemma. *)
    Lemma in_arrseq_implies_arrives:
      forall t j,
        j \in arr_seq t ->
        arrives_in arr_seq j.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (t : instant) (j : Job),
j \in arr_seq t -> arrives_in arr_seq j
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (t : instant) (j : Job),
j \in arr_seq t -> arrives_in arr_seq j by move=> t ? ?; exists t. Qed.

    (** Next, we prove that if a job belongs to the prefix
         (jobs_arrived_between t1 t2), then it indeed arrives between t1 and
         t2. *)
    Lemma in_arrivals_implies_arrived_between:
      forall j t1 t2,
        j \in arrivals_between arr_seq t1 t2 ->
        arrived_between j t1 t2.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
arrived_between j t1 t2
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
arrived_between j t1 t2 by move=> ? ? ? /mem_bigcat_nat_exists[t0 [/job_arrival_at <-]]. Qed.

    (** Similarly, if a job belongs to the prefix (jobs_arrived_before t),
           then it indeed arrives before time t. *)
    Lemma in_arrivals_implies_arrived_before:
      forall j t,
        j \in arrivals_before arr_seq t ->
        arrived_before j t.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t : instant),
j \in arrivals_before arr_seq t -> arrived_before j t
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t : instant),
j \in arrivals_before arr_seq t -> arrived_before j t by move=> ? ? /in_arrivals_implies_arrived_between. Qed.

    (** Similarly, we prove that if a job from the arrival sequence arrives
        before t, then it belongs to the sequence (jobs_arrived_before t). *)
    Lemma arrived_between_implies_in_arrivals:
      forall j t1 t2,
        arrives_in arr_seq j ->
        arrived_between j t1 t2 ->
        j \in arrivals_between arr_seq t1 t2.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t1 t2 : instant),
arrives_in arr_seq j ->
arrived_between j t1 t2 ->
j \in arrivals_between arr_seq t1 t2
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t1 t2 : instant),
arrives_in arr_seq j ->
arrived_between j t1 t2 ->
j \in arrivals_between arr_seq t1 t2
      move=> j t1 t2 [a_j arrj] before; apply: mem_bigcat_nat (arrj).
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t1, t2, a_j: instant
arrj: j \in arrivals_at arr_seq a_j
before: arrived_between j t1 t2
t1 <= a_j < t2
      by rewrite -(job_arrival_at arrj).
    Qed.

    (** Any job in arrivals between time instants [t1] and [t2] must arrive
       in the interval <<[t1,t2)>>. *)
    Lemma job_arrival_between_P:
      forall j P t1 t2,
        j \in arrivals_between_P arr_seq P t1 t2 ->
        t1 <= job_arrival j < t2.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (P : Job -> bool) (t1 t2 : instant),
j \in arrivals_between_P arr_seq P t1 t2 ->
t1 <= job_arrival j < t2
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (P : Job -> bool) (t1 t2 : instant),
j \in arrivals_between_P arr_seq P t1 t2 ->
t1 <= job_arrival j < t2
      move=> j P t1 t2.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
P: Job -> bool
t1, t2: instant
j \in arrivals_between_P arr_seq P t1 t2 ->
t1 <= job_arrival j < t2
      rewrite mem_filter => /andP[Pj /mem_bigcat_nat_exists[i [+ iitv]]].
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
P: Job -> bool
t1, t2: instant
Pj: P j
i: nat
iitv: t1 <= i < t2
j \in arrivals_at arr_seq i ->
t1 <= job_arrival j < t2
      by move=> /job_arrival_at ->.
    Qed.

    (** Any job [j] is in the sequence [arrivals_between t1 t2] given
     that [j] arrives in the interval <<[t1,t2)>>. *)
    Lemma job_in_arrivals_between:
      forall j t1 t2,
        arrives_in arr_seq j ->
        t1 <= job_arrival j < t2 ->
        j \in arrivals_between arr_seq t1 t2.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t1 t2 : nat),
arrives_in arr_seq j ->
t1 <= job_arrival j < t2 ->
j \in arrivals_between arr_seq t1 t2
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t1 t2 : nat),
arrives_in arr_seq j ->
t1 <= job_arrival j < t2 ->
j \in arrivals_between arr_seq t1 t2
      move=> j t1 t2 [t jarr] jitv; apply: mem_bigcat_nat (jarr).
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t1, t2: nat
t: instant
jarr: j \in arrivals_at arr_seq t
jitv: t1 <= job_arrival j < t2
t1 <= t < t2
      by rewrite -(job_arrival_at jarr).
    Qed.

    (** Next, we prove that if the arrival sequence doesn't contain duplicate
        jobs, the same applies for any of its prefixes. *)
    Lemma arrivals_uniq:
      arrival_sequence_uniq arr_seq ->
      forall t1 t2, uniq (arrivals_between arr_seq t1 t2).
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
arrival_sequence_uniq arr_seq ->
forall t1 t2 : instant,
uniq (arrivals_between arr_seq t1 t2)
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
arrival_sequence_uniq arr_seq ->
forall t1 t2 : instant,
uniq (arrivals_between arr_seq t1 t2)
      move=> SET t1 t2; apply: bigcat_nat_uniq => // j t1' t2'.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
SET: arrival_sequence_uniq arr_seq
t1, t2: instant
j: Job
t1', t2': nat
j \in arrivals_at arr_seq t1' ->
j \in arrivals_at arr_seq t2' -> t1' = t2'
      by move=> /job_arrival_at <- /job_arrival_at <-.
    Qed.

    (** Also note that there can't by any arrivals in an empty time interval. *)
    Lemma arrivals_between_geq:
      forall t1 t2,
        t1 >= t2 ->
        arrivals_between arr_seq t1 t2  = [::].
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall t1 t2 : nat,
t2 <= t1 -> arrivals_between arr_seq t1 t2 = [::]
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall t1 t2 : nat,
t2 <= t1 -> arrivals_between arr_seq t1 t2 = [::] by move=> ? ? ?; rewrite /arrivals_between big_geq. Qed.

    (** Conversely, if a job arrives, the considered interval is non-empty. *)
    Corollary arrivals_between_nonempty :
      forall t1 t2 j,
        j \in arrivals_between arr_seq t1 t2 -> t1 < t2.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (t1 t2 : instant) (j : Job),
j \in arrivals_between arr_seq t1 t2 -> t1 < t2
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (t1 t2 : instant) (j : Job),
j \in arrivals_between arr_seq t1 t2 -> t1 < t2 by move=> j1 j2 t; apply: contraPltn=> LEQ; rewrite arrivals_between_geq. Qed.

    (** Given jobs [j1] and [j2] in [arrivals_between_P arr_seq P t1 t2], the fact that
        [j2] arrives strictly before [j1] implies that [j2] also belongs in the sequence
        [arrivals_between_P arr_seq P t1 (job_arrival j1)]. *)
    Lemma arrival_lt_implies_job_in_arrivals_between_P :
      forall (j1 j2 : Job) (P : Job -> bool) (t1 t2 : instant),
        j1 \in arrivals_between_P arr_seq P t1 t2 ->
        j2 \in arrivals_between_P arr_seq P t1 t2 ->
        job_arrival j2 < job_arrival j1 ->
        j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1).
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j1 j2 : Job) (P : Job -> bool)
  (t1 t2 : instant),
j1 \in arrivals_between_P arr_seq P t1 t2 ->
j2 \in arrivals_between_P arr_seq P t1 t2 ->
job_arrival j2 < job_arrival j1 ->
j2
  \in arrivals_between_P arr_seq P t1 (job_arrival j1)
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j1 j2 : Job) (P : Job -> bool)
  (t1 t2 : instant),
j1 \in arrivals_between_P arr_seq P t1 t2 ->
j2 \in arrivals_between_P arr_seq P t1 t2 ->
job_arrival j2 < job_arrival j1 ->
j2
  \in arrivals_between_P arr_seq P t1 (job_arrival j1)
      move=> j1 j2 P t1 t2.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant
j1 \in arrivals_between_P arr_seq P t1 t2 ->
j2 \in arrivals_between_P arr_seq P t1 t2 ->
job_arrival j2 < job_arrival j1 ->
j2
  \in arrivals_between_P arr_seq P t1 (job_arrival j1)
      rewrite !mem_filter => /andP[_ j1arr] /andP[Pj2 j2arr] arr_lt.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant
j1arr: j1 \in arrivals_between arr_seq t1 t2
Pj2: P j2
j2arr: j2 \in arrivals_between arr_seq t1 t2
arr_lt: job_arrival j2 < job_arrival j1
P j2 &&
(j2 \in arrivals_between arr_seq t1 (job_arrival j1))
      rewrite Pj2/=; apply: job_in_arrivals_between.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant
j1arr: j1 \in arrivals_between arr_seq t1 t2
Pj2: P j2
j2arr: j2 \in arrivals_between arr_seq t1 t2
arr_lt: job_arrival j2 < job_arrival j1
arrives_in arr_seq j2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant
j1arr: j1 \in arrivals_between arr_seq t1 t2
Pj2: P j2
j2arr: j2 \in arrivals_between arr_seq t1 t2
arr_lt: job_arrival j2 < job_arrival j1
t1 <= job_arrival j2 < job_arrival j1
      -
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant
j1arr: j1 \in arrivals_between arr_seq t1 t2
Pj2: P j2
j2arr: j2 \in arrivals_between arr_seq t1 t2
arr_lt: job_arrival j2 < job_arrival j1
arrives_in arr_seq j2
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant
j1arr: j1 \in arrivals_between arr_seq t1 t2
Pj2: P j2
j2arr: j2 \in arrivals_between arr_seq t1 t2
arr_lt: job_arrival j2 < job_arrival j1
t1 <= job_arrival j2 < job_arrival j1 exact: in_arrivals_implies_arrived j2arr.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant
j1arr: j1 \in arrivals_between arr_seq t1 t2
Pj2: P j2
j2arr: j2 \in arrivals_between arr_seq t1 t2
arr_lt: job_arrival j2 < job_arrival j1
t1 <= job_arrival j2 < job_arrival j1
      -
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j1, j2: Job
P: Job -> bool
t1, t2: instant
j1arr: j1 \in arrivals_between arr_seq t1 t2
Pj2: P j2
j2arr: j2 \in arrivals_between arr_seq t1 t2
arr_lt: job_arrival j2 < job_arrival j1
t1 <= job_arrival j2 < job_arrival j1 by rewrite (job_arrival_between_ge j2arr).
    Qed.


    (** We observe that, by construction, the sequence of arrivals is
        sorted by arrival times. To this end, we first define the
        order relation. *)
    Definition by_arrival_times (j1 j2 : Job) : bool := job_arrival j1 <= job_arrival j2.

    (** Trivially, the arrivals at any one point in time are ordered
        w.r.t. arrival times. *)
    Lemma arrivals_at_sorted :
      forall t,
        sorted by_arrival_times (arrivals_at arr_seq t).
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall t : instant,
sorted by_arrival_times (arrivals_at arr_seq t)
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall t : instant,
sorted by_arrival_times (arrivals_at arr_seq t)
      move=> t.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t: instant
sorted by_arrival_times (arrivals_at arr_seq t)
      have AT_t : forall j, j \in (arrivals_at arr_seq t) -> job_arrival j = t
        by move=> j; apply job_arrival_at.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t: instant
AT_t: forall j : Job,
j \in arrivals_at arr_seq t ->
job_arrival j = t
sorted by_arrival_times (arrivals_at arr_seq t)
      case: (arrivals_at arr_seq t) AT_t => // j' js AT_t.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t: instant
j': Job
js: seq Job
AT_t: forall j : Job,
j \in j' :: js -> job_arrival j = t
sorted by_arrival_times (j' :: js)
      apply /(pathP j') => i LT.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t: instant
j': Job
js: seq Job
AT_t: forall j : Job,
j \in j' :: js -> job_arrival j = t
i: nat
LT: i < size js
by_arrival_times (nth j' (j' :: js) i) (nth j' js i)
      rewrite /by_arrival_times !AT_t //;
        last by apply mem_nth; auto.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t: instant
j': Job
js: seq Job
AT_t: forall j : Job,
j \in j' :: js -> job_arrival j = t
i: nat
LT: i < size js
nth j' js i \in j' :: js
      rewrite in_cons; apply /orP; right.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t: instant
j': Job
js: seq Job
AT_t: forall j : Job,
j \in j' :: js -> job_arrival j = t
i: nat
LT: i < size js
nth j' js i \in js
      by exact: mem_nth.
   Qed.

    (** By design, the list of arrivals in any interval is sorted. *)
    Lemma arrivals_between_sorted :
      forall t1 t2,
        sorted by_arrival_times (arrivals_between arr_seq t1 t2).
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall t1 t2 : instant,
sorted by_arrival_times
  (arrivals_between arr_seq t1 t2)
    Proof.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall t1 t2 : instant,
sorted by_arrival_times
  (arrivals_between arr_seq t1 t2)
      move=> t1 t2.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1, t2: instant
sorted by_arrival_times
  (arrivals_between arr_seq t1 t2)
      rewrite /arrivals_between.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1, t2: instant
sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
      elim: t2 => [|t2 SORTED];
        first by rewrite big_nil.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
sorted by_arrival_times
  (\cat_(t1<=t<t2.+1)arrivals_at arr_seq t)
      case: (leqP t1 t2) => T1T2;
        last by rewrite big_geq.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
sorted by_arrival_times
  (\cat_(t1<=t<t2.+1)arrivals_at arr_seq t)
      rewrite (big_cat_nat _ _ _ T1T2 _) //=.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
sorted by_arrival_times
  (\cat_(t1<=i<t2)arrivals_at arr_seq i ++
   \cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
      case A1: (\cat_(t1<=t<t2)arrivals_at arr_seq t) => [|j js];
        first by rewrite cat0s big_nat1; exact: arrivals_at_sorted.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
sorted by_arrival_times
  ((j :: js) ++
   \cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
      have CAT : path by_arrival_times j (\cat_(t1<=t<t2)arrivals_at arr_seq t ++ \cat_(t2<=i<t2.+1)arrivals_at arr_seq i).
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times j
  (\cat_(t1<=t<t2)arrivals_at arr_seq t ++
   \cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
CAT: path by_arrival_times j
  (\cat_(t1<=t<t2)arrivals_at arr_seq t ++
   \cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
sorted by_arrival_times
  ((j :: js) ++
   \cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
      {
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times j
  (\cat_(t1<=t<t2)arrivals_at arr_seq t ++
   \cat_(t2<=i<t2.+1)arrivals_at arr_seq i) rewrite cat_path; apply /andP; split.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times j
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times
  (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t))
  (\cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
        {
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times j
  (\cat_(t1<=t<t2)arrivals_at arr_seq t) move: SORTED.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t) ->
path by_arrival_times j
  (\cat_(t1<=t<t2)arrivals_at arr_seq t) rewrite /sorted A1 => PATH_js.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
PATH_js: path by_arrival_times j js
path by_arrival_times j (j :: js)
          by rewrite /path -/(path _ _ js) /by_arrival_times; apply /andP; split. }
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times
  (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t))
  (\cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
        {
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times
  (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t))
  (\cat_(t2<=i<t2.+1)arrivals_at arr_seq i) rewrite big_nat1.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
path by_arrival_times
  (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t))
  (arrivals_at arr_seq t2)
          case A2: (arrivals_at arr_seq t2) => // [j' js'].
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
path by_arrival_times
  (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t))
  (j' :: js')
          apply path_le with (x' := j').
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
transitive (T:=Job) by_arrival_times
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
by_arrival_times
  (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) j'
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
path by_arrival_times j' (j' :: js')
          {
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
transitive (T:=Job) by_arrival_times by rewrite /transitive/by_arrival_times; lia. }
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
by_arrival_times
  (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) j'
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
path by_arrival_times j' (j' :: js')
          {
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
by_arrival_times
  (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) j' rewrite /by_arrival_times.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
job_arrival
  (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) <=
job_arrival j'
            have -> : job_arrival j' = t2
              by apply job_arrival_at; rewrite A2; apply mem_head.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
job_arrival
  (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)) <=
t2
            set L := (last j (\cat_(t1<=t<t2)arrivals_at arr_seq t)).
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
L:= last j (\cat_(t1<=t<t2)arrivals_at arr_seq t): Job
job_arrival L <= t2
            have EX : exists t', L \in arrivals_at arr_seq t' /\ t1 <= t' < t2
              by apply mem_bigcat_nat_exists; rewrite /L A1 last_cons; exact: mem_last.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
L:= last j (\cat_(t1<=t<t2)arrivals_at arr_seq t): Job
EX: exists t' : instant,
  L \in arrivals_at arr_seq t' /\ t1 <= t' < t2
job_arrival L <= t2
            move: EX => [t' [IN /andP [t1t' t't2]]].
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
L:= last j (\cat_(t1<=t<t2)arrivals_at arr_seq t): Job
t': instant
IN: L \in arrivals_at arr_seq t'
t1t': t1 <= t'
t't2: t' < t2
job_arrival L <= t2
            have -> : job_arrival L = t' by apply job_arrival_at.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
L:= last j (\cat_(t1<=t<t2)arrivals_at arr_seq t): Job
t': instant
IN: L \in arrivals_at arr_seq t'
t1t': t1 <= t'
t't2: t' < t2
t' <= t2
            by lia. }
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
path by_arrival_times j' (j' :: js')
          {
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
path by_arrival_times j' (j' :: js') move: (arrivals_at_sorted t2); rewrite /sorted A2 => PATH'.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
PATH': path by_arrival_times j' js'
path by_arrival_times j' (j' :: js')
            rewrite /path -/(path _ _ js') {1}/by_arrival_times.
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
j': Job
js': seq Job
A2: arrivals_at arr_seq t2 = j' :: js'
PATH': path by_arrival_times j' js'
(job_arrival j' <= job_arrival j') &&
path by_arrival_times j' js'
            by apply /andP; split => //. } } }
Job: JobType
Task: TaskType
H: JobArrival Job
H0: JobTask Job Task
arr_seq: arrival_sequence Job
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
t1: instant
t2: nat
SORTED: sorted by_arrival_times
  (\cat_(t1<=t<t2)arrivals_at arr_seq t)
T1T2: t1 <= t2
j: Job
js: seq Job
A1: \cat_(t1<=t<t2)arrivals_at arr_seq t = j :: js
CAT: path by_arrival_times j
  (\cat_(t1<=t<t2)arrivals_at arr_seq t ++
   \cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
sorted by_arrival_times
  ((j :: js) ++
   \cat_(t2<=i<t2.+1)arrivals_at arr_seq i)
      by move: CAT; rewrite /sorted A1 cat_cons {1}/path -/(path _ _ (js ++ _)) => /andP [_ CAT].
   Qed.

  End ArrivalTimes.

End ArrivalSequencePrefix.

(** In this section, we establish a few auxiliary facts about the
    relation between the property of being scheduled and arrival
    predicates to facilitate automation. *)
Section ScheduledImpliesArrives.

  (** Consider any type of jobs. *)
  Context {Job : JobType}.
  Context `{JobArrival Job}.

  (** Consider any kind of processor state model, ... *)
  Context {PState : ProcessorState Job}.

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

  (** ... and any schedule of this arrival sequence ... *)
  Variable sched : schedule PState.
  Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.

  (** ... where jobs do not execute before their arrival. *)
  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.


  (** Next, consider a job [j] ... *)
  Variable j : Job.

  (** ... which is scheduled at a time instant [t]. *)
  Variable t : instant.
  Hypothesis H_scheduled_at : scheduled_at sched j t.

  (** Then we show that [j] arrives in [arr_seq]. *)
  Lemma arrives_in_jobs_come_from_arrival_sequence :
    arrives_in arr_seq j.
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
arrives_in arr_seq j
  Proof.
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
arrives_in arr_seq j
    by apply: H_jobs_come_from_arrival_sequence H_scheduled_at.
  Qed.

  (** Job [j] has arrived by time instant [t]. *)
  Lemma arrived_between_jobs_must_arrive_to_execute :
    has_arrived j t.
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
has_arrived j t
  Proof.
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
has_arrived j t
    by apply: H_jobs_must_arrive_to_execute H_scheduled_at.
  Qed.

  (** Finally, for any future time [t'], job [j] arrives before [t']. *)
  Lemma arrivals_before_scheduled_at :
    forall t',
      t < t' ->
      j \in arrivals_before arr_seq t'.
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
forall t' : nat,
t < t' -> j \in arrivals_before arr_seq t'
  Proof.
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
forall t' : nat,
t < t' -> j \in arrivals_before arr_seq t'
    move=> t' LTtt'.
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat
LTtt': t < t'
j \in arrivals_before arr_seq t'
    apply: arrived_between_implies_in_arrivals => //.
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat
LTtt': t < t'
arrives_in arr_seq j
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat
LTtt': t < t'
arrived_between j 0 t'
    -
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat
LTtt': t < t'
arrives_in arr_seq j
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat
LTtt': t < t'
arrived_between j 0 t' by apply: arrives_in_jobs_come_from_arrival_sequence.
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat
LTtt': t < t'
arrived_between j 0 t'
    -
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat
LTtt': t < t'
arrived_between j 0 t' apply: leq_ltn_trans LTtt'.
Job: JobType
H: JobArrival Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence
  sched arr_seq
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute
  sched
j: Job
t: instant
H_scheduled_at: scheduled_at sched j t
t': nat
job_arrival j <= t
      by apply: arrived_between_jobs_must_arrive_to_execute.
  Qed.

End ScheduledImpliesArrives.

(** We add some of the above lemmas to the "Hint Database"
    [basic_rt_facts], so the [auto] tactic will be able to use them. *)
Global Hint Resolve
       any_ready_job_is_pending
       arrivals_before_scheduled_at
       arrivals_uniq
       arrived_between_implies_in_arrivals
       arrived_between_jobs_must_arrive_to_execute
       arrives_in_jobs_come_from_arrival_sequence
       backlogged_implies_arrived
       job_scheduled_implies_ready
       jobs_must_arrive_to_be_ready
       jobs_must_arrive_to_be_ready
       ready_implies_arrived
       valid_schedule_implies_jobs_must_arrive_to_execute
       valid_schedule_jobs_come_from_arrival_sequence
       valid_schedule_jobs_must_be_ready_to_execute
       uniq_valid_arrival
       consistent_times_valid_arrival
       job_arrival_arrives_at
  : basic_rt_facts.