Library prosa.analysis.facts.behavior.arrivals


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

Welcome to Coq 8.11.2 (June 2020)

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


Require Export prosa.behavior.all.
Require Export prosa.util.all.

Arrival Sequence

First, we relate the stronger to the weaker arrival predicates.
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 41)
  
  Job : JobType
  H : JobArrival Job
  ============================
  forall (j : Job) (t1 t2 : instant),
  arrived_between j t1 t2 -> arrived_before j t2

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


  Proof.
    movej t1 t2.

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

1 subgoal (ID 44)
  
  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 50)
  
  Job : JobType
  H : JobArrival Job
  ============================
  forall (j : Job) (t : instant), arrived_before j t -> has_arrived j t

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


  Proof.
    movej t.

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

1 subgoal (ID 52)
  
  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 62)
  
  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 50)
  
  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 65)
  
  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

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


    movej t READY.

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

1 subgoal (ID 68)
  
  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 69)
  
  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 63)
  
  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.
    movej t READY.

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

1 subgoal (ID 66)
  
  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 67)
  
  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 74)
  
  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 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),
   scheduled_at sched j t -> job_ready sched j t) ->
  forall (j : Job) (t : instant), scheduled_at sched j t -> has_arrived j t

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


    moveREADY_IF_SCHED j t SCHED.

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

1 subgoal (ID 90)
  
  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 92)
  
  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 87)
  
  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 100)
  
  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

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


    movej t /andP [READY _].

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

1 subgoal (ID 142)
  
  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.

End Arrived.

In this section, we establish useful facts about arrival sequence prefixes.
Assume that job arrival times are known.
  Context {Job: JobType}.
  Context `{JobArrival Job}.

Consider any job arrival sequence.
  Variable arr_seq: arrival_sequence Job.

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

First, 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 41)
  
  Job : JobType
  H : JobArrival Job
  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 48)
  
  Job : JobType
  H : JobArrival Job
  arr_seq : arrival_sequence Job
  t1, t, t2 : nat
  GE : t1 <= t
  LE : t <= t2
  ============================
  \cat_(t1<=t0<t2|true)arrivals_at arr_seq t0 =
  \cat_(t1<=t0<t|true)arrivals_at arr_seq t0 ++
  \cat_(t<=t0<t2|true)arrivals_at arr_seq t0

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


        by rewrite (@big_cat_nat _ _ _ t).

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

No more subgoals.

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


    Qed.

Second, 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 61)
  
  Job : JobType
  H : JobArrival Job
  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.

Third, 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 78)
  
  Job : JobType
  H : JobArrival Job
  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 86)
  
  Job : JobType
  H : JobArrival Job
  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 130)
  
  Job : JobType
  H : JobArrival Job
  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 176)
  
  Job : JobType
  H : JobArrival Job
  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'|true)arrivals_at arr_seq t

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


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

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

1 subgoal (ID 181)
  
  Job : JobType
  H : JobArrival Job
  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|true)arrivals_at arr_seq i ++
        \cat_(t1<=i<t2'|true)arrivals_at arr_seq i

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


      rewrite mem_cat; apply/orP; right.

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

1 subgoal (ID 227)
  
  Job : JobType
  H : JobArrival Job
  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'|true)arrivals_at arr_seq i

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


      rewritebig_cat_nat with (n := t2); [simpl | by done | by done].

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

1 subgoal (ID 232)
  
  Job : JobType
  H : JobArrival Job
  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|true)arrivals_at arr_seq i ++
        \cat_(t2<=i<t2'|true)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.
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 44)
  
  Job : JobType
  H : JobArrival Job
  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 45)
  
  Job : JobType
  H : JobArrival Job
  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 49)
  
  Job : JobType
  H : JobArrival Job
  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 50)
  
  Job : JobType
  H : JobArrival Job
  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 75)
  
  Job : JobType
  H : JobArrival Job
  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.

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 56)
  
  Job : JobType
  H : JobArrival Job
  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 57)
  
  Job : JobType
  H : JobArrival Job
  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 61)
  
  Job : JobType
  H : JobArrival Job
  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 62)
  
  Job : JobType
  H : JobArrival Job
  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 87)
  
  Job : JobType
  H : JobArrival Job
  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 67)
  
  Job : JobType
  H : JobArrival Job
  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 70)
  
  Job : JobType
  H : JobArrival Job
  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 74)
  
  Job : JobType
  H : JobArrival Job
  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 79)
  
  Job : JobType
  H : JobArrival Job
  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 80)
  
  Job : JobType
  H : JobArrival Job
  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

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


      movej t1 t2 [a_j ARRj] BEFORE.

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

1 subgoal (ID 95)
  
  Job : JobType
  H : JobArrival Job
  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 108)
  
  Job : JobType
  H : JobArrival Job
  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

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


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

(* ----------------------------------[ 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 85)
  
  Job : JobType
  H : JobArrival Job
  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 86)
  
  Job : JobType
  H : JobArrival Job
  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 91)
  
  Job : JobType
  H : JobArrival Job
  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 93)
  
  Job : JobType
  H : JobArrival Job
  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 98)
  
  Job : JobType
  H : JobArrival Job
  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 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 92)
  
  Job : JobType
  H : JobArrival Job
  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.

  End ArrivalTimes.

End ArrivalSequencePrefix.