# Library prosa.analysis.facts.model.workload

Require Export prosa.model.aggregate.workload.

Require Export prosa.analysis.facts.behavior.arrivals.

Require Export prosa.analysis.facts.behavior.arrivals.

# Lemmas about Workload of Sets of Jobs

In this file, we establish basic facts about the workload of sets of jobs.
Consider any type of tasks ...

... and any type of jobs associated with these tasks.

Context {Job : JobType}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

To begin with, we establish an auxiliary rewriting lemma that allows us to
introduce a filter on the considered set of jobs, provided the filter
predicate P2 is implied by the job-selection predicate P1.

Lemma workload_of_jobs_filter :

∀ (P1 P2 : pred Job) (jobs : seq Job),

(∀ j, j \in jobs → P1 j → P2 j) →

workload_of_jobs P1 jobs = workload_of_jobs P1 [seq j <- jobs | P2 j ].

∀ (P1 P2 : pred Job) (jobs : seq Job),

(∀ j, j \in jobs → P1 j → P2 j) →

workload_of_jobs P1 jobs = workload_of_jobs P1 [seq j <- jobs | P2 j ].

Next, consider any job arrival sequence consistent with the arrival times
of the jobs.

Variable arr_seq : arrival_sequence Job.

Hypothesis H_consistent : consistent_arrival_times arr_seq.

Hypothesis H_consistent : consistent_arrival_times arr_seq.

If at some point in time t the predicate P by which we select jobs
from the set of arrivals in an interval

`[t1, t2)`

becomes certainly
false, then we may disregard all jobs arriving at time t or later.
Lemma workload_of_jobs_nil_tail :

∀ {P t1 t2 t},

t ≤ t2 →

(∀ j, j \in (arrivals_between arr_seq t1 t2) → job_arrival j ≥ t → ~~ P j) →

workload_of_jobs P (arrivals_between arr_seq t1 t2)

= workload_of_jobs P (arrivals_between arr_seq t1 t).

∀ {P t1 t2 t},

t ≤ t2 →

(∀ j, j \in (arrivals_between arr_seq t1 t2) → job_arrival j ≥ t → ~~ P j) →

workload_of_jobs P (arrivals_between arr_seq t1 t2)

= workload_of_jobs P (arrivals_between arr_seq t1 t).

For simplicity, let's define a local name.

We observe that the cumulative workload of all jobs arriving in a time
interval

`[t1, t2)`

and respecting a predicate P can be split into two parts.
Lemma workload_of_jobs_cat:

∀ t t1 t2 P,

t1 ≤ t ≤ t2 →

workload_of_jobs P (arrivals_between t1 t2) =

workload_of_jobs P (arrivals_between t1 t) + workload_of_jobs P (arrivals_between t t2).

∀ t t1 t2 P,

t1 ≤ t ≤ t2 →

workload_of_jobs P (arrivals_between t1 t2) =

workload_of_jobs P (arrivals_between t1 t) + workload_of_jobs P (arrivals_between t t2).

Consider a job j ...

... and a duplicate-free sequence of jobs jobs.

To help with rewriting, we prove that the workload of jobs
minus the job cost of j is equal to the workload of all jobs
except j. To define the workload of all jobs, since
workload_of_jobs expects a predicate, we use predT, which
is the always-true predicate.

Lemma workload_minus_job_cost :

workload_of_jobs (fun jhp : Job ⇒ jhp != j) jobs =

workload_of_jobs predT jobs - job_cost j.

workload_of_jobs (fun jhp : Job ⇒ jhp != j) jobs =

workload_of_jobs predT jobs - job_cost j.

In this section, we prove the relation between two different ways of constraining
workload_of_jobs to only those jobs that arrive prior to a given time.

Assume that arrival times are consistent and that arrivals are unique.

Consider a time interval

`[t1, t2)`

and a time instant t.
Let P be an arbitrary predicate on jobs.

Consider the window

`[t1,t2)`

. We prove that the total workload of the jobs
arriving in this window before some t is the same as the workload of the jobs
arriving in `[t1,t)`

. Note that we only require t1 to be less-or-equal
than t2. Consequently, the interval `[t1,t)`

may be empty.
Lemma workload_equal_subset :

workload_of_jobs (fun j ⇒ (job_arrival j ≤ t) && P j) (arrivals_between t1 t2)

≤ workload_of_jobs (fun j ⇒ P j) (arrivals_between t1 (t + ε)).

End Subset.

workload_of_jobs (fun j ⇒ (job_arrival j ≤ t) && P j) (arrivals_between t1 t2)

≤ workload_of_jobs (fun j ⇒ P j) (arrivals_between t1 (t + ε)).

End Subset.

In this section, we prove a few useful properties regarding the
predicate of workload_of_jobs.

First, we show that workload of jobs for an unsatisfiable
predicate is equal to 0.

We show that workload_of_jobs conditioned on P can be split into two summands:
(1) workload_of_jobs conditioned on P ∧ P' and
(2) workload_of_jobs conditioned on P ∧ ~~ P'.

Lemma workload_of_jobs_case_on_pred :

workload_of_jobs P jobs =

workload_of_jobs (fun j ⇒ P j && P' j) jobs + workload_of_jobs (fun j ⇒ P j && ~~ P' j) jobs.

workload_of_jobs P jobs =

workload_of_jobs (fun j ⇒ P j && P' j) jobs + workload_of_jobs (fun j ⇒ P j && ~~ P' j) jobs.

We show that if P is indistinguishable from P' on set
jobs, then workload_of_jobs conditioned on P is equal to
workload_of_jobs conditioned on P'.

Lemma workload_of_jobs_equiv_pred :

{in jobs, P =1 P'} →

workload_of_jobs P jobs = workload_of_jobs P' jobs.

End PredicateProperties.

End WorkloadFacts.

{in jobs, P =1 P'} →

workload_of_jobs P jobs = workload_of_jobs P' jobs.

End PredicateProperties.

End WorkloadFacts.