Library probsa.rt.analysis.partition_transfer

(* --------------------------------- ProBsa --------------------------------- *)
From probsa.probability Require Export law_of_total_prob.
From probsa.rt.analysis Require Export pETs_to_pWCETs.

(* ---------------------------------- Main ---------------------------------- *)

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 (* Return the first component of the pair. *)
           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 (* Return the second component of the pair. *)
           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.

  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.

  End ExtendPartition.

End PartitionTransfer.