Commit 3fe914e0 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Remove incomplete/broken files and fix Makefile

parent 578dd89e
......@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
# coq_makefile arrival_sequence.v bertogna_edf_comp.v bertogna_edf_theory.v bertogna_fp_comp.v bertogna_fp_jitter_comp.v bertogna_fp_jitter_theory.v bertogna_fp_theory.v extralib.v ExtraRelations.v guan_fp_comp.v guan_fp_theory.v interference_bound_edf.v interference.v job.v platform.v priority.v response_time.v schedulability.v schedule.v ssromega.v task_arrival.v task.v util_divround.v util_lemmas.v Vbase.v workload_bound.v workload_guan.v workload_jitter.v workload.v
# coq_makefile arrival_sequence.v bertogna_edf_comp.v bertogna_edf_theory.v bertogna_fp_comp.v bertogna_fp_theory.v interference_bound_edf.v interference.v job.v platform.v priority.v response_time.v schedulability.v schedule.v ssromega.v task_arrival.v task.v util_divround.v util_lemmas.v Vbase.v workload_bound.v workload.v
#
.DEFAULT_GOAL := all
......@@ -84,13 +84,7 @@ VFILES:=arrival_sequence.v\
bertogna_edf_comp.v\
bertogna_edf_theory.v\
bertogna_fp_comp.v\
bertogna_fp_jitter_comp.v\
bertogna_fp_jitter_theory.v\
bertogna_fp_theory.v\
extralib.v\
ExtraRelations.v\
guan_fp_comp.v\
guan_fp_theory.v\
interference_bound_edf.v\
interference.v\
job.v\
......@@ -106,8 +100,6 @@ VFILES:=arrival_sequence.v\
util_lemmas.v\
Vbase.v\
workload_bound.v\
workload_guan.v\
workload_jitter.v\
workload.v
-include $(addsuffix .d,$(VFILES))
......
Require Import Vbase job task schedule task_arrival priority workload_jitter
bertogna_fp_jitter_theory interference platform
schedulability response_time util_divround util_lemmas
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
Module ResponseTimeIterationFPWithJitter.
Import Job ScheduleOfTaskWithJitter SporadicTaskset SporadicTaskArrival Priority WorkloadWithJitter ResponseTimeAnalysisJitter Interference Platform Schedulability ResponseTime.
Section Analysis.
Context {sporadic_task_with_jitter: eqType}.
Variable task_cost: sporadic_task_with_jitter -> nat.
Variable task_period: sporadic_task_with_jitter -> nat.
Variable task_deadline: sporadic_task_with_jitter -> nat.
Variable task_jitter: sporadic_task_with_jitter -> nat.
Let task_with_response_time := (sporadic_task_with_jitter * nat)%type.
Context {Job: eqType}.
Variable job_cost: Job -> nat.
Variable job_deadline: Job -> nat.
Variable job_task: Job -> sporadic_task_with_jitter.
Variable job_jitter: Job -> nat.
Variable num_cpus: nat.
Variable higher_eq_priority: fp_policy sporadic_task_with_jitter.
(* Next we define the fixed-point iteration for computing
Bertogna's response-time bound for any task in ts. *)
Let I (tsk: sporadic_task_with_jitter)
(R_prev: seq task_with_response_time) (delta: time) :=
total_interference_bound_fp_jitter task_cost task_period task_jitter
tsk R_prev delta higher_eq_priority.
(* First, given a sequence of pairs R_prev = [..., (tsk_hp, R_hp)] of
response-time bounds for the higher-priority tasks, we compute
the response-time bound of tsk using the following iteration:
R_tsk <- f^step (R_tsk),
where f is the response-time recurrence,
step is the number of iterations,
and f^0 = task_cost tsk. *)
Definition per_task_rta (tsk: sporadic_task_with_jitter)
(R_prev: seq task_with_response_time) (step: nat) :=
iter step
(fun t => task_cost tsk +
div_floor (I tsk R_prev t) num_cpus)
(task_cost tsk).
(* To ensure that the iteration converges, we will apply per_task_rta
a "sufficient" number of times: task_deadline tsk + 1.
Note that (deadline + 1) is a pessimistic bound on the number of
steps, but we don't care about precise runtime complexity here. *)
Let max_steps (tsk: sporadic_task_with_jitter) :=
task_deadline tsk + 1.
(* Next we compute the response-time bounds for the entire task set.
Since high-priority tasks may not be schedulable, we allow the
computation to fail.
Thus, given the response-time bound of previous tasks, we either
(a) append the response-time bound (tsk, R) of the current task
to the list of pairs, or,
(b) return None if the response-time analysis failed. *)
Definition R_list_helper (hp_pairs: option (seq task_with_response_time))
(tsk: sporadic_task_with_jitter) :=
if hp_pairs is Some rt_bounds then
let R := per_task_rta tsk rt_bounds (max_steps tsk) in
let R' := R + task_jitter tsk in
if R' <= task_deadline tsk then
Some (rcons rt_bounds (tsk, R'))
else None
else None.
(* To return the complete list of response-time bounds for any task set,
we just apply foldl (reduce) using the function above. *)
Definition R_list (ts: taskset_of sporadic_task_with_jitter) : option (seq task_with_response_time) :=
foldl R_list_helper (Some [::]) ts.
(* The schedulability test simply checks if we got a list of
response-time bounds (i.e., if the computation did not fail). *)
Definition fp_schedulable (ts: taskset_of sporadic_task_with_jitter) :=
R_list ts != None.
Section AuxiliaryLemmas.
(* In this section, we prove several helper lemmas about the
list of response-time bounds, such as:
(1) Equality among tasks in R_list and in the task set.
(2) If (tsk, R) \in R_list, then R <= task_deadline tsk.
(3) If (tsk, R) \in R_list, then R >= task_cost tsk.
(4) If per_task_rta returns a bound <= deadline, then the
iteration reached a fixed-point. *)
Lemma R_list_rcons_prefix :
forall ts' hp_bounds tsk1 tsk2 R,
R_list (rcons ts' tsk1) = Some (rcons hp_bounds (tsk2, R)) ->
R_list ts' = Some hp_bounds.
Proof.
intros ts hp_bounds tsk1 tsk2 R SOME.
rewrite -cats1 in SOME.
unfold R_list in *.
rewrite foldl_cat in SOME.
simpl in SOME.
unfold R_list_helper in SOME.
desf; rewrite Heq; rename H0 into EQ.
move: EQ => /eqP EQ.
rewrite eqseq_rcons in EQ.
move: EQ => /andP [/eqP EQ _].
by f_equal.
Qed.
Lemma R_list_rcons_task :
forall ts' hp_bounds tsk1 tsk2 R,
R_list (rcons ts' tsk1) = Some (rcons hp_bounds (tsk2, R)) ->
tsk1 = tsk2.
Proof.
intros ts hp_bounds tsk1 tsk2 R SOME.
rewrite -cats1 in SOME.
unfold R_list in *.
rewrite foldl_cat in SOME.
simpl in SOME.
unfold R_list_helper in SOME.
desf; rename H0 into EQ.
move: EQ => /eqP EQ.
rewrite eqseq_rcons in EQ.
move: EQ => /andP [_ /eqP EQ].
by inversion EQ.
Qed.
Lemma R_list_rcons_response_time :
forall ts' hp_bounds tsk R,
R_list (rcons ts' tsk) = Some (rcons hp_bounds (tsk, R)) ->
R = per_task_rta tsk hp_bounds (max_steps tsk) + task_jitter tsk.
Proof.
intros ts hp_bounds tsk R SOME.
rewrite -cats1 in SOME.
unfold R_list in SOME.
rewrite foldl_cat in SOME.
simpl in SOME.
unfold R_list_helper in SOME.
desf; rename H0 into EQ; move: EQ => /eqP EQ.
rewrite eqseq_rcons in EQ; move: EQ => /andP [/eqP EQ1 /eqP EQ2].
by inversion EQ2; rewrite EQ1.
Qed.
Lemma R_list_le_deadline :
forall ts' rt_bounds tsk R,
R_list ts' = Some rt_bounds ->
(tsk, R) \in rt_bounds ->
R <= task_deadline tsk.
Proof.
intros ts; induction ts as [| ts' tsk_lst] using last_ind.
{
intros rt_bounds tsk R SOME IN.
by inversion SOME; subst; rewrite in_nil in IN.
}
{
intros rt_bounds tsk_i R SOME IN.
destruct (lastP rt_bounds) as [|rt_bounds (tsk_lst', R_lst)];
first by rewrite in_nil in IN.
rewrite mem_rcons in_cons in IN; move: IN => /orP IN.
destruct IN as [LAST | FRONT].
{
move: LAST => /eqP LAST.
rewrite -cats1 in SOME.
unfold R_list in *.
rewrite foldl_cat in SOME.
simpl in SOME.
unfold R_list_helper in SOME.
desf; rename H0 into EQ.
move: EQ => /eqP EQ.
rewrite eqseq_rcons in EQ.
move: EQ => /andP [_ /eqP EQ].
inversion EQ; subst.
by apply Heq0.
}
{
apply IHts with (rt_bounds := rt_bounds); last by ins.
by apply R_list_rcons_prefix in SOME.
}
}
Qed.
Lemma R_list_ge_cost :
forall ts' rt_bounds tsk R,
R_list ts' = Some rt_bounds ->
(tsk, R) \in rt_bounds ->
R >= task_cost tsk.
Proof.
intros ts; induction ts as [| ts' tsk_lst] using last_ind.
{
intros rt_bounds tsk R SOME IN.
by inversion SOME; subst; rewrite in_nil in IN.
}
{
intros rt_bounds tsk_i R SOME IN.
destruct (lastP rt_bounds) as [|rt_bounds (tsk_lst', R_lst)];
first by rewrite in_nil in IN.
rewrite mem_rcons in_cons in IN; move: IN => /orP IN.
destruct IN as [LAST | FRONT].
{
move: LAST => /eqP LAST.
rewrite -cats1 in SOME.
unfold R_list in *.
rewrite foldl_cat in SOME.
simpl in SOME.
unfold R_list_helper in SOME.
desf; rename H0 into EQ.
move: EQ => /eqP EQ.
rewrite eqseq_rcons in EQ.
move: EQ => /andP [_ /eqP EQ].
inversion EQ; subst.
by destruct (max_steps tsk_lst');
[by apply leq_addr | by rewrite -addnA leq_addr].
}
{
apply IHts with (rt_bounds := rt_bounds); last by ins.
by apply R_list_rcons_prefix in SOME.
}
}
Qed.
Lemma R_list_non_empty :
forall ts' rt_bounds tsk,
R_list ts' = Some rt_bounds ->
(tsk \in ts' <->
exists R,
(tsk, R) \in rt_bounds).
Proof.
intros ts; induction ts as [| ts' tsk_lst] using last_ind.
{
intros rt_bounds tsk SOME.
inversion SOME; rewrite in_nil; split; first by ins.
by intro EX; des; rewrite in_nil in EX.
}
{
intros rt_bounds tsk_i SOME.
destruct (lastP rt_bounds) as [|rt_bounds (tsk_lst', R_lst)].
{
split; last first; intro EX; des; first by rewrite in_nil in EX.
unfold R_list in *.
rewrite -cats1 foldl_cat in SOME.
simpl in SOME.
unfold R_list_helper in *; desf; rename H0 into EQ.
destruct l; first by ins.
by rewrite rcons_cons in EQ; inversion EQ.
}
split.
{
intros IN; rewrite mem_rcons in_cons in IN; move: IN => /orP IN.
destruct IN as [LAST | FRONT].
{
move: LAST => /eqP LAST; subst tsk_i.
generalize SOME; apply R_list_rcons_task in SOME; subst tsk_lst'; intro SOME.
exists R_lst.
by rewrite mem_rcons in_cons; apply/orP; left.
}
{
apply R_list_rcons_prefix in SOME.
exploit (IHts rt_bounds tsk_i); [by ins | intro EX].
apply EX in FRONT; des.
by exists R; rewrite mem_rcons in_cons; apply/orP; right.
}
}
{
intro IN; des.
rewrite mem_rcons in_cons in IN; move: IN => /orP IN.
destruct IN as [LAST | FRONT].
{
move: LAST => /eqP LAST.
inversion LAST; subst tsk_i R; clear LAST.
apply R_list_rcons_task in SOME; subst.
by rewrite mem_rcons in_cons; apply/orP; left.
}
{
rewrite mem_rcons in_cons; apply/orP; right.
exploit (IHts rt_bounds tsk_i);
[by apply R_list_rcons_prefix in SOME | intro EX].
by apply EX; exists R.
}
}
}
Qed.
(* To prove convergence of R, we first show convergence of rt_rec. *) Lemma per_task_rta_converges:
forall ts' tsk rt_bounds,
valid_sporadic_taskset task_cost task_period task_deadline ts' ->
R_list ts' = Some rt_bounds ->
per_task_rta tsk rt_bounds (max_steps tsk) <= task_deadline tsk ->
per_task_rta tsk rt_bounds (max_steps tsk) =
per_task_rta tsk rt_bounds (max_steps tsk).+1.
Proof.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
(* To simplify, let's call the function f.*)
intros ts' tsk rt_bounds VALID SOME LE;
set (f := per_task_rta tsk rt_bounds); fold f in LE.
(* First prove that f is monotonic.*)
assert (MON: forall x1 x2, x1 <= x2 -> f x1 <= f x2).
{
intros x1 x2 LEx; unfold f, per_task_rta.
apply fun_mon_iter_mon; [by ins | by ins; apply leq_addr |].
clear LEx x1 x2; intros x1 x2 LEx.
unfold div_floor, I, total_interference_bound_fp_jitter.
rewrite big_seq_cond [\sum_(i <- _ | let '(tsk_other, _) := i in
_ && (tsk_other != tsk))_]big_seq_cond.
rewrite leq_add2l leq_div2r // leq_sum //.
intros i; destruct (i \in rt_bounds) eqn:HP;
last by rewrite andFb.
destruct i as [i R]; intros _.
have GE_COST := (R_list_ge_cost ts' rt_bounds i R).
have INts := (R_list_non_empty ts' rt_bounds i SOME).
destruct INts as [_ EX]; exploit EX; [by exists R | intro IN].
unfold interference_bound_jitter; simpl.
rewrite leq_min; apply/andP; split.
{
apply leq_trans with (n := W_jitter task_cost task_period task_jitter i R x1);
first by apply geq_minl.
specialize (VALID i IN); des.
by apply W_jitter_monotonic; try (by ins); apply GE_COST.
}
{
apply leq_trans with (n := x1 - task_cost tsk + 1);
first by apply geq_minr.
by rewrite leq_add2r leq_sub2r //.
}
}
(* Either f converges by the deadline or not. *)
unfold max_steps in *; rewrite -> addn1 in *.
destruct ([exists k in 'I_(task_deadline tsk).+1,
f k == f k.+1]) eqn:EX.
{
move: EX => /exists_inP EX; destruct EX as [k _ ITERk].
move: ITERk => /eqP ITERk.
by apply iter_fix with (k := k);
[by ins | by apply ltnW, ltn_ord].
}
apply negbT in EX; rewrite negb_exists_in in EX.
move: EX => /forall_inP EX.
assert (GROWS: forall k: 'I_(task_deadline tsk).+1,
f k < f k.+1).
{
intros k; rewrite ltn_neqAle; apply/andP; split; first by apply EX.
apply MON, leqnSn.
}
(* If it doesn't converge, then it becomes larger than the deadline.
But initialy we assumed otherwise. Contradiction! *)
assert (BY1: f (task_deadline tsk).+1 > task_deadline tsk).
{
clear MON LE EX.
induction (task_deadline tsk).+1; first by ins.
apply leq_ltn_trans with (n := f n);
last by apply (GROWS (Ordinal (ltnSn n))).
apply IHn; intros k.
by apply (GROWS (widen_ord (leqnSn n) k)).
}
by apply leq_ltn_trans with (m := f (task_deadline tsk).+1) in BY1;
[by rewrite ltnn in BY1 | by ins].
Qed.
Lemma per_task_rta_fold :
forall tsk rt_bounds,
task_cost tsk +
div_floor (I tsk rt_bounds (per_task_rta tsk rt_bounds (max_steps tsk))) num_cpus
= per_task_rta tsk rt_bounds (max_steps tsk).+1.
Proof.
by ins.
Qed.
Lemma R_list_unzip1 :
forall ts' tsk hp_bounds R,
transitive higher_eq_priority ->
uniq (rcons ts' tsk) ->
sorted higher_eq_priority (rcons ts' tsk) ->
R_list (rcons ts' tsk) = Some (rcons hp_bounds (tsk, R)) ->
[seq tsk_hp <- rcons ts' tsk | is_interfering_task_fp higher_eq_priority tsk tsk_hp] =
unzip1 hp_bounds.
Proof.
intros ts tsk hp_bounds R TRANS.
revert tsk hp_bounds R.
induction ts as [| ts' tsk_lst] using last_ind.
{
intros tsk hp_bounds R _ _ SOME; simpl in *.
unfold is_interfering_task_fp.
rewrite eq_refl andbF.
destruct hp_bounds; first by ins.
unfold R_list in SOME; inversion SOME; desf.
by destruct hp_bounds.
}
{
intros tsk hp_bounds R UNIQ SORTED SOME.
destruct (lastP hp_bounds) as [| hp_bounds (tsk_lst', R_lst)].
{
apply R_list_rcons_prefix in SOME.
unfold R_list in SOME.
rewrite -cats1 foldl_cat in SOME.
unfold R_list_helper in SOME.
inversion SOME; desf.
by destruct l.
}
generalize SOME; apply R_list_rcons_prefix, R_list_rcons_task in SOME; subst tsk_lst'; intro SOME.
specialize (IHts tsk_lst hp_bounds R_lst).
rewrite filter_rcons in IHts.
unfold is_interfering_task_fp in IHts.
rewrite eq_refl andbF in IHts.
assert (NOTHP: is_interfering_task_fp higher_eq_priority tsk tsk = false).
{
by unfold is_interfering_task_fp; rewrite eq_refl andbF.
} rewrite filter_rcons NOTHP; clear NOTHP.
assert (HP: is_interfering_task_fp higher_eq_priority tsk tsk_lst).
{
unfold is_interfering_task_fp; apply/andP; split.
{
apply order_sorted_rcons with (x := tsk_lst) in SORTED; try (by ins).
by rewrite mem_rcons in_cons; apply/orP; left.
}
{
rewrite 2!rcons_uniq mem_rcons in_cons negb_or in UNIQ.
move : UNIQ => /andP [/andP [UNIQ _] _].
by rewrite eq_sym in UNIQ.
}
} rewrite filter_rcons HP; clear HP.
unfold unzip1; rewrite map_rcons /=; f_equal.
assert (SHIFT: [seq tsk_hp <- ts' | is_interfering_task_fp higher_eq_priority tsk tsk_hp] = [seq tsk_hp <- ts'
| is_interfering_task_fp higher_eq_priority tsk_lst tsk_hp]).
{
apply eq_in_filter; red.
unfold is_interfering_task_fp; intros x INx.
rewrite 2!rcons_uniq mem_rcons in_cons negb_or in UNIQ.
move: UNIQ => /andP [/andP [NEQ NOTIN] /andP [NOTIN' UNIQ]].
destruct (x == tsk) eqn:EQtsk.
{
move: EQtsk => /eqP EQtsk; subst.
by rewrite INx in NOTIN.
}
destruct (x == tsk_lst) eqn:EQlst.
{
move: EQlst => /eqP EQlst; subst.
by rewrite INx in NOTIN'.
}
rewrite 2!andbT.
generalize SORTED; intro SORTED'.
have bla := order_sorted_rcons.
apply order_sorted_rcons with (x0 := x) in SORTED; try (by ins);
last by rewrite mem_rcons in_cons; apply/orP; right.
rewrite SORTED.
apply sorted_rcons_prefix in SORTED'.
by apply order_sorted_rcons with (x0 := x) in SORTED'.
} rewrite SHIFT; clear SHIFT.
apply IHts.
by rewrite rcons_uniq in UNIQ; move: UNIQ => /andP [_ UNIQ].
by apply sorted_rcons_prefix in SORTED.
by apply R_list_rcons_prefix in SOME.
}
Qed.
End AuxiliaryLemmas.
Section Proof.
(* Consider a task set ts. *)
Variable ts: taskset_of sporadic_task_with_jitter.
(* Assume that higher_eq_priority is a total order.
Actually, it just needs to be total over the task set,
but to weaken the assumption, I have to re-prove many lemmas
about ordering in ssreflect. This can be done later. *)
Hypothesis H_valid_policy: valid_fp_policy higher_eq_priority.
Hypothesis H_unique_priorities: antisymmetric higher_eq_priority.
(* Assume the task set has no duplicates, ... *)
Hypothesis H_ts_is_a_set: uniq ts.
(* ...all tasks have valid parameters, ... *)
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* ...restricted deadlines, ...*)
Hypothesis H_restricted_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
(* ...and tasks are ordered by increasing priorities. *)
Hypothesis H_sorted_ts: sorted higher_eq_priority ts.
(* Next, consider any arrival sequence such that...*)
Context {arr_seq: arrival_sequence Job}.
(* ...all jobs come from task set ts, ...*)
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
(* ...they have valid parameters,...*)
Hypothesis H_valid_job_parameters:
forall (j: JobIn arr_seq),
valid_sporadic_job_with_jitter task_cost task_deadline task_jitter job_cost job_deadline job_task job_jitter j.
(* ... and satisfy the sporadic task model.*)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
(* Then, consider any platform with at least one CPU such that...*)
Variable sched: schedule num_cpus arr_seq.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
(* ...jobs only execute after the jitter and no longer
than their execution costs,... *)
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_jitter sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* ...and do not execute in parallel. *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
(* Assume the platform satisfies the global scheduling invariant. *)
Hypothesis H_global_scheduling_invariant:
FP_scheduling_invariant_holds job_cost job_task num_cpus sched ts higher_eq_priority.
Definition no_deadline_missed_by_task (tsk: sporadic_task_with_jitter) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Definition no_deadline_missed_by_job :=
job_misses_no_deadline job_cost job_deadline sched.
Section HelperLemma.
(* The following lemma states that the response-time bounds
computed using R_list are valid. *)
Lemma R_list_has_response_time_bounds :
forall rt_bounds tsk R,
R_list ts = Some rt_bounds ->
(tsk, R) \in rt_bounds ->
forall j : JobIn arr_seq,
job_task j = tsk ->
completed job_cost sched j (job_arrival j + R).
Proof.
unfold valid_fp_policy, fp_is_transitive, fp_is_reflexive,
fp_is_total in *.
rename H_valid_job_parameters into JOBPARAMS,
H_valid_task_parameters into TASKPARAMS,
H_restricted_deadlines into RESTR,
H_completed_jobs_dont_execute into COMP,
H_jobs_execute_after_jitter into MUSTARRIVE,
H_global_scheduling_invariant into INVARIANT,
H_sorted_ts into SORT,
H_unique_priorities into UNIQ,
H_all_jobs_from_taskset into ALLJOBS,
H_ts_is_a_set into SET.
destruct H_valid_policy as [REFL [TRANS TOTAL]]; clear ALLJOBS.
unfold fp_schedulable, R_list in *.
induction ts as [| ts' tsk_i IH] using last_ind.
{
intros rt_bounds tsk R SOME IN.
by inversion SOME; subst; rewrite in_nil in IN.
}
{
intros rt_bounds tsk R SOME IN j JOBj.
destruct (lastP rt_bounds) as [| hp_bounds (tsk_lst, R_lst)];
first by rewrite in_nil in IN.
rewrite mem_rcons in_cons in IN; move: IN => /orP IN.
destruct IN as [LAST | BEGINNING]; last first.
{
apply IH with (rt_bounds := hp_bounds) (tsk := tsk); try (by ins).
by rewrite rcons_uniq in SET; move: SET => /andP [_ SET].
by ins; red; ins; apply TASKPARAMS; rewrite mem_rcons in_cons; apply/orP; right.
by ins; apply RESTR; rewrite mem_rcons in_cons; apply/orP; right.
by apply sorted_rcons_prefix in SORT.
{
intros tsk0 j0 t IN0 JOB0 BACK0.
exploit (INVARIANT tsk0 j0 t); try (by ins);
[by rewrite mem_rcons in_cons; apply/orP; right | intro INV].
rewrite -cats1 count_cat /= in INV.
unfold is_interfering_task_fp in INV.
generalize SOME; apply R_list_rcons_task in SOME; subst tsk_i; intro SOME.
assert (HP: higher_eq_priority tsk_lst tsk0 = false).
{
apply order_sorted_rcons with (x := tsk0) in SORT; [|by ins | by ins].
apply negbTE; apply/negP; unfold not; intro BUG.
exploit UNIQ; [by apply/andP; split; [by apply SORT | by ins] | intro EQ].
by rewrite rcons_uniq -EQ IN0 in SET.
}
by rewrite HP 2!andFb 2!addn0 in INV.
}
by apply R_list_rcons_prefix in SOME.
}
{
move: LAST => /eqP LAST.
inversion LAST as [[EQ1 EQ2]].
rewrite -> EQ1 in *; rewrite -> EQ2 in *; clear EQ1 EQ2 LAST.
generalize SOME; apply R_list_rcons_task in SOME; subst tsk_i; intro SOME.
generalize SOME; apply R_list_rcons_prefix in SOME; intro SOME'.
generalize SOME'; apply R_list_rcons_response_time in SOME'; intro SOME''; rewrite SOME'.
have BOUND := bertogna_cirinei_response_time_bound_fp_with_jitter.
unfold is_response_time_bound_of_task in BOUND.
apply BOUND with (task_cost := task_cost) (task_period := task_period) (task_deadline := task_deadline) (job_deadline := job_deadline) (job_task := job_task) (tsk := tsk_lst) (job_jitter := job_jitter)
(ts := rcons ts' tsk_lst) (hp_bounds := hp_bounds)
(higher_eq_priority := higher_eq_priority); clear BOUND; try (by ins).
by rewrite mem_rcons in_cons eq_refl orTb.
by apply R_list_unzip1 with (R := R_lst); try (by ins).
{
intros hp_tsk R0 HP j0 JOB0.
apply IH with (rt_bounds := hp_bounds) (tsk := hp_tsk); try (by ins).
by rewrite rcons_uniq in SET; move: SET => /andP [_ SET].
by red; ins; apply TASKPARAMS; rewrite mem_rcons in_cons; apply/orP; right.
by ins; apply RESTR; rewrite mem_rcons in_cons; apply/orP; right.
by apply sorted_rcons_prefix in SORT.
{
intros tsk0 j1 t IN0 JOB1 BACK0.
exploit (INVARIANT tsk0 j1 t); try (by ins);
[by rewrite mem_rcons in_cons; apply/orP; right | intro INV].
rewrite -cats1 count_cat /= addn0 in INV.
unfold is_interfering_task_fp in INV.