Library prosa.analysis.facts.behavior.arrivals


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)

Require Export prosa.behavior.all.
Require Export prosa.util.all.
Require Export prosa.model.task.arrivals.

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:
    ∀ j t1 t2,
      arrived_between j t1 t2 →
      arrived_before j t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 27)
  
  Job : JobType
  H : JobArrival Job
  ============================
  forall (j : Job) (t1 t2 : instant),
  arrived_between j t1 t2 -> arrived_before j t2

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ j t1 t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 30)
  
  Job : JobType
  H : JobArrival Job
  j : Job
  t1, t2 : instant
  ============================
  arrived_between j t1 t2 -> arrived_before j t2

----------------------------------------------------------------------------- *)

    now rewrite /arrived_before /arrived_between ⇒ /andP [_ CLAIM].

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

A job that arrives before a time [t] certainly has arrived by time [t].
  Lemma arrived_before_has_arrived:
    ∀ j t,
      arrived_before j t →
      has_arrived j t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 36)
  
  Job : JobType
  H : JobArrival Job
  ============================
  forall (j : Job) (t : instant), arrived_before j t -> has_arrived j t

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ j t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 38)
  
  Job : JobType
  H : JobArrival Job
  j : Job
  t : instant
  ============================
  arrived_before j t -> has_arrived j t

----------------------------------------------------------------------------- *)

    rewrite /arrived_before /has_arrived.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 48)
  
  Job : JobType
  H : JobArrival Job
  j : Job
  t : instant
  ============================
  job_arrival j < t -> job_arrival j <= t

----------------------------------------------------------------------------- *)

    now apply ltnW.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  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 : Type}.
  Context `{ProcessorState Job PState}.

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 `{JobReady Job PState}.

First, we note that readiness models are by definition consistent w.r.t. [pending].
  Lemma any_ready_job_is_pending:
    ∀ j t,
      job_ready sched j t → pending sched j t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 36)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  ============================
  forall (j : Job) (t : instant), job_ready sched j t -> pending sched j t

----------------------------------------------------------------------------- *)

  Proof.
    move: H5 ⇒ [is_ready CONSISTENT].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 51)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  is_ready : schedule PState -> Job -> instant -> bool
  CONSISTENT : forall (sched : schedule PState) (j : Job) (t : instant),
               is_ready sched j t -> pending sched j t
  ============================
  forall (j : Job) (t : instant), job_ready sched j t -> pending sched j t

----------------------------------------------------------------------------- *)

    move⇒ j t READY.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 54)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  is_ready : schedule PState -> Job -> instant -> bool
  CONSISTENT : forall (sched : schedule PState) (j : Job) (t : instant),
               is_ready sched j t -> pending sched j t
  j : Job
  t : instant
  READY : job_ready sched j t
  ============================
  pending sched j t

----------------------------------------------------------------------------- *)

    apply CONSISTENT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 55)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  is_ready : schedule PState -> Job -> instant -> bool
  CONSISTENT : forall (sched : schedule PState) (j : Job) (t : instant),
               is_ready sched j t -> pending sched j t
  j : Job
  t : instant
  READY : job_ready sched j t
  ============================
  is_ready sched j t

----------------------------------------------------------------------------- *)

    by exact READY.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Next, we observe that a given job must have arrived to be ready...
  Lemma ready_implies_arrived:
    ∀ j t, job_ready sched j t → has_arrived j t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 49)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  ============================
  forall (j : Job) (t : instant), job_ready sched j t -> has_arrived j t

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ j t READY.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 52)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  j : Job
  t : instant
  READY : job_ready sched j t
  ============================
  has_arrived j t

----------------------------------------------------------------------------- *)

    move: (any_ready_job_is_pending j t READY).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 53)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  j : Job
  t : instant
  READY : job_ready sched j t
  ============================
  pending sched j t -> has_arrived j t

----------------------------------------------------------------------------- *)

    by rewrite /pending ⇒ /andP [ARR _].

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 60)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  ============================
  jobs_must_be_ready_to_execute sched -> jobs_must_arrive_to_execute sched

----------------------------------------------------------------------------- *)

  Proof.
    rewrite /jobs_must_be_ready_to_execute /jobs_must_arrive_to_execute.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 72)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  ============================
  (forall (j : Job) (t : instant),
   scheduled_at sched j t -> job_ready sched j t) ->
  forall (j : Job) (t : instant), scheduled_at sched j t -> has_arrived j t

----------------------------------------------------------------------------- *)

    move⇒ READY_IF_SCHED j t SCHED.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 76)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  READY_IF_SCHED : forall (j : Job) (t : instant),
                   scheduled_at sched j t -> job_ready sched j t
  j : Job
  t : instant
  SCHED : scheduled_at sched j t
  ============================
  has_arrived j t

----------------------------------------------------------------------------- *)

    move: (READY_IF_SCHED j t SCHED) ⇒ READY.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 78)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  READY_IF_SCHED : forall (j : Job) (t : instant),
                   scheduled_at sched j t -> job_ready sched j t
  j : Job
  t : instant
  SCHED : scheduled_at sched j t
  READY : job_ready sched j t
  ============================
  has_arrived j t

----------------------------------------------------------------------------- *)

    by apply ready_implies_arrived.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Since backlogged jobs are by definition ready, any backlogged job must have arrived.
  Corollary backlogged_implies_arrived:
    ∀ j t,
      backlogged sched j t → has_arrived j t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 73)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  ============================
  forall (j : Job) (t : instant), backlogged sched j t -> has_arrived j t

----------------------------------------------------------------------------- *)

  Proof.
    rewrite /backlogged.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 86)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  ============================
  forall (j : Job) (t : instant),
  job_ready sched j t && ~~ scheduled_at sched j t -> has_arrived j t

----------------------------------------------------------------------------- *)

    move⇒ j t /andP [READY _].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 127)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  j : Job
  t : instant
  READY : job_ready sched j t
  ============================
  has_arrived j t

----------------------------------------------------------------------------- *)

    now apply ready_implies_arrived.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Similarly, since backlogged jobs are by definition pending, any backlogged job must be incomplete.
  Lemma backlogged_implies_incomplete:
    ∀ j t,
      backlogged sched j t → ~~ completed_by sched j t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 88)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  ============================
  forall (j : Job) (t : instant),
  backlogged sched j t -> ~~ completed_by sched j t

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ j t BACK.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 91)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  j : Job
  t : instant
  BACK : backlogged sched j t
  ============================
  ~~ completed_by sched j t

----------------------------------------------------------------------------- *)

    have suff: pending sched j t.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 97)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  j : Job
  t : instant
  BACK : backlogged sched j t
  ============================
  pending sched j t -> ~~ completed_by sched j t

subgoal 2 (ID 98) is:
 (pending sched j t -> ~~ completed_by sched j t) ->
 ~~ completed_by sched j t

----------------------------------------------------------------------------- *)

    - by move /andP ⇒ [_ INCOMP].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 98)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  j : Job
  t : instant
  BACK : backlogged sched j t
  ============================
  (pending sched j t -> ~~ completed_by sched j t) ->
  ~~ completed_by sched j t

----------------------------------------------------------------------------- *)

    - apply; move: BACK ⇒ /andP [READY _].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 183)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  H0 : JobCost Job
  H1 : JobArrival Job
  H2 : ProcessorState Job PState
  H3 : JobCost Job
  H4 : JobArrival Job
  H5 : JobReady Job PState
  j : Job
  t : instant
  READY : job_ready sched j t
  ============================
  pending sched j t

----------------------------------------------------------------------------- *)

      by apply any_ready_job_is_pending.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  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:
      ∀ 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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 26)
  
  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.
      unfold arrivals_between; intros t1 t t2 GE LE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 32)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  t1, t, t2 : nat
  GE : t1 <= t
  LE : t <= t2
  ============================
  \cat_(t1<=t0<t2)arrivals_at arr_seq t0 =
  \cat_(t1<=t0<t)arrivals_at arr_seq t0 ++
  \cat_(t<=t0<t2)arrivals_at arr_seq t0

----------------------------------------------------------------------------- *)

        by rewrite (@big_cat_nat _ _ _ t).

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    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:
      ∀ 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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 36)
  
  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.
      intros P t t1 t2 INEQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 41)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  P : Job -> bool
  t, t1, t2 : nat
  INEQ : 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

----------------------------------------------------------------------------- *)

      rewrite -filter_cat.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 47)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  P : Job -> bool
  t, t1, t2 : nat
  INEQ : t1 <= t < t2
  ============================
  arrivals_between_P arr_seq P t1 t2 =
  [seq j <- arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2
     | P j]

----------------------------------------------------------------------------- *)

      now rewrite -arrivals_between_cat ⇒ //; ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

The same observation applies to membership in the set of arrived jobs.
    Lemma arrivals_between_mem_cat:
      ∀ 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).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 55)
  
  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.
        by intros j t1 t t2 GE LE; rewrite (arrivals_between_cat _ t).

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    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:
      ∀ 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'.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 72)
  
  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.
      intros j t1 t1' t2 t2' GE1 LE2 IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 80)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  j : Job
  t1, t1', t2, t2' : nat
  GE1 : t1' <= t1
  LE2 : t2 <= t2'
  IN : j \in arrivals_between arr_seq t1 t2
  ============================
  j \in arrivals_between arr_seq t1' t2'

----------------------------------------------------------------------------- *)

      move: (leq_total t1 t2) ⇒ /orP [BEFORE | AFTER];
                                  last by rewrite /arrivals_between big_geq // in IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 123)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  j : Job
  t1, t1', t2, t2' : nat
  GE1 : t1' <= t1
  LE2 : t2 <= t2'
  IN : j \in arrivals_between arr_seq t1 t2
  BEFORE : t1 <= t2
  ============================
  j \in arrivals_between arr_seq t1' t2'

----------------------------------------------------------------------------- *)

      rewrite /arrivals_between.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 168)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  j : Job
  t1, t1', t2, t2' : nat
  GE1 : t1' <= t1
  LE2 : t2 <= t2'
  IN : j \in arrivals_between arr_seq t1 t2
  BEFORE : t1 <= t2
  ============================
  j \in \cat_(t1'<=t<t2')arrivals_at arr_seq t

----------------------------------------------------------------------------- *)

      rewrite → big_cat_nat with (n := t1); [simpl | by done | by apply: (leq_trans BEFORE)].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 172)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  j : Job
  t1, t1', t2, t2' : nat
  GE1 : t1' <= t1
  LE2 : t2 <= t2'
  IN : j \in arrivals_between arr_seq t1 t2
  BEFORE : t1 <= t2
  ============================
  j
    \in \cat_(t1'<=i<t1)arrivals_at arr_seq i ++
        \cat_(t1<=i<t2')arrivals_at arr_seq i

----------------------------------------------------------------------------- *)

      rewrite mem_cat; apply/orP; right.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 218)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  j : Job
  t1, t1', t2, t2' : nat
  GE1 : t1' <= t1
  LE2 : t2 <= t2'
  IN : j \in arrivals_between arr_seq t1 t2
  BEFORE : t1 <= t2
  ============================
  j \in \cat_(t1<=i<t2')arrivals_at arr_seq i

----------------------------------------------------------------------------- *)

      rewrite → big_cat_nat with (n := t2); [simpl | by done | by done].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 222)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  j : Job
  t1, t1', t2, t2' : nat
  GE1 : t1' <= t1
  LE2 : t2 <= t2'
  IN : j \in arrivals_between arr_seq t1 t2
  BEFORE : t1 <= t2
  ============================
  j
    \in \cat_(t1<=i<t2)arrivals_at arr_seq i ++
        \cat_(t2<=i<t2')arrivals_at arr_seq i

----------------------------------------------------------------------------- *)

        by rewrite mem_cat; apply/orP; left.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    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.

First, 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:
      ∀ j t1 t2,
        j \in arrivals_between arr_seq t1 t2 →
        arrives_in arr_seq j.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 30)
  
  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.
      rename H_consistent_arrival_times into CONS.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 31)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  CONS : consistent_arrival_times arr_seq
  ============================
  forall (j : Job) (t1 t2 : instant),
  j \in arrivals_between arr_seq t1 t2 -> arrives_in arr_seq j

----------------------------------------------------------------------------- *)

      intros j t1 t2 IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 35)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  CONS : consistent_arrival_times arr_seq
  j : Job
  t1, t2 : instant
  IN : j \in arrivals_between arr_seq t1 t2
  ============================
  arrives_in arr_seq j

----------------------------------------------------------------------------- *)

      apply mem_bigcat_nat_exists in IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 37)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  CONS : consistent_arrival_times arr_seq
  j : Job
  t1, t2 : instant
  IN : exists i : nat, j \in arrivals_at arr_seq i /\ t1 <= i < t2
  ============================
  arrives_in arr_seq j

----------------------------------------------------------------------------- *)

      move: IN ⇒ [arr [IN _]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 61)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  CONS : consistent_arrival_times arr_seq
  j : Job
  t1, t2 : instant
  arr : nat
  IN : j \in arrivals_at arr_seq arr
  ============================
  arrives_in arr_seq j

----------------------------------------------------------------------------- *)

        by ∃ arr.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

We also prove a weaker version of the above lemma.
    Lemma in_arrseq_implies_arrives:
      ∀ t j,
        j \in arr_seq t →
        arrives_in arr_seq j.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 39)
  
  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.
      move ⇒ t j J_ARR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 42)
  
  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
  J_ARR : j \in arr_seq t
  ============================
  arrives_in arr_seq j

----------------------------------------------------------------------------- *)

      ∃ t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 44)
  
  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
  J_ARR : j \in arr_seq t
  ============================
  j \in arrivals_at arr_seq t

----------------------------------------------------------------------------- *)

      now rewrite /arrivals_at.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    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:
      ∀ j t1 t2,
        j \in arrivals_between arr_seq t1 t2 →
        arrived_between j t1 t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 51)
  
  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.
      rename H_consistent_arrival_times into CONS.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 52)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  CONS : consistent_arrival_times arr_seq
  ============================
  forall (j : Job) (t1 t2 : instant),
  j \in arrivals_between arr_seq t1 t2 -> arrived_between j t1 t2

----------------------------------------------------------------------------- *)

      intros j t1 t2 IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 56)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  CONS : consistent_arrival_times arr_seq
  j : Job
  t1, t2 : instant
  IN : j \in arrivals_between arr_seq t1 t2
  ============================
  arrived_between j t1 t2

----------------------------------------------------------------------------- *)

      apply mem_bigcat_nat_exists in IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 58)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  CONS : consistent_arrival_times arr_seq
  j : Job
  t1, t2 : instant
  IN : exists i : nat, j \in arrivals_at arr_seq i /\ t1 <= i < t2
  ============================
  arrived_between j t1 t2

----------------------------------------------------------------------------- *)

      move: IN ⇒ [t0 [IN /= LT]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 82)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  CONS : consistent_arrival_times arr_seq
  j : Job
  t1, t2 : instant
  t0 : nat
  IN : j \in arrivals_at arr_seq t0
  LT : t1 <= t0 < t2
  ============================
  arrived_between j t1 t2

----------------------------------------------------------------------------- *)

        by apply CONS in IN; rewrite /arrived_between IN.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    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:
      ∀ j t,
        j \in arrivals_before arr_seq t →
        arrived_before j t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 62)
  
  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.
      intros j t IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 65)
  
  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 : instant
  IN : j \in arrivals_before arr_seq t
  ============================
  arrived_before j t

----------------------------------------------------------------------------- *)

      have: arrived_between j 0 t by apply in_arrivals_implies_arrived_between.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 69)
  
  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 : instant
  IN : j \in arrivals_before arr_seq t
  ============================
  arrived_between j 0 t -> arrived_before j t

----------------------------------------------------------------------------- *)

        by rewrite /arrived_between /=.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    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:
      ∀ j t1 t2,
        arrives_in arr_seq j →
        arrived_between j t1 t2 →
        j \in arrivals_between arr_seq t1 t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 74)
  
  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.
      rename H_consistent_arrival_times into CONS.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 75)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  CONS : 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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 90)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  CONS : 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
  ============================
  j \in arrivals_between arr_seq t1 t2

----------------------------------------------------------------------------- *)

      have SAME := ARRj; apply CONS in SAME; subst a_j.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 103)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  CONS : consistent_arrival_times arr_seq
  j : Job
  t1, t2 : instant
  ARRj : j \in arrivals_at arr_seq (job_arrival j)
  BEFORE : arrived_between j t1 t2
  ============================
  j \in arrivals_between arr_seq t1 t2

----------------------------------------------------------------------------- *)

      now apply mem_bigcat_nat with (j := (job_arrival j)).

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

Any job in arrivals between time instants [t1] and [t2] must arrive in the interval [t1,t2).
    Lemma job_arrival_between:
      ∀ j P t1 t2,
        j \in arrivals_between_P arr_seq P t1 t2 →
        t1 ≤ job_arrival j < t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 89)
  
  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.
      intros × ARR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 94)
  
  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
  ARR : j \in arrivals_between_P arr_seq P t1 t2
  ============================
  t1 <= job_arrival j < t2

----------------------------------------------------------------------------- *)

      move: ARR; rewrite mem_filter ⇒ /andP [PJ JARR].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 141)
  
  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
  JARR : j \in arrivals_between arr_seq t1 t2
  ============================
  t1 <= job_arrival j < t2

----------------------------------------------------------------------------- *)

      apply mem_bigcat_nat_exists in JARR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 143)
  
  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
  JARR : exists i : nat, j \in arrivals_at arr_seq i /\ t1 <= i < t2
  ============================
  t1 <= job_arrival j < t2

----------------------------------------------------------------------------- *)

      move : JARR ⇒ [i [ARR INEQ]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 166)
  
  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
  ARR : j \in arrivals_at arr_seq i
  INEQ : t1 <= i < t2
  ============================
  t1 <= job_arrival j < t2

----------------------------------------------------------------------------- *)

      apply H_consistent_arrival_times in ARR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 168)
  
  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
  ARR : job_arrival j = i
  INEQ : t1 <= i < t2
  ============================
  t1 <= job_arrival j < t2

----------------------------------------------------------------------------- *)

      now rewrite ARR.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    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:
      ∀ j t1 t2,
        arrives_in arr_seq j →
        t1 ≤ job_arrival j < t2 →
        j \in arrivals_between arr_seq t1 t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 103)
  
  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.
      intros × ARR INEQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 108)
  
  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
  ARR : arrives_in arr_seq j
  INEQ : t1 <= job_arrival j < t2
  ============================
  j \in arrivals_between arr_seq t1 t2

----------------------------------------------------------------------------- *)

      apply mem_bigcat_nat with (j := job_arrival j) ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 112)
  
  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
  ARR : arrives_in arr_seq j
  INEQ : t1 <= job_arrival j < t2
  ============================
  j \in arrivals_at arr_seq (job_arrival j)

----------------------------------------------------------------------------- *)

      move : ARR ⇒ [t J_IN].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 146)
  
  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
  INEQ : t1 <= job_arrival j < t2
  t : instant
  J_IN : j \in arrivals_at arr_seq t
  ============================
  j \in arrivals_at arr_seq (job_arrival j)

----------------------------------------------------------------------------- *)

      now rewrite → H_consistent_arrival_times with (t := t).

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    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 →
      ∀ t1 t2, uniq (arrivals_between arr_seq t1 t2).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 109)
  
  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.
      rename H_consistent_arrival_times into CONS.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 110)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  CONS : consistent_arrival_times arr_seq
  ============================
  arrival_sequence_uniq arr_seq ->
  forall t1 t2 : instant, uniq (arrivals_between arr_seq t1 t2)

----------------------------------------------------------------------------- *)

      unfold arrivals_up_to; intros SET t1 t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 114)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  CONS : consistent_arrival_times arr_seq
  SET : arrival_sequence_uniq arr_seq
  t1, t2 : instant
  ============================
  uniq (arrivals_between arr_seq t1 t2)

----------------------------------------------------------------------------- *)

      apply bigcat_nat_uniq; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 116)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  CONS : consistent_arrival_times arr_seq
  SET : arrival_sequence_uniq arr_seq
  t1, t2 : instant
  ============================
  forall (x : Job) (i1 i2 : nat),
  x \in arrivals_at arr_seq i1 -> x \in arrivals_at arr_seq i2 -> i1 = i2

----------------------------------------------------------------------------- *)

      intros x t t' IN1 IN2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 121)
  
  Job : JobType
  Task : TaskType
  H : JobArrival Job
  H0 : JobTask Job Task
  arr_seq : arrival_sequence Job
  CONS : consistent_arrival_times arr_seq
  SET : arrival_sequence_uniq arr_seq
  t1, t2 : instant
  x : Job
  t, t' : nat
  IN1 : x \in arrivals_at arr_seq t
  IN2 : x \in arrivals_at arr_seq t'
  ============================
  t = t'

----------------------------------------------------------------------------- *)

        by apply CONS in IN1; apply CONS in IN2; subst.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

Also note that there can't by any arrivals in an empty time interval.
    Lemma arrivals_between_geq:
      ∀ t1 t2,
        t1 ≥ t2 →
        arrivals_between arr_seq t1 t2 = [::].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 115)
  
  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.
        by intros ? ? GE; rewrite /arrivals_between big_geq.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    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:
      ∀ (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).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 137)
  
  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.
      intros × J1_IN J2_IN ARR_LT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 145)
  
  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 : j1 \in arrivals_between_P arr_seq P t1 t2
  J2_IN : j2 \in arrivals_between_P arr_seq P t1 t2
  ARR_LT : job_arrival j2 < job_arrival j1
  ============================
  j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1)

----------------------------------------------------------------------------- *)

      rewrite mem_filter in J2_IN; move : J2_IN ⇒ /andP [PJ2 J2ARR] ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 213)
  
  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 : j1 \in arrivals_between_P arr_seq P t1 t2
  ARR_LT : job_arrival j2 < job_arrival j1
  PJ2 : P j2
  J2ARR : j2 \in arrivals_between arr_seq t1 t2
  ============================
  j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1)

----------------------------------------------------------------------------- *)

      rewrite mem_filter; apply /andP; split ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 267)
  
  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 : j1 \in arrivals_between_P arr_seq P t1 t2
  ARR_LT : job_arrival j2 < job_arrival j1
  PJ2 : P j2
  J2ARR : j2 \in arrivals_between arr_seq t1 t2
  ============================
  j2 \in arrivals_between arr_seq t1 (job_arrival j1)

----------------------------------------------------------------------------- *)

      apply mem_bigcat_nat_exists in J2ARR; move : J2ARR ⇒ [i [J2_IN INEQ]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 313)
  
  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 : j1 \in arrivals_between_P arr_seq P t1 t2
  ARR_LT : job_arrival j2 < job_arrival j1
  PJ2 : P j2
  i : nat
  J2_IN : j2 \in arrivals_at arr_seq i
  INEQ : t1 <= i < t2
  ============================
  j2 \in arrivals_between arr_seq t1 (job_arrival j1)

----------------------------------------------------------------------------- *)

      apply mem_bigcat_nat with (j := i) ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 314)
  
  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 : j1 \in arrivals_between_P arr_seq P t1 t2
  ARR_LT : job_arrival j2 < job_arrival j1
  PJ2 : P j2
  i : nat
  J2_IN : j2 \in arrivals_at arr_seq i
  INEQ : t1 <= i < t2
  ============================
  t1 <= i < job_arrival j1

----------------------------------------------------------------------------- *)

      apply H_consistent_arrival_times in J2_IN; rewrite J2_IN in ARR_LT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 364)
  
  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 : j1 \in arrivals_between_P arr_seq P t1 t2
  PJ2 : P j2
  i : nat
  J2_IN : job_arrival j2 = i
  INEQ : t1 <= i < t2
  ARR_LT : i < job_arrival j1
  ============================
  t1 <= i < job_arrival j1

----------------------------------------------------------------------------- *)

      now ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

  End ArrivalTimes.

End ArrivalSequencePrefix.