Library probsa.rt.analysis.partition_transfer

From probsa.probability Require Export law_of_total_prob.
From probsa.rt.analysis Require Export pETs_to_pWCETs.

Partition Transfer

Given a partition P of Ω_of S, we can modify partition P so it is still a valid partition in a new system Ω_of (replace_jobs_pET j S). This section provides functions that do this transformation.

Note that both functions defined in this section work in the same way as partition_ext (defined in /probability/partition.v). However, due to more sophisticated types, we must repeat this construction, providing suitable types. The main reason is that even though Ω_of (replace_jobs_pET j S) can be eventually simplified to Ω × ℕ, Coq cannot see it.

Section PartitionTransfer.

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

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

The functions proj1 and proj2 are equivalent to the usual projections of the same names with the only difference that the resulting type is Ω_of (replace_jobs_pET j S) → Ω_of S, which adds some extra hurdles to the otherwise trivial match.

  Definition proj1 (S : system) (j : Job) (ω : Ω_of (replace_job_pET j S)) : Ω_of S :=
    (match pWCET_pmf, S with
     | Build_ProbWCET pWCET_pmf0 pWCET_nonnegative pWCET_sum1, Build_system Ω_of0 μ_of 𝓐_of 𝓒_of ⇒
         fun (ω : Ω_of (@replace_job_pET _ (Build_ProbWCET _ pWCET_pmf0 pWCET_nonnegative pWCET_sum1)
                                        _ _ j (Build_system _ μ_of 𝓐_of 𝓒_of))) ⇒
           match ω return Ω_of (Build_system _ μ_of 𝓐_of 𝓒_of) with
           | pair ω1 ω2 ⇒ ω1
           end
     end) ω.

  Definition proj2 (S : system) (j : Job) (ω : Ω_of (replace_job_pET j S)) : work :=
    (match pWCET_pmf, S with
     | Build_ProbWCET pWCET_pmf0 pWCET_nonnegative pWCET_sum1, Build_system Ω_of0 μ_of 𝓐_of 𝓒_of ⇒
         fun (ω : Ω_of (@replace_job_pET _ (Build_ProbWCET _ pWCET_pmf0 pWCET_nonnegative pWCET_sum1)
                                       _ _ j (Build_system _ μ_of 𝓐_of 𝓒_of))) ⇒
           match ω with
           | pair ω1 ω2 ⇒ ω2
           end
     end) ω.

  Section ExtendPartition.

Consider a system S.

Variable S : @system Job.

Assume that there exists some partition P.

Variable P : @Ω_partition (Ω_of S) (μ_of S).

Next, let S' be a system in which a job j's pET is replaced with the corresponding pWCET via the function replace_job_pET.

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

Then, we show that one can extend partition P to system S' via ignoring the additional dimension. That is, ω ∈ P◁{i} iff (ω, c) ∈ P'◁{i}.

(Note that p ignores the second component of ω' by using the projection proj1.)

    Program Definition extend_partition : @Ω_partition (Ω_of S') (μ_of S') :=
      match P, S with
        Build_Ω_partition I p_orig COV DIS, Build_system Ω μ 𝓐 𝓒 ⇒
          {|
            I := I;
            p := fun i ω' ⇒ p_orig i (proj1 _ _ ω')
          |}
      end.
    Next Obligation.
      unfold proj1 in *; destruct pWCET_pmf as [pWCET nonneg sum1].
      destruct ω as [ω1 ω2]; apply: COV.
      move: H; rewrite //= /distrib_prod /prod_pmf ⇒ //= ⇒ POS.
      move: (POS) (nonneg (job_task j) ω2) ⇒ POS1c POS2c.
      by unfold task.pWCET_pmf in *; nra.
    Qed.

  End ExtendPartition.

Later in the proof we have to consider a system (Ω, μ|B) with a measure restricted to some event B. One can extend a partition of (Ω, μ|B) to a partition of (Ω', μ'|B') using a similar idea. The main difference is that the measure of the partition is different — restrict (μ_of S') B'.

  Section ExtendPartition.

    Program Definition extend_partition'
            (S : system) (j : Job)
            (B : pred (Ω_of S))
            {pos : PosProb (μ_of S) B}
            (P : @Ω_partition (Ω_of S) (restrict (μ_of S) B))
            (B' : pred (Ω_of (replace_job_pET j S)))
            {pos' : PosProb (μ_of (replace_job_pET j S)) B'}
            (Le : ∀ ω, B' ω → B (proj1 S j ω)) :
      let S' := replace_job_pET j S in @Ω_partition (Ω_of S') (restrict (μ_of S') B') :=
      match P, S with
        Build_Ω_partition I p_orig COV DIS, Build_system Ω μ 𝓐 𝓒 ⇒
          {|
            I := I;
            p := fun i ω' ⇒ p_orig i (proj1 _ _ ω')
          |}
      end.
    Next Obligation.
      unfold proj1 in *; destruct pWCET_pmf as [pWCET nonneg sum1].
      move: ω H ⇒ [ω1 ω2]; destruct μ as [μ1 POS1 SUM1].
      move ⇒ POS; apply: COV ⇒ //=.
      rewrite /pmf_restricted ⇒ //=.
      destruct (B' (ω1,ω2)) eqn:HB; first last.
      { by rewrite //= /pmf_restricted HB in POS; apply Rlt_irrefl in POS. }
      rewrite //= /pmf_restricted HB in POS.
      have L : ∀ a b, a / b > 0 → b > 0 → a > 0.
      { by clear; intros; apply Rinv_0_lt_compat in H0; nra. }
      set (μ := {| pmf := μ1; pmf_pos := POS1; pmf_sum1 := SUM1 |}).
      set (μ_tsk := {| pmf := pWCET (job_task j);
                      pmf_pos := nonneg (job_task j);
                      pmf_sum1 := sum1 (job_task j) |}).
      set μ_prod := distrib_prod μ μ_tsk.
      specialize (L (μ_prod (ω1, ω2)) (ℙ <μ_prod>{[ B']})).
      eapply L in POS; [clear L | by apply pos'].
      rewrite //= /prod_pmf //= in POS.
      have L: ∀ ω1 ω2, B' (ω1 , ω2 ) → B ω1 by intros; apply Le in H.
      erewrite L; [clear L | by exact HB].
      rewrite /Rdiv; apply Rlt_mult_inv_pos; last by done.
      move: (POS1 ω1) (nonneg (job_task j) ω2) ⇒ POS1c POS2c.
      by rewrite /task.pWCET_pmf in POS2c; nra.
    Defined.

  End ExtendPartition.

End PartitionTransfer.