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 `{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.
(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 ].
Proof.
moveP1 P2 jobs IMPL.
apply: eq_biglj.
case: (boolP (j \in jobs)) ⇒ // IN.
rewrite !andTb.
case: (boolP (P1 j)) ⇒ //= P1j; first by rewrite (IMPL j IN P1j).
by rewrite andbF.
Qed.

We establish that if the predicate P1 implies the predicate P2, then the cumulative workload of jobs that respect P1 is bounded by the cumulative workload of jobs that respect P2.
(P1 P2 : pred Job) (jobs : seq Job),
( j, P1 j P2 j)
Proof.
moveP1 P2 jobs IMPLIES; rewrite /workload_of_jobs.
apply: leq_sum_seq_predj' _.
by apply: IMPLIES.
Qed.

The cumulative workload of jobs from an empty sequence is always zero.
(P : pred Job), workload_of_jobs P [::] = 0.
Proof. by move ⇒ ?; rewrite /workload_of_jobs big_nil. Qed.

The workload of a set of jobs can be equivalently rewritten as sum over their tasks.
{P : pred Job} (Q : pred Task) {js : seq Job} (ts : seq Task),
{in js, j, (job_task j) \in ts}
{in js, j, P j Q (job_task j)}
uniq js
uniq ts
let P_and_job_of tsk_o j := P j && (job_task j == tsk_o) in
= \sum_(tsk_o <- ts | Q tsk_o ) workload_of_jobs (P_and_job_of tsk_o) js.
Proof.
moveP Q js ts IN_ts PQ UJ UT //=.
apply: sum_over_partitions_eq ⇒ // [j IN Px|]; last exact: filter_uniq.
rewrite mem_filter; apply/andP; split; last by apply: IN_ts.
by apply: PQ.
Qed.

Next, consider any job arrival sequence consistent with the arrival times of the jobs.
In this section, we bound the workload of jobs of a particular task by the task's RBF.

Consider a valid arrival curve that is respected by the task tsk.
Suppose all arrivals have WCET-compliant job costs.
Consider an instant t1 and a duration Δ.
Variable t1 : instant.
Variable Δ : duration.

We prove that the workload of jobs of a task tsk in any interval is bound by the request bound function of the task in that interval.
Proof.
apply: (@leq_trans (task_cost tsk × number_of_task_arrivals arr_seq tsk t1 (t1 + Δ))).
apply: sum_majorant_constantj IN TSK.
have: valid_job_cost j; last by rewrite /valid_job_cost; move: TSK ⇒ /eqP →.
exact/H_valid_job_cost/in_arrivals_implies_arrived. }
{ rewrite leq_mul2l; apply/orP; right.
Qed.

For convenience, we combine the preceding bound with workload_of_jobs_weaken, as the two are often used together.
P,
(arrivals_between arr_seq t1 (t1 + Δ))
Proof.
moveP.
have LEQ: ar, workload_of_jobs (fun j : JobP j && (job_task j == tsk)) ar
by movear; apply: workload_of_jobs_weakenj /andP [_ +].
Qed.

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.
{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).
Proof.
moveP t1 t2 t LE IMPL.
have → : arrivals_between arr_seq t1 t = [seq j <- (arrivals_between arr_seq t1 t2) | job_arrival j < t]
by apply: arrivals_between_filter.
rewrite (workload_of_jobs_filter _ (fun jjob_arrival j < t)) // ⇒ j IN Pj.
case: (leqP t (job_arrival j)) ⇒ // TAIL.
by move: (IMPL j IN TAIL) ⇒ /negP.
Qed.

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.
t t1 t2 P,
t1 t t2
workload_of_jobs P (arrivals_between t1 t2) =
Proof.
movet t1 t2 P /andP [GE LE].
by rewrite (arrivals_between_cat _ _ t) // big_cat.
Qed.

Consider a job j ...
Variable j : Job.

... and a duplicate-free sequence of jobs jobs.
Variable jobs : seq Job.
Hypothesis H_jobs_uniq : uniq jobs.

Further, assume that j is contained in jobs.
Hypothesis H_j_in_jobs : j \in 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.
workload_of_jobs (fun jhp : Jobjhp != j) jobs =
workload_of_jobs predT jobs - job_cost j.
Proof.
rewrite [in RHS](big_rem j) //= addnC -subnBA //= subnn subn0.
rewrite [in LHS]big_seq_cond [in RHS]big_seq_cond.
apply eq_biglj'.
rewrite Bool.andb_true_r.
destruct (j' \in rem (T:=Job) j jobs) eqn:INjobs ⇒ [|//].
apply /negP ⇒ /eqP EQUAL.
by rewrite EQUAL mem_rem_uniqF in INjobs.
Qed.

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

Assume that arrival times are consistent and that arrivals are unique.
Consider a time interval `[t1, t2)` and a time instant t.
Variable t1 t2 t : instant.
Hypothesis H_t1_le_t2 : t1 t2.

Let P be an arbitrary predicate on jobs.
Variable P : pred Job.

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.
workload_of_jobs (fun j(job_arrival j t) && P j) (arrivals_between t1 t2)
workload_of_jobs (fun jP j) (arrivals_between t1 (t + ε)).
Proof.
clear H_jobs_uniq H_j_in_jobs H_t1_le_t2.
rewrite -[in X in X _]big_filter -[in X in _ X]big_filter.
apply leq_sum_sub_uniq; first by apply filter_uniq, arrivals_uniq.
movej'; rewrite mem_filter ⇒ [/andP [/andP [A /andP [C D]] _]].
rewrite mem_filter; apply/andP; split⇒ [//|].
apply job_in_arrivals_between; eauto.
- by eapply in_arrivals_implies_arrived; eauto 2.
- apply in_arrivals_implies_arrived_between in A; auto; move: A ⇒ /andP [A E].
by apply/andP; split; lia.
Qed.

End Subset.

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

First, we show that workload of jobs for an unsatisfiable predicate is equal to 0.
Proof. by rewrite /workload_of_jobs; apply big_pred0. Qed.

Next, consider two arbitrary predicates P and P'.
Variable P P' : pred Job.

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'.
workload_of_jobs (fun jP j && P' j) jobs + workload_of_jobs (fun jP j && ~~ P' j) jobs.
Proof.
rewrite /workload_of_jobs !big_mkcond [in X in _ = X]big_mkcond
[in X in _ = _ + X]big_mkcond //= -big_split //=.
apply: eq_big_seqj' IN.
by destruct (P _), (P' _); simpl; lia.
Qed.

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