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.

Next, consider any job arrival sequence consistent with the arrival times of the jobs.
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; last by done.
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; rt_eauto.
movej'; rewrite mem_filter ⇒ [/andP [/andP [A /andP [C D]] _]].
rewrite mem_filter; apply/andP; split; first by done.
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 unfold ε; 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'.