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.
Require Export prosa.model.task.arrivals.
Consider any kinds of jobs with arrival times.
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 337)
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 340)
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.
∀ j t1 t2,
arrived_between j t1 t2 →
arrived_before j t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 337)
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 340)
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 346)
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 348)
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 358)
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.
∀ j t,
arrived_before j t →
has_arrived j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 346)
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 348)
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 358)
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].
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.
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 346)
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 361)
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 364)
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 365)
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.
∀ j t,
job_ready sched j t → pending sched j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 346)
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 361)
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 364)
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 365)
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 359)
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 362)
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 363)
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.
∀ j t, job_ready sched j t → has_arrived j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 359)
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 362)
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 363)
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 370)
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 382)
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 386)
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 388)
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.
jobs_must_be_ready_to_execute sched →
jobs_must_arrive_to_execute sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 370)
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 382)
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 386)
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 388)
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 383)
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 396)
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 438)
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.
∀ j t,
backlogged sched j t → has_arrived j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 383)
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 396)
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 438)
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.
Consider any kind of tasks and jobs.
Context {Job: JobType}.
Context {Task : TaskType}.
Context `{JobArrival Job}.
Context `{JobTask Job Task}.
Context {Task : TaskType}.
Context `{JobArrival Job}.
Context `{JobTask Job Task}.
Consider any job arrival sequence.
We begin with basic lemmas for manipulating the sequences.
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 337)
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 344)
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|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 337)
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 344)
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|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.
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 348)
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 353)
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 359)
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.
∀ 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 348)
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 353)
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 359)
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 368)
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.
∀ 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 368)
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 385)
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 393)
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 437)
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 483)
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'|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 488)
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|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 534)
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'|true)arrivals_at arr_seq i
----------------------------------------------------------------------------- *)
rewrite → big_cat_nat with (n := t2); [simpl | by done | by done].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 539)
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|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 385)
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 393)
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 437)
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 483)
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'|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 488)
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|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 534)
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'|true)arrivals_at arr_seq i
----------------------------------------------------------------------------- *)
rewrite → big_cat_nat with (n := t2); [simpl | by done | by done].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 539)
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|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 340)
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 341)
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 345)
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 346)
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 371)
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.
∀ j t1 t2,
j \in arrivals_between arr_seq t1 t2 →
arrives_in arr_seq j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 340)
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 341)
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 345)
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 346)
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 371)
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 349)
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 352)
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 354)
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.
∀ t j,
j \in arr_seq t →
arrives_in arr_seq j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 349)
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 352)
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 354)
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 361)
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 362)
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 366)
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 367)
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 392)
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.
∀ j t1 t2,
j \in arrivals_between arr_seq t1 t2 →
arrived_between j t1 t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 361)
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 362)
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 366)
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 367)
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 392)
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 372)
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 375)
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 379)
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.
∀ j t,
j \in arrivals_before arr_seq t →
arrived_before j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 372)
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 375)
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 379)
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 384)
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 385)
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 400)
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 413)
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.
∀ 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 384)
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 385)
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 400)
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 413)
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 399)
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 404)
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 452)
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 453)
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 477)
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 478)
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.
∀ j P t1 t2,
j \in arrivals_between_P arr_seq P t1 t2 →
t1 ≤ job_arrival j < t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 399)
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 404)
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 452)
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 453)
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 477)
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 478)
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 413)
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 418)
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 422)
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 457)
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.
∀ 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 413)
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 418)
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 422)
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 457)
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 419)
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 420)
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 425)
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 427)
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 432)
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.
arrival_sequence_uniq arr_seq →
∀ t1 t2, uniq (arrivals_between arr_seq t1 t2).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 419)
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 420)
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 425)
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 427)
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 432)
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 426)
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.
∀ t1 t2,
t1 ≥ t2 →
arrivals_between arr_seq t1 t2 = [::].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 426)
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 448)
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 456)
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 525)
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 580)
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 627)
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 628)
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 679)
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.
∀ (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 448)
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 456)
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 525)
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 580)
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 627)
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 628)
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 679)
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.