Built with
Alectryon , running Coq+SerAPI v8.14.0+0.14.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.behavior.all .Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.util.all .Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.model.task.arrivals.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** * Arrival Sequence *)
(** First, we relate the stronger to the weaker arrival predicates. *)
Section ArrivalPredicates .
(** Consider any kinds of jobs with arrival times. *)
Context {Job : JobType} `{JobArrival Job}.
(** A job that arrives in some interval <<[t1, t2)>> certainly arrives before
time [t2]. *)
Lemma arrived_between_before :
forall j t1 t2 ,
arrived_between j t1 t2 ->
arrived_before j t2.Job : JobType H : JobArrival Job
forall (j : Job) (t1 t2 : instant),
arrived_between j t1 t2 -> arrived_before j t2
Proof .Job : JobType H : JobArrival Job
forall (j : Job) (t1 t2 : instant),
arrived_between j t1 t2 -> arrived_before j t2
move => j t1 t2.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].
Qed .
(** A job that arrives before a time [t] certainly has arrived by time
[t]. *)
Lemma arrived_before_has_arrived :
forall j t ,
arrived_before j t ->
has_arrived j t.Job : JobType H : JobArrival Job
forall (j : Job) (t : instant),
arrived_before j t -> has_arrived j t
Proof .Job : JobType H : JobArrival Job
forall (j : Job) (t : instant),
arrived_before j t -> has_arrived j t
move => j t.Job : JobType H : JobArrival Job j : Job t : instant
arrived_before j t -> has_arrived j t
rewrite /arrived_before /has_arrived.Job : JobType H : JobArrival Job j : Job t : instant
job_arrival j < t -> job_arrival j <= t
now apply ltnW.
Qed .
End ArrivalPredicates .
(** In this section, we relate job readiness to [has_arrived]. *)
Section Arrived .
(** Consider any kinds of jobs and any kind of processor state. *)
Context {Job : JobType} {PState : Type }.
Context `{ProcessorState Job PState}.
(** Consider any schedule... *)
Variable sched : schedule PState.
(** ...and suppose that jobs have a cost, an arrival time, and a
notion of readiness. *)
Context `{JobCost Job}.
Context `{JobArrival Job}.
Context `{JobReady Job PState}.
(** First, we note that readiness models are by definition consistent
w.r.t. [pending]. *)
Lemma any_ready_job_is_pending :
forall j t ,
job_ready sched j t -> pending sched j t.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 .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
move : H5 => [is_ready CONSISTENT].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.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 tj : Job t : instant READY : job_ready sched j t
pending sched j t
apply CONSISTENT.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 tj : Job t : instant READY : job_ready sched j t
is_ready sched j t
by exact READY.
Qed .
(** Next, we observe that a given job must have arrived to be ready... *)
Lemma ready_implies_arrived :
forall j t , job_ready sched j t -> has_arrived j t.Job : JobType PState : 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 .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
move => j t READY.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).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 _].
Qed .
(** ...and lift this observation also to the level of whole schedules. *)
Lemma jobs_must_arrive_to_be_ready :
jobs_must_be_ready_to_execute sched ->
jobs_must_arrive_to_execute sched.Job : JobType PState : 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 .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
rewrite /jobs_must_be_ready_to_execute /jobs_must_arrive_to_execute.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.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 tj : Job t : instant SCHED : scheduled_at sched j t
has_arrived j t
move : (READY_IF_SCHED j t SCHED) => READY.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 tj : Job t : instant SCHED : scheduled_at sched j t READY : job_ready sched j t
has_arrived j t
by apply ready_implies_arrived.
Qed .
(** Furthermore, in a valid schedule, jobs must arrive to execute. *)
Corollary valid_schedule_implies_jobs_must_arrive_to_execute :
forall arr_seq ,
valid_schedule sched arr_seq ->
jobs_must_arrive_to_execute sched.Job : JobType PState : 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 arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
jobs_must_arrive_to_execute sched
Proof .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 arr_seq : arrival_sequence Job,
valid_schedule sched arr_seq ->
jobs_must_arrive_to_execute sched
move => arr_seq [??].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 arr_seq : arrival_sequence Job _a_ : jobs_come_from_arrival_sequence sched arr_seq _b_ : jobs_must_be_ready_to_execute sched
jobs_must_arrive_to_execute sched
by apply jobs_must_arrive_to_be_ready.
Qed .
(** Since backlogged jobs are by definition ready, any backlogged job must have arrived. *)
Corollary backlogged_implies_arrived :
forall j t ,
backlogged sched j t -> has_arrived j t.Job : JobType PState : 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 .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
rewrite /backlogged.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 _].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.
Qed .
(** Similarly, since backlogged jobs are by definition pending, any
backlogged job must be incomplete. *)
Lemma backlogged_implies_incomplete :
forall j t ,
backlogged sched j t -> ~~ completed_by sched j t.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState
forall (j : Job) (t : instant),
backlogged sched j t -> ~~ completed_by sched j t
Proof .Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState
forall (j : Job) (t : instant),
backlogged sched j t -> ~~ completed_by sched j t
move => j t BACK.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState j : Job t : instant BACK : backlogged sched j t
~~ completed_by sched j t
have suff : pending sched j t.Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState j : Job t : instant BACK : backlogged sched j t
pending sched j t -> ~~ completed_by sched j t
- Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState j : Job t : instant BACK : backlogged sched j t
pending sched j t -> ~~ completed_by sched j t
by move /andP => [_ INCOMP].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState j : Job t : instant BACK : backlogged sched j t
(pending sched j t -> ~~ completed_by sched j t) ->
~~ completed_by sched j t
- Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState j : Job t : instant BACK : backlogged sched j t
(pending sched j t -> ~~ completed_by sched j t) ->
~~ completed_by sched j t
apply ; move : BACK => /andP [READY _].Job : JobType PState : Type H : ProcessorState Job PState sched : schedule PState H0 : JobCost Job H1 : JobArrival Job H2 : ProcessorState Job PState H3 : JobCost Job H4 : JobArrival Job H5 : JobReady Job PState j : Job t : instant READY : job_ready sched j t
pending sched j t
by apply any_ready_job_is_pending.
Qed .
End Arrived .
(** We add some of the above lemmas to the "Hint Database"
[basic_facts], so the [auto] tactic will be able to use them. *)
Global Hint Resolve
valid_schedule_implies_jobs_must_arrive_to_execute
jobs_must_arrive_to_be_ready
: basic_facts.
(** In this section, we establish useful facts about arrival sequence prefixes. *)
Section ArrivalSequencePrefix .
(** Consider any kind of tasks and jobs. *)
Context {Job : JobType}.
Context {Task : TaskType}.
Context `{JobArrival Job}.
Context `{JobTask Job Task}.
(** Consider any job arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** We begin with basic lemmas for manipulating the sequences. *)
Section Composition .
(** We show that the set of arriving jobs can be split
into disjoint intervals. *)
Lemma arrivals_between_cat :
forall t1 t t2 ,
t1 <= t ->
t <= t2 ->
arrivals_between arr_seq t1 t2 =
arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall t1 t t2 : nat,
t1 <= t ->
t <= t2 ->
arrivals_between arr_seq t1 t2 =
arrivals_between arr_seq t1 t ++
arrivals_between arr_seq t t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall t1 t t2 : nat,
t1 <= t ->
t <= t2 ->
arrivals_between arr_seq t1 t2 =
arrivals_between arr_seq t1 t ++
arrivals_between arr_seq t t2
unfold arrivals_between; intros t1 t t2 GE LE.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<=t<t2)arrivals_at arr_seq t =
\cat_(t1<=t<t)arrivals_at arr_seq t ++
\cat_(t<=t<t2)arrivals_at arr_seq t
by rewrite (@big_cat_nat _ _ _ t).
Qed .
(** We also prove a stronger version of the above lemma
in the case of arrivals that satisfy a predicate [P]. *)
Lemma arrivals_P_cat :
forall P t t1 t2 ,
t1 <= t < t2 ->
arrivals_between_P arr_seq P t1 t2 =
arrivals_between_P arr_seq P t1 t ++ arrivals_between_P arr_seq P t t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall (P : Job -> bool) (t t1 t2 : nat),
t1 <= t < t2 ->
arrivals_between_P arr_seq P t1 t2 =
arrivals_between_P arr_seq P t1 t ++
arrivals_between_P arr_seq P t t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall (P : Job -> bool) (t t1 t2 : nat),
t1 <= t < t2 ->
arrivals_between_P arr_seq P t1 t2 =
arrivals_between_P arr_seq P t1 t ++
arrivals_between_P arr_seq P t t2
intros P t t1 t2 INEQ.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.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.
Qed .
(** The same observation applies to membership in the set of
arrived jobs. *)
Lemma arrivals_between_mem_cat :
forall j t1 t t2 ,
t1 <= t ->
t <= t2 ->
j \in arrivals_between arr_seq t1 t2 =
(j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall (j : Job) (t1 t t2 : nat),
t1 <= t ->
t <= t2 ->
(j \in arrivals_between arr_seq t1 t2) =
(j
\in arrivals_between arr_seq t1 t ++
arrivals_between arr_seq t t2)
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall (j : Job) (t1 t t2 : nat),
t1 <= t ->
t <= t2 ->
(j \in arrivals_between arr_seq t1 t2) =
(j
\in arrivals_between arr_seq t1 t ++
arrivals_between arr_seq t t2)
by intros j t1 t t2 GE LE; rewrite (arrivals_between_cat _ t).
Qed .
(** We observe that we can grow the considered interval without
"losing" any arrived jobs, i.e., membership in the set of arrived jobs
is monotonic. *)
Lemma arrivals_between_sub :
forall j t1 t1' t2 t2' ,
t1' <= t1 ->
t2 <= t2' ->
j \in arrivals_between arr_seq t1 t2 ->
j \in arrivals_between arr_seq t1' t2'.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall (j : Job) (t1 t1' t2 t2' : nat),
t1' <= t1 ->
t2 <= t2' ->
j \in arrivals_between arr_seq t1 t2 ->
j \in arrivals_between arr_seq t1' t2'
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job
forall (j : Job) (t1 t1' t2 t2' : nat),
t1' <= t1 ->
t2 <= t2' ->
j \in arrivals_between arr_seq t1 t2 ->
j \in arrivals_between arr_seq t1' t2'
intros j t1 t1' t2 t2' GE1 LE2 IN.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.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.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job j : Job t1, t1', t2, t2' : nat GE1 : t1' <= t1 LE2 : t2 <= t2' IN : j \in arrivals_between arr_seq t1 t2 BEFORE : t1 <= t2
j \in \cat_(t1'<=t<t2')arrivals_at arr_seq t
rewrite -> big_cat_nat with (n := t1); [simpl | by done | by apply : (leq_trans BEFORE)].Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job j : Job t1, t1', t2, t2' : nat GE1 : t1' <= t1 LE2 : t2 <= t2' IN : j \in arrivals_between arr_seq t1 t2 BEFORE : t1 <= t2
j
\in \cat_(t1'<=i<t1)arrivals_at arr_seq i ++
\cat_(t1<=i<t2')arrivals_at arr_seq i
rewrite mem_cat; apply /orP; right .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job j : Job t1, t1', t2, t2' : nat GE1 : t1' <= t1 LE2 : t2 <= t2' IN : j \in arrivals_between arr_seq t1 t2 BEFORE : t1 <= t2
j \in \cat_(t1<=i<t2')arrivals_at arr_seq i
rewrite -> big_cat_nat with (n := t2); [simpl | by done | by done ].Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job j : Job t1, t1', t2, t2' : nat GE1 : t1' <= t1 LE2 : t2 <= t2' IN : j \in arrivals_between arr_seq t1 t2 BEFORE : t1 <= t2
j
\in \cat_(t1<=i<t2)arrivals_at arr_seq i ++
\cat_(t2<=i<t2')arrivals_at arr_seq i
by rewrite mem_cat; apply /orP; left .
Qed .
End Composition .
(** Next, we relate the arrival prefixes with job arrival times. *)
Section ArrivalTimes .
(** Assume that job arrival times are consistent. *)
Hypothesis H_consistent_arrival_times :
consistent_arrival_times arr_seq.
(** First, we prove that if a job belongs to the prefix
(jobs_arrived_before t), then it arrives in the arrival sequence. *)
Lemma in_arrivals_implies_arrived :
forall j t1 t2 ,
j \in arrivals_between arr_seq t1 t2 ->
arrives_in arr_seq j.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
arrives_in arr_seq j
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
arrives_in arr_seq j
rename H_consistent_arrival_times into CONS.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.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.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 _]].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 exists arr .
Qed .
(** We also prove a weaker version of the above lemma. *)
Lemma in_arrseq_implies_arrives :
forall t j ,
j \in arr_seq t ->
arrives_in arr_seq j.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (t : instant) (j : Job),
j \in arr_seq t -> arrives_in arr_seq j
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (t : instant) (j : Job),
j \in arr_seq t -> arrives_in arr_seq j
move => t j J_ARR.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t : instant j : Job J_ARR : j \in arr_seq t
arrives_in arr_seq j
exists t .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq t : instant j : Job J_ARR : j \in arr_seq t
j \in arrivals_at arr_seq t
now rewrite /arrivals_at.
Qed .
(** Next, we prove that if a job belongs to the prefix
(jobs_arrived_between t1 t2), then it indeed arrives between t1 and
t2. *)
Lemma in_arrivals_implies_arrived_between :
forall j t1 t2 ,
j \in arrivals_between arr_seq t1 t2 ->
arrived_between j t1 t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
arrived_between j t1 t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
j \in arrivals_between arr_seq t1 t2 ->
arrived_between j t1 t2
rename H_consistent_arrival_times into CONS.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.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.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]].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.
Qed .
(** Similarly, if a job belongs to the prefix (jobs_arrived_before t),
then it indeed arrives before time t. *)
Lemma in_arrivals_implies_arrived_before :
forall j t ,
j \in arrivals_before arr_seq t ->
arrived_before j t.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t : instant),
j \in arrivals_before arr_seq t -> arrived_before j t
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t : instant),
j \in arrivals_before arr_seq t -> arrived_before j t
intros j t IN.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job t : 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.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 /=.
Qed .
(** Similarly, we prove that if a job from the arrival sequence arrives
before t, then it belongs to the sequence (jobs_arrived_before t). *)
Lemma arrived_between_implies_in_arrivals :
forall j t1 t2 ,
arrives_in arr_seq j ->
arrived_between j t1 t2 ->
j \in arrivals_between arr_seq t1 t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
arrives_in arr_seq j ->
arrived_between j t1 t2 ->
j \in arrivals_between arr_seq t1 t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : instant),
arrives_in arr_seq j ->
arrived_between j t1 t2 ->
j \in arrivals_between arr_seq t1 t2
rename H_consistent_arrival_times into CONS.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.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.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)).
Qed .
(** Any job in arrivals between time instants [t1] and [t2] must arrive
in the interval <<[t1,t2)>>. *)
Lemma job_arrival_between :
forall j P t1 t2 ,
j \in arrivals_between_P arr_seq P t1 t2 ->
t1 <= job_arrival j < t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (P : Job -> bool) (t1 t2 : instant),
j \in arrivals_between_P arr_seq P t1 t2 ->
t1 <= job_arrival j < t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (P : Job -> bool) (t1 t2 : instant),
j \in arrivals_between_P arr_seq P t1 t2 ->
t1 <= job_arrival j < t2
intros * ARR.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j : Job 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].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.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]].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.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.
Qed .
(** Any job [j] is in the sequence [arrivals_between t1 t2] given
that [j] arrives in the interval <<[t1,t2)>>. *)
Lemma job_in_arrivals_between :
forall j t1 t2 ,
arrives_in arr_seq j ->
t1 <= job_arrival j < t2 ->
j \in arrivals_between arr_seq t1 t2.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : nat),
arrives_in arr_seq j ->
t1 <= job_arrival j < t2 ->
j \in arrivals_between arr_seq t1 t2
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j : Job) (t1 t2 : nat),
arrives_in arr_seq j ->
t1 <= job_arrival j < t2 ->
j \in arrivals_between arr_seq t1 t2
intros * ARR INEQ.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) => //.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].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).
Qed .
(** Next, we prove that if the arrival sequence doesn't contain duplicate
jobs, the same applies for any of its prefixes. *)
Lemma arrivals_uniq :
arrival_sequence_uniq arr_seq ->
forall t1 t2 , uniq (arrivals_between arr_seq t1 t2).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
arrival_sequence_uniq arr_seq ->
forall t1 t2 : instant,
uniq (arrivals_between arr_seq t1 t2)
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
arrival_sequence_uniq arr_seq ->
forall t1 t2 : instant,
uniq (arrivals_between arr_seq t1 t2)
rename H_consistent_arrival_times into CONS.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.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 .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.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 .
Qed .
(** Also note that there can't by any arrivals in an empty time interval. *)
Lemma arrivals_between_geq :
forall t1 t2 ,
t1 >= t2 ->
arrivals_between arr_seq t1 t2 = [::].Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall t1 t2 : nat,
t2 <= t1 -> arrivals_between arr_seq t1 t2 = [::]
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall t1 t2 : nat,
t2 <= t1 -> arrivals_between arr_seq t1 t2 = [::]
by intros ? ? GE; rewrite /arrivals_between big_geq.
Qed .
(** Given jobs [j1] and [j2] in [arrivals_between_P arr_seq P t1 t2], the fact that
[j2] arrives strictly before [j1] implies that [j2] also belongs in the sequence
[arrivals_between_P arr_seq P t1 (job_arrival j1)]. *)
Lemma arrival_lt_implies_job_in_arrivals_between_P :
forall (j1 j2 : Job) (P : Job -> bool) (t1 t2 : instant),
(j1 \in arrivals_between_P arr_seq P t1 t2) ->
(j2 \in arrivals_between_P arr_seq P t1 t2) ->
job_arrival j2 < job_arrival j1 ->
j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1).Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j1 j2 : Job) (P : Job -> bool)
(t1 t2 : instant),
j1 \in arrivals_between_P arr_seq P t1 t2 ->
j2 \in arrivals_between_P arr_seq P t1 t2 ->
job_arrival j2 < job_arrival j1 ->
j2
\in arrivals_between_P arr_seq P t1 (job_arrival j1)
Proof .Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq
forall (j1 j2 : Job) (P : Job -> bool)
(t1 t2 : instant),
j1 \in arrivals_between_P arr_seq P t1 t2 ->
j2 \in arrivals_between_P arr_seq P t1 t2 ->
job_arrival j2 < job_arrival j1 ->
j2
\in arrivals_between_P arr_seq P t1 (job_arrival j1)
intros * J1_IN J2_IN ARR_LT.Job : JobType Task : TaskType H : JobArrival Job H0 : JobTask Job Task arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq j1, j2 : Job P : Job -> bool t1, t2 : instant 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] => //.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 => //.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]].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) => //.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.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.
Qed .
End ArrivalTimes .
End ArrivalSequencePrefix .