From f5252f57fedc06a1942fb6ddd836fde9a5963690 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Sat, 5 Apr 2025 00:24:19 +0200
Subject: [PATCH] prove sRTA (starting with a non-IID system)
---
rt/analysis/pRTA/pRTA_full.v | 102 +++
rt/analysis/scheduler_properties.v | 365 ++++++++
rt/analysis/transformation_properties.v | 1076 +++++++++++++++++++++++
rt/analysis/work_bound.v | 6 +-
util/seq.v | 179 ++++
5 files changed, 1725 insertions(+), 3 deletions(-)
create mode 100644 rt/analysis/pRTA/pRTA_full.v
create mode 100644 rt/analysis/scheduler_properties.v
create mode 100644 rt/analysis/transformation_properties.v
create mode 100644 util/seq.v
diff --git a/rt/analysis/pRTA/pRTA_full.v b/rt/analysis/pRTA/pRTA_full.v
new file mode 100644
index 0000000..5068a5e
--- /dev/null
+++ b/rt/analysis/pRTA/pRTA_full.v
@@ -0,0 +1,102 @@
+(* --------------------------------- ProBsa --------------------------------- *)
+From probsa.rt.analysis Require Export transformation_properties.
+From probsa.rt.analysis Require Export scheduler_properties.
+From probsa.rt.analysis.pRTA Require Export pRTA.
+
+(* ---------------------------------- Main ---------------------------------- *)
+Section ProbabilisticRTA.
+
+ Context {Task : TaskType}
+ {FP : FP_policy Task}
+ {D : TaskDeadline Task}
+ {T : SporadicModel Task}
+ {pWCET_pmf : ProbWCET Task}.
+
+ Hypothesis H_priority_is_total : total FP.
+ Hypothesis H_priority_is_reflexive : reflexive hep_task.
+ Hypothesis H_priority_is_transitive : transitive hep_task.
+
+ Variable ts : seq Task.
+ Hypothesis H_ts_uniq : uniq ts.
+
+ Hypothesis H_restricted_deadlines : restricted_deadlines ts.
+ Hypothesis H_valid_sporadic : valid_taskset_inter_arrival_times ts.
+
+ Variable tsk : Task.
+ Hypothesis H_tsk_in_ts : tsk \in ts.
+
+ Context {Ω} {μ : measure Ω}.
+
+ Context {Job : finType}
+ {job_cost : JobCostRV Job Ω μ}
+ {job_arrival : JobArrivalRV Job Ω μ}
+ {job_task : JobTask Job Task}.
+ Hypothesis H_arrivals_agree_with_costs : arrivals_cost_consistent.
+
+ Variable h : instant.
+ Hypothesis H_horizon_after_deadlines :
+ forall j ω, (odflt0 (job_deadline j) ω < h)%nat.
+
+ Hypothesis H_all_jobs_from_ts : forall j, job_task j \in ts.
+ Hypothesis H_sporadic : pr_taskset_respects_sporadic_task_model ts.
+ Hypothesis H_axiomatic_pWCET : axiomatic_pWCET μ.
+
+ (** Here, [FP_FP_sched] is an implementation of a fully preemptive
+ FP scheduler with the classical notion of readiness and where
+ jobs are terminated if a deadline is missed. The theorem below
+ makes use of several properties of the scheduler, such as work
+ conservation. All necessary properties are proven in
+ [probsa.rt.analysis.scheduler_properties]. *)
+ Let 𝓡 j := response_time (compute_pr_schedule FP_FP_sched) (Some h) j.
+
+ (** Consider a job of task [tsk]. *)
+ Variable j : Job.
+ Hypothesis H_job_of_task : job_of_task tsk j.
+
+ Theorem probabilistic_rta_fp_fp :
+ ℙ<μ>{[ D tsk ⟨<⟩ 𝓡 j ]} <= Λ ts tsk.
+ Proof.
+ have TOT : total_priorities
+ by intros ? ?; unfold hep_job_at, JLFP_to_JLDP, hep_job, FP_to_JLFP.
+ have REF : reflexive_priorities
+ by intros ? ?; unfold hep_job_at, JLFP_to_JLDP, hep_job, FP_to_JLFP.
+ have TRN : transitive_priorities
+ by intros ? ? ? ?; unfold hep_job_at, JLFP_to_JLDP, hep_job, FP_to_JLFP;
+ apply H_priority_is_transitive.
+ apply: Rle_trans.
+ { by apply probabilistic_rt_monotonicity_of_iid_pWCET => //; apply FP_FP_sched_is_rt_monotonic => //. }
+ { apply: probabilistic_rta_fp; eauto 1; try set (S := replace_all_pETs _).
+ { by apply: transformation_respects_big_horizon; intros; apply H_horizon_after_deadlines. }
+ { by unfold pr_work_conserving; apply FP_FP_sched_is_work_conserving. }
+ { by apply FP_FP_sched_respects_policy_at_preemption_point. }
+ { by apply FP_FP_sched_respects_jobs_come_from_arrival_sequence. }
+ { by apply FP_FP_sched_respects_completed_jobs_dont_execute. }
+ { by apply FP_FP_sched_respects_jobs_must_arrive_to_execute. }
+ { by apply FP_FP_sched_respects_jobs_must_be_ready_to_execute. }
+ { by intros; apply transformation_respects_consistent_arrivals => //; apply H_arrivals_agree_with_costs. }
+ { by intros ? ? ?; apply H_all_jobs_from_ts. }
+ { by apply: sporadic_task_model_respected. }
+ { by apply: replaced_pETs_are_independent. }
+ { intros; unfold nth_cost.
+ destruct pWCET_pmf as [pWCET nonneg sum1]; simpl.
+ destruct task_job eqn:TSK; last first.
+ { intros ?; apply Rge_trans with 1%R.
+ { by rewrite pr_xpredT_ext //; apply Rge_refl. }
+ { by apply Rle_ge, pr_le_1. }
+ }
+ { intros ?; apply: Rge_trans.
+ { apply replaced_pETs_bounded_by_pWCETs with (tsko := tsk0).
+ by move: TSK; intros EQ; apply nth_mem_o in EQ; apply EQ. }
+ { by apply Rle_refl. }
+ }
+ }
+ { by apply pETs_have_same_distribution. }
+ { by apply: replaced_pETs_are_cond_independent. }
+ { by intros; apply replaced_pETs_are_independent_from_arr_seq_partition. }
+ { by intros; apply replaced_cond_pETs_bounded_by_pWCETs. }
+ }
+ Qed.
+
+End ProbabilisticRTA.
+
+Print Assumptions probabilistic_rta_fp.
diff --git a/rt/analysis/scheduler_properties.v b/rt/analysis/scheduler_properties.v
new file mode 100644
index 0000000..75ecfd9
--- /dev/null
+++ b/rt/analysis/scheduler_properties.v
@@ -0,0 +1,365 @@
+(* --------------------------------- Prosa ---------------------------------- *)
+From prosa.implementation Require Import facts.ideal_uni.prio_aware.
+
+(* --------------------------------- ProBsa --------------------------------- *)
+From probsa.util Require Export seq.
+From probsa.util.prosa Require Export prio_aware.
+From probsa.rt.model Require Export scheduler.
+From probsa.rt.model Require Export abort_readiness.
+From probsa.rt.model.assumptions Require Export basic.
+From probsa.rt.model.assumptions Require Export pr_respects_policy pr_must_be_ready pr_work_conserving.
+
+Local Open Scope nat_scope.
+
+(* ---------------------------------- Main ---------------------------------- *)
+Section SustainableUniFPFP.
+
+ Context {Job : finType}
+ {job_arrival : JobArrival Job}
+ {job_deadline : JobDeadline Job}
+ {JLDP : JLDP_policy Job}.
+
+ Context {job_cost1 : JobCost Job}
+ {job_cost2 : JobCost Job}.
+
+ Hypothesis H_cost_monotone : forall j, job_cost1 j >= job_cost2 j.
+
+ Let job_ready1 := @abort_ready_instance Job _ job_arrival job_cost1 job_deadline.
+ Let job_ready2 := @abort_ready_instance Job _ job_arrival job_cost2 job_deadline.
+
+ Variable arr_seq : arrival_sequence Job.
+
+ Let sched1 := @uni_schedule Job job_cost1 job_arrival arr_seq job_ready1 fully_preemptive_model JLDP.
+ Let sched2 := @uni_schedule Job job_cost2 job_arrival arr_seq job_ready2 fully_preemptive_model JLDP.
+
+ Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
+ Hypothesis H_arrival_sequence_uniq : arrival_sequence_uniq arr_seq.
+
+ Hypothesis H_total : forall t, total (hep_job_at t).
+ Hypothesis H_reflexive : forall t, reflexive (hep_job_at t).
+ Hypothesis H_transitive : forall t, transitive (hep_job_at t).
+
+ Section ScheduledAtMonotone.
+
+ Variables j : Job.
+ Variables t : instant.
+
+ Hypothesis H_j_sched1 : scheduled_at sched1 j t.
+ Hypothesis H_j_not_completed_sched2 : ~~ completed_by sched2 j t.
+
+ Hypothesis H_service_monotone_wrt_schedules :
+ forall (j : Job),
+ ~~ completed_by sched2 j t ->
+ service sched1 j t <= service sched2 j t.
+
+ Local Lemma j_scheduled_at_t_in_sched2 :
+ scheduled_at sched2 j t.
+ Proof.
+ move: (H_j_sched1) => SUPR; apply scheduled_job_is_supremum in SUPR; last first.
+ { by rewrite /preemption_time; destruct (uni_schedule _ _). }
+ apply supremum_monotone_wrt_subset
+ with (xs := @jobs_backlogged_at
+ _ _ _ _ _ arr_seq
+ match t return _ with
+ | O => @empty_schedule _ (ideal.processor_state _) None
+ | S t' => @schedule_up_to
+ _ _ (@allocation_at
+ _ _ _ arr_seq _ _ (@choose_highest_prio_job _ JLDP))
+ None t'
+ end t
+ ) in SUPR; try done.
+ { apply scheduled_job_is_supremum_new in SUPR.
+ { by apply SUPR. }
+ { by rewrite /preemption_time; destruct (uni_schedule _ _). }
+ }
+ { by rewrite filter_uniq //; apply arrivals_uniq => //. }
+ { apply seq.subseq_filter => s IN.
+ destruct t.
+ { rewrite /backlogged !scheduled_at_def //=.
+ destruct (0 < _); last first.
+ { by rewrite !andbT andbF. }
+ { rewrite !andbT /pending.
+ destruct has_arrived; last by rewrite andFb.
+ rewrite !andTb /completed_by -!ltnNge => SERV.
+ apply: leq_trans; first apply: SERV.
+ by apply H_cost_monotone.
+ }
+ }
+ { clear SUPR H_j_sched1.
+ rewrite /backlogged !scheduled_at_def !schedule_up_to_empty //= !andbT.
+ destruct (_ < _ ); last by rewrite andbF.
+ rewrite !andbT /pending; destruct has_arrived; last by rewrite andFb.
+ rewrite !andTb; apply contra => COMPI.
+ have [COMP2 | NCOMP2] := boolP (@completed_by _ _ (sched2) job_cost2 s i.+1).
+ { apply: leq_trans; first by apply: COMP2.
+ rewrite /sched1 /service /service_during big_nat_cond [X in _ <= X]big_nat_cond.
+ apply leq_sum => k /andP [/andP [_ L] _].
+ by rewrite !service_at_def; erewrite schedule_up_to_identical_prefix; [ | | apply L].
+ }
+ feed (H_service_monotone_wrt_schedules s); [ by eassumption | clear NCOMP2].
+ apply: leq_trans; [apply: leq_trans; last by apply COMPI | ]; first by apply H_cost_monotone.
+ apply: leq_trans; [apply: leq_trans; last by apply H_service_monotone_wrt_schedules | ].
+ { rewrite /sched1 /service /service_during big_nat_cond [X in _ <= X]big_nat_cond.
+ apply leq_sum => k /andP [/andP [_ L] _].
+ rewrite !service_at_def.
+ by erewrite schedule_up_to_identical_prefix; [ | | apply L] => //.
+ }
+ { rewrite /sched1 /service /service_during big_nat_cond [X in _ <= X]big_nat_cond.
+ apply leq_sum => k /andP [/andP [_ L] _].
+ rewrite !service_at_def.
+ by erewrite schedule_up_to_identical_prefix; [ | | apply L] => //.
+ }
+ }
+ }
+ { have VNPR : valid_nonpreemptive_readiness job_ready1 by intros ?.
+ have NCR : nonclairvoyant_readiness job_ready1
+ by intros ? ? ? ? ? ? ? => //=; f_equal; apply: identical_prefix_pending; eauto 1.
+ have USV := @uni_schedule_valid Job _ _ arr_seq job_ready1 NCR fully_preemptive_model VNPR JLDP.
+ destruct USV as [JFAS MBR].
+ have HA : has_arrived j t by apply jobs_must_arrive_to_be_ready in MBR; apply MBR.
+ have GED : t < prosa.behavior.job.job_deadline j
+ by apply MBR in H_j_sched1; move: H_j_sched1 => /andP [_ DEAD].
+ rewrite mem_filter; apply/andP; split; last first.
+ { by apply arrived_between_implies_in_arrivals; [ | eapply JFAS, H_j_sched1 | apply HA ]. }
+ { apply/andP; split; last first.
+ { by destruct t; rewrite scheduled_at_def // schedule_up_to_empty. }
+ { apply/andP; split => //; apply/andP; split => //.
+ move: H_j_not_completed_sched2; apply contra => NCOMP2.
+ apply: leq_trans; first by apply: NCOMP2.
+ rewrite /sched1 /service /service_during big_nat_cond [X in _ <= X]big_nat_cond.
+ apply leq_sum => i /andP [/andP [_ L] _].
+ destruct t; first by done.
+ rewrite !service_at_def.
+ by erewrite schedule_up_to_identical_prefix; [ | | apply L] => //.
+ }
+ }
+ }
+ Qed.
+
+ End ScheduledAtMonotone.
+
+ Local Lemma service_monotone_wrt_sched :
+ forall (j : Job) (t : instant),
+ ~~ completed_by sched2 j t ->
+ service sched1 j t <= service sched2 j t.
+ Proof.
+ intros; move: j H.
+ induction t; intros s.
+ { by rewrite /service /service_during /service_at !big_geq //=. }
+ { intros NCOMP.
+ have [COMPt | NCOMPs] := boolP (@completed_by _ _ sched2 job_cost2 s t).
+ { exfalso; move: NCOMP => /negP NCOMP; apply: NCOMP.
+ by eapply completion_monotonic; last by eassumption.
+ }
+ { have SERV := IHt _ NCOMPs.
+ have [SCHED1 | NSCHED1] := boolP (scheduled_at sched1 s t); last first.
+ { rewrite -!service_last_plus_before.
+ apply: leq_add; first by done.
+ apply leq_trans with 0; last by done.
+ rewrite leqn0 service_at_def eqb0.
+ by move: NSCHED1; rewrite scheduled_at_def.
+ }
+ { have SCHED2 : scheduled_at sched2 s t
+ by apply j_scheduled_at_t_in_sched2 => //.
+ rewrite -!service_last_plus_before.
+ apply: leq_add; first by done.
+ by move: SCHED1 SCHED2; rewrite !scheduled_at_def !service_at_def => /eqP -> /eqP ->.
+ }
+ }
+ }
+ Qed.
+
+ Lemma sustainable_uni_fp_fp :
+ forall t j,
+ completed_by (H := job_cost1) sched1 j t ->
+ completed_by sched2 j t.
+ Proof.
+ intros.
+ have [COMP2 | NCOMP2] := boolP (@completed_by _ _ sched2 job_cost2 j t) => //.
+ move: (NCOMP2) => /negP NCOM; exfalso; apply: NCOM.
+ apply: leq_trans; last by apply service_monotone_wrt_sched.
+ apply: leq_trans; last by apply H.
+ by apply H_cost_monotone.
+ Qed.
+
+End SustainableUniFPFP.
+
+(** Consider a task set together with two vectors [A] and [C]
+ describing job arrivals and job costs respectively. The scheduler
+ [FP_FP_sched] defined below mirrors the behaviour of
+ [uni_schedule] in an environment defined by the task set, [A] and [C]. *)
+Section UniScheduleAsSchedulerAC.
+
+ Context {Task : TaskType}
+ {FP : FP_policy Task}
+ {D : TaskDeadline Task}.
+
+ Context {Job : finType}
+ {job_task : JobTask Job Task}.
+
+ Let arr_seq (A : Job -> option instant) : arrival_sequence Job :=
+ fun t =>
+ [seq j <- index_enum Job |
+ if A j is Some ta
+ then t == ta
+ else false
+ ].
+
+ Let job_deadline (A : Job -> option nat) : JobDeadline Job :=
+ fun (j : Job) =>
+ odflt 0 (match A j with Some a => Some (a + D (job_task j)) | None => None end).
+
+ Let readiness (A C : Job -> option nat) :=
+ @abort_ready_instance
+ _ _ (fun j => odflt 0 (A j)) (fun j => odflt 0 (C j)) (job_deadline A).
+
+ Let JLDP : JLDP_policy Job :=
+ @JLFP_to_JLDP _ (@FP_to_JLFP Job Task _ FP).
+
+ Definition FP_FP_sched : @scheduler𝗔𝗖 Job :=
+ fun (A C : Job -> option nat) t =>
+ @uni_schedule
+ Job
+ (fun j => odflt 0 (C j)) (fun j => odflt 0 (A j))
+ (arr_seq A)
+ (readiness A C)
+ fully_preemptive_model
+ JLDP
+ t.
+
+End UniScheduleAsSchedulerAC.
+
+Section SchedulerProperties.
+
+ Context {Task : TaskType}
+ {FP : FP_policy Task}
+ {D : TaskDeadline Task}.
+
+ Context {Ω} {μ : measure Ω}.
+ Context {Job : finType}
+ {job_cost : JobCostRV Job Ω μ}
+ {job_arrival : JobArrivalRV Job Ω μ}
+ {job_task : JobTask Job Task}.
+
+ Hypothesis H_total : total_priorities.
+ Hypothesis H_reflexive : reflexive_priorities.
+ Hypothesis H_transitive : transitive_priorities.
+
+ Let pr_sched := @compute_pr_schedule Ω μ Job job_arrival job_cost FP_FP_sched.
+
+ Lemma abortion_readiness_is_nonclairvoyant :
+ forall ω, @nonclairvoyant_readiness _ _ _ _ (pr_abort_ready_instance ω).
+ Proof.
+ intros ? ? ? ? ? ? ? ?.
+ simpl; f_equal.
+ by apply: identical_prefix_pending; eauto 1.
+ Qed.
+
+ Lemma FP_FP_sched_respects_completed_jobs_dont_execute :
+ pr_completed_jobs_dont_execute pr_sched.
+ Proof.
+ intros ω.
+ apply: valid_schedule_implies_completed_jobs_dont_execute; eauto 1.
+ apply: np_schedule_valid.
+ { by apply abortion_readiness_is_nonclairvoyant. }
+ { by intros *; apply: supremum_in. }
+ { by unfold job_preemptable, fully_preemptive_model. }
+ Qed.
+
+ Lemma FP_FP_sched_respects_jobs_must_arrive_to_execute :
+ pr_jobs_must_arrive_to_execute pr_sched.
+ Proof.
+ intros ω.
+ apply: valid_schedule_implies_jobs_must_arrive_to_execute; eauto 1.
+ apply: np_schedule_valid.
+ { by apply abortion_readiness_is_nonclairvoyant. }
+ { by intros *; apply: supremum_in. }
+ { by unfold job_preemptable, fully_preemptive_model. }
+ Qed.
+
+ Lemma FP_FP_sched_respects_jobs_come_from_arrival_sequence :
+ pr_jobs_come_from_arrival_sequence pr_sched.
+ Proof.
+ intros ω.
+ apply np_schedule_valid.
+ { by apply abortion_readiness_is_nonclairvoyant. }
+ { by intros *; apply: supremum_in. }
+ { by unfold job_preemptable, fully_preemptive_model. }
+ Qed.
+
+ Lemma FP_FP_sched_is_work_conserving :
+ pr_work_conserving pr_sched pr_abort_ready_instance.
+ Proof.
+ intros ω.
+ apply: uni_schedule_work_conserving.
+ { by apply pr_consistent_arrival_times. }
+ { by apply abortion_readiness_is_nonclairvoyant. }
+ Qed.
+
+ Lemma FP_FP_sched_respects_policy_at_preemption_point :
+ pr_respects_policy_at_preemption_point pr_sched pr_abort_ready_instance.
+ Proof.
+ intros ω; apply schedule_respects_policy => //.
+ { by apply pr_consistent_arrival_times. }
+ { by apply abortion_readiness_is_nonclairvoyant. }
+ Qed.
+
+ Lemma FP_FP_sched_respects_jobs_must_be_ready_to_execute :
+ pr_jobs_must_be_ready_to_execute pr_sched pr_abort_ready_instance.
+ Proof.
+ intros ?.
+ apply np_schedule_valid.
+ { by apply abortion_readiness_is_nonclairvoyant. }
+ { by intros *; apply: supremum_in. }
+ { by unfold job_preemptable, fully_preemptive_model. }
+ Qed.
+
+ Lemma FP_FP_sched_is_rt_monotonic :
+ forall horizon,
+ rt_monotonic_scheduler (Some horizon) FP_FP_sched.
+ Proof.
+ intros * A C ju j r c1 c2 LE.
+ set (Cs := update C ju c1); set (Cl := update C ju c2).
+ have UNI :
+ forall t j,
+ @completed_by _ _ (FP_FP_sched A Cl) (fun j => odflt 0 (Cl j)) j t ->
+ @completed_by _ _ (FP_FP_sched A Cs) (fun j => odflt 0 (Cs j)) j t.
+ { apply sustainable_uni_fp_fp; eauto 1; last first.
+ { by intros ?; rewrite filter_uniq // index_enum_uniq. }
+ { intros s t; rewrite /arrives_at /arrivals_at mem_filter.
+ destruct (A s) eqn:EQ; last by done.
+ rewrite /prosa.behavior.job.job_arrival EQ //=.
+ by move=> /andP [/eqP -> _].
+ }
+ { by intros ?; rewrite /Cs /Cl /update; destruct (j0 == ju); [apply LE | done]. }
+ }
+ unfold FP_FP_sched, scheduler𝗔𝗖_to_rt𝗔𝗖 in *; simpl in *.
+ destruct (scheduler.min_completion_time).
+ { destruct (A j) as [aj | ] eqn:Aj; last by done.
+ destruct s as [rt1 [COMP1 MIN1]].
+ have [LErt1|GTrt1] := leqP horizon rt1.
+ { intros _.
+ destruct (scheduler.min_completion_time); last by done.
+ destruct s as [rt2 [COMP2 MIN2]].
+ destruct (horizon <= rt2) eqn:GTrt2 => //.
+ move: GTrt2 => /negP/negP; rewrite -ltnNge => GTrt2.
+ exfalso; unfold FP_FP_sched, scheduler𝗔𝗖_to_completed𝗔𝗖 in *.
+ apply (MIN1 rt2); first by apply/leP; apply: leq_trans; [apply GTrt2 | apply LErt1].
+ by apply UNI; apply COMP2. }
+ { rewrite //= ltn_subRL => LTrt1.
+ destruct (scheduler.min_completion_time); last by done.
+ destruct s as [rt2 [COMP2 MIN2]].
+ destruct (horizon <= rt2) eqn:GTrt2 => //.
+ rewrite //= ltn_subRL; move_neq_up GErt2; unfold FP_FP_sched, scheduler𝗔𝗖_to_completed𝗔𝗖 in *.
+ apply (MIN1 rt2); first by apply/leP; apply: leq_ltn_trans; [apply GErt2 | apply LTrt1].
+ by apply UNI; apply COMP2. }
+ }
+ { destruct (A j) as [aj | ] eqn:Aj; last by done.
+ intros _; destruct (scheduler.min_completion_time); last by done.
+ destruct s as [rt2 [COMP2 MIN2]].
+ exfalso; apply: (n rt2); unfold scheduler𝗔𝗖_to_completed𝗔𝗖 in *.
+ by apply UNI, COMP2.
+ }
+ Qed.
+
+End SchedulerProperties.
diff --git a/rt/analysis/transformation_properties.v b/rt/analysis/transformation_properties.v
new file mode 100644
index 0000000..f809045
--- /dev/null
+++ b/rt/analysis/transformation_properties.v
@@ -0,0 +1,1076 @@
+(* --------------------------------- ProBsa --------------------------------- *)
+From probsa.rt.model Require Export pRBF assumptions.basic.
+From probsa.rt.analysis Require Export axiomatic_pWCET_full.
+
+Local Open Scope nat_scope.
+
+(* ---------------------------------- Main ---------------------------------- *)
+(** In this file we prove lemmas that establish properties of a system
+ after the axiomatic-pWCET transformation .*)
+
+(** In this section we prove that, given a system that satisfies the
+ sporadic task model, a new system generated by the transformation
+ will also satisfy the sporadic task model. That is, the
+ transformation respects the sporadic model. *)
+Section TransformationRespectsSporadicTaskModel.
+
+ (** Consider any type of tasks with a notion of pWCET ... *)
+ Context {Task : TaskType}
+ {D : TaskDeadline Task}
+ {T : SporadicModel Task}
+ {pWCET_pmf : ProbWCET Task}.
+
+ (** ...and their jobs. *)
+ Context {Job : finType}
+ {job_task : JobTask Job Task}.
+
+ (** Consider a scheduling algorithm [ζ] that receives two vectors: a
+ vector of arrival times [𝗔] and a vector of job costs [𝗖]. *)
+ Variable ζ : @scheduler𝗔𝗖 Job.
+
+ (** Let [sched] denote a schedule generated by [ζ] for a given
+ system [S]. *)
+ Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).
+
+ (** Most of the properties are proved by a three-step
+ procedure. First, we show that a single step of the
+ transformation preserves the property in question. Second, we
+ show that [n] steps of the transformation preserve the
+ property. Finally, we show that if [n = |jobs|], then the
+ property holds for the final system. *)
+ Section Step1.
+
+ (** Consider a system [S]. *)
+ Variable S : @system Job.
+
+ (** Next, consider two arbitrary jobs: job [j] and job [j_rep],
+ whose pET we modify. *)
+ Variable (j_rep : Job) (j : Job).
+
+ (** Suppose we use the construction [replace_job_pET] presented
+ in [probsa/rt/analysis/pETs_to_pWCETs] to replace the
+ execution cost of given job [j_rep]. Let [S'] denote the
+ resulting system. *)
+ Let S' : system := replace_job_pET j_rep S.
+
+ (** Then, given a task set [ts], ...*)
+ Variable ts : seq Task.
+
+ (** ... if [S] respects the sporadic task model, then [S'] also
+ satisfies the sporadic task model. *)
+ Lemma sporadic_task_model_respected_step :
+ pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S) ts ->
+ pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S') ts .
+ Proof.
+ intros * SPO; unfold S' in *; clear S' => //=.
+ destruct S as [Ω μ A C].
+ destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in *.
+ set (μ_tsk := {| pmf := pWCET (job_task j_rep);
+ pmf_pos := nonneg (job_task j_rep);
+ pmf_sum1 := sum1 (job_task j_rep) |}) in *.
+ intros [ω n].
+ specialize (SPO ω).
+ intros ? IN j1 j2 NEQ ARR1 ARR2 TSK1 TSK2 LE.
+ by apply SPO => //.
+ Qed.
+
+ End Step1.
+
+ (** In the next step, we apply the transformation to an arbitrary
+ subset of jobs [jobs].*)
+ Section Step2.
+
+ Variables (ts : seq Task) (jobs : seq Job) (S : @system Job).
+ Let S' : system := foldr replace_job_pET S jobs.
+
+ Lemma sporadic_task_model_respected_steps :
+ pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S) ts ->
+ pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S') ts.
+ Proof.
+ induction jobs as [| j_rep jobs']; destruct S as [Ω μ 𝓐 𝓒]; first by done.
+ intros SPO ? ?.
+ unfold S' in *; clear S'.
+ simpl in ω.
+ apply sporadic_task_model_respected_step.
+ apply IHjobs'.
+ by apply SPO.
+ Qed.
+
+ End Step2.
+
+ (** Finally, we apply the previous lemma to a set of jobs that
+ coincides with the set of all jobs. *)
+ Section Step3.
+
+ Variable S : @system Job.
+ Let S' := replace_all_pETs S.
+
+ Variable ts : seq Task.
+
+ Lemma sporadic_task_model_respected :
+ pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S) ts ->
+ pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S') ts.
+ Proof.
+ by intros; apply sporadic_task_model_respected_steps.
+ Qed.
+
+ End Step3.
+
+End TransformationRespectsSporadicTaskModel.
+
+(** In the following, we repeat the same procedure for all the
+ necessary properties. Next, we prove that the transformation
+ respects the assumption about the termination horizon of the
+ system. *)
+Section TransformationRespectsBigHorizon.
+
+ Context {Task : TaskType}
+ {D : TaskDeadline Task}
+ {T : SporadicModel Task}
+ {pWCET_pmf : ProbWCET Task}.
+
+ Context {Job : finType}
+ {job_task : JobTask Job Task}.
+
+ Let job_deadline (S : system) (j : Job) :=
+ @job_deadline _ _ _ (@job_deadline_from_task_deadline _ _ _ _ D (𝓐_of S) _) j.
+
+ Variable ζ : @scheduler𝗔𝗖 Job.
+ Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).
+
+ Section Step1.
+
+ Variable (S : @system Job) (j_rep : Job) (j : Job).
+ Let S' : system := replace_job_pET j_rep S.
+
+ Variable h : instant.
+ Hypothesis BIG : forall (ω : Ω_of S), odflt0 (job_deadline S j) ω < h.
+
+ Lemma transformation_respects_big_horizon_step :
+ forall (ω : Ω_of S'), odflt0 (job_deadline S' j) ω < h.
+ Proof.
+ unfold S' in *; clear S' => //=.
+ destruct S as [Ω μ A C].
+ destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in *.
+ set (μ_tsk := {| pmf := pWCET (job_task j_rep);
+ pmf_pos := nonneg (job_task j_rep);
+ pmf_sum1 := sum1 (job_task j_rep) |}) in *.
+ intros [ω a].
+ by apply BIG.
+ Qed.
+
+ End Step1.
+
+ Section Step2.
+
+ Variables (S : @system Job) (jobs : seq Job) (j : Job).
+ Let S' : system := foldr replace_job_pET S jobs.
+
+ Variable h : instant.
+ Hypothesis H_horizon_big : forall (ω : Ω_of S), odflt0 (job_deadline S j) ω < h.
+
+ Lemma transformation_respects_big_horizon_steps :
+ forall ω, odflt0 (job_deadline S' j) ω < h.
+ Proof.
+ induction jobs as [| j_rep jobs']; first by done.
+ unfold S' in *; clear S'.
+ intros ω => //=.
+ apply transformation_respects_big_horizon_step.
+ by intros; apply IHjobs'.
+ Qed.
+
+ End Step2.
+
+ Section Step3.
+
+ Variable S : @system Job.
+ Let S' : system := replace_all_pETs S.
+
+ Variable h : instant.
+ Hypothesis H_horizon_big : forall (j : Job) (ω : Ω_of S), odflt0 (job_deadline S j) ω < h.
+
+ Lemma transformation_respects_big_horizon :
+ forall (j : Job) (ω : Ω_of S'),
+ odflt0 (job_deadline S' j) ω < h.
+ Proof.
+ by intros; apply transformation_respects_big_horizon_steps.
+ Qed.
+
+ End Step3.
+
+End TransformationRespectsBigHorizon.
+
+Section TransformationRespectsArrivalsCostConsistent.
+
+ Context {Task : TaskType}
+ {D : TaskDeadline Task}
+ {T : SporadicModel Task}
+ {pWCET_pmf : ProbWCET Task}.
+
+ Context {Job : finType}
+ {job_task : JobTask Job Task}.
+
+ Variable ζ : @scheduler𝗔𝗖 Job.
+ Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).
+
+ Section Step1.
+
+ Variable (S : @system Job) (j_rep : Job) (j : Job).
+ Let S' : system := replace_job_pET j_rep S.
+
+ Lemma transformation_respects_consistent_arrivals_step :
+ arrivals_cost_consistent (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) ->
+ arrivals_cost_consistent (job_arrival := 𝓐_of S') (job_cost := 𝓒_of S').
+ Proof.
+ intros SOME * ARR; unfold S' in *; clear S' => //=.
+ destruct S as [Ω μ A C].
+ destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in *.
+ set (μ_tsk := {| pmf := pWCET (job_task j_rep);
+ pmf_pos := nonneg (job_task j_rep);
+ pmf_sum1 := sum1 (job_task j_rep) |}) in *.
+ destruct ω as [ω n].
+ destruct (_ == _) eqn:EQ; first by done.
+ by apply SOME.
+ Qed.
+
+ End Step1.
+
+ Section Step2.
+
+ Variables (jobs_rep : seq Job) (S : @system Job).
+ Let S' : system := foldr replace_job_pET S jobs_rep.
+
+ Lemma transformation_respects_consistent_arrivals_steps :
+ arrivals_cost_consistent (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) ->
+ arrivals_cost_consistent (job_arrival := 𝓐_of S') (job_cost := 𝓒_of S').
+ Proof.
+ induction jobs_rep as [| j_rep jobs]; destruct S as [Ω μ 𝓐 𝓒].
+ { by simpl in *. }
+ { simpl; intros.
+ apply transformation_respects_consistent_arrivals_step.
+ by apply IHjobs, H.
+ }
+ Qed.
+
+ End Step2.
+
+ Section ProofOfLemmas3.
+
+ Variable S : @system Job.
+ Let S' := replace_all_pETs S.
+
+ Lemma transformation_respects_consistent_arrivals :
+ arrivals_cost_consistent (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) ->
+ arrivals_cost_consistent (job_arrival := 𝓐_of S') (job_cost := 𝓒_of S').
+ Proof.
+ by intros; apply transformation_respects_consistent_arrivals_steps.
+ Qed.
+
+ End ProofOfLemmas3.
+
+End TransformationRespectsArrivalsCostConsistent.
+
+Section TransformationPreservesArrivalSequence.
+
+ Context {Task : TaskType}
+ {D : TaskDeadline Task}
+ {pWCET_pmf : ProbWCET Task}.
+
+ Context {Job : finType}
+ {job_task : JobTask Job Task}.
+
+ Variable ζ : @scheduler𝗔𝗖 Job.
+ Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).
+
+ Variable (S : @system Job) (j_rep : Job).
+ Let S' : system := replace_job_pET j_rep S.
+
+ Lemma transformation_preserves_arr_seq :
+ forall ξ' : imgT (arr_seq (job_arrival := 𝓐_of S')),
+ exists ξ : imgT (arr_seq (job_arrival := 𝓐_of S)),
+ forall t, proj1_sig ξ t = proj1_sig ξ' t.
+ Proof.
+ intros [ξ INS'].
+ unshelve econstructor.
+ { unshelve econstructor; first by apply ξ.
+ unfold S' in *; clear S'.
+ destruct S as [Ω μ A C], pWCET_pmf as [pWCET nonneg sum1]; simpl in *.
+ move: (INS'); rewrite !unfold_in => /exCP [[ω n] /eqP EQ].
+ apply/exCP; exists ω; rewrite -EQ; apply/eqP.
+ have FE := @FunctionalExtensionality.functional_extensionality nat (seq Job) (arr_seq ω) (arr_seq (ω, n)).
+ by apply: FE => t; reflexivity.
+ }
+ { by simpl; intros; reflexivity. }
+ Qed.
+
+End TransformationPreservesArrivalSequence.
+
+(** In this section we show that in the transformed system all pETs
+ (related to jobs of the same task) have the same distribution. *)
+Section TransformationEnsuresIdenticalCosts.
+
+ Context {Task : TaskType}
+ {D : TaskDeadline Task}
+ {pWCET_pmf : ProbWCET Task}.
+
+ Context {Job : finType}
+ {job_task : JobTask Job Task}.
+
+ Variable ζ : @scheduler𝗔𝗖 Job.
+ Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).
+
+ Section Step1.
+
+ Variable (S : @system Job) (j_rep : Job) (j : Job).
+ Let S' := replace_job_pET j_rep S.
+
+ Section CostBoundedByPWCET.
+
+ Variable tsk : Task.
+ Hypothesis H_job_of_task : job_of_task tsk j_rep.
+
+ Lemma replaced_pETs_bounded_by_pWCETs_step :
+ odflt0 (𝓒_of S' j_rep) ⪯ to_distrib pWCET_pmf tsk.
+ Proof.
+ unfold S' in *; clear S' => //=.
+ destruct S as [Ω μ A C].
+ destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in *.
+ set (μ_tsk := {| pmf := pWCET (job_task j_rep);
+ pmf_pos := nonneg (job_task j_rep);
+ pmf_sum1 := sum1 (job_task j_rep) |}) in *.
+ rewrite eq_refl => k.
+ rewrite (pr_joint_pred_eq _ _ _ (fun ω => true) (fun ω => ω <= k)).
+ { rewrite pr_xpredT Rmult_1_l.
+ by move: H_job_of_task => /eqP TSK2; rewrite /μ_tsk -TSK2; apply Rge_refl. }
+ { by intros [ω n]. }
+ Qed.
+
+ Lemma pWCETs_bounded_by_replaced_pETs_step :
+ to_distrib pWCET_pmf tsk ⪯ odflt0 (𝓒_of S' j_rep).
+ Proof.
+ unfold S' in *; clear S' => //=.
+ destruct S as [Ω μ A C].
+ destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in *.
+ set (μ_tsk := {| pmf := pWCET (job_task j_rep);
+ pmf_pos := nonneg (job_task j_rep);
+ pmf_sum1 := sum1 (job_task j_rep) |}) in *.
+ rewrite eq_refl => k.
+ rewrite (pr_joint_pred_eq _ _ _ (fun ω => true) (fun ω => ω <= k)).
+ { rewrite pr_xpredT Rmult_1_l.
+ by move: H_job_of_task => /eqP TSKo; rewrite /μ_tsk -TSKo; apply Rge_refl. }
+ { by intros [ω n]. }
+ Qed.
+
+ End CostBoundedByPWCET.
+
+ Section CostBounds.
+
+ Hypothesis H_jobs_neq : j_rep != j.
+
+ Lemma nonreplaced_pETs_dont_change_1_step :
+ odflt0 (𝓒_of S' j) ⪯ odflt0 (𝓒_of S j).
+ Proof.
+ unfold S' in *; clear S' => //=.
+ destruct S as [Ω μ A C].
+ destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in *.
+ set (μ_tsk := {| pmf := pWCET (job_task j_rep);
+ pmf_pos := nonneg (job_task j_rep);
+ pmf_sum1 := sum1 (job_task j_rep) |}) in *.
+ have NEQ2 : (j_rep == j) = false by apply/eqP/eqP.
+ rewrite NEQ2 => k; rewrite /cdf.
+ rewrite (pr_joint_pred_eq _ _ _ (odflt0 (C j) ⟨<=⟩ k) (fun ω => true)).
+ { by rewrite pr_xpredT Rmult_1_r; apply Rge_refl. }
+ { by intros [ω n]; rewrite andbT. }
+ Qed.
+
+ Lemma nonreplaced_pETs_dont_change_2_step :
+ odflt0 (𝓒_of S j) ⪯ odflt0 (𝓒_of S' j).
+ Proof.
+ unfold S' in *; clear S' => //=.
+ destruct S as [Ω μ A C].
+ destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in *.
+ set (μ_tsk := {| pmf := pWCET (job_task j_rep);
+ pmf_pos := nonneg (job_task j_rep);
+ pmf_sum1 := sum1 (job_task j_rep) |}) in *.
+ have NEQ2 : (j_rep == j) = false by apply/eqP/eqP.
+ rewrite NEQ2 => k; rewrite /cdf.
+ rewrite (pr_joint_pred_eq _ _ _ (odflt0 (C j) ⟨<=⟩ k) (fun ω => true)).
+ { by rewrite pr_xpredT Rmult_1_r; apply Rge_refl. }
+ { by intros [ω n]; rewrite andbT. }
+ Qed.
+
+ End CostBounds.
+
+ End Step1.
+
+ Section Step2.
+
+ Variable jobs_rep : seq Job.
+ Hypothesis H_jobs_uniq : uniq jobs_rep.
+
+ Variable S : @system Job.
+ Let S' := foldr replace_job_pET S jobs_rep.
+
+ Variables (j : Job) (tsk : Task).
+ Hypothesis H_j_in_reps : j \in jobs_rep.
+ Hypothesis H_job_of_task : job_of_task tsk j.
+
+ Lemma replaced_pETs_bounded_by_pWCETs_steps :
+ odflt0 (𝓒_of S' j) ⪯ to_distrib pWCET_pmf tsk.
+ Proof.
+ induction jobs_rep as [| j_rep jobs]; destruct S as [Ω μ 𝓐 𝓒]; first by done.
+ unfold S' in *; clear S'.
+ move: H_j_in_reps; rewrite in_cons => /orP [/eqP EQ | IN] TSK.
+ { by subst j_rep; apply replaced_pETs_bounded_by_pWCETs_step => //. }
+ { apply: Rge_trans; first apply nonreplaced_pETs_dont_change_1_step.
+ { by apply/eqP => EQ; subst; move: H_jobs_uniq; rewrite //= IN andFb. }
+ apply IHjobs => //.
+ by move: H_jobs_uniq; simpl => /andP [_ UNIQo]; apply: UNIQo.
+ }
+ Qed.
+
+ Lemma pWCETs_bounded_by_replaced_pETs_steps :
+ to_distrib pWCET_pmf tsk ⪯ odflt0 (𝓒_of S' j).
+ Proof.
+ induction jobs_rep as [| j_rep jobs]; destruct S as [Ω μ 𝓐 𝓒]; first by done.
+ unfold S' in *; clear S'.
+ move: H_j_in_reps; rewrite in_cons => /orP [/eqP EQ | IN] TSK.
+ { by subst j_rep; apply pWCETs_bounded_by_replaced_pETs_step => //. }
+ { apply: Rge_trans; last apply nonreplaced_pETs_dont_change_2_step; last first.
+ { by apply/eqP => EQ; subst; move: H_jobs_uniq; rewrite //= IN andFb. }
+ apply IHjobs => //.
+ by move: H_jobs_uniq; simpl => /andP [_ UNIQo]; apply: UNIQo.
+ }
+ Qed.
+
+ End Step2.
+
+ Section Step3.
+
+ Variable S : @system Job.
+ Let S' := replace_all_pETs S.
+
+ Lemma replaced_pETs_bounded_by_pWCETs :
+ forall (j : Job) (tsko : Task),
+ job_of_task tsko j ->
+ odflt0 (𝓒_of S' j) ⪯ to_distrib pWCET_pmf tsko.
+ Proof.
+ intros; apply replaced_pETs_bounded_by_pWCETs_steps => //.
+ - by apply index_enum_uniq.
+ - by apply mem_index_enum.
+ Qed.
+
+ Lemma pWCETs_bounded_by_replaced_pETs :
+ forall (j : Job) (tsko : Task),
+ job_of_task tsko j ->
+ to_distrib pWCET_pmf tsko ⪯ odflt0 (𝓒_of S' j).
+ Proof.
+ intros; apply pWCETs_bounded_by_replaced_pETs_steps => //.
+ - by apply index_enum_uniq.
+ - by apply mem_index_enum.
+ Qed.
+
+ Lemma pETs_have_same_distribution :
+ ∀ (j1 j2 : Job),
+ job_task j1 = job_task j2 ->
+ odflt0 (𝓒_of S' j1) ⪯ odflt0 (𝓒_of S' j2).
+ Proof.
+ intros * TSK.
+ apply: func_dom_trans.
+ { apply replaced_pETs_bounded_by_pWCETs_steps.
+ - by apply index_enum_uniq.
+ - by apply mem_index_enum.
+ - by rewrite /job_of_task /concept.job_task.
+ }
+ { apply pWCETs_bounded_by_replaced_pETs_steps.
+ - by apply index_enum_uniq.
+ - by apply mem_index_enum.
+ - by rewrite TSK /job_of_task /concept.job_task.
+ }
+ Qed.
+
+ End Step3.
+
+End TransformationEnsuresIdenticalCosts.
+
+(** In this section, we show that, in the transformed system, all pETs
+ are independent. *)
+Section TransformationEnsuresIndependentCosts.
+
+ Context {Task : TaskType}
+ {D : TaskDeadline Task}
+ {pWCET_pmf : ProbWCET Task}.
+
+ Context {Job : finType}
+ {job_task : JobTask Job Task}.
+
+ Variable ζ : @scheduler𝗔𝗖 Job.
+ Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).
+
+ Section Step1.
+
+ Variable (S : @system Job) (j_rep : Job) (j : Job).
+ Let S' : system := replace_job_pET j_rep S.
+
+ Variable jobs : seq Job.
+ Hypothesis H_jrep_notin_jobs : j_rep \notin jobs.
+
+ Lemma replaced_pETs_are_independent_step :
+ indep2 (𝓒_of S' j_rep) (rvar_list [seq 𝓒_of S' j | j <- jobs]).
+ Proof.
+ unfold S' in *; clear S' => //=.
+ destruct S as [Ω μ A C].
+ destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in *.
+ set (μ_tsk := {| pmf := pWCET (job_task j_rep);
+ pmf_pos := nonneg (job_task j_rep);
+ pmf_sum1 := sum1 (job_task j_rep) |}) in *.
+ intros a b; rewrite /pr_eq.
+ have EQ : forall a b c, a = b -> ((a == c) = (b == c)).
+ { clear. intros. subst. by done. }
+ rewrite (pr_joint_pred_eq
+ _ _ _
+ (fun (ω : Ω) => (rvar_list [seq C j | j <- jobs]) ω == b)
+ (fun (ω : nat) => Some ω == a)); last first.
+ { intros [ω n]; rewrite eq_refl andbC; f_equal.
+ simpl; apply: EQ.
+ induction jobs as [ | jo jobso]; first by done.
+ rewrite //= IHjobso; clear IHjobso; last first.
+ { by apply/negP; intros IN; move: (H_jrep_notin_jobs); rewrite in_cons IN orbT. }
+ apply/eqP; rewrite eqseq_cons; apply/andP; split; last by done.
+ have NEQ: j_rep == jo = false.
+ { by apply/negP => /eqP EQ; subst; move: (H_jrep_notin_jobs); rewrite in_cons eq_refl orTb. }
+ by rewrite NEQ.
+ }
+ rewrite (pr_joint_pred_eq _ _ _ xpredT (fun ω => Some ω == a)); last first.
+ { by rewrite eq_refl //=; intros [ω n]. }
+ rewrite (pr_joint_pred_eq
+ _ _ _ (fun (ω : Ω) => (rvar_list [seq C j | j <- jobs]) ω == b) xpredT
+ ); last first.
+ { intros [ω n]; rewrite //= andbT; apply: EQ.
+ induction jobs as [ | jo jobso]; first by done.
+ rewrite //= IHjobso; clear IHjobso; last first.
+ { by apply/negP; intros IN; move: (H_jrep_notin_jobs); rewrite in_cons IN orbT. }
+ apply/eqP; rewrite eqseq_cons; apply/andP; split; last by done.
+ have NEQ: j_rep == jo = false.
+ { by apply/negP => /eqP EQ; subst; move: H_jrep_notin_jobs; rewrite in_cons eq_refl orTb. }
+ by rewrite NEQ.
+ }
+ by rewrite !pr_xpredT Rmult_1_l Rmult_1_r Rmult_comm.
+ Qed.
+
+ Lemma transformation_respects_independence_step :
+ independent [seq 𝓒_of S j | j <- jobs] ->
+ independent [seq 𝓒_of S' j | j <- jobs].
+ Proof.
+ intros IND cs LEN; unfold S' in *; clear S' => //=.
+ destruct S as [Ω μ A C].
+ destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in *.
+ set (μ_tsk := {| pmf := pWCET (job_task j_rep);
+ pmf_pos := nonneg (job_task j_rep);
+ pmf_sum1 := sum1 (job_task j_rep) |}) in *.
+ apply: eq_tr4.
+ { apply IND.
+ rewrite -!seq_ext.size_legacy size_map; rewrite -!seq_ext.size_legacy size_map in LEN.
+ by apply LEN.
+ }
+ { rewrite (pr_joint_pred_eq
+ _ _ _ (fun (ω : Ω) => (rvar_list [seq C j | j <- jobs]) ω == cs) xpredT
+ ); last first.
+ { intros [ω n]; rewrite andbT zip_foldr_andb_seq_eq; last first.
+ { by move: LEN; rewrite -!seq_ext.size_legacy !size_map => ->. }
+ move: cs LEN; clear IND.
+ induction jobs as [ | jo jobso]; first by intros [].
+ intros []; first by done.
+ rewrite -!seq_ext.size_legacy !size_map //= => LEN; apply eq_add_S in LEN.
+ rewrite IHjobso; f_equal.
+ { by have ->: j_rep == jo = false
+ by apply/negP => /eqP EQ; subst; move: (H_jrep_notin_jobs); rewrite in_cons eq_refl orTb. }
+ { by apply/negP; intros IN; move: (H_jrep_notin_jobs); rewrite in_cons IN orbT. }
+ { by rewrite -!seq_ext.size_legacy !size_map. }
+ }
+ { rewrite !pr_xpredT Rmult_1_r.
+ apply pr_eq_pred => ω; rewrite !unfold_in zip_foldr_andb_seq_eq; last first.
+ { by move: LEN; rewrite -!seq_ext.size_legacy !size_map => ->. }
+ f_equal; rewrite !zip_map_rvar_eq; f_equal; f_equal.
+ by clear; induction jobs as [ | jo jobso]; [done | rewrite //= -IHjobso].
+ }
+ }
+ { f_equal; rewrite !zip_map_pr_eq.
+ move: cs LEN; clear IND; induction jobs as [ | jo jobso]; first by intros [].
+ intros []; first by done.
+ rewrite -!seq_ext.size_legacy !size_map //= => LEN; apply eq_add_S in LEN.
+ rewrite IHjobso; f_equal.
+ { have NEQ: j_rep == jo = false.
+ { by apply/negP => /eqP EQ; subst; move: (H_jrep_notin_jobs); rewrite in_cons eq_refl orTb. }
+ rewrite /pr_eq (pr_joint_pred_eq _ _ _ (fun ω => C jo ω == o) xpredT); last first.
+ { by rewrite NEQ //=; intros [ω n]; rewrite andbT. }
+ by rewrite pr_xpredT Rmult_1_r.
+ }
+ { by apply/negP; intros IN; move: (H_jrep_notin_jobs); rewrite in_cons IN orbT. }
+ { by rewrite -!seq_ext.size_legacy !size_map. }
+ }
+ Qed.
+
+ End Step1.
+
+ Section Step2.
+
+ Variable jobs_rep : seq Job.
+ Hypothesis H_jobs_uniq : uniq jobs_rep.
+
+ Variable S : @system Job.
+ Let S' : system := foldr replace_job_pET S jobs_rep.
+
+ Lemma replaced_pETs_are_independent_steps :
+ independent [seq 𝓒_of S' j | j <- jobs_rep].
+ Proof.
+ induction jobs_rep as [| j_rep jobs]; destruct S as [Ω μ 𝓐 𝓒].
+ { by intros; apply independent_nil. }
+ { intros; simpl.
+ apply indep2_independent_cons.
+ { by apply replaced_pETs_are_independent_step; move: H_jobs_uniq => /andP [H _]. }
+ { apply transformation_respects_independence_step => //.
+ by move: H_jobs_uniq => /andP [H _].
+ apply IHjobs.
+ by move: H_jobs_uniq => /andP [_ H].
+ }
+ }
+ Qed.
+
+ End Step2.
+
+ Section Step3.
+
+ Variable S : @system Job.
+ Let S' : system := replace_all_pETs S.
+
+ Lemma replaced_pETs_are_independent :
+ independent [seq 𝓒_of S' j | j <- index_enum Job].
+ Proof.
+ intros; apply replaced_pETs_are_independent_steps.
+ by apply index_enum_uniq.
+ Qed.
+
+ End Step3.
+
+End TransformationEnsuresIndependentCosts.
+
+(** Finally, we show that in the transformed system, all pETs are
+ independent of the arrival sequence, as well as independent of
+ each other conditioned on an arrival sequence. *)
+Section TransformationEnsuresCostsIndependentFromArrivals.
+
+ Context {Task : TaskType}
+ {D : TaskDeadline Task}
+ {pWCET_pmf : ProbWCET Task}.
+
+ Context {Job : finType}
+ {job_task : JobTask Job Task}.
+
+ Variable ζ : @scheduler𝗔𝗖 Job.
+ Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).
+
+ Section Step1.
+
+ Variable (S : @system Job) (j_rep : Job) (j : Job).
+ Let S' : system := replace_job_pET j_rep S.
+
+ Section IndependentArrSeq.
+
+ Variable ξa : arrival_sequence Job.
+ Let ξf := ξ_fix (arr_seq (job_arrival := 𝓐_of S)) ξa.
+ Let ξf' := ξ_fix (arr_seq (job_arrival := 𝓐_of S')) ξa.
+
+ Variable jobs : seq Job.
+ Hypothesis H_jrep_notin_jobs : j_rep \notin jobs.
+
+ Lemma transformation_respects_pET_indep_arr_seq_cons_step :
+ @indep2 _ _ _ (μ_of S)
+ {| rvar_fun := λ ω, [seq 𝓒_of S j0 ω | j0 <- jobs] |}
+ {| rvar_fun := ξf |} ->
+ @indep2 _ _ _ (μ_of S')
+ {| rvar_fun := λ ω, [seq 𝓒_of S' j0 ω | j0 <- j_rep :: jobs] |}
+ {| rvar_fun := ξf' |}.
+ Proof.
+ intros IND; unfold S' in *; clear S'.
+ destruct S as [Ω μ A C]; destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in *.
+ intros [ | c cs] b.
+ { rewrite //= pr_xpred0 /pr_eq eq_refl //=; symmetry.
+ by apply Rmult_eq_0_compat_r; apply pr_zero => [ω n]. }
+ { rewrite (pr_joint_pred_eq
+ _ _ _
+ (fun (ω : Ω) => ((rvar_list [seq C j | j <- jobs]) ω == cs) && (ξf ω == b))
+ (fun (ω : nat) => Some ω == c)); last first.
+ { intros [ω n] => //=; rewrite eq_refl eqseq_cons -andbA andbC; do 3 f_equal.
+ clear IND; induction jobs as [ | jo jobso]; first by done.
+ rewrite //= IHjobso; clear IHjobso; last first.
+ { by apply/negP; intros IN; move: H_jrep_notin_jobs; rewrite in_cons IN orbT. }
+ apply/eqP; rewrite eqseq_cons; apply/andP; split; last by done.
+ have NEQ: j_rep == jo = false.
+ { by apply/negP => /eqP EQ; subst; move: H_jrep_notin_jobs; rewrite in_cons eq_refl orTb. }
+ by rewrite NEQ.
+ }
+ rewrite /pr_eq (pr_joint_pred_eq
+ _ _ _
+ (fun ω => ((rvar_list [seq C j | j <- jobs]) ω == cs))
+ (fun ω => Some ω == c)); last first.
+ { intros [ω n] => //=; rewrite eq_refl eqseq_cons andbC; do 2 f_equal.
+ clear IND; induction jobs as [ | jo jobso]; first by done.
+ rewrite //= IHjobso; clear IHjobso; last first.
+ { by apply/negP; intros IN; move: H_jrep_notin_jobs; rewrite in_cons IN orbT. }
+ apply/eqP; rewrite eqseq_cons; apply/andP; split; last by done.
+ by have ->: j_rep == jo = false
+ by apply/negP => /eqP EQ; subst; move: H_jrep_notin_jobs; rewrite in_cons eq_refl orTb.
+ }
+ rewrite /pr_eq (pr_joint_pred_eq
+ _ _ _ (fun (ω : Ω) => (ξf ω == b)) (xpredT)); last first.
+ { by intros [ω n]; rewrite andbT; reflexivity. }
+ rewrite pr_xpredT Rmult_1_r Rmult_comm.
+ symmetry; rewrite Rmult_assoc Rmult_comm Rmult_assoc; apply Rmult_eq_compat_l; symmetry.
+ apply: eq_tr4; first apply (IND cs b).
+ { apply pr_eq_pred => ω; rewrite !unfold_in //=.
+ by do 2 f_equal; clear IND H_jrep_notin_jobs;
+ induction jobs as [ | jo jobso]; [ | rewrite //= IHjobso].
+ }
+ { rewrite Rmult_comm; apply Rmult_eq_compat_r.
+ apply pr_eq_pred => ω; rewrite !unfold_in //=.
+ by do 2 f_equal; clear IND H_jrep_notin_jobs;
+ induction jobs as [ | jo jobso]; [ | rewrite //= IHjobso].
+ }
+ }
+ Qed.
+
+ Lemma transformation_respects_pET_indep_arr_seq_eq_step :
+ @indep2 _ _ _ (μ_of S)
+ {| rvar_fun := λ ω, [seq 𝓒_of S j ω | j <- jobs] |}
+ {| rvar_fun := ξf |} ->
+ @indep2 _ _ _ (μ_of S')
+ {| rvar_fun := λ ω, [seq 𝓒_of S' j ω | j <- jobs] |}
+ {| rvar_fun := ξf' |}.
+ Proof.
+ intros IND; unfold S' in *; clear S'.
+ destruct S as [Ω μ A C]; destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in *.
+ intros cs b.
+ rewrite (pr_joint_pred_eq
+ _ _ _ (fun ω => ((rvar_list [seq C j | j <- jobs]) ω == cs) && (ξf ω == b)) xpredT
+ ); last first.
+ { intros [ω n] => //=. rewrite andbT; do 2 f_equal.
+ clear IND; induction jobs as [ | jo jobso]; first by done.
+ rewrite //= IHjobso; clear IHjobso; last first.
+ { by apply/negP; intros IN; move: H_jrep_notin_jobs; rewrite in_cons IN orbT. }
+ apply/eqP; rewrite eqseq_cons; apply/andP; split; last by done.
+ by have ->: j_rep == jo = false
+ by apply/negP => /eqP EQ; subst; move: H_jrep_notin_jobs; rewrite in_cons eq_refl orTb.
+ }
+ rewrite /pr_eq (pr_joint_pred_eq
+ _ _ _ (fun ω => ((rvar_list [seq C j | j <- jobs]) ω == cs)) xpredT
+ ); last first.
+ { intros [ω n] => //=; rewrite andbT; do 2 f_equal.
+ clear IND; induction jobs as [ | jo jobso]; first by done.
+ rewrite //= IHjobso; clear IHjobso; last first.
+ { by apply/negP; intros IN; move: H_jrep_notin_jobs; rewrite in_cons IN orbT. }
+ apply/eqP; rewrite eqseq_cons; apply/andP; split; last by done.
+ by have ->: j_rep == jo = false
+ by apply/negP => /eqP EQ; subst; move: H_jrep_notin_jobs; rewrite in_cons eq_refl orTb.
+ }
+ rewrite /pr_eq (pr_joint_pred_eq _ _ _ (fun ω => (ξf ω == b)) (xpredT)); last first.
+ { by intros [ω n]; rewrite andbT; reflexivity. }
+ rewrite pr_xpredT Rmult_comm !Rmult_1_r !Rmult_1_l.
+ apply: eq_tr4; first apply (IND cs b).
+ { apply pr_eq_pred => ω; rewrite !unfold_in //=.
+ by do 2 f_equal; clear IND H_jrep_notin_jobs;
+ induction jobs as [| jo jobso] ; [ | rewrite //= IHjobso]. }
+ { apply Rmult_eq_compat_r.
+ apply pr_eq_pred => ω; rewrite !unfold_in //=.
+ by do 2 f_equal; clear IND H_jrep_notin_jobs;
+ induction jobs as [| jo jobso]; [ | rewrite //= IHjobso]. }
+ Qed.
+
+ Lemma transformation_respects_pET_indep_arr_seq_remove_step :
+ @indep2 _ _ _ (μ_of S)
+ {| rvar_fun := λ ω, [seq 𝓒_of S j0 ω | j0 <- jobs & predC1 j0 j_rep] |}
+ {| rvar_fun := ξf |} ->
+ @indep2 _ _ _ (μ_of S')
+ {| rvar_fun := λ ω, [seq 𝓒_of S' j0 ω | j0 <- jobs] |}
+ {| rvar_fun := ξf' |}.
+ Proof.
+ intros IND; unfold S' in *; clear S'.
+ destruct S as [Ω μ A C]; destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in *.
+ intros cs b.
+ have [/eqP SEQ|SNEQ] := boolP (size cs == size jobs); last first.
+ { apply eq_tr3 with 0%R.
+ { apply pr_zero => [ω n]; apply/eqP.
+ rewrite eqbF_neg negb_and; apply/orP; left.
+ apply/negP => /eqP EQ; subst cs.
+ move: SNEQ => /negP SNEQ; apply: SNEQ.
+ by rewrite size_map.
+ }
+ { symmetry; apply Rmult_eq_0_compat_r.
+ apply pr_zero => [ω n]; apply/eqP => EQ; subst cs.
+ move: SNEQ => /negP SNEQ; apply: SNEQ.
+ by rewrite size_map.
+ }
+ }
+ set (csN := [seq p.2 | p <- zip jobs cs & j_rep != p.1]).
+ set (csE := [seq p.2 | p <- zip jobs cs & j_rep == p.1]).
+ rewrite /pr_eq (pr_joint_pred_eq
+ _ _ _
+ (fun (ω : Ω) => ((rvar_list [seq C j | j <- jobs & j_rep != j]) ω == csN) && (ξf ω == b))
+ (fun (n : nat) => [seq Some n | j <- jobs & j_rep == j] == csE)
+ ); last first.
+ { intros [ω n]; symmetry; rewrite andbC andbA.
+ f_equal; unfold csN, csE; clear csN csE H_jrep_notin_jobs IND.
+ move: cs SEQ; induction jobs as [|jo jobso]; first by intros [].
+ intros []; first by done.
+ intros; simpl.
+ have [/eqP EQa | NEQa] := boolP (j_rep == jo).
+ { by rewrite //= !eqseq_cons -IHjobso;
+ [rewrite andbA; f_equal | apply eq_add_S, SEQ]. }
+ { by rewrite //= !eqseq_cons -IHjobso;
+ [rewrite andbC -!andbA; f_equal; rewrite andbC; f_equal
+ | apply eq_add_S, SEQ]. }
+ }
+ rewrite (pr_joint_pred_eq
+ _ _ _
+ (fun (ω : Ω) => ((rvar_list [seq C j | j <- jobs & j_rep != j]) ω == csN))
+ (fun (n : nat) => [seq Some n | j <- jobs & j_rep == j] == csE)
+ ); last first.
+ { intros [ω n]; symmetry.
+ unfold csN, csE; clear csN csE H_jrep_notin_jobs IND; move: cs SEQ.
+ induction jobs as [ | jo jobso]; first by intros [].
+ intros []; [by done | intros; simpl].
+ have [/eqP EQa | NEQa] := boolP (j_rep == jo).
+ { by rewrite //= !eqseq_cons -IHjobso;
+ [rewrite andbC -!andbA; f_equal; rewrite andbC; f_equal
+ | apply eq_add_S, SEQ]. }
+ { by rewrite //= !eqseq_cons -IHjobso;
+ [rewrite andbA; f_equal | apply eq_add_S, SEQ]. }
+ }
+ rewrite /pr_eq (pr_joint_pred_eq _ _ _ (fun ω => ξf ω == b) xpredT); last first.
+ { by intros [ω n]; rewrite andbT; reflexivity. }
+ rewrite pr_xpredT Rmult_comm !Rmult_1_r.
+ set (μ_tsk := {| pmf := pWCET (job_task j_rep);
+ pmf_pos := nonneg (job_task j_rep);
+ pmf_sum1 := sum1 (job_task j_rep) |}) in *.
+ symmetry; rewrite Rmult_assoc Rmult_comm Rmult_assoc; apply Rmult_eq_compat_l; symmetry.
+ apply: eq_tr4; first apply (IND csN b).
+ { apply pr_eq_pred => ω; rewrite !unfold_in //=; unfold csN in *.
+ do 2 f_equal; clear IND H_jrep_notin_jobs csN csE; move: cs SEQ.
+ induction jobs as [| jo jobso]; first by done.
+ intros []; [by done | intros; simpl].
+ (have [/eqP EQa | NEQa] := boolP (j_rep == jo));
+ by simpl; erewrite IHjobso; [reflexivity | apply eq_add_S, SEQ].
+ }
+ { rewrite Rmult_comm; apply Rmult_eq_compat_r.
+ rewrite /pr_eq; apply pr_eq_pred => ω; rewrite !unfold_in //=; unfold csN in *.
+ do 2 f_equal; clear IND H_jrep_notin_jobs csN csE; move: cs SEQ.
+ induction jobs as [| jo jobso]; first by done.
+ intros []; [by done | intros; simpl].
+ (have [/eqP EQa | NEQa] := boolP (j_rep == jo));
+ by simpl; erewrite IHjobso; [reflexivity | apply eq_add_S, SEQ].
+ }
+ Qed.
+
+ End IndependentArrSeq.
+
+ Section IndependentArrSeqPartition.
+
+ Variable jobs : seq Job.
+ Hypothesis H_jrep_notin_jobs : j_rep \notin jobs.
+
+ Lemma transformation_respects_pET_indep_arr_seq_eq_part_step :
+ (forall (ξpart := @partition_on_ξ (Ω_of S) (μ_of S) Job (𝓐_of S)) (ξ : I ξpart),
+ @indep2 _ _ _ (μ_of S)
+ {| rvar_fun := λ ω : Ω_of S, [seq 𝓒_of S j0 ω | j0 <- jobs] |}
+ {| rvar_fun := [eta ξpart◁{ξ}] |}
+ ) ->
+ forall (ξpart := @partition_on_ξ (Ω_of S') (μ_of S') Job (𝓐_of S')) (ξ : I ξpart),
+ @indep2 _ _ _ (μ_of S')
+ {| rvar_fun := λ ω : Ω_of S', [seq 𝓒_of S' j0 ω | j0 <- jobs] |}
+ {| rvar_fun := [eta ξpart◁{ξ}] |}.
+ Proof.
+ intros IND *; apply transformation_respects_pET_indep_arr_seq_eq_step => //.
+ rename ξ into ξs'.
+ have [ξs EQ] := transformation_preserves_arr_seq _ _ ξs'; simpl in EQ.
+ destruct S as [Ω μ A C].
+ destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in *.
+ set (μ_tsk := {| pmf := pWCET (job_task j_rep);
+ pmf_pos := nonneg (job_task j_rep);
+ pmf_sum1 := sum1 (job_task j_rep) |}) in *.
+ specialize (IND ξs); destruct ξs' as [ξ' INξ'], ξs as [ξ INξ].
+ intros ? ?; apply: eq_tr4; first by apply IND.
+ { apply pr_eq_pred => ω; rewrite !unfold_in.
+ f_equal => //=; unfold ξ_fix; do 2 f_equal.
+ simpl in EQ; clear INξ' IND INξ.
+ apply (@FunctionalExtensionality.functional_extensionality _ _ ξ' ξ).
+ by intros; symmetry; apply EQ.
+ }
+ { f_equal; apply pr_eq_pred => ω; rewrite !unfold_in.
+ f_equal => //=; unfold ξ_fix; f_equal.
+ apply (@FunctionalExtensionality.functional_extensionality _ _ ξ' ξ).
+ by intros; symmetry; apply EQ.
+ }
+ Qed.
+
+ Lemma transformation_respects_pET_indep_arr_seq_remove_part_step :
+ (forall (ξpart := @partition_on_ξ (Ω_of S) (μ_of S) Job (𝓐_of S)) (ξ : I ξpart),
+ @indep2 _ _ _ (μ_of S)
+ {| rvar_fun := λ ω : Ω_of S, [seq 𝓒_of S j0 ω | j0 <- jobs & predC1 j0 j_rep] |}
+ {| rvar_fun := [eta ξpart◁{ξ}] |}
+ ) ->
+ forall (ξpart := @partition_on_ξ (Ω_of S') (μ_of S') Job (𝓐_of S')) (ξ : I ξpart),
+ @indep2 _ _ _ (μ_of S')
+ {| rvar_fun := λ ω : Ω_of S', [seq 𝓒_of S' j0 ω | j0 <- jobs] |}
+ {| rvar_fun := [eta ξpart◁{ξ}] |}.
+ Proof.
+ intros IND *; apply transformation_respects_pET_indep_arr_seq_remove_step => //.
+ rename ξ into ξs'.
+ have [ξs EQ] := transformation_preserves_arr_seq _ _ ξs'; simpl in EQ.
+ destruct S as [Ω μ A C].
+ destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in *.
+ set (μ_tsk := {| pmf := pWCET (job_task j_rep);
+ pmf_pos := nonneg (job_task j_rep);
+ pmf_sum1 := sum1 (job_task j_rep) |}) in *.
+ specialize (IND ξs); destruct ξs' as [ξ' INξ'], ξs as [ξ INξ].
+ intros ? ?; apply: eq_tr4; first by apply IND.
+ { apply pr_eq_pred => ω; rewrite !unfold_in.
+ f_equal => //=; unfold ξ_fix; do 2 f_equal.
+ simpl in EQ; clear INξ' IND INξ.
+ apply (@FunctionalExtensionality.functional_extensionality _ _ ξ' ξ).
+ by intros; symmetry; apply EQ.
+ }
+ { f_equal; apply pr_eq_pred => ω; rewrite !unfold_in.
+ f_equal => //=; unfold ξ_fix; f_equal.
+ apply (@FunctionalExtensionality.functional_extensionality _ _ ξ' ξ).
+ by intros; symmetry; apply EQ.
+ }
+ Qed.
+
+ End IndependentArrSeqPartition.
+
+ End Step1.
+
+ Section Step2.
+
+ Variable jobs_rep : seq Job.
+ Hypothesis H_jrep_notin_jobs : uniq jobs_rep.
+
+ Variable S : @system Job.
+ Let S' : system := foldr replace_job_pET S jobs_rep.
+
+ Let ξpart := @partition_on_ξ (Ω_of S') (μ_of S') Job (𝓐_of S').
+ Variable (ξ : I ξpart).
+
+ Lemma replaced_pETs_are_independent_from_arr_seq_partition_steps :
+ forall (jobs : seq Job),
+ (forall j, j \in jobs -> j \in jobs_rep) ->
+ @indep2 _ _ _ (μ_of S')
+ {| rvar_fun := λ ω : Ω_of S', [seq 𝓒_of S' j0 ω | j0 <- jobs] |}
+ {| rvar_fun := [eta ξpart◁{ξ}] |}.
+ Proof.
+ induction jobs_rep as [| j_rep jobs_repo]; destruct S as [Ω μ 𝓐 𝓒].
+ { intros; destruct jobs.
+ { intros [] ?; simpl.
+ { by symmetry; rewrite /pr_eq //= pr_xpredT_ext // Rmult_1_l. }
+ { by rewrite //= pr_xpred0; symmetry; apply Rmult_eq_0_compat_r, pr_zero. }
+ }
+ { exfalso; specialize (H s); feed H; last by done.
+ by rewrite in_cons eq_refl orTb.
+ }
+ }
+ { intros * SUB; set (ξe := {| rvar_fun := [eta ξpart◁{ξ}] |}).
+ have [IN|NIN] := boolP (j_rep \in jobs).
+ { apply transformation_respects_pET_indep_arr_seq_remove_part_step => //; intros.
+ apply IHjobs_repo; first by move: H_jrep_notin_jobs => /andP [_ T].
+ intros *; rewrite mem_filter /predC1.
+ move => /andP [NEQ INj]; specialize (SUB _ INj).
+ move: SUB; rewrite in_cons.
+ move => /orP [/eqP EQ| INr] => //; subst.
+ by simpl in NEQ; rewrite eq_refl in NEQ.
+ }
+ { apply transformation_respects_pET_indep_arr_seq_eq_part_step => //; intros.
+ apply IHjobs_repo; first by move: H_jrep_notin_jobs => /andP [_ T].
+ intros; specialize (SUB _ H).
+ move: SUB; rewrite in_cons.
+ move => /orP [/eqP EQ| INr] => //.
+ by subst; move: NIN; rewrite H.
+ }
+ }
+ Qed.
+
+ End Step2.
+
+ Section Step3.
+
+ Variable S : @system Job.
+ Let S' := replace_all_pETs S.
+
+ Let ξpart := @partition_on_ξ (Ω_of S') (μ_of S') Job (𝓐_of S').
+ Variable (ξ : I ξpart).
+ Variable (ρ : PosProb (μ_of S') (ξpart◁{ξ})).
+
+ Lemma replaced_pETs_are_independent_from_arr_seq_partition :
+ ∀ (jobs : seq Job),
+ @indep2 _ _ _ (μ_of S')
+ {| rvar_fun := λ ω, [seq 𝓒_of S' j0 ω | j0 <- jobs] |}
+ {| rvar_fun := [eta ξpart◁{ξ}] |}.
+ Proof.
+ intros.
+ apply replaced_pETs_are_independent_from_arr_seq_partition_steps.
+ apply index_enum_uniq.
+ by intros; apply mem_index_enum.
+ Qed.
+
+ Lemma replaced_pETs_are_cond_independent :
+ @independent
+ _ _ (restrict (μ_of S') (ξpart◁{ξ}))
+ [seq mkRvar _ (𝓒_of S' j) | j <- index_enum Job].
+ Proof.
+ intros ? LEN.
+ rewrite -!seq_ext.size_legacy size_map in LEN.
+ rewrite fold_prob_to_cond_prob pr_cond_indep2; last first.
+ { eapply indep2_fn_extl with
+ (X1 := {| rvar_fun := λ ω : Ω_of S', [seq 𝓒_of S' j0 ω | j0 <- index_enum Job] |})
+ (f := fun X1 => fold_right andb true [seq Xb.1 == Xb.2 | Xb <- seq.zip X1 lb]).
+ { by intros; rewrite //= zip_map_rvar_eq; reflexivity. }
+ { by apply replaced_pETs_are_independent_from_arr_seq_partition. }
+ }
+ apply: eq_tr4.
+ { by apply replaced_pETs_are_independent; rewrite -!seq_ext.size_legacy size_map; apply LEN. }
+ { apply pr_eq_pred => ω; rewrite !unfold_in.
+ by f_equal; rewrite !zip_map_rvar_eq; f_equal.
+ }
+ { rewrite !zip_map_pr_eq !foldr_big !big_map; apply eq_big; first by done.
+ intros [j t] _; rewrite /pr_eq fold_prob_to_cond_prob pr_cond_indep2; first by reflexivity.
+ eapply indep2_fn_extl with
+ (X1 := {| rvar_fun := λ ω : Ω_of S', [seq 𝓒_of S' j0 ω | j0 <- [::j]] |})
+ (f := fun X1 => fold_right andb true [seq Xb.1 == Xb.2 | Xb <- seq.zip X1 [::t]]).
+ { by intros; rewrite //= andbT; reflexivity. }
+ { by apply replaced_pETs_are_independent_from_arr_seq_partition. }
+ }
+ Qed.
+
+ Lemma replaced_cond_pETs_bounded_by_pWCETs :
+ ∀ (j : Job) (tsk : Task),
+ job_of_task tsk j →
+ mkRvar (restrict (μ_of S') (ξpart◁{ξ})) [eta odflt0 (𝓒_of S' j)] ⪯ to_distrib pWCET_pmf tsk.
+ Proof.
+ intros; intros ?.
+ rewrite fold_prob_to_cond_prob.
+ rewrite pr_cond_indep2; last first.
+ { apply indep2_fn_extl with (X1 := {| rvar_fun := [eta odflt0 (𝓒_of S' j)] |}) (f := fun X1 => X1 <= h).
+ { by intros; reflexivity. }
+ apply indep2_fn_extl with (X1 := 𝓒_of S' j) (f := odflt 0).
+ { by intros; reflexivity. }
+ apply indep2_fn_extl with
+ (X1 := {| rvar_fun := λ ω : Ω_of S', [seq 𝓒_of S' j0 ω | j0 <- [::j]] |})
+ (f := head None).
+ { by intros; reflexivity. }
+ apply replaced_pETs_are_independent_from_arr_seq_partition.
+ }
+ by eapply Rge_trans, replaced_pETs_bounded_by_pWCETs, H; apply Rge_refl.
+ Qed.
+
+ End Step3.
+
+End TransformationEnsuresCostsIndependentFromArrivals.
diff --git a/rt/analysis/work_bound.v b/rt/analysis/work_bound.v
index 975d34e..fb98d26 100644
--- a/rt/analysis/work_bound.v
+++ b/rt/analysis/work_bound.v
@@ -33,9 +33,9 @@ Section PrTaskWorkloadBoundedNthCost.
(** Assume that job costs are independent of the (prob.) arrival sequence. *)
Let ξpart := partition_on_ξ μ : Ω_partition.
- Hypothesis H_job_costs_independent_arr_seq :
+ Hypothesis job_costs_independent_arr_seq :
let ξpart := partition_on_ξ μ : Ω_partition in
- forall (ξ : I ξpart) `(!PosProb μ (ξpart◁{ξ})) (jobs : seq Job),
+ forall (ξ : I ξpart) `{!PosProb μ (ξpart◁{ξ})} (jobs : seq Job),
indep2
(mkRvar μ (fun ω => [seq job_cost j ω | j <- jobs]))
(mkRvar μ (fun ω => ξpart◁{ξ} ω)).
@@ -61,7 +61,7 @@ Section PrTaskWorkloadBoundedNthCost.
{ by rewrite //= in IHjobs; rewrite //= !big_cons //= IHjobs. }
}
eapply indep2_fn_extl; first by intros; apply: EQ.
- by apply H_job_costs_independent_arr_seq, PosProb0.
+ by apply job_costs_independent_arr_seq, PosProb0.
Qed.
diff --git a/util/seq.v b/util/seq.v
new file mode 100644
index 0000000..09bdcaa
--- /dev/null
+++ b/util/seq.v
@@ -0,0 +1,179 @@
+(* --------------------------- Reals and SSReflect -------------------------- *)
+From mathcomp Require Export ssreflect ssrbool eqtype ssrnat seq.
+
+(* --------------------------------- Prosa ---------------------------------- *)
+Require Export prosa.util.list.
+
+(* ---------------------------------- Main ---------------------------------- *)
+Lemma seq_split_take_drop :
+ forall {X : eqType} (e : X) (xs : seq X),
+ (e \in xs) ->
+ xs = take (index e xs) xs ++ [:: e] ++ drop (index e xs).+1 xs.
+Proof.
+ intros * IN.
+ induction xs; first by done.
+ simpl; destruct ( _ == _ ) eqn:EQ.
+ { by rewrite //= drop0; move: EQ => /eqP EQ; subst. }
+ { rewrite //= {1}IHxs //=.
+ by move: IN; rewrite in_cons eq_sym EQ orFb. }
+Qed.
+
+Lemma seq_split :
+ forall {X : eqType} (e : X) (xs : seq X),
+ (e \in xs) ->
+ exists xs1 xs2,
+ xs = xs1 ++ [::e] ++ xs2
+ /\ (e \notin xs1).
+Proof.
+ intros * IN.
+ set (i := index e xs).
+ exists (take i xs), (drop i.+1 xs).
+ repeat split.
+ { by apply seq_split_take_drop. }
+ { apply/negP => INT; apply index_ltn in INT.
+ by rewrite ltnn in INT.
+ }
+Qed.
+
+Lemma choose_superior_default_or_in_seq :
+ forall {X : eqType} (R : rel X) (a e : X) (ys : seq X),
+ foldr (choose_superior R) (Some a) ys = Some e ->
+ a = e \/ e \in ys.
+Proof.
+ intros; induction ys.
+ { by inversion H; subst; left. }
+ { simpl in H.
+ destruct (foldr (choose_superior R) (Some a) ys) eqn:FLR.
+ { unfold choose_superior in H; destruct (R a0 s) eqn:REL.
+ { inversion H; subst; right.
+ by rewrite in_cons eq_refl orTb. }
+ { inversion H; subst; apply IHys in H.
+ by destruct H; [subst; left | right; rewrite in_cons H orbT].
+ }
+ }
+ { by inversion H; subst; right; rewrite in_cons eq_refl orTb. }
+ }
+Qed.
+
+Lemma foldr_choose_superior_not_none :
+ forall {X : eqType} (R : rel X) (e : X) (ys : seq X),
+ ~ foldr (choose_superior R) (Some e) ys = None.
+Proof.
+ intros; induction ys; first by simpl.
+ simpl; intros ?; apply: IHys.
+ destruct (foldr (choose_superior R) (Some e) ys).
+ { by unfold choose_superior in H; destruct (R a s). }
+ { by done. }
+Qed.
+
+Lemma foldr_choose_superior_in_seq :
+ forall {X : eqType} (R : rel X) (ys : seq X) (y e : X),
+ (y \in ys) ->
+ (R y e) ->
+ foldr (choose_superior R) (Some e) ys = Some e ->
+ e \in ys.
+Proof.
+ intros * IN Rye FL.
+ have FF := seq_split _ _ IN.
+ destruct FF as [xs1 [xs2 [EQ NIN]]].
+ subst; rewrite !foldr_cat in FL.
+ simpl in FL; clear IN.
+ destruct (foldr (choose_superior R) (Some e) xs2) eqn:EQ.
+ { simpl in FL; destruct (R y s) eqn: RR.
+ { eapply choose_superior_default_or_in_seq in FL; destruct FL as []; subst.
+ { by rewrite !mem_cat mem_seq1 eq_refl orbT. }
+ { by rewrite !mem_cat H. }
+ }
+ { apply choose_superior_default_or_in_seq in FL.
+ destruct FL as []; subst.
+ { by rewrite RR in Rye. }
+ { by rewrite !mem_cat H. }
+ }
+ }
+ { by eapply foldr_choose_superior_not_none in EQ. }
+Qed.
+
+Lemma supremum_monotone_wrt_subset :
+ forall {X : eqType} (R : rel X) (e : X) (xs ys : seq X),
+ reflexive R ->
+ total R ->
+ transitive R ->
+ uniq ys ->
+ subseq xs ys ->
+ (e \in xs) ->
+ supremum R ys = Some e ->
+ supremum R xs = Some e.
+Proof.
+ intros * REF TOT TR UNIQ SUB IN SUP.
+ have INy : e \in ys by apply: supremum_in; eassumption.
+ move: (seq_split e ys INy) => [ys1 [ys2 [EQ NINy]]]; subst ys.
+ have NR1 : forall y, y \in ys2 -> R e y.
+ { intros; apply supremum_spec with (y0 := y) in SUP => //.
+ by rewrite mem_cat mem_cat H !orbT. }
+ have NR2 : forall y, y \in ys1 -> ~~ R y e.
+ { intros; apply/negP => Rye; clear INy SUB IN.
+ rewrite /supremum !foldr_cat in SUP.
+ destruct (foldr (choose_superior R) None ys2) eqn:FLD2.
+ { have EQ : foldr (choose_superior R) (Some s) [:: e] = Some e.
+ { by rewrite //= NR1; [reflexivity | apply supremum_in in FLD2]. }
+ rewrite EQ in SUP; clear EQ FLD2.
+ eapply foldr_choose_superior_in_seq in SUP; eauto 1.
+ by rewrite SUP in NINy.
+ }
+ { eapply foldr_choose_superior_in_seq in SUP; eauto 1.
+ by rewrite SUP in NINy.
+ }
+ }
+ have L2: exists xs1 xs2, xs = xs1 ++ [::e] ++ xs2 /\ e \notin xs1.
+ { set (i := index e xs).
+ exists (take i xs), (drop i.+1 xs).
+ repeat split.
+ { by apply seq_split_take_drop. }
+ { apply/negP => INT; apply index_ltn in INT.
+ by rewrite ltnn in INT.
+ }
+ }
+ clear IN; move: L2 => [xs1 [xs2 [EQ NINx]]]; subst xs.
+ have L22: subseq xs1 ys1 /\ subseq xs2 ys2.
+ { apply/andP; erewrite <-uniq_subseq_pivot.
+ { by instantiate (1 := e); apply SUB. }
+ { by done. }
+ }
+ clear SUB; move: L22 => [SUB1 SUB2].
+ have L3 : forall x : X, x \in xs1 -> ~~ R x e.
+ { by intros * IN; apply NR2; apply: mem_subseq; eauto 1. }
+ have L4 : forall x : X, x \in xs2 -> R e x.
+ { by intros * IN; apply NR1; apply: mem_subseq; eauto 1. }
+ rewrite /supremum foldr_cat foldr_cat.
+ have FLEQ: foldr (choose_superior R) (Some e) xs1 = Some e.
+ { clear SUB1 SUB2 NINy NINx.
+ induction xs1; first by done.
+ rewrite //= IHxs1.
+ { simpl.
+ have -> : R a e = false.
+ { apply/eqP; rewrite eqbF_neg; apply L3.
+ by rewrite in_cons eq_refl orTb.
+ }
+ reflexivity.
+ }
+ { by intros; apply L3; rewrite in_cons H orbT. }
+ }
+ destruct (foldr _ None _) eqn:FL3; last by apply FLEQ.
+ destruct (foldr _ (Some s) _) eqn:FLe.
+ { simpl in FLe.
+ rewrite L4 in FLe; last by apply: supremum_in; apply FL3.
+ inversion FLe; subst s0; clear FLe.
+ by apply FLEQ.
+ }
+ { by simpl in FLe; destruct (R e s). }
+Qed.
+
+Lemma subseq_filter :
+ forall {X : eqType} (xs : seq X) (P1 P2 : pred X),
+ (forall x, x \in xs -> P1 x -> P2 x) ->
+ subseq [seq x <- xs | P1 x] [seq x <- xs | P2 x].
+Proof.
+ intros; rewrite subseq_filter; apply/andP; split.
+ { by apply/allP => x; rewrite mem_filter => /andP [Px INx]; apply H. }
+ { by apply filter_subseq. }
+Qed.
--
GitLab