Require Import prosa.classic.util.all.
Require Import prosa.classic.model.schedule.global.workload prosa.classic.model.schedule.global.response_time
prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.model.schedule.global.jitter.job prosa.classic.model.schedule.global.jitter.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.

Variable R_tsk: time. (* Known response-time bound for the task *)
Variable delta: time. (* Length of the interval *)

(* Bound on the number of jobs that execute completely in the interval *)
Definition max_jobs_jitter :=
div_floor (delta + task_jitter tsk + R_tsk - task_cost tsk) (task_period tsk).

(* Bertogna and Cirinei's bound on the workload of a task in an interval of length delta *)
Definition W_jitter :=
let e_k := (task_cost tsk) in
let p_k := (task_period tsk) in
minn e_k (delta + task_jitter tsk + R_tsk - e_k - max_jobs_jitter × p_k) + max_jobs_jitter × e_k.

Section BasicLemmas.

(* Let tsk be any task...*)

(* ...with period > 0. *)
Hypothesis H_period_positive: task_period tsk > 0.

(* Let R1 <= R2 be two response-time bounds that
are larger than the cost of the tsk. *)

Variable R1 R2: time.
Hypothesis H_R_lower_bound: R1 task_cost tsk.
Hypothesis H_R1_le_R2: R1 R2.

(* Then, Bertogna and Cirinei's workload bound is monotonically increasing. *)
Lemma W_monotonic :
t1 t2,
t1 t2
Proof.
intros t1 t2 LEt.
unfold workload_bound, W_jitter, max_jobs_jitter, div_floor; rewrite 2!subndiv_eq_mod.
set e := task_cost tsk; set p := task_period tsk; set j := task_jitter tsk.
set x1 := t1 + j + R1.
set x2 := t2 + j + R2.
set delta := x2 - x1.
last by rewrite leq_add // leq_add //.

induction delta; first by rewrite addn0 leqnn.
{
apply (leq_trans IHdelta).

(* Prove special case for p <= 1. *)
destruct (leqP p 1) as [LTp | GTp].
{
rewrite leq_eqVlt in LTp; move: LTp ⇒ /orP LTp; des;
last by rewrite ltnS in LTp; apply (leq_trans H_period_positive) in LTp.
{
rewrite LTp 2!modn1 2!divn1.
rewrite leq_add2l leq_mul2r; apply/orP; right.
by rewrite leq_sub2r // leq_add2l.
}
}
(* Harder case: p > 1. *)
{
assert (EQ: (x1 + delta.+1 - e) = (x1 + delta - e).+1).
{
rewrite -[(x1 + delta - e).+1]addn1.
{
apply (leq_trans H_R_lower_bound).
}
} rewriteEQ in *; clear EQ.

have DIV := divSn_cases (x1 + delta - e) p GTp; des.
{
rewrite DIV leq_add2r leq_min; apply/andP; split;
first by rewrite geq_minl.
by apply leq_trans with (n := (x1 + delta - e) %% p);
[by rewrite geq_minr | by rewrite -DIV0 addn1 leqnSn].
}
{
rewrite -[minn e _]add0n -addnA; apply leq_add; first by ins.
rewrite -DIV mulnDl mul1n [_ + e]addnC.
by apply leq_add; [by rewrite geq_minl | by ins].
}
}
}
Qed.

End BasicLemmas.

Context {Job: eqType}.
Variable job_arrival: Job time.
Variable job_cost: Job time.
Variable job_deadline: Job time.
Variable job_jitter: Job time.

(* Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.

(* ...where jobs have valid parameters. *)
Hypothesis H_jobs_have_valid_parameters:
j,
arrives_in arr_seq j

(* Consider any schedule of this arrival sequence. *)
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.

(* Assumption: jobs only execute after the jitter.
This is used to discard the workload of jobs that arrive after
the end of the interval t1 + delta. *)

Hypothesis H_jobs_must_arrive_to_execute:
jobs_execute_after_jitter job_arrival job_jitter sched.

(* Assumption: jobs do not execute after they completed.
This is used to eliminate jobs that complete before the start of the interval t1. *)

Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.

(* Assumption: Jobs are sequential.
This is required to use interval lengths as a measure of service. *)

Hypothesis H_sequential_jobs: sequential_jobs sched.

This is necessary to conclude that consecutive jobs ordered by arrival times
are separated by at least 'period' times units. *)

(* Before starting the proof, let's give simpler names to the definitions. *)
Let job_has_completed_by := completed job_cost sched.

(* Now we define the theorem. Let tsk be any task in the taskset. *)

(* Assumption: the task must have valid parameters:
a) period > 0 (used in divisions)
b) deadline of the jobs = deadline of the task
c) cost <= period
(used to prove that the distance between the first and last
jobs is at least (cost + n*period), where n is the number
of middle jobs. If cost >> period, the claim does not hold
for every task set. *)

(* Assumption: the task must have a constrained deadline.
This is required to prove that n_k (max_jobs) from Bertogna
and Cirinei's formula accounts for at least the number of
middle jobs (i.e., number of jobs - 2 in the worst case). *)

(* Consider an interval t1, t1 + delta). *)
Variable t1 delta: time.

(* Assume that a response-time bound R_tsk for that task in any
schedule of this processor platform is also given,
such that R_tsk >= task_cost tsk, and task_jitter tsk + R_tsk <= task_deadline tsk. *)

Variable R_tsk: time.

Hypothesis H_response_time_ge_cost: R_tsk task_cost tsk.

Hypothesis H_response_time_bound :
j,
arrives_in arr_seq j
job_task j = tsk
job_arrival j + task_jitter tsk + R_tsk < t1 + delta
job_has_completed_by j (job_arrival j + task_jitter tsk + R_tsk).

Section MainProof.

(* In this section, we prove that the workload of a task in the
interval t1, t1 + delta) is bounded by W. *)

(* Let's simplify the names a bit. *)
Let t2 := t1 + delta.
Let n_k := max_jobs_jitter task_cost task_period task_jitter tsk R_tsk delta.

(* Since we only care about the workload of tsk, we restrict
our view to the set of jobs of tsk scheduled in t1, t2). *)

Let scheduled_jobs :=

(* Now, let's consider the list of interfering jobs sorted by arrival time. *)
Let earlier_arrival := fun x yjob_arrival x job_arrival y.
Let sorted_jobs := (sort earlier_arrival scheduled_jobs).

(* The first step consists in simplifying the sum corresponding
to the workload. *)

Section SimplifyJobSequence.

(* After switching to the definition of workload based on a list
of jobs, we show that sorting the list preserves the sum. *)

workload_joblist job_task sched tsk t1 t2 =
\sum_(i <- sorted_jobs) service_during sched i t1 t2.
Proof.
unfold workload_joblist; fold scheduled_jobs.
rewrite (perm_big sorted_jobs) /= //.
by rewrite -(perm_sort earlier_arrival).
Qed.

(* Remember that both sequences have the same set of elements *)
j,
(j \in scheduled_jobs) = (j \in sorted_jobs).
Proof.
by apply perm_mem; rewrite -(perm_sort earlier_arrival).
Qed.

(* Remember that all jobs in the sorted sequence is an
interfering job of task tsk. *)

j_i,
j_i \in sorted_jobs
arrives_in arr_seq j_i
job_task j_i = tsk
service_during sched j_i t1 t2 != 0
j_i \in jobs_scheduled_between sched t1 t2.
Proof.
rename H_jobs_come_from_arrival_sequence into FROMarr.
intros j_i LTi.
rewrite -workload_bound_job_in_same_sequence mem_filter in LTi; des.
have IN := LTi0.
unfold jobs_scheduled_between in *; rewrite mem_undup in IN.
apply mem_bigcat_nat_exists in IN; des.
rewrite mem_scheduled_jobs_eq_scheduled in IN.
repeat split; try (by done); first by apply (FROMarr j_i i).
apply service_implies_cumulative_service with (t := i);
first by apply/andP; split.
by rewrite -not_scheduled_no_service negbK.
Qed.

(* Remember that consecutive jobs are ordered by arrival. *)
i elem,
i < (size sorted_jobs).-1
earlier_arrival (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1).
Proof.
intros i elem LT.
assert (SORT: sorted earlier_arrival sorted_jobs).
by apply sort_sorted; unfold total, earlier_arrival; ins; apply leq_total.
by destruct sorted_jobs; simpl in *; [by rewrite ltn0 in LT | by apply/pathP].
Qed.

End SimplifyJobSequence.

(* Next, we show that if the number of jobs is no larger than n_k,
the workload bound trivially holds. *)

size sorted_jobs n_k
\sum_(i <- sorted_jobs) service_during sched i t1 t2
Proof.
intros LEnk.
rewrite -[\sum_(_ <- _ | _) _]add0n leq_add //.
apply leq_trans with (n := \sum_(x <- sorted_jobs) task_cost tsk);
last by rewrite big_const_seq iter_addn addn0 mulnC leq_mul2r; apply/orP; right.
rewrite [\sum_(_ <- _) service_during _ _ _ _]big_seq_cond.
rewrite [\sum_(_ <- _) task_cost _]big_seq_cond.
apply leq_sum; intros j_i; move/andP ⇒ [INi _].
apply workload_bound_all_jobs_from_tsk in INi; des.
[by apply H_completed_jobs_dont_execute | by apply INi0 |].
by apply H_jobs_have_valid_parameters.
Qed.

(* Otherwise, assume that the number of jobs is larger than n_k >= 0.
First, consider the simple case with only one job. *)

(* Assume that there's at least one job in the sorted list. *)
Hypothesis H_at_least_one_job: size sorted_jobs > 0.

Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.

(* The first job is an interfering job of task tsk. *)
arrives_in arr_seq j_fst
job_task j_fst = tsk
service_during sched j_fst t1 t2 != 0
j_fst \in jobs_scheduled_between sched t1 t2.
Proof.
by apply workload_bound_all_jobs_from_tsk, mem_nth.
Qed.

(* The workload bound holds for the single job. *)
\sum_(0 i < 1) service_during sched (nth elem sorted_jobs i) t1 t2
Proof.
unfold workload_bound, W_jitter; fold n_k.
have INfst := workload_bound_j_fst_is_job_of_tsk; des.
rewrite big_nat_recr // big_geq // [nth]lock /= -lock add0n.
destruct n_k; last first.
{
rewrite -[service_during _ _ _ _]add0n; rewrite leq_add //.
rewrite -[service_during _ _ _ _]add0n [_× task_cost tsk]mulSnr.
apply leq_add; first by done.
[| by apply INfst0 | by apply H_jobs_have_valid_parameters].
}
{
rewrite 2!mul0n addn0 subn0 leq_min; apply/andP; split;
first by eapply cumulative_service_le_task_cost;
[| by apply INfst0 | by apply H_jobs_have_valid_parameters].
rewrite -addnBA // -[service_during _ _ _ _]addn0.
rewrite -addnA; apply leq_add; last by done.
by apply cumulative_service_le_delta.
}
Qed.

(* Next, consider the last case where there are at least two jobs:
the first job j_fst, and the last job j_lst. *)

(* There are at least two jobs. *)
Variable num_mid_jobs: nat.
Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.

Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.

(* The last job is an interfering job of task tsk. *)
arrives_in arr_seq j_lst
job_task j_lst = tsk
service_during sched j_lst t1 t2 != 0
j_lst \in jobs_scheduled_between sched t1 t2.
Proof.
by rewrite H_at_least_two_jobs.
Qed.

(* The response time of the first job must fall inside the interval. *)
t1 job_arrival j_fst + task_jitter tsk + R_tsk.
Proof.
rename H_jobs_have_valid_parameters into JOBPARAMS.
unfold valid_sporadic_job_with_jitter in ×.
rewrite leqNgt; apply /negP; unfold not; intro LTt1.
{
apply mem_nth; instantiate (1 := 0).
apply ltn_trans with (n := 1); [by done | by rewrite H_at_least_two_jobs].
}
instantiate (1 := elem); move ⇒ [FSTARR [FSTtsk [/eqP FSTserv FSTin]]].
apply FSTserv.
( try ( apply cumulative_service_after_job_rt_zero with (job_arrival0 := job_arrival)
(job_cost0 := job_cost) (R := task_jitter tsk + R_tsk) ) ||
apply cumulative_service_after_job_rt_zero with (job_arrival := job_arrival)
(job_cost := job_cost) (R := task_jitter tsk + R_tsk));
[by done | | by rewrite addnA ltnW].
rewrite addnA; apply H_response_time_bound; try (by done).
by apply leq_trans with (n := t1); last by apply leq_addr.
Qed.

(* The arrival of the last job must also fall inside the interval. *)
job_arrival j_lst < t2.
Proof.
rewrite leqNgt; apply/negP; unfold not; intro LT2.
{
apply mem_nth; instantiate (1 := num_mid_jobs.+1).
}
instantiate (1 := elem); move ⇒ [LSTarr [LSTtsk [/eqP LSTserv LSTin]]].
apply LSTserv.
apply (cumulative_service_before_job_arrival_zero job_arrival); last by done.
try ( by apply arrival_before_jitter with (job_jitter0 := job_jitter) ) ||
by apply arrival_before_jitter with (job_jitter := job_jitter).
Qed.

(* Next, we upper-bound the service of the first and last jobs using their arrival times. *)
service_during sched j_fst t1 t2 +
service_during sched j_lst t1 t2
(job_arrival j_fst + task_jitter tsk + R_tsk - t1) + (t2 - job_arrival j_lst).
Proof.
apply leq_add; unfold service_during.
{
rewrite -[_ + _ - _]mul1n -[1×_]addn0 -iter_addn -big_const_nat.
apply leq_trans with (n := \sum_(t1 t < job_arrival j_fst + task_jitter tsk + R_tsk)
service_at sched j_fst t);
last by apply leq_sum; ins; apply service_at_most_one.
destruct (job_arrival j_fst + task_jitter tsk + R_tsk < t2) eqn:LEt2; last first.
{
unfold t2; apply negbT in LEt2; rewrite -ltnNge in LEt2.
rewritebig_cat_nat with (n := t1 + delta) (p := job_arrival j_fst + task_jitter tsk + R_tsk);
[by apply leq_addr | by apply leq_addr | by done].
}
{
rewritebig_cat_nat with (n := job_arrival j_fst + task_jitter tsk + R_tsk);
[simpl
| by apply ltnW].
rewrite [\sum_(_ _ < t2)_]
(cumulative_service_after_job_rt_zero job_arrival job_cost _ _ _
(task_jitter tsk + R_tsk)); rewrite ?leqnn //; first by rewrite addn0 leqnn.
have ALL := workload_bound_all_jobs_from_tsk j_fst.
feed ALL; first by apply mem_nth; rewrite H_at_least_two_jobs.
move: ALL ⇒ [FSTarr [FSTtsk _]].
by apply H_response_time_bound.
}
}
{
rewrite -[_ - _]mul1n -[1 × _]addn0 -iter_addn -big_const_nat.
destruct (job_arrival j_lst t1) eqn:LT.
{
apply leq_trans with (n := \sum_(job_arrival j_lst t < t2)
service_at sched j_lst t);
last by apply leq_sum; ins; apply service_at_most_one.
rewritebig_cat_nat with (m := job_arrival j_lst) (n := t1);
[by apply leq_addl | by done | by apply leq_addr].
}
{
apply negbT in LT; rewrite -ltnNge in LT.
rewritebig_cat_nat with (n := job_arrival j_lst);
[| by apply ltnW
| by apply ltnW, workload_bound_last_job_arrives_before_end_of_interval].
rewrite /= -[\sum_(_ _ < _) 1]add0n; apply leq_add;
last by apply leq_sum; ins; apply service_at_most_one.
rewrite (cumulative_service_before_job_arrival_zero job_arrival);
[by apply leqnn | | by apply leqnn].
try ( by apply arrival_before_jitter with (job_jitter0 := job_jitter) ) ||
by apply arrival_before_jitter with (job_jitter := job_jitter).
}
}
Qed.

(* Simplify the expression from the previous lemma. *)
job_arrival j_fst + task_jitter tsk + R_tsk - t1 + (t2 - job_arrival j_lst) =
delta + task_jitter tsk + R_tsk - (job_arrival j_lst - job_arrival j_fst).
Proof.
have lemma1 := workload_bound_last_job_arrives_before_end_of_interval.
have lemma2 := workload_bound_response_time_of_first_job_inside_interval.
rewrite addnBA; last by apply ltnW.
rewrite addnBAC; last by done.

rewrite addnC; unfold t2.
rewrite [t1 + _]addnC -[delta + t1 - _]subnBA // subnn subn0.
rewrite addnA -subnBA; last first.
{
unfold j_fst, j_lst; rewrite -[_.+1]add0n.
apply prev_le_next; last by rewrite add0n H_at_least_two_jobs ltnSn.
by ins; apply workload_bound_jobs_ordered_by_arrival.
}
Qed.

(* Bound the service of the middle jobs. *)
\sum_(0 i < num_mid_jobs)
service_during sched (nth elem sorted_jobs i.+1) t1 t2
num_mid_jobs × task_cost tsk.
Proof.
apply leq_trans with (n := num_mid_jobs × task_cost tsk);
last by rewrite leq_mul2l; apply/orP; right.
apply leq_trans with (n := \sum_(0 i < num_mid_jobs) task_cost tsk);
last by rewrite big_const_nat iter_addn addn0 mulnC subn0.
rewrite big_nat_cond [\sum_(0 i < num_mid_jobs) task_cost _]big_nat_cond.
apply leq_sum; intros i; rewrite andbT; move ⇒ /andP LT; des.
{
instantiate (1 := nth elem sorted_jobs i.+1).
apply mem_nth; rewrite H_at_least_two_jobs.
by rewrite ltnS; apply leq_trans with (n := num_mid_jobs).
}
move ⇒ [ARRin [JOBtsk _]].
[by apply H_completed_jobs_dont_execute | | by apply H_jobs_have_valid_parameters].
Qed.

(* Conclude that the distance between first and last is at least num_mid_jobs + 1 periods. *)
job_arrival j_lst - job_arrival j_fst num_mid_jobs.+1 × (task_period tsk).
Proof.
assert (EQnk: num_mid_jobs.+1=(size sorted_jobs).-1).
by rewrite H_at_least_two_jobs.
unfold j_fst, j_lst; rewrite EQnk telescoping_sum;
last by ins; apply workload_bound_jobs_ordered_by_arrival.
rewrite -[_ × _ tsk]addn0 mulnC -iter_addn -{1}[_.-1]subn0 -big_const_nat.
rewrite big_nat_cond [\sum_(0 i < _)(_-_)]big_nat_cond.
apply leq_sum; intros i; rewrite andbT; move ⇒ /andP LT; des.

(* To simplify, call the jobs 'cur' and 'next' *)
set cur := nth elem sorted_jobs i.
set next := nth elem sorted_jobs i.+1.

have ALL := workload_bound_all_jobs_from_tsk.

(* Show that cur arrives earlier than next *)
assert (ARRle: job_arrival cur job_arrival next).
by unfold cur, next; apply workload_bound_jobs_ordered_by_arrival.

by apply mem_nth, (ltn_trans LT0); destruct sorted_jobs.
intros [CURarr [CURtsk [_ CURin]]].

by apply mem_nth; destruct sorted_jobs.
intros [NEXTarr [NEXTtsk [_ NEXTin]]].

(* Use the sporadic task model to conclude that cur and next are separated
by at least (task_period tsk) units. Of course this only holds if cur != next.
Since we don't know much about the list (except that it's sorted), we must
also prove that it doesn't contain duplicates. *)

assert (CUR_LE_NEXT: job_arrival cur + task_period (job_task cur) job_arrival next).
{
unfold cur, next, not; intro EQ; move: EQ ⇒ /eqP EQ.
rewrite nth_uniq in EQ; first by move: EQ ⇒ /eqP EQ; lia.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/scheduled_jobs filter_uniq // undup_uniq.
by rewrite CURtsk NEXTtsk.
}
by rewrite leq_subRL_impl // -CURtsk.
Qed.

(* Prove that n_k is at least the number of the middle jobs *)
n_k num_mid_jobs.
Proof.
rename H_valid_task_parameters into PARAMS.
rewrite leqNgt; apply/negP; unfold not; intro LTnk.
assert (DISTmax: job_arrival j_lst - job_arrival j_fst delta + task_period tsk).
{
apply leq_trans with (n := n_k.+2 × task_period tsk).
{
apply leq_trans with (n := delta + task_jitter tsk + R_tsk - task_cost tsk);
by apply ltnW, ltn_ceil, PARAMS0.
}
apply leq_trans with (num_mid_jobs.+1 × task_period tsk);
first by rewrite leq_mul2r; apply/orP; right.
}
rewrite <- leq_add2r with (p := job_arrival j_fst) in DISTmax.
rewrite addnC addnBAC in DISTmax; last first.
{
unfold j_fst, j_lst; rewrite -[_.+1]add0n.
apply prev_le_next; last by rewrite H_at_least_two_jobs add0n leqnn.
by ins; apply workload_bound_jobs_ordered_by_arrival.
}
rewrite -subnBA // subnn subn0 in DISTmax.
have BEFOREt2 := workload_bound_last_job_arrives_before_end_of_interval.
generalize BEFOREt2; move: BEFOREt2; rewrite {1}ltnNge; move ⇒ /negP BEFOREt2'.
intros BEFOREt2; apply BEFOREt2'; clear BEFOREt2'.
apply leq_trans with (n := job_arrival j_fst + task_deadline tsk + delta);
last first.
{
apply leq_trans with (n := job_arrival j_fst + task_period tsk + delta); last by done.
}
{
unfold t2; rewrite leq_add2r.
apply leq_trans with (n := job_arrival j_fst + task_jitter tsk + R_tsk);
}
Qed.

(* If n_k = num_mid_jobs, then the workload bound holds. *)
num_mid_jobs = n_k
service_during sched j_lst t1 t2 +
service_during sched j_fst t1 t2 +
\sum_(0 i < num_mid_jobs)
service_during sched (nth elem sorted_jobs i.+1) t1 t2
Proof.
rename H_valid_task_parameters into PARAMS.
unfold workload_bound, W_jitter; fold n_k.
moveNK; rewrite -NK.
last by apply workload_bound_service_of_middle_jobs.
apply leq_trans with (n := delta + task_jitter tsk + R_tsk -
(job_arrival j_lst - (job_arrival j_fst))).
{
}
rewrite leq_min; apply/andP; split.
{
rewrite leq_subLR [_ + task_cost _]addnC -leq_subLR.
apply leq_trans with (num_mid_jobs.+1 × task_period tsk);
last by apply workload_bound_many_periods_in_between.
rewrite NK ltnW // -ltn_divLR; last by apply PARAMS0.
unfold n_k, max_jobs_jitter, div_floor.
by unfold n_k, max_jobs_jitter, div_floor.
}
{
rewrite -subnDA; apply leq_sub2l.
apply leq_trans with (n := num_mid_jobs.+1 × task_period tsk);
last by apply workload_bound_many_periods_in_between.
by rewrite leq_add2l; last by apply PARAMS3.
}
Qed.

(* If n_k = num_mid_jobs + 1, then the workload bound holds. *)
num_mid_jobs.+1 = n_k
service_during sched j_lst t1 t2 +
service_during sched j_fst t1 t2 +
\sum_(0 i < num_mid_jobs)
service_during sched (nth elem sorted_jobs i.+1) t1 t2
Proof.
have MID := workload_bound_service_of_middle_jobs.
rename H_jobs_have_valid_parameters into JOBPARAMS.
unfold valid_sporadic_job_with_jitter in *; des.
unfold workload_bound, W_jitter; fold n_k.
moveNK; rewrite -NK.
apply leq_add; last first.
apply MID.
rewrite leq_min; apply/andP; split.
{
assert (SIZE: 0 < size sorted_jobs).
by rewrite H_at_least_two_jobs.
have INfst := workload_bound_j_fst_is_job_of_tsk SIZE elem;
have INlst := workload_bound_j_lst_is_job_of_tsk; des.
have PARAMSfst := JOBPARAMS j_fst INfst; des.
have PARAMSlst := JOBPARAMS j_lst INlst; des.
try ( by apply leq_add; apply cumulative_service_le_task_cost with
}
{
rewrite subnAC subnK; last first.
{
assert (TMP: delta + task_jitter tsk + R_tsk = task_cost tsk + (delta + task_jitter tsk + R_tsk - task_cost tsk));
first by rewrite subnKC; [by ins | by rewrite -[task_cost _]add0n; apply leq_add].
rewrite TMP; clear TMP.
}
apply leq_trans with (n := delta + task_jitter tsk + R_tsk - num_mid_jobs.+1 × task_period tsk);
last by rewrite leq_sub2r // leq_add2r leq_addr.
apply leq_trans with (delta + task_jitter tsk +R_tsk - (job_arrival j_lst - job_arrival j_fst)).
{
}
{
by apply leq_sub2l, workload_bound_many_periods_in_between.
}
}
Qed.

(* Using the lemmas above, we prove the main theorem about the workload bound. *)
workload_of tsk t1 (t1 + delta) workload_bound.
Proof.
unfold workload_of, workload_bound, W_jitter in *; ins; des.
fold n_k.

(* Use the definition of workload based on list of jobs. *)

(* Now we order the list by job arrival time. *)

(* Next, we show that the workload bound holds if n_k
is no larger than the number of interferings jobs. *)

destruct (size sorted_jobs n_k) eqn:NUM;
first by apply workload_bound_holds_for_at_most_n_k_jobs.
apply negbT in NUM; rewrite -ltnNge in NUM.

(* Find some dummy element to use in the nth function *)
assert (EX: elem: Job, True).
destruct sorted_jobs; [ by rewrite ltn0 in NUM | by s].
destruct EX as [elem _].

(* Now we index the sum to access the first and last elements. *)
rewrite (big_nth elem).

(* First, we show that the bound holds for an empty list of jobs. *)
destruct (size sorted_jobs) as [| n] eqn:SIZE;
first by rewrite big_geq.

(* Then, we show the same for a singleton set of jobs. *)
destruct n as [| num_mid_jobs];
first by apply workload_bound_holds_for_a_single_job; rewrite SIZE.

(* Knowing that we have at least two elements, we take first and last out of the sum *)
rewrite [nth]lock big_nat_recl // big_nat_recr // /= -lock.

(* There are two cases to be analyze since n <= n_k < n + 2,
where n is the number of middle jobs. *)

have NK := workload_bound_n_k_covers_middle_jobs num_mid_jobs SIZE elem.
move: NK; rewrite leq_eqVlt orbC leq_eqVlt; move ⇒ /orP [NK | /eqP NK].
move: NK ⇒ /orP [/eqP NK | NK]; last by rewrite ltnS leqNgt NK in NUM.
{
(* Case 1: n_k = n + 1, where n is the number of middle jobs. *)
by apply (workload_bound_n_k_equals_num_mid_jobs_plus_1 num_mid_jobs).
}
{
(* Case 2: n_k = n, where n is the number of middle jobs. *)
by apply (workload_bound_n_k_equals_num_mid_jobs num_mid_jobs).
}
Qed.

End MainProof.