Library probsa.rt.analysis.axiomatic_pWCET_step

From prosa.model Require Import processor.ideal.

From probsa.util Require Export misc bigop_inf.
From probsa.probability Require Export pred law_of_total_prob.
From probsa.rt.model Require Export task events axiomatic_pWCET scheduler rt_monotonic.
From probsa.rt.analysis Require Export pETs_to_pWCETs partition_transfer.

From mathcomp Require Import finfun.

In this file, we prove Theorem 1 presented in the paper "What really is pWCET? A Rigorous Axiomatic Definition of pWCET" by Bozhko et al. (RTSS'23).

Step-by-step Proof of Theorem 1

In the following, we present the proof of Theorem 1 in the above-cited paper. Due to the length of the proof and the nature of Coq, we cannot start this section with the statement of the theorem. Instead, we will first prove many "stepping stone" lemmas and then combine them together to obtain a complete proof. Readers who would like to see the final statement of the theorem first are referred to section ProofOfTheorem1.

Section StepByStepProof.

In this section, we demonstrate a step-by-step proof of the main claim (Theorem 1 from the paper). It is important to note that Coq's preferred method of proof is a "bottom-up" approach, while most humans are prefer following a top-down derivation. In other words, in Coq it is easier to present proofs in the following way: first simple facts are proven, then one can use these simple facts to construct more sophisticated facts, then even more sophisticated ones, and so on until the final goal is reached. Yet, a reasonable question for a human would be "where is this going?"

Therefore, we adopt a more paper-like approach in which we present the proof as a series of implications: C → Goal, B → C, A → B. This allows us to begin with the final goal (assuming that some facts are given) and then gradually work our way towards the "leafs" of the overall argument pertaining to specific details.

Assume horizon defines (an upper bound on) the termination time of the system. If horizon = None, the system does not necessarily terminate. Note, however, that in either case our proof assumes there to be a finite number of jobs for technical reasons. As the horizon can be chosen to be arbitrarily large (the proof does not depend on its magnitude), e.g., hundreds of even thousands of years, assuming the existence of a finite horizon is not unreasonable for a computing system.

Variable horizon : option instant.

Consider any type of tasks with a notion of pWCET...

Context {Task : TaskType}
{pWCET_pmf : ProbWCET Task}.

...and their jobs.

Context {Job : finType}
{job_task : JobTask Job Task}.

Consider a response-time monotonic scheduling algorithm ζ, where response-time monotonic means the following: assuming that all arrival times are fixed, an increase of the execution cost of any job cannot cause a decrease in the response time of any job. Recall that ζ receives two vectors: a vector of arrival times 𝗔 and a vector of job costs 𝗖.

Variable ζ : @scheduler 𝗔𝗖 Job.
Hypothesis H_rt_monotonic : rt_monotonic_scheduler horizon ζ.

For brevity, let sched denote the probabilistic schedule generated by ζ for a given system S.

Let sched S := compute_pr_schedule ζ (job_arrival := 𝓐 _of S) (job_cost := 𝓒 _of S).

As before, consider four parameters that describe a system under analysis: a sample space Ω, a measure μ, job arrival times 𝓐, and job execution costs 𝓒.

  Variable Ω : countType.
  Variable μ : measure Ω.
  Variable 𝓐 : JobArrivalRV Job Ω μ.
  Variable 𝓒 : JobCostRV Job Ω μ.

Let us use these parameters to construct a system S.

Let S := {| Ω_of := Ω; μ_of := μ; 𝓐 _of := 𝓐; 𝓒 _of := 𝓒 |}.

Next, we assume that the aforementioned pWCET is an axiomatic pWCET. That is, for any job j and any arrival sequence ξ, there exists a partition of Ω into positive-probability events such that both partition dominance and partition independence are satisfied.

Hypothesis H_axiomatic_pWCET :
axiomatic_pWCET (μ_of S) (job_arrival := 𝓐 _of S) (job_cost := 𝓒 _of S).

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.

Variable j_rep : Job.
Let S' := replace_job_pET j_rep S.

For convenience, let tsk denote j's task...

Let tsk := job_task j_rep.

... and let μ_tsk denote the measure induced by pWCET.

  Let μ_tsk :=
    match pWCET_pmf with
    | Build_ProbWCET pWCET nonneg sum1 ⇒
        {| pmf := pWCET tsk;
          pmf_pos := nonneg tsk;
          pmf_sum1 := sum1 tsk |}
    end.

Next, consider an arbitrary job j of any task and a duration r.

Variables (j : Job) (r : duration).

Finally, let Exc denote the event that j's response time exceeds r time units in system S ...

  Let Exc := λ ω : Ω_of S , exceeds (response_time
                                      (job_arrival := 𝓐 _of S) (job_cost := 𝓒 _of S)
                                      (sched S) horizon j ω)
                                   r.

... and let Exc' denote the event that j's response time exceeds r time units in system S'.

  Let Exc' := λ ω : Ω_of S', exceeds (response_time
                                        (job_arrival := 𝓐 _of S') (job_cost := 𝓒 _of S')
                                        (sched S') horizon j ω)
                                     r.

The remainder of this file serves for the most part to relate the probability of Exc with the probability of Exc', namely to establish that ℙ<μ_of S>{[ Exc ]} ≤ ℙ<μ_of S'>{[ Exc' ]}.

Step 1

Now we are ready to start the proof. First, we do a case analysis on all possible arrival sequences.

Section Step1.

Consider a partition ξpart of the sample space Ω_of S of system S into events corresponding to different arrival sequences.

Let ξpart := partition_on_ξ μ.

Here ξpart is an (indexed) set of events, where an ξi-th event denoted as ξpart◁{ξi} represents a subset of Ω where the arrival sequence is equal to ξi.

(Readers focused on technical detail may be interested in noting that the indices of partition ξpart are arrival sequences themselves. This detail may be safely skipped over by more casual readers.)

As discussed in the paper, one can transfer the partition ξpart to the system S' and denote it as ξpart'. For further details see the function partition_transfer.extend_partition.

Let ξpart' := extend_partition S ξpart j_rep.

Partitions ξpart and ξpart' are so similar that one can prove equivalence. For example, two indices ξi and ξi' that are "pickle equivalent" can be shown to be identical. (Pickle equivalence is a very strong notion of equivalence; one can intuitively view it simply as an equality between two elements of similar types; for further details see util.bigop_inf.pickle_bij.)

    Remark ξi_eq_ξ' :
      ∀ (ξi : I ξpart) (ξi' : I ξpart'),
        pickle_bij ξi ξi' → ξi = ξi'.
    Proof.
      by intros ? ? ξ_equivalence; destruct ξ_equivalence as [u [EQ4 EQ5]];
      rewrite EQ4 in EQ5; inversion EQ5; subst ξi'.
    Qed.

Now, recall that we present the proof in a top-down (C → Goal) fashion, starting with the overall theorem.

So, assuming that for any two elements of partitions ξi : I ξpart and ξi' : I ξpart' that are "pickle"-equivalent, it holds that ℙ{[ Exc1 ∩ ξpart◁{ξi} ]} ≤ ℙ{[ Exc2 ∩ ξpart'◁{ξi'} ]}, ...

    Hypothesis H_ineq_ξ_partitioned :
      ∀ (ξi : I ξpart) (ξi' : I ξpart') (ξEQU : pickle_bij ξi ξi'),
        ℙ <μ_of S >{[ Exc ∩ ξpart ◁{ξi } ]} ≤ ℙ <μ_of S'>{[ Exc' ∩ ξpart'◁{ξi'} ]}.

... we can show that ℙ<μ_of S>{[ Exc1 ]} ≤ ℙ<μ_of S'>{[ Exc2 ]}. Or, in other words, we reduced the lemma statement to the hypothesis statement.

    Lemma transformation_is_pRT_monotone_step1 :
      ℙ <μ_of S >{[ Exc ]} ≤ ℙ <μ_of S'>{[ Exc' ]}.
    Proof.
      rewrite (law_of_total_probability_prod _ _ ξpart)
              (law_of_total_probability_prod _ _ ξpart') -/S'.
      intros; apply leq_SeriesC.
      { eapply ex_seriesC_le; last by eapply ex_series_pr_eq_over_partition.
        intros ?; split.
        - by apply Rge_le, ge_pr_0.
        - by apply pr_leq_intersectionr.
      }
      { eapply ex_seriesC_le; last by eapply ex_series_pr_eq_over_partition.
        intros ?; split.
        - by apply Rge_le, ge_pr_0.
        - by apply pr_leq_intersectionr.
      }
      { intros; split; intros PICK; unfold is_some in ×.
        { replace (@I _ _ _) with (@I (Ω_of S) (μ_of S) ξpart); [by done | clear PICK].
          unfold ξpart', partition.I, S', replace_job_pET.
          by destruct pWCET_pmf as [pWCET nonneg sum1], ξpart ⇒ //=.
        }
        { replace (@I _ _ _) with (@I (Ω_of S) (μ_of S) ξpart) in PICK; [by done | clear PICK].
          unfold ξpart', partition.I, S', replace_job_pET.
          by destruct pWCET_pmf as [pWCET nonneg sum1], ξpart ⇒ //=.
        }
      }
      by intros; apply H_ineq_ξ_partitioned.
    Qed.

  End Step1.

Step 2

Now, we know that if we have the inequality with partitions on arrival sequences H_ineq_ξ_partitioned, then we are done. But how do we prove such an inequality? In the next step, we prove the required inequality by introducing a new hypothesis from which it can be established. We then continue in this manner until reaching a hypothesis that is easy enough to prove without introducing new hypotheses.

In the second step, we replace the partition over all arrival sequences with an event encoding one arrival sequence.

Section Step2.

First, let us state the premise of our hypothesis H_ineq_ξ_partitioned.

Again, consider a partition ξpart of the sample space of system S into events corresponding to different arrival sequences...

Let ξpart := partition_on_ξ μ.

... and ξpart to system S' and denote it as ξpart'.

Let ξpart' := extend_partition S ξpart j_rep.

Consider a pair of arbitrary pickle-equivalent elements ξi and ξi'.

Variables (ξi : I ξpart) (ξi' : I ξpart').
Hypothesis ξ_equivalence : pickle_bij ξi ξi'.

As already discussed, pickle-equivalence is quite strong and we can show that both indices ξi and ξi' correspond to the same arrival sequence ξ. Because of the way partitions on arrival sequences are constructed, we can extract an arrival sequence by unpacking a partition.

Variable ξ : arrival_sequence Job.
Hypothesis H_part_unpack_ξ : match ξi with exist ξ IN ⇒ ξ end = ξ.

Instead of clunky indices ξi : I ξpart and ξi' : I ξpart', we will use "plain" predicates ξf and ξf' that correspond to a fixed arrival sequence ξ in S and S', respectively.

Let ξf := (λ ω , arr_seq ω == ξ ) : pred (Ω_of S).
Let ξf' := (λ ω , arr_seq (proj1 S j_rep ω) == ξ ) : pred (Ω_of S').

During this step, we replace indices with predicates.

    Hypothesis H_ineq_ξ_fixed :
      ℙ <μ_of S >{[ ξf ]} > 0 → ℙ <μ_of S >{[ Exc ∩ ξf ]} ≤ ℙ <μ_of S'>{[ Exc' ∩ ξf' ]}.

    Lemma transformation_is_pRT_monotone_step2 :
      ℙ <μ_of S >{[ Exc ∩ ξpart ◁{ξi } ]} ≤ ℙ <μ_of S'>{[ Exc' ∩ ξpart'◁{ξi'} ]}.
    Proof.
      destruct pWCET_pmf as [pWCET nonneg sum1].
      have EQ : ξi = ξi'.
      { by destruct ξ_equivalence as [u [EQ4 EQ5]]; rewrite EQ4 in EQ5; inversion EQ5; subst ξi'. }
      subst ξi'; clear ξ_equivalence.
      have A : (∀ ω, ¬ ξpart ◁{ξi } ω ∨ μ_of S ω = 0)
               ∨ (∃ ω , ξpart ◁{ξi } ω ∧ μ_of S ω > 0).
      { destruct (ClassicalEpsilon.excluded_middle_informative
                    (∃ ω , p ξpart ξi ω ∧ μ_of S ω > 0)).
        - by right.
        - left; move: n ⇒ /forallNP ALL.
          intros ω; specialize (ALL ω); move: ALL ⇒ /not_andP [L|R]; first by left.
          right; destruct μ; apply Rnot_gt_le in R; move: (pmf_pos ω) R.
          by rewrite //=; nra.
      }
      destruct A as [ZERO | POS].
      { replace (pr _ _) with 0; first by apply Rge_le, ge_pr_0.
        symmetry; apply SeriesC_0 ⇒ ω.
        specialize (ZERO ω); destruct ZERO as [NP | Z].
        - by rewrite /intersection /pred.pred_intersection;
          move: NP ⇒ /negP NP; apply negbTE in NP; rewrite NP andb_false_r.
        - by unfold intersection, pred.pred_intersection ⇒ //=; destruct (_ && _ ).
      }
      destruct POS as [ω [INωξ POSμω]], ξi as [ξp IN]; subst ξp.
      erewrite pr_eq_pred with (Q := Exc ∩ ξf);
        first erewrite pr_eq_pred with (Q := Exc' ∩ ξf');
        first apply H_ineq_ξ_fixed.
      - by eapply pr_pos; eauto.
      - by intros [ω1 ω2] ⇒ //=.
      - by intros c ⇒ //=.
    Qed.

  End Step2.

Step 3

Now, we can forget about ξpart and ξpart' and use ξ, ξf, and ξf' instead. Notice that here we use ξ to denote the deterministic arrival sequence. Predicates ξf and ξf' denote events that result in ξ in systems S and S', respectively.

  Variable ξ : arrival_sequence Job.
  Let ξf := (λ ω , arr_seq ω == ξ ) : pred (Ω_of S).
  Let ξf' := (λ ω , arr_seq (proj1 S j_rep ω) == ξ ) : pred (Ω_of S').

Without loss of generality, we can assume that ξ appears with positive probability (otherwise the LHS of the inequality from Step 2 is equal to 0).

Hypothesis H_ξ_pos_prob : ℙ <μ >{[ ξf ]} > 0.

In this step, we introduce a partition (that guarantees partition-independence and partition-dominance) of the probability space by exploiting H_axiomatic_pWCET, the assumption of axiomatic pWCET.

Section Step3.

Consider some countable type I and define a family of predicates part : I → pred Ω. Consider an index Pi : i and assume that part Pi has positive probability. Note that part might depend on ξf.

Next, let us assume the following: we have an event Sf := part Pi in system S such that the event ensures (1) the validity of the pWCET bound and (2) the partition-independence of job j_rep.

Let us define Sf's twin Sf' ω := Sf (proj1 ω) in S' (recall that proj1 simply returns the first component of a tuple).

With this, let us assume that the inequality that now includes Sf and Sf' holds:

ℙ<μ_of S>{[ (Exc1 ∩ ξf) ∩ Sf ]} ≤ ℙ<μ_of S'>{[ (Exc2 ∩ ξf') ∩ Sf' ]} .

    Hypothesis H_ineq_Ω_part :
      ∀ (I : countType) (part : I → pred Ω) (Pi : I) (ρ : PosProb μ (ξf ∩ part Pi)),
        let Sf := part Pi : pred (Ω_of S) in
        let Sf' := (λ ω , Sf (proj1 S j_rep ω)) : pred (Ω_of S') in

        (∀ (x : nat ),
            𝔽<μ >{[ odflt0 (𝓒 j_rep) | ξf ∩ Sf ]}(x ) ≥ pWCET_cdf (job_task j_rep) x ) →

        (∀ (𝗖 : Job → option work) (jobs : seq Job ),
            j_rep \notin jobs →
            ℙ <μ >{[ 𝓒 _fix 𝗖 [:: j_rep] ∩ 𝓒 _fix 𝗖 jobs | ξf ∩ Sf ]}
            = ℙ <μ >{[ 𝓒 _fix 𝗖 [:: j_rep] | ξf ∩ Sf ]} × ℙ <μ >{[ 𝓒 _fix 𝗖 jobs | ξf ∩ Sf ]}) →

        ℙ <μ_of S >{[ (Exc ∩ ξf ) ∩ Sf ]} ≤ ℙ <μ_of S'>{[ (Exc' ∩ ξf') ∩ Sf' ]}.

Then, we can prove the inequality that we assumed in the previous step (Step2). Notice that in order to apply the conclusion of H_ineq_Ω_part, we need to provide all the premises of the hypothesis. In particular, we have to present a countable type with a family of predicates where every event ensures partition-independence and partition-dominance.

This is possible only because we assumed that the given pWCET satisfies our axiomatic pWCET definition. Again, essentially, we prove that we can reduce the lemma to the hypothesis using the properties ensured by axiomatic pWCET.

    Lemma transformation_is_pRT_monotone_step3 :
      ℙ <μ_of S >{[ Exc ∩ ξf ]} ≤ ℙ <μ_of S'>{[ Exc' ∩ ξf' ]}.
    Proof.
      edestruct (@H_axiomatic_pWCET j_rep ξ) as [P [CONDB INDP]].
      set(P' := extend_partition S P j_rep).
      rewrite (law_of_total_probability_prod _ _ P).
      rewrite (law_of_total_probability_prod _ _ P').
      eapply leq_SeriesC.
      { eapply ex_seriesC_le; last by eapply ex_series_pr_eq_over_partition.
        intros ?; split.
        - by apply Rge_le, ge_pr_0.
        - by apply pr_leq_intersectionr.
      }
      { eapply ex_seriesC_le; last by eapply ex_series_pr_eq_over_partition.
        intros ?; split.
        - by apply Rge_le, ge_pr_0.
        - by apply pr_leq_intersectionr.
      }
      { intros; split; intros PICK; unfold is_some in ×.
        - destruct (pickle_inv i) eqn:EQ; last by done.
          by destruct P; rewrite EQ.
        - destruct (pickle_inv i) eqn:EQ; last by done.
          by destruct P; rewrite EQ.
      }
      intros P__i P__i' P__EQU.
      destruct P as [I pa COV DIS], P__EQU as [idx [EQ1 EQ2]].
      rewrite EQ1 in EQ2; inversion EQ2; subst P__i'.
      have ALT: ℙ <μ >{[ ξf ∩ pa P__i ]} = 0 ∨ PosProb μ (ξf ∩ pa P__i).
      { by apply pr_pos_or_zero. }
      destruct ALT as [ZERO|POS].
      { eapply Rle_trans.
        eapply pr_mono_pred with (Q := ξf ∩ pa P__i).
        { by intros i; rewrite pred_cap_assoc; apply pred_cap_and. }
        { by rewrite ZERO; apply Rge_le, ge_pr_0. }
      }
      unfold proj1 in *; destruct pWCET_pmf as [pWCET nonneg sum1].
      by erewrite pr_eq_pred with (Q := (Exc' ∩ ξf') ∩ (λ ω , pa P__i (proj1 S j_rep ω)));
        first eapply H_ineq_Ω_part; [apply INDP | eauto | intros [ω1 ω2] ⇒ //=].
    Qed.

  End Step3.

Step 4

As before, now we need to prove the inequality we assumed in the previous step. For this, let us introduce all premises of the assumed inequality as variables and hypotheses.

  Variable (Idx : countType) (part : Idx → pred Ω) (Pi : Idx).

  Let Sf := part Pi : pred (Ω_of S).
  Let Sf' := (λ ω , Sf (proj1 S j_rep ω)) : pred (Ω_of S').

  Variable ρ1 : PosProb (μ_of S) (ξf ∩ Sf).
  Variable ρ2 : PosProb (μ_of S') (ξf' ∩ Sf').

  Hypothesis H_pWCET_bounds_cond_cdf :
    ∀ (x : nat ), 𝔽<μ >{[ odflt0 (𝓒 j_rep) | ξf ∩ Sf ]}(x ) ≥ pWCET_cdf (job_task j_rep) x.

  Hypothesis H_cond_independence :
    ∀ (𝗖 : Job → option work) (jobs : seq Job ),
      j_rep \notin jobs →
      ℙ <μ >{[ 𝓒 _fix 𝗖 [:: j_rep] ∩ 𝓒 _fix 𝗖 jobs | ξf ∩ Sf ]}
      = ℙ <μ >{[ 𝓒 _fix 𝗖 [:: j_rep] | ξf ∩ Sf ]} × ℙ <μ >{[ 𝓒 _fix 𝗖 jobs | ξf ∩ Sf ]}.

In this step, we transform our inequality by moving ξf ∩ Sf and ξf' ∩ Sf' to the conditional part.

Section Step4.

First, note that both ξf ∩ Sf and ξf' ∩ Sf' have the same probability. This is due to the fact that our transformation does not change the probabilities of arrival sequences or partitions.

    Remark ξf_and_Sf_eq_prob :
      ℙ <μ_of S >{[ ξf ∩ Sf ]} = ℙ <μ_of S'>{[ ξf' ∩ Sf' ]}.
    Proof.
      unfold proj1 in *; destruct pWCET_pmf as [pWCET nonneg sum1].
      have PM1 := pair_marginal1 μ μ_tsk (λ ω0 : Ω , ξf ω0 && Sf ω0).
      erewrite pr_eq_pred with (Q := (λ (ω : Ω × nat ), (fun ω1 ⇒ ξf ω1 && Sf ω1) ω .1));
        last by intros []; rewrite !unfold_in //=.
      by rewrite PM1; apply pr_eq_pred ⇒ ω.
    Qed.

As before, we show that one can reduce the inequality stated in the lemma to the statement stated in the hypothesis. In other words, we can indeed condition on ξf ∩ Sf and ξf' ∩ Sf'. Then, both of them cancel out, since the probability is equal.

    Hypothesis H_ineq_conditional :
      ℙ <μ_of S >{[ Exc | ξf ∩ Sf ]} ≤ ℙ <μ_of S'>{[ Exc' | ξf' ∩ Sf' ]}.

    Lemma transformation_is_pRT_monotone_step4 :
      ℙ <μ_of S >{[ Exc ∩ ξf ∩ Sf ]} ≤ ℙ <μ_of S'>{[ Exc' ∩ ξf' ∩ Sf' ]}.
    Proof.
      erewrite →pr_eq_pred with (Q := (Exc ∩ (ξf ∩ Sf )));
        last by intros ω'; rewrite !unfold_in //=; symmetry; apply andb_assoc.
      erewrite →pr_eq_pred with (Q := (Exc' ∩ (ξf' ∩ (Sf'))));
        last by intros ω'; rewrite !unfold_in //=; symmetry; apply andb_assoc.
      rewrite [ℙ < μ_of S >{[ _ ]}]pr_cond_axiomatic' [ℙ < μ_of S'>{[ _ ]}]pr_cond_axiomatic'.
      apply Rmult_le_compat.
      { by apply Rge_le, ge_pr_0. }
      { by apply Rge_le, ge_pr_0. }
      { by rewrite ξf_and_Sf_eq_prob; clear; nra. }
      { by apply H_ineq_conditional. }
    Qed.

  End Step4.

Step 5

For simplicity, let us introduce a few local names for functions extracting cost vectors. For example, given ω \in Ω_of S, sample_costs returns a vector of all costs fixed for this specific evolution ω.

Let sample_costs (ω : Ω_of S) := job.sample_costs ω (job_cost := 𝓒 _of S).
Let sample_costs' (ω : Ω_of S') := job.sample_costs ω (job_cost := 𝓒 _of S').

For simplicity, let 𝓡 denote a function that computes the response time of any job for given fixed vectors 𝗔 and 𝗖.

Let 𝓡 := scheduler 𝗔𝗖 _to_rt 𝗔𝗖 horizon ζ.

In this step, we replace events Exc and Exc' with events λ ω ⇒ exceeds (𝓡 𝗔 (sample_costs ω) j) r, where the arrival times are fixed to be a specific vector of arrival times. Note that previously we had a general random variable describing the response-time distribution, but now we have algorithm 𝓡 instead.

Section Step5.

Note that here we assume that we are given any vector 𝗔 describing job arrivals without restriction that it must agree with ξ. Inside of the proof, we indeed construct 𝗔 as a transformation of ξ; however, for further proofs, it is not relevant, so we just forget this information and use a generic function Job → option instant.

    Hypothesis H_ineq_algorithmic_𝓡 :
      ∀ (𝗔 : Job → option instant),
        ℙ <μ_of S >{[ λ ω , exceeds (𝓡 𝗔 (sample_costs ω) j) r | ξf ∩ Sf ]}
        ≤ ℙ <μ_of S'>{[ λ ω , exceeds (𝓡 𝗔 (sample_costs' ω) j) r | ξf' ∩ Sf' ]}.

The inequality involving Exc and Exc' is implied by the inequality involving 𝓡.

    Lemma transformation_is_pRT_monotone_step5 :
      ℙ <μ_of S >{[ Exc | ξf ∩ Sf ]} ≤ ℙ <μ_of S'>{[ Exc' | ξf' ∩ Sf' ]}.
    Proof.
      set (μ__r := restrict (μ_of S) (ξf ∩ Sf)) in ×.
      set (μ__r' := restrict (μ_of S') (ξf' ∩ Sf')) in ×.
      rewrite /pr_cond -/μ__r -/μ__r'.
      rewrite →pr_eq_pred with
        (Q := fun (ω : Ω_of S) ⇒
                exceeds (𝓡 (sample_arrivals ω) (sample_costs ω) j) r);
        last by intros ω; rewrite !unfold_in; f_equal; apply valid_𝓡.
      rewrite →pr_eq_pred with
        (Q := fun (ω : Ω_of S') ⇒
                exceeds (𝓡 (sample_arrivals (job_arrival := 𝓐 _of S') ω) (sample_costs' ω) j) r);
        last by intros ω; rewrite !unfold_in; f_equal; apply valid_𝓡.
      unfold ξf, ξf' in ×.
      have EX :
        ∃ (𝗔 : Job → option instant ),
          (∀ ω : Ω_of S, μ__r ω > 0 → sample_arrivals (job_arrival := 𝓐 _of S) ω = 𝗔 )
          ∧ (∀ ω : Ω_of S', μ__r' ω > 0 → sample_arrivals (job_arrival := 𝓐 _of S') ω = 𝗔 ).
      { have EX: ∃ ω : Ω , arr_seq ω == ξ.
        { apply pr_pos_inv in H_ξ_pos_prob.
          by destruct H_ξ_pos_prob as [ω [EQ POS]]; ∃ ω. }
        destruct EX as [ω INωξ].
        ∃ (fun j ⇒ 𝓐 _of S j ω); split.
        { intros ω' POS.
          apply functional_extensionality_dep ⇒ jt.
          rewrite //= /pmf_restricted /intersection/pred.pred_intersection /ξ_fix //= in POS.
          destruct (_ == _) eqn:EQ in POS; last by rewrite //= in POS; nra.
          by apply eq_arr_seq_impl_eq_job_arrival ⇒ t'; move : EQ INωξ ⇒ /eqP → /eqP →.
        }
        { intros ω' POS.
          apply functional_extensionality_dep ⇒ jt.
          rewrite /sample_arrivals //= /pmf_restricted /intersection/pred.pred_intersection //= in POS.
          unfold proj1 in *; destruct pWCET_pmf as [pWCET nonneg sum1].
          destruct ω' as [ω' n]; simpl in ×.
          destruct (_ == _) eqn:EQ in POS; last by rewrite //= in POS; nra.
          by unfold sample_arrivals; simpl; eapply eq_arr_seq_impl_eq_job_arrival ⇒ t'; move : EQ INωξ ⇒ /eqP → /eqP →.
        }
      }
      edestruct EX as [𝗔 [EQA EQA']].
      rewrite →pr_eq_pred_pos with (Q := fun (ω : Ω_of S) ⇒ exceeds (𝓡 𝗔 (sample_costs ω) j) r);
        last by intros ω' POS; do 2 f_equal; apply EQA.
      rewrite →pr_eq_pred_pos with (Q := fun (ω : Ω_of S') ⇒ exceeds (𝓡 𝗔 (sample_costs' ω) j) r);
        last by intros ω' POS; do 2 f_equal; apply EQA'.
      clear EQA EQA' EX.
      by unfold μ__r, μ__r'; rewrite !fold_prob_to_cond_prob.
    Qed.

  End Step5.

Step 6

Assume that we are given a list of job arrivals.

Variable (𝗔 : Job → option instant).

For technical reasons, we need to distinguish between jobs costs operating in a probabilistic space with a measure μ_of S (μ_of S') and the ones operating with the restricted measure restrict (μ_of S) (ξf ∩ Sf) (and restrict (μ_of S') (ξf' ∩ Sf')).

Recall that a partition of the probability space must take measures into account (to satisfy certain assumptions). Since we restrict Ω_of S to a subset that satisfies predicate ξf ∩ Sf (and a subset of Ω_of S' that satisfies predicate ξf' ∩ Sf'), we have to adapt some of the notions to these new measures.

Let μr := restrict (μ_of S) (ξf ∩ Sf) : measure (Ω_of S).
Let μr' := restrict (μ_of S') (ξf' ∩ Sf') : measure (Ω_of S').

Next, we define random variables, which are the same as those introduced earlier, except for the measure (μr instead of μ and μr' instead of μ'.

Let 𝓒 r j := mkRvar μr (𝓒 _of S j).
Let 𝓒 r' j := mkRvar μr' (𝓒 _of S' j).

Similarly, we need to provide a new notion of projection that accounts for the restricted measure.

  Definition proj ω :
    ∀ (ω : Ω_of S'), (ξf' ∩ Sf') ω → (ξf ∩ Sf ) (proj1 S j_rep ω).
  Proof.
    by rewrite /replace_job_pET /proj1 /intersection/pred.pred_intersection //= ⇒
      [[ω c] /andP [Fξ FS]].
  Defined.

Now, we want to fix the job costs of all jobs except j_rep (recall that j_rep is the job for which we want to replace pET with pWCET). For this, again, we introduce partitioning of Ω into subsets, each containing a unique job cost assignment (and the job cost of j_rep is left unspecified).

Let CSpart := partition_on_𝓒 s (job_cost := 𝓒 r) μr (rem j_rep (enum Job)).
Let CSpart' := extend_partition' S j_rep (ξf ∩ Sf) CSpart (ξf' ∩ Sf') proj ω.

In the next step, we introduce CSpart◁{Cs} and CSpart'◁{Cs'} into the inequality. They ensure that the costs of all jobs (except j_rep) are fixed.

Section Step6.

Assume that the inequality holds when conditioned on job-cost partitions (excluding j_rep), ...

    Hypothesis H_ineq_costs_partitioned :
      ∀ (Cs : I CSpart) (Cs' : I CSpart') (CsEQU : pickle_bij Cs Cs'),
        ℙ <μ_of S >{[
            (λ ω , exceeds (𝓡 𝗔 (sample_costs ω) j) r )
              ∩ CSpart ◁{Cs } | ξf ∩ Sf ]}
        ≤ ℙ <μ_of S'>{[
            (λ ω , exceeds (𝓡 𝗔 (sample_costs' ω) j) r )
              ∩ CSpart'◁{Cs'} | ξf' ∩ Sf' ]}.

... then we can derive the inequality also without conditioning on costs.

    Lemma transformation_is_pRT_monotone_step6 :
      ℙ <μ_of S >{[ λ ω , exceeds (𝓡 𝗔 (sample_costs ω) j) r | ξf ∩ Sf ]}
      ≤ ℙ <μ_of S'>{[ λ ω , exceeds (𝓡 𝗔 (sample_costs' ω) j) r | ξf' ∩ Sf' ]}.
    Proof.
      rewrite /pr_cond -/μr -/μr'.
      erewrite law_of_total_probability_prod with (S0 := CSpart).
      erewrite law_of_total_probability_prod with (S0 := CSpart').
      eapply leq_SeriesC.
      { eapply ex_seriesC_le; last by eapply ex_series_pr_eq_over_partition.
        intros ?; split.
        - by apply Rge_le, ge_pr_0.
        - by apply pr_leq_intersectionr.
      }
      { eapply ex_seriesC_le; last by eapply ex_series_pr_eq_over_partition.
        intros ?; split.
        - by apply Rge_le, ge_pr_0.
        - by apply pr_leq_intersectionr.
      }
      { intros; split; intros PICK; unfold is_some in ×.
        - by destruct (pickle_inv i) eqn:EQ.
        - by destruct (pickle_inv i) eqn:EQ.
      }
      intros Cs Cs' CsEQU.
      rewrite /μr /μr' !fold_prob_to_cond_prob.
      by apply H_ineq_costs_partitioned.
    Qed.

  End Step6.

Step 7

As before, we now proceed to derive the premise of the prior step.

To this end, consider two equivalent events corresponding to the same setting of job costs in the two systems.

Variable (Cs : I CSpart) (Cs' : I CSpart') (CsEQU : pickle_bij Cs Cs').

Consider two partitions of Ω_of S and Ω_of S' into cost of all jobs except j_rep.

Let Cpart := partition_on_𝓒 μr (job_cost := 𝓒 r) j_rep.
Let Cpart' := partition_on_𝓒 μr' (job_cost := 𝓒 r') j_rep.

Similarly to how we replaced job arrivals with 𝗔, we can do a similar trick to replace job costs with a vector 𝗖. However, what do we do with the cost of the unspecified job j_rep? First, we can perform another round of partitioning and apply the law of total Probability (LTP) on the remaining job cost (note that we get a new sum ∑[∞]_{c<-option work} ... in the inequality). Second, we can update 𝗖 with the specified value of j_rep 𝓡 𝗔 (update 𝗖 j_rep c) j. For now, we replace only the LHS.

Section Step7.

Note that on the LHS of the below hypothesis, we now have the following term: ∑[∞]_{c<-option work} ℙ<μ_of S>{[ exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r && (CSpart◁{Cs} & Cpart◁{c})| ξf ∩ Sf ]}.

An important result of this transformation is that now exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r is a boolean value (true/false) and event CSpart◁{Cs} & Cpart◁{c} defines a subset of Ω_of S such that all job costs are fixed.

To extract a vector of job costs from the partition CSpart◁{Cs}, we find one ω ∈ CSpart◁{Cs} and compute the vector of costs for this ω. The resulting vector of costs will agree with the jobs in the system, given CSpart◁{Cs} is true.

Note that we use the construction update 𝗖 j_rep c to update the cost of job j_rep in vector 𝗖 with a new value c. This is a way to define the notion of "reassembling" two job-cost-fixing vectors used in the paper.

    Hypothesis H_ineq_cost_partitioned :
      ∀ (ω o : Ω_of S),
        CSpart ◁{Cs } ω o →
        let 𝗖 := (fun j ⇒ 𝓒 _of S j ω o) in

        ∑[∞]_{c <-option work }
         ℙ <μ_of S >{[ λ ω ,
              [&& exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ,
                CSpart ◁{Cs } ω &
                  Cpart ◁{c } ω ]
                   | ξf ∩ Sf ]}
        ≤ ℙ <μ_of S'>{[
              (λ ω , exceeds (𝓡 𝗔 (sample_costs' ω) j) r )
                ∩ CSpart'◁{Cs'}
            | ξf' ∩ Sf' ]}.

As before, we show that the prior step's premise follows from the hypothesis introduced here; that is, how the premise of Step 6 follows from the premise of Step 7.

    Lemma transformation_is_pRT_monotone_step7 :
      ℙ <μ_of S >{[ (λ ω , exceeds (𝓡 𝗔 (sample_costs ω) j) r ) ∩ CSpart ◁{Cs } | ξf ∩ Sf ]}
      ≤ ℙ <μ_of S'>{[ (λ ω , exceeds (𝓡 𝗔 (sample_costs' ω) j) r ) ∩ CSpart'◁{Cs'} | ξf' ∩ Sf' ]}.
    Proof.
      rewrite /pr_cond -/S' -/μr -/μr'; erewrite law_of_total_probability_prod with (S0 := Cpart).
      have A : (∀ ω, (¬ p CSpart Cs ω ) ∨ μ_of S ω = 0)
               ∨ (∃ ω , p CSpart Cs ω ∧ μ_of S ω > 0).
      { destruct (ClassicalEpsilon.excluded_middle_informative
                    (∃ ω , p CSpart Cs ω ∧ μ_of S ω > 0)); first by right.
        left; move: n ⇒ /forallNP ALL.
        intros ω'; specialize (ALL ω'); move: ALL ⇒ /not_andP [L|R]; first by left.
        right; move: R ⇒ //=.
        by clear; destruct μ; move: (pmf_pos ω') ⇒ //=; nra.
      }
      destruct A as [ZERO | [ω1 [INω1ξ POSμω1]]].
      { replace (_) with 0; first by apply Rge_le, ge_pr_0.
        symmetry; apply SeriesC_0 ⇒ i; apply SeriesC_0 ⇒ ω'.
        specialize (ZERO ω'); destruct ZERO as [NP | Z].
        - by rewrite /intersection/pred.pred_intersection;
          move: NP ⇒ /negP NP; apply negbTE in NP; rewrite NP andb_false_r.
        - rewrite /μr /restrict/ pmf_restricted //= !Z.
          rewrite /Rdiv /intersection/pred.pred_intersection Rmult_0_l.
          by destruct ( _ && _ ); first destruct ( _ && _ ).
      }
      set (𝗖 := fun j ⇒ 𝓒 _of S j ω1).
      have ->:
           ∑[∞]_{i <-I Cpart }
           ℙ <μr >{[ ((λ ω , exceeds (𝓡 𝗔 (sample_costs ω) j) r ) ∩ (p CSpart Cs )) ∩ (p Cpart i )]}
           = ∑[∞]_{c <- I Cpart }
              ℙ < μr >{[ λ ω , [&& exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ,
                   (p CSpart Cs ω ) & ((p Cpart c ω ))] ]}.
      { eapply SeriesC_ext ⇒ c.
        apply pr_eq_pred_pos ⇒ ω' POS.
        rewrite /in_mem /intersection/pred.pred_intersection -andb_assoc.
        apply andb_id2r ⇒ /andP [PCs /eqP PC].
        replace _ with (exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r); first by reflexivity.
        do 3 f_equal.
        apply functional_extensionality_dep ⇒ s.
        rewrite /sample_costs /update.
        destruct (s == j_rep) eqn:EQ.
        { by move : EQ ⇒ /eqP EQ; subst s; move: PC; rewrite /𝓒 _of //= ⇒ →. }
        move: POS; rewrite /restrict //=/ intersection /pred.pred_intersection /pmf_restricted.
        destruct (Sf) eqn:PPP; last first.
        { by rewrite andb_false_r; nra. }
        { move ⇒ _; move: PCs ⇒ /forallP PCs.
          have NEQ : s != j_rep.
          { by apply/eqP ⇒ EQsj; subst s; rewrite eq_refl in EQ. }
          specialize (PCs (to_fintype s j_rep NEQ)).
          move: INω1ξ ⇒ /forallP INω1ξ.
          specialize (INω1ξ (to_fintype s j_rep NEQ)).
          move : INω1ξ ⇒ /eqP ⇒ // EQf.
          by rewrite /𝗖 -EQf; apply/eqP.
        }
      }
      by apply H_ineq_cost_partitioned.
    Qed.

  End Step7.

Step 8

We can prove that there is at least one ωo that satisfies the current partition CSpart◁{Cs} ωo. We can use ωo to compute 𝗖. Such a cost assignment agrees with CSpart◁{Cs} because ωo satisfies the initial predicate.

  Variable ω o : Ω_of S.
  Hypothesis H_ω o_in_Cs : CSpart ◁{Cs } ω o.
  Let 𝗖 := (fun j ⇒ 𝓒 _of S j ω o ) : Job → option work.

Similarly to Step 7, which focused on the LHS, we now replace the RHS.

Section Step8.

Notice that both sides now have all costs fully fixed.

    Hypothesis H_ineq_cost_partitioned :
      ∑[∞]_{c <-option work }
       ℙ <μ_of S >{[ λ ω ,
            [&& exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ,
                CSpart ◁{Cs } ω &
                Cpart ◁{c } ω ] | ξf ∩ Sf ]}
      ≤ ∑[∞]_{c <-option work }
         ℙ <μ_of S'>{[ λ ω ,
            [&& exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ,
                CSpart'◁{Cs'} ω &
                Cpart'◁{c } ω ] | ξf' ∩ Sf' ]}.

From the above hypothesis, we can obtain the premise of Step 7.

    Lemma transformation_is_pRT_monotone_step8 :
      ∑[∞]_{c <-option work }
       ℙ <μ_of S >{[ λ ω ,
            [&& exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ,
                CSpart ◁{Cs } ω &
                Cpart ◁{c } ω ] | ξf ∩ Sf ]}
      ≤ ℙ <μ_of S'>{[
            (λ ω , exceeds (𝓡 𝗔 (sample_costs' ω) j) r )
              ∩ CSpart'◁{Cs'} | ξf' ∩ Sf' ]}.
    Proof.
      rewrite /pr_cond; erewrite law_of_total_probability_prod with (S0 := Cpart').
      have → :
        ∑[∞]_{i <-I Cpart'}
         ℙ < μr' >{[ (λ ω , exceeds (𝓡 𝗔 (sample_costs' ω) j) r ) ∩ (p CSpart' Cs') ∩ (p Cpart' i ) ]}
        = (∑[∞]_{c <- [countType of option nat] }
            ℙ < μr' >{[ λ ω',
                [&& exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ,
                  CSpart'◁{Cs'} ω'
                  & (Cpart'◁{c } ω')] ]} ).
      { unfold proj ω, proj1, proj2 in *; destruct pWCET_pmf as [pWCET nonneg sum1].
        apply SeriesC_ext ⇒ c; rewrite /sample_costs' //= eq_refl.
        apply pr_eq_pred_pos ⇒ ω' POS.
        rewrite /intersection /pred.pred_intersection -!andb_assoc.
        destruct ω' as [ω' n].
        apply andb_id2r ⇒ INF.
        replace _ with (exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r); first by reflexivity.
        do 2 f_equal.
        apply functional_extensionality_dep ⇒ s.
        rewrite /update /sample_costs /job.sample_costs eq_sym.
        destruct (j_rep == s) eqn:EQ.
        { by move: INF EQ ⇒ /andP [INF /eqP EQ2] /eqP EQ; subst s. }
        move: INF ⇒ /andP [PP _].
        f_equal.
        move: POS; rewrite /restrict //=.
        rewrite /intersection /pred.pred_intersection/pmf_restricted.
        simpl.
        destruct (let '(ω0, _) := (ω', n) in Sf ω0) eqn:PPP; last first.
        { by rewrite /Sf' !PPP //= andb_false_r; nra. }
        { move ⇒ _; move: PP ⇒ /forallP PP.
          have NEQ : s != j_rep.
          { by apply/eqP ⇒ EQsj; subst s; rewrite eq_refl in EQ. }
          specialize (PP (to_fintype s j_rep NEQ)).
          move: H_ω o_in_Cs ⇒ /forallP H_ωo_in_Cs'.
          specialize (H_ωo_in_Cs' (to_fintype s j_rep NEQ)).
          rewrite /𝗖; move : H_ωo_in_Cs' ⇒ /eqP ⇒ //= <-.
          by destruct CsEQU as [i [EQ1 EQ2]];
          rewrite EQ1 in EQ2; inversion EQ2; subst Cs'; apply/eqP.
        }
      }
      by apply H_ineq_cost_partitioned.
    Qed.

  End Step8.

Step 9

Let us define a random variable following the pWCET distribution. This random variable describes j_rep's cost after its pET has been replaced. For more details, see the file rt/analysis/pETs_to_pWCETs and specifically the transformation replace_job_pET. Recall that μ_tsk is the measure induced by the given pWCET distribution.

Let 𝓒 _pWCET := mkRvar μ_tsk Some.

Finally, we can use the independence property H_cond_independence to factorize the LHS. At the same time, we can factorize the RHS just by construction.

Section Step9.

On the technical side, this is a pretty involved proof. However, intuitively we simply apply the partition-independence property of Sf. Note that the probability of CSpart◁{Cs} ω && 𝓒 j_rep ω == c factors into two probabilities: CSpart◁{Cs} and 𝓒 j_rep == c.

    Remark LHS_factorization :
      ∑[∞]_{c <-option nat }
       I [ exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ]
        × ℙ <μ_of S >{[ λ ω , (CSpart ◁{Cs } ω ) && (𝓒 j_rep ω == c ) | ξf ∩ Sf ]}
      = ∑[∞]_{c <-option nat }
         I [ exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ]
          × (ℙ <μ_of S >{[CSpart ◁{Cs } | ξf ∩ Sf ]} × ℙ <μ_of S >{[ 𝓒 j_rep ⟨=⟩ c | ξf ∩ Sf ]}).
    Proof.
      rewrite /pr_cond.
      apply SeriesC_ext ⇒ c.
      have BL : ∀ a b c d, b = c → a = d → a × b = c × d.
      { by clear; intros; nra. }
      have L :
        ℙ <μr >{[ λ ω : Ω , [∀ j0, Cs j0 == 𝓒 (ssval j0) ω] && (𝓒 j_rep ω == c)]}
        = ℙ <μr >{[ λ ω : Ω , [∀ j0, Cs j0 == 𝓒 (ssval j0) ω] ]} × ℙ <μr >{[ λ ω : Ω , (𝓒 j_rep ω == c)]}.
      { set (𝗖2 := fun s ⇒ if j_rep == s then c else (𝓒 s ω o )).
        specialize (H_cond_independence 𝗖2 (rem j_rep (enum Job))).
        feed H_cond_independence.
        { by rewrite mem_rem_uniqF ⇒ //=; apply enum_uniq. }
        rewrite !fold_prob_to_cond_prob cond_prob_posprob_irrelevance.
        erewrite pr_cond_eq_pred with
          (Q := λ ω0 : Ω , [∀ j0, Cs j0 == 𝓒 (ssval j0) ω0] && (𝓒 j_rep ω0 == c))
          in H_cond_independence.
        { rewrite H_cond_independence; apply: BL.
          { apply pr_cond_eq_pred ⇒ ω' EQ.
            rewrite /𝓒 _fix /𝗖2 /job.sample_costs.
            split; [move ⇒ /allP EQf | ].
            { apply/forallP ⇒ [[s IN]].
              move: H_ω o_in_Cs ⇒ /forallP ALL.
              move: (ALL {| ssval := s; ssvalP := IN |}) ⇒ /eqP →.
              move: (EQf s IN) ⇒ /eqP EQn; inversion EQn ⇒ //=.
              rewrite H0; destruct (j_rep == s) eqn:EQ6; last by done.
              move: EQ6 ⇒ /eqP EQ6; subst s.
              by rewrite mem_rem_uniqF in IN; last apply enum_uniq.
            }
            { move ⇒ /forallP ALL1; apply/allP ⇒ s IN2.
              apply/eqP; f_equal.
              move: H_ω o_in_Cs ⇒ /forallP ALL.
              destruct (j_rep == s) eqn:EQ6.
              { move: EQ6 ⇒ /eqP EQ6; subst s.
                rewrite mem_rem_uniqF in IN2; first by done.
                by apply enum_uniq.
              }
              by move: (ALL {| ssval := s; ssvalP := IN2 |})
                         (ALL1{| ssval := s; ssvalP := IN2 |}) ⇒ /eqP <- /eqP <-.
            }
          }
          { apply pr_cond_eq_pred ⇒ ω' EQ.
            rewrite /𝓒 _fix /𝗖2 /job.sample_costs.
            split; [move ⇒ /allP EQf | ].
            { specialize (EQf j_rep).
              feed EQf; first by rewrite mem_seq1.
              move: EQf ⇒ /eqP EQf; inversion EQf.
              by rewrite eq_refl in H0; apply/eqP.
            }
            { move ⇒ /eqP EQ3.
              apply/andP; split; last by done.
              by rewrite eq_refl EQ3.
            }
          }
        }
        { intros ω' EQ.
          rewrite /𝓒 _fix /𝗖2 /intersection /pred.pred_intersection/sample_costs //= eq_refl.
          split.
          { move ⇒ /andP [/andP [/eqP A _] /allP B].
            inversion_clear A; apply/andP; split; last by done.
            apply/forallP ⇒ [[s IN2]].
            destruct (j_rep == s) eqn:EQ6.
            { move: EQ6 (IN2) ⇒ /eqP EQ6 IN3; subst s.
              by rewrite mem_rem_uniqF in IN2; last apply enum_uniq.
            }
            move: (B s IN2) ⇒ /eqP T; inversion T; clear T.
            move: H_ω o_in_Cs ⇒ /forallP ALL.
            move: (ALL {| ssval := s; ssvalP := IN2 |}) ⇒ /eqP →.
            by rewrite /job.sample_costs EQ6 in H0; rewrite H0.
          }
          { move ⇒ /andP [/forallP A /eqP EQc].
            apply/andP; split; first by rewrite /job.sample_costs EQc eq_refl.
            apply/allP ⇒ s IN2.
            destruct (j_rep == s) eqn:EQ6.
            { move: EQ6 ⇒ /eqP EQ6; subst s.
              by rewrite mem_rem_uniqF in IN2; last apply enum_uniq. }
            have NEQ : s != j_rep.
            { apply/eqP ⇒ EQsj; subst s.
              by rewrite eq_refl in EQ6. }
            move: H_ω o_in_Cs ⇒ /forallP ALL.
            move: (ALL {| ssval := s; ssvalP := IN2 |}) ⇒ /eqP <-.
            rewrite /job.sample_costs.
            move: (A {| ssval := s; ssvalP := IN2 |}) ⇒ /eqP <-.
            by apply/eqP.
          }
        }
      }
      by apply Rmult_eq_compat_l, L.
      Unshelve.
      { by eauto. }
    Qed.

Next, we show that the probability part of the RHS can be factorized into two terms: ℙ<μ>{[ CSpart◁{Cs} | ξf ∩ Sf]} and ℙ<μ_tsk>{[ fun cω ⇒ Some cω == c ]}. Note that the first factor is no longer a probability with respect to S' --- it is a probability with respect to S. For the second term, it is a probability over the probability space described in the file pETs_to_pWCETs.

    Remark RHS_factorization :
      ∑[∞]_{c <-option work }
       I [exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ]
        × ℙ <μ_of S'>{[ λ ω , CSpart'◁{Cs'} ω && (Cpart'◁{c } ω ) | ξf' ∩ Sf']}
      = ∑[∞]_{c <-option work }
         I [exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ]
          × (ℙ <μ >{[ CSpart ◁{Cs } | ξf ∩ Sf ]} × ℙ <μ_tsk >{[ 𝓒 _pWCET ⟨=⟩ c ]}).
    Proof.
      eapply SeriesC_ext ⇒ c.
      apply Rmult_eq_compat_l.
      rewrite /pr_cond !fold_prob_to_cond_prob.
      unshelve erewrite <-pr_cond_xpredT.
      unfold proj ω, proj1 in *; destruct pWCET_pmf as [pWCET nonneg sum1].
      apply pr_cond_joint_pred_eq_cond_eq.
      { intros []; destruct CsEQU as [i [EQ1 EQ2]].
        rewrite EQ1 in EQ2; inversion EQ2; subst Cs'.
        by rewrite /Cpart' /partition_on_𝓒 //= eq_refl.
      }
      { by intros []; rewrite andb_true_r. }
    Qed.

As usual, let us state a new premise.

    Hypothesis H_ineq_introduce_independence :
      ∑[∞]_{c <-option work }
       I [exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ]
        × (ℙ <μ_of S >{[ CSpart ◁{Cs } | ξf ∩ Sf ]} × ℙ <μ_of S >{[ 𝓒 j_rep ⟨=⟩ c | ξf ∩ Sf ]})
      ≤ ∑[∞]_{c <-option work }
         I [exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ]
          × (ℙ <μ_of S >{[ CSpart ◁{Cs } | ξf ∩ Sf ]} × ℙ <μ_tsk >{[ 𝓒 _pWCET ⟨=⟩ c ]}).

From the preceding factorized inequality, we can derive the premise of the previous step.

    Lemma transformation_is_pRT_monotone_step9 :
      ∑[∞]_{c <-option work }
       ℙ <μ_of S >{[ λ ω ,
            [&& exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ,
                CSpart ◁{Cs } ω &
                Cpart ◁{c } ω ] | ξf ∩ Sf ]}
      ≤ ∑[∞]_{c <-option work }
         ℙ <μ_of S'>{[ λ ω ,
            [&& exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ,
                CSpart'◁{Cs'} ω &
                (Cpart'◁{c } ω )] | ξf' ∩ Sf' ]}.
    Proof.
      erewrite SeriesC_ext; last by intros c; apply pr_bool_move.
      apply Rge_le.
      erewrite SeriesC_ext; last by intros c; apply pr_bool_move.
      apply Rle_ge.
      rewrite LHS_factorization.
      rewrite RHS_factorization.
      by eapply H_ineq_introduce_independence.
    Qed.

  End Step9.

Step 10

In this step, we remove ℙ<μ_of S>{[ CSpart◁{Cs} | ξf ∩ Sf ]} on the LHS and ℙ<μ_of S>{[ CSpart◁{Cs} | ξf ∩ Sf' ]} on the RHS.

Section Step10.

Let us assume that we can prove the following inequality, where ℙ<μ_of S>{[ CSpart◁{Cs} | ξf ∩ Sf ]} on both sides cancel out, ...

    Hypothesis H_ineq_without_other_costs :
      ∑[∞]_{c <-option work }
       I [exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ] × ℙ <μ_of S >{[ 𝓒 j_rep ⟨=⟩ c | ξf ∩ Sf ]}
      ≤ ∑[∞]_{c <-option work }
         I [exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ] × ℙ <μ_tsk >{[ 𝓒 _pWCET ⟨=⟩ c ]}.

... then we can easily arrive at the preceding step's premise.

    Lemma transformation_is_pRT_monotone_step10:
      ∑[∞]_{c <-option work }
       I [exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ]
        × (ℙ <μ_of S >{[ CSpart ◁{Cs } | ξf ∩ Sf ]} × ℙ <μ_of S >{[ 𝓒 j_rep ⟨=⟩ c | ξf ∩ Sf ]})
      ≤ ∑[∞]_{c <-option work }
         I [exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ]
          × (ℙ <μ_of S >{[ CSpart ◁{Cs } | ξf ∩ Sf ]} × ℙ <μ_tsk >{[ 𝓒 _pWCET ⟨=⟩ c ]}).
    Proof.
      apply Rge_le.
      erewrite SeriesC_ext; last by (move ⇒ n);
        rewrite Rmult_comm Rmult_assoc [in X in (_ × X)]Rmult_comm.
      rewrite SeriesC_scal_l.
      apply Rle_ge.
      erewrite SeriesC_ext; last by (move ⇒ n);
        rewrite Rmult_comm Rmult_assoc [in X in (_ × X)]Rmult_comm.
      rewrite SeriesC_scal_l.
      apply Rmult_le_compat.
      { by apply Rge_le, ge_pr_0. }
      { apply SeriesC_pos ⇒ n; apply Rmult_le_0_compat.
        - by destruct ( exceeds _ _ ) ⇒ //=; nra.
        - by apply Rge_le, ge_pr_0.
      }
      { nra. }
      by apply H_ineq_without_other_costs.
    Qed.

  End Step10.

Step 11

We have successfully removed constraints on job costs of jobs that are not equal to j_rep. Depending on the cost of j_rep, we can still get different behavior. In this section, we do a case analysis on the "critical" value of the cost of j_rep.

Section Step11.

There are three possibilities: (1) whatever cost of job j_rep we pick, the response time of job j never exceeds r, (2) whatever cost of job j_rep we pick, the response time of job j always exceeds r, and (3) there is some critical value c0 such that j's response time will exceed r if and only if j_rep's job cost is larger than r.

    Lemma cost_causing_exceedance_of_r :
       (∃ (c0 : option work ), ∀ (c : option work),
          is_true (c0 ⟨<⟩ c) ↔ exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r )
      ∨ (∀ (c : option work), exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r )
      ∨ (∀ (c : option work), ¬ exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ).
    Proof.
      destruct (swithing_point_of_monotone_function
                  (fun c ⇒ exceeds (𝓡 𝗔 (update 𝗖 j_rep (Some c)) j) r)) as [F | [F|F]].
      { intros × LE E.
        by eapply H_rt_monotonic; last apply E.
      }
      { right; right; intros × EXC.
        destruct c; last first.
        { specialize (F 0%nat); apply: F.
          by eapply H_rt_monotonic; last by apply EXC. }
        { by specialize (F w); apply: F. }
      }
      { left; destruct F as [t0 EQUI].
        ∃ (Some t0); intros []; last first.
        { split; intros CONTR; first by done.
          exfalso; unfold rt_monotonic_scheduler in ×.
          eapply H_rt_monotonic with (c2 := Some 0%nat) in CONTR; last by done.
          by eapply EQUI in CONTR.
        }
        { by split; intros EP; apply EQUI. }
      }
      { right; left.
        intros []; first last.
        { specialize (F 0%nat).
          by eapply H_rt_monotonic; last by apply F. }
        { apply F. }
      }
    Qed.

Note that case (1) is easy since the inequality reduces to 0 ≤ 0.

    Remark jobs_rt_never_exceeds_r :
      (∀ c : option work , ¬ exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ) →
      ∑[∞]_{c <-option work }
       I [exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ]
        × ℙ <μ >{[ 𝓒 j_rep ⟨=⟩ c | ξf ∩ Sf ]}
      ≤ ∑[∞]_{c <-option work }
         I [exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ]
          × ℙ <μ_tsk >{[ 𝓒 _pWCET ⟨=⟩ c ]}.
    Proof.
      intros ALT.
      rewrite /pr_cond !SeriesC_0; first by nra.
      { intros c; move: (ALT c) ⇒ /negP/eqP AA.
        destruct (exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r); first by done.
        by rewrite Rmult_0_l.
      }
      { intros c; move: (ALT c) ⇒ /negP/eqP AA.
        destruct (exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r); first by done.
        by rewrite Rmult_0_l.
      }
    Qed.

Note that case (2) is easy since the inequality reduces to 1 ≤ 1.

    Remark jobs_rt_always_exceeds_r :
      (∀ c : option work , exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ) →
      ∑[∞]_{c <-option work }
       I [exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ]
        × ℙ <μ >{[ 𝓒 j_rep ⟨=⟩ c | ξf ∩ Sf ]}
      ≤ ∑[∞]_{c <-option work }
         I [exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ]
          × ℙ <μ_tsk >{[ 𝓒 _pWCET ⟨=⟩ c ]}.
    Proof.
      intros ALT; rewrite /pr_cond.
      erewrite SeriesC_ext; last first.
      { by intros; rewrite ALT; simpl; rewrite Rmult_1_l; reflexivity. }
      apply Rge_le.
      erewrite SeriesC_ext; last first.
      { intros; rewrite ALT; simpl; rewrite Rmult_1_l; reflexivity. }
      apply Rle_ge.
      have TP := @law_of_total_probability
                   _ μr xpredT [countType of option nat] (fun i ω ⇒ 𝓒 j_rep ω == i).
      feed_n 2%nat TP.
      { by intros ? _; ∃ (𝓒 j_rep ω). }
      { by move ⇒ a s d /eqP <- /eqP <-. }
      erewrite SeriesC_ext; last first.
      { intros ?.
        erewrite pr_eq_pred with (Q := λ ω : Ω , (𝓒 j_rep ω == n) && true).
        { reflexivity. }
        { by intros ?; rewrite !unfold_in andb_true_r. }
      }
      rewrite -TP; clear TP.
      have ->: ℙ <μr >{[ xpredT ]} = ℙ <μ_tsk >{[ xpredT ]} by rewrite !pr_xpredT.
      have TP := @law_of_total_probability.
      erewrite TP with (I := (option_countType (nat_countType)))
                       (B := fun (x : option_countType (nat_countType)) (ω : nat) ⇒
                               (Some ω == x)).
      apply leq_SeriesC.
      apply ex_series_pr_eq_over_disjoint.
      { by move ⇒ ω a b; unfold "∩", pred.pred_intersection ⇒
          /andP [/eqP <- _] /andP [/eqP <- _]. }
      apply ex_series_pr_eq_over_disjoint.
      { by move ⇒ ω a b ⇒ /eqP <- /eqP <-. }
      { by intros. }
      { move ⇒ x y [i [EQ1' EQ2']].
        rewrite EQ1' in EQ2'; inversion EQ2'; subst y.
        apply pr_mono_pred ⇒ ω.
        by unfold "∩", pred.pred_intersection ⇒ /andP [A _].
      }
      { by intros ω POS; ∃ (Some ω). }
      { by move ⇒ ω a b ⇒ /eqP <- /eqP <-. }
    Qed.

Case (3) is interesting; so let us assume that c0 is the critical value, after which the response time of job j will exceed r.

However, then I[exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r] can be transformed into c0 ⟨<⟩ c. We use the fancy ⟨<⟩ to account for the fact that both costs can be ⊥.

    Hypothesis H_ineq_c0_causes_exceedance :
      ∀ (c0 : option work),
        (∀ c , is_true (c0 ⟨<⟩ c) ↔ exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ) →
        ∑[∞]_{c <-option work } I [c0 ⟨<⟩ c ] × ℙ <μ_of S >{[ 𝓒 j_rep ⟨=⟩ c | ξf ∩ Sf ]}
        ≤ ∑[∞]_{c <-option work } I [c0 ⟨<⟩ c ] × ℙ <μ_tsk >{[ 𝓒 _pWCET ⟨=⟩ c ]}.

Given the hypothesis, we can prove the prior step's premise.

    Lemma transformation_is_pRT_monotone_step11 :
      ∑[∞]_{c <-option work }
       I [exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ] × ℙ <μ_of S >{[ 𝓒 j_rep ⟨=⟩ c | ξf ∩ Sf ]}
      ≤ ∑[∞]_{c <-option work }
         I [exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r ] × ℙ <μ_tsk >{[ 𝓒 _pWCET ⟨=⟩ c ]}.
    Proof.
      rewrite /pr_cond.
      edestruct cost_causing_exceedance_of_r as [ALT | [ALT | ALT]]; first last.
      { by apply jobs_rt_never_exceeds_r. }
      { by apply jobs_rt_always_exceeds_r. }
      destruct ALT as [c0 One].
      have L2 : ∀ (A B : bool), A ↔ B → I [A ] = I [B ].
      { by intros [] []; (done || intros []; exfalso; auto). }
      erewrite SeriesC_ext; last first.
      { intros c; apply Rmult_eq_compat_r, L2.
        instantiate (1 := c0 ⟨<⟩ c).
        by split; intros; apply One.
      }
      apply Rge_le.
      erewrite SeriesC_ext; last first.
      { intros c; apply Rmult_eq_compat_r, L2.
        instantiate (1 := c0 ⟨<⟩ c).
        by split; intros; apply One.
      }
      by apply Rle_ge, H_ineq_c0_causes_exceedance.
    Qed.

  End Step11.

Step 12

Let us now assume that there is a cost c0 (of job j_rep) with the property that any cost strictly higher causes j to have a response time larger than r.

  Variable c0 : option work.
  Hypothesis H_c0_causes_exceedance :
    ∀ c , is_true (c0 ⟨<⟩ c) ↔ exceeds (𝓡 𝗔 (update 𝗖 j_rep c) j) r.

Note that ∑_{c} I[c0 < c] ℙ{ X = c } is equivalent to ℙ{X > c0}. We use this property to simplify I[...] on both sides.

Section Step12.

Assuming that the following inequality, which is very similar to our initial assumption H_pWCET_bounds_cond_cdf, ...

    Hypothesis H_almost_pWCET_bounds_cond_cdf :
      ℙ <μ_of S >{[ (𝓒 j_rep ) ⟨<=⟩ c0 | ξf ∩ Sf ]} ≥
        ℙ <μ_tsk >{[ 𝓒 _pWCET ⟨<=⟩ c0 ]}.

... we can prove the inequality assumed in the previous step.

    Lemma transformation_is_pRT_monotone_step12 :
      ∑[∞]_{c <- option nat } I [c0 ⟨<⟩ c ] × ℙ <μ_of S >{[ 𝓒 j_rep ⟨=⟩ c | ξf ∩ Sf ]}
      ≤ ∑[∞]_{c <- option nat } I [c0 ⟨<⟩ c ] × ℙ <μ_tsk >{[ 𝓒 _pWCET ⟨=⟩ c ]}.
    Proof.
      by rewrite //= !bigop_inf_option_cdf_lt; apply: pr_ineq_compl.
    Qed.

  End Step12.

Step 13

In the last step, we exploit the top-level assumption H_pWCET_bounds_cond_cdf to finish the proof.

Section Step13.

Notice that the following statement is very close to the pWCET guarantee H_pWCET_bounds_cond_cdf.

    Lemma transformation_is_pRT_monotone_step13 :
      ℙ <μ_of S >{[ 𝓒 j_rep ⟨<=⟩ c0 | ξf ∩ Sf ]} ≥
        ℙ <μ_tsk >{[ 𝓒 _pWCET ⟨<=⟩ c0 ]}.
    Proof.
      destruct c0 as [|]; unfold "⟨<=⟩", onat_onat_bool_leqop ⇒ //=; last first.
      { unfold proj ω, proj1 in *; destruct pWCET_pmf as [pWCET nonneg sum1].
        eapply Rge_trans, H_pWCET_bounds_cond_cdf.
        reflexivity.
      }
      { unfold "⟨<=⟩", onrvar_onat_pred_leqop, "⟨<=⟩", onat_onat_bool_leqop; simpl.
        unfold proj ω, proj1 in *; destruct pWCET_pmf as [pWCET nonneg sum1].
        eapply Rge_trans, H_pWCET_bounds_cond_cdf.
        reflexivity.
      }
    Qed.

Also, note that we did not make any new assumptions in this section; hence, we are done.

End Step13.

End StepByStepProof.

Statement and Proof of Theorem 1

Now we can combine all the steps to prove that a single job cost can be replaced with the corresponding pWCET while preserving response-time monotonicity (Theorem 1 in the paper).

Section ProofOfTheorem1.

Assume horizon defines the termination time of the system. If horizon = None, the system does not terminate; however, as discussed at the beginning of the file, we assume a finite number of jobs in either case.

Variable horizon : option instant.

Consider any type of tasks with a notion of pWCET.

Context {Task : TaskType}
{pWCET_pmf : ProbWCET Task}.

Note that the arrivals and costs are determined by the system, which is defined next.

Context {Job : finType}
{job_task : JobTask Job Task}.

Consider a response-time monotonic scheduling algorithm ζ, where response-time monotonic means the following: assuming that all arrival times are fixed, an increase of the execution cost of any job cannot cause a decrease of the response time of any job. Recall that ζ receives two vectors: a vector of arrival times 𝗔 and a vector of job costs 𝗖.

Variable ζ : @scheduler 𝗔𝗖 Job.
Hypothesis H_rt_monotonic : rt_monotonic_scheduler horizon ζ.

Let sched denote a schedule generated by ζ.

Let sched S := compute_pr_schedule ζ (job_arrival := 𝓐 _of S) (job_cost := 𝓒 _of S).

Let S be an arbitrary system ...

Variable S : @system Job.

... and let j_rep be a job whose cost we want to replace.

Variable j_rep : Job.

Let S' be the system where we replace j_rep's cost with the corresponding pWCET via replace_job_pET.

Let S' := replace_job_pET j_rep S.

Consider an arbitrary job j ...

Variable j : Job.

... and its response times 𝓡j and 𝓡j' in schedules sched S and sched S', respectively.

Let 𝓡 j := response_time (sched S) (job_arrival := 𝓐 _of S) (job_cost := 𝓒 _of S) horizon j.
Let 𝓡 j' := response_time (sched S') (job_arrival := 𝓐 _of S') (job_cost := 𝓒 _of S') horizon j.

If pWCET satisfies our notion of axiomatic pWCET, ...

Hypothesis H_axiomatic_pWCET :
axiomatic_pWCET (μ_of S) (job_arrival := 𝓐 _of S) (job_cost := 𝓒 _of S).

... then the response-time distribution of job j in schedule sched S is ⪯-bounded by the response-time distribution of job j in schedule sched S'. That is, 𝓡j ⪯ 𝓡j'.

  Lemma prob_rt_monotonic_axiomatic_pWCET_replace_pET :
    𝓡 j ⪯ 𝓡 j'.
  Proof.
    intros t.
    destruct S as [Ω μ arrs costs]. clear S.
    set (S := {| Ω_of := Ω; μ_of := μ; 𝓐 _of := arrs; 𝓒 _of := costs |}) in ×.
    set (ξ__part := @partition_on_ξ _ μ _ arrs).
    set (ξ__part' := @extend_partition _ _ _ _ S ξ__part j_rep).
    set (tsk := job_task j_rep).
    apply transformation_is_pRT_monotone_step1; first by apply H_axiomatic_pWCET.
    move ⇒ ξi ξi' ξEQU.
    have HH := transformation_is_pRT_monotone_step2 horizon ζ _ _ _ _ _ _ _ _ ξi ξi' ξEQU.
    specialize (HH H_axiomatic_pWCET).
    destruct ξi as [ξ IN].
    specialize (HH j t ξ).
    apply: HH ⇒ //= ⇒ POSξ; clear ξi' ξEQU.
    apply transformation_is_pRT_monotone_step3 ⇒ //.
    intros.
    set ξf := (λ ω , arr_seq ω == ξ) : Ω → bool.
    set ξf' := (λ '(ω , c ), arr_seq ω == ξ) : (Ω × nat ) → bool.
    eapply transformation_is_pRT_monotone_step4 ⇒ //.
    eapply transformation_is_pRT_monotone_step5; eauto; intros.
    eapply transformation_is_pRT_monotone_step6; eauto; intros.
    eapply transformation_is_pRT_monotone_step7; eauto; intros.
    eapply transformation_is_pRT_monotone_step8; eauto.
    eapply transformation_is_pRT_monotone_step9; eauto.
    eapply transformation_is_pRT_monotone_step10; eauto.
    eapply transformation_is_pRT_monotone_step11; eauto. intros.
    eapply transformation_is_pRT_monotone_step12; eauto.
    eapply transformation_is_pRT_monotone_step13; eauto.
    Unshelve.
    { unfold PosProb; simpl.
      unfold proj ω, proj1 in *; destruct pWCET_pmf as [pWCET nonneg sum1].
      set (μ_tsk := {| pmf := pWCET tsk;
                      pmf_pos := nonneg tsk;
                      pmf_sum1 := sum1 tsk |}).
      have PM1 := pair_marginal1 μ μ_tsk (λ ω0 : Ω, ξf ω0 && Sf ω0).
      erewrite pr_eq_pred with
        (Q := λ ω : prod_countType Ω nat_countType, (arr_seq ω .1 == ξ) && Sf ω .1 ); first last.
      { by intros []; rewrite !unfold_in ⇒ //=. }
      by rewrite PM1; apply ρ.
    }
  Qed.

End ProofOfTheorem1.