# Library prosa.analysis.facts.behavior.arrivals

Require Export prosa.behavior.all.

Require Export prosa.util.all.

Require Export prosa.model.task.arrivals.

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.
Furthermore, we restate a common hypothesis to make its
implication easier to discover.

Lemma consistent_times_valid_arrival :

∀ arr_seq,

valid_arrival_sequence arr_seq → consistent_arrival_times arr_seq.

∀ arr_seq,

valid_arrival_sequence arr_seq → consistent_arrival_times arr_seq.

We restate another common hypothesis to make its implication
easier to discover.

Lemma uniq_valid_arrival :

∀ arr_seq,

valid_arrival_sequence arr_seq → arrival_sequence_uniq arr_seq.

End ArrivalPredicates.

∀ arr_seq,

valid_arrival_sequence arr_seq → arrival_sequence_uniq arr_seq.

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.

Next, we observe that a given job must have arrived to be ready...

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

jobs_must_be_ready_to_execute sched → jobs_must_arrive_to_execute sched.

Furthermore, in a valid schedule, jobs must arrive to execute.

Corollary valid_schedule_implies_jobs_must_arrive_to_execute :

∀ arr_seq,

valid_schedule sched arr_seq → jobs_must_arrive_to_execute sched.

∀ arr_seq,

valid_schedule sched arr_seq → jobs_must_arrive_to_execute sched.

Since backlogged jobs are by definition ready, any backlogged job must have arrived.

Similarly, since backlogged jobs are by definition pending, any
backlogged job must be incomplete.

Finally, we restate common hypotheses on the well-formedness of
schedules to make their implications more easily
discoverable. First, on the readiness of scheduled jobs, ...

Lemma job_scheduled_implies_ready :

jobs_must_be_ready_to_execute sched →

∀ j t,

scheduled_at sched j t → job_ready sched j t.

jobs_must_be_ready_to_execute sched →

∀ j t,

scheduled_at sched j t → job_ready sched j t.

... second, on the origin of scheduled jobs, and ...

Lemma valid_schedule_jobs_come_from_arrival_sequence :

∀ arr_seq,

valid_schedule sched arr_seq →

jobs_come_from_arrival_sequence sched arr_seq.

∀ arr_seq,

valid_schedule sched arr_seq →

jobs_come_from_arrival_sequence sched arr_seq.

... third, on the readiness of jobs in valid schedules.

Lemma valid_schedule_jobs_must_be_ready_to_execute :

∀ arr_seq,

valid_schedule sched arr_seq → jobs_must_be_ready_to_execute sched.

End Arrived.

∀ arr_seq,

valid_schedule sched arr_seq → jobs_must_be_ready_to_execute sched.

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.

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

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.

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

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).

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

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

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

End Composition.

Next, we relate the arrival prefixes with job arrival times.

Assume that job arrival times are consistent.

To make the hypothesis and its implication easier to discover,
we restate it as a trivial lemma.

Similarly, to simplify subsequent proofs, we restate the
H_consistent_arrival_times assumption as a trivial
corollary.

To begin with actual properties, we observe that any job in
the set of all arrivals between time instants t1 and t2
must arrive in the interval

`[t1,t2)`

.
Lemma job_arrival_between :

∀ {j t1 t2},

j \in arrivals_between arr_seq t1 t2 → t1 ≤ job_arrival j < t2.

∀ {j t1 t2},

j \in arrivals_between arr_seq t1 t2 → t1 ≤ job_arrival j < t2.

For convenience, we restate the left bound of the above lemma...

Corollary job_arrival_between_ge :

∀ {j t1 t2},

j \in arrivals_between arr_seq t1 t2 → t1 ≤ job_arrival j.

∀ {j t1 t2},

j \in arrivals_between arr_seq t1 t2 → t1 ≤ job_arrival j.

... as well as the right bound separately as corollaries.

Corollary job_arrival_between_lt :

∀ {j t1 t2},

j \in arrivals_between arr_seq t1 t2 → job_arrival j < t2.

∀ {j t1 t2},

j \in arrivals_between arr_seq t1 t2 → job_arrival j < t2.

Second, 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.

∀ j t1 t2,

j \in arrivals_between arr_seq t1 t2 →

arrives_in arr_seq j.

We also prove a weaker version of the above lemma.

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.

∀ j t1 t2,

j \in arrivals_between arr_seq t1 t2 →

arrived_between j t1 t2.

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.

∀ j t,

j \in arrivals_before arr_seq t →

arrived_before j t.

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.

∀ j t1 t2,

arrives_in arr_seq j →

arrived_between j t1 t2 →

j \in arrivals_between arr_seq t1 t2.

Lemma job_arrival_between_P:

∀ j P t1 t2,

j \in arrivals_between_P arr_seq P t1 t2 →

t1 ≤ job_arrival j < t2.

∀ j P t1 t2,

j \in arrivals_between_P arr_seq P t1 t2 →

t1 ≤ job_arrival j < 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.

∀ j t1 t2,

arrives_in arr_seq j →

t1 ≤ job_arrival j < t2 →

j \in arrivals_between arr_seq t1 t2.

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).

arrival_sequence_uniq arr_seq →

∀ t1 t2, uniq (arrivals_between arr_seq t1 t2).

Also note that there can't by any arrivals in an empty time interval.

Conversely, if a job arrives, the considered interval is non-empty.

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).

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

We observe that, by construction, the sequence of arrivals is
sorted by arrival times. To this end, we first define the
order relation.

Trivially, the arrivals at any one point in time are ordered
w.r.t. arrival times.

By design, the list of arrivals in any interval is sorted.

Lemma arrivals_between_sorted :

∀ t1 t2,

sorted by_arrival_times (arrivals_between arr_seq t1 t2).

End ArrivalTimes.

End ArrivalSequencePrefix.

∀ t1 t2,

sorted by_arrival_times (arrivals_between arr_seq t1 t2).

End ArrivalTimes.

End ArrivalSequencePrefix.

In this section, we establish a few auxiliary facts about the
relation between the property of being scheduled and arrival
predicates to facilitate automation.

Consider any type of jobs.

Consider any kind of processor state model, ...

... any job arrival sequence with consistent arrivals, ....

Variable arr_seq : arrival_sequence Job.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

... and any schedule of this arrival sequence ...

Variable sched : schedule PState.

Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.

Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.

... where jobs do not execute before their arrival.

Next, consider a job j ...

... which is scheduled at a time instant t.

Lemma arrivals_before_scheduled_at :

∀ t',

t < t' →

j \in arrivals_before arr_seq t'.

End ScheduledImpliesArrives.

∀ t',

t < t' →

j \in arrivals_before arr_seq t'.

End ScheduledImpliesArrives.

We add some of the above lemmas to the "Hint Database"
basic_rt_facts, so the auto tactic will be able to use them.

Global Hint Resolve

arrivals_before_scheduled_at

arrivals_uniq

arrived_between_implies_in_arrivals

arrived_between_jobs_must_arrive_to_execute

arrives_in_jobs_come_from_arrival_sequence

jobs_must_arrive_to_be_ready

valid_schedule_implies_jobs_must_arrive_to_execute

valid_schedule_jobs_come_from_arrival_sequence

valid_schedule_jobs_must_be_ready_to_execute

: basic_rt_facts.

arrivals_before_scheduled_at

arrivals_uniq

arrived_between_implies_in_arrivals

arrived_between_jobs_must_arrive_to_execute

arrives_in_jobs_come_from_arrival_sequence

jobs_must_arrive_to_be_ready

valid_schedule_implies_jobs_must_arrive_to_execute

valid_schedule_jobs_come_from_arrival_sequence

valid_schedule_jobs_must_be_ready_to_execute

: basic_rt_facts.