Library rt.restructuring.analysis.basic_facts.arrivals
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.restructuring.behavior Require Export all.
From rt.util Require Import all.
In this section, we relate job readiness to [has_arrived].
Consider any kinds of jobs and any kind of processor state.
Consider any schedule...
...and suppose that jobs have a cost, an arrival time, and a notion of
readiness.
Context `{JobCost Job}.
Context `{JobArrival Job}.
(* We give the readiness typeclass instance a name here because we rely on it
explicitly in proofs. *)
Context {ReadyParam : JobReady Job PState}.
Context `{JobArrival Job}.
(* We give the readiness typeclass instance a name here because we rely on it
explicitly in proofs. *)
Context {ReadyParam : 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
ReadyParam : JobReady Job PState
============================
forall (j : Job) (t : instant), job_ready sched j t -> pending sched j t
----------------------------------------------------------------------------- *)
Proof.
move: ReadyParam ⇒ [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
ReadyParam : 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 68)
Job : JobType
PState : Type
H : ProcessorState Job PState
sched : schedule PState
H0 : JobCost Job
H1 : JobArrival Job
ReadyParam : 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
ReadyParam : 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.
∀ 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
ReadyParam : JobReady Job PState
============================
forall (j : Job) (t : instant), job_ready sched j t -> pending sched j t
----------------------------------------------------------------------------- *)
Proof.
move: ReadyParam ⇒ [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
ReadyParam : 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 68)
Job : JobType
PState : Type
H : ProcessorState Job PState
sched : schedule PState
H0 : JobCost Job
H1 : JobArrival Job
ReadyParam : 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
ReadyParam : 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
ReadyParam : 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 66)
Job : JobType
PState : Type
H : ProcessorState Job PState
sched : schedule PState
H0 : JobCost Job
H1 : JobArrival Job
ReadyParam : 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
ReadyParam : 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.
∀ 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
ReadyParam : 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 66)
Job : JobType
PState : Type
H : ProcessorState Job PState
sched : schedule PState
H0 : JobCost Job
H1 : JobArrival Job
ReadyParam : 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
ReadyParam : 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
ReadyParam : 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
ReadyParam : 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 90)
Job : JobType
PState : Type
H : ProcessorState Job PState
sched : schedule PState
H0 : JobCost Job
H1 : JobArrival Job
ReadyParam : 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
ReadyParam : 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.
End Arrived.
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
ReadyParam : 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
ReadyParam : 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 90)
Job : JobType
PState : Type
H : ProcessorState Job PState
sched : schedule PState
H0 : JobCost Job
H1 : JobArrival Job
ReadyParam : 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
ReadyParam : 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.
End Arrived.
In this section, we establish useful facts about arrival sequence prefixes.
Assume that job arrival times are known.
Consider any job arrival sequence.
In this section, we prove some lemmas about arrival sequence prefixes.
We begin with basic lemmas for manipulating the sequences.
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.
∀ 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.
∀ 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
----------------------------------------------------------------------------- *)
rewrite → big_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
----------------------------------------------------------------------------- *)
rewrite → big_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.
∀ 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
----------------------------------------------------------------------------- *)
rewrite → big_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
----------------------------------------------------------------------------- *)
rewrite → big_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.
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.
∀ 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.
∀ 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.
∀ 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
----------------------------------------------------------------------------- *)
move ⇒ j 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.
∀ 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
----------------------------------------------------------------------------- *)
move ⇒ j 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.
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 Lemmas.
End ArrivalSequencePrefix.
∀ 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 Lemmas.
End ArrivalSequencePrefix.