Library probsa.rt.analysis.independent.cost_and_workload

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype choice fintype bigop seq.

From probsa.rt.model Require Export events workload assumptions.basic.

Section JobCostWorkloadIndependent.

  Context {Ω} {μ : measure Ω}.

  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {FP : FP_policy Task}.

  Context {Job : finType}
          {job_cost : JobCostRV Job Ω μ}
          {job_arrival : JobArrivalRV Job Ω μ}
          {job_task : JobTask Job Task}.

  Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.

  Variable (ts : seq Task) (tsk : Task).
  Hypothesis H_tsk_in_ts : tsk \in ts.

Consider a job of task tsk.
  Variable j : Job.
  Hypothesis H_job_of_task : job_of_task tsk j.

Assume that job costs conditioned on an arrival sequence are independent.
  Hypothesis H_job_costs_cond_independent :
    let ξpart := partition_on_ξ μ : Ω_partition in
    ∀ (ξ : I ξpart) `(!PosProb μ (ξpart◁{ξ})),
      independent [
          seq mkRvar (restrict μ (ξpart◁{ξ})) (job_cost j)
        | j <- index_enum Job].

  Let ξpart := partition_on_ξ μ : Ω_partition.
  Variable (ξ : I ξpart) (ω : Ω).
  Hypothesis INωξ : ξpart◁{ξ} ω.
  Hypothesis POS : PosProb μ (ξpart◁{ξ}).

  Variable (t : instant) (Δ : duration).

We define two random variables on the restricted probability space (conditioned on a fixed arrival sequence ξ):
𝓒 - The cost of job j (defaulting to 0 if the job doesn't arrive). This represents the workload contribution of our specific job.
𝓦 - The total workload of all tasks with higher or equal priority than tsk distinct from tsk over the interval [t - D tsko, t + Δ) for each such task tsko. This represents the interfering workload from higher-priority tasks. Note: The specific interval [t - D tsko, t + Δ)>> is used because it's later required for the pRTA proof.
  Let 𝓒 :=
        mkRvar _ [eta odflt0 (job_cost j)]
        : rvar (restrict μ (ξpart◁{ξ})) [eqType of work].

  Let 𝓦 :=
        mkRvar _ (fun ω ⇒
                    \sum_(tsko <- ts | hep_task tsko tsk && (tsko != tsk))
                     pr_workload_of_task tsko (t - D tsko) (t + Δ) ω
                 )
        : rvar (restrict μ (ξpart◁{ξ})) [eqType of work].

We show that these two random variables are independent: the cost of job j does not depend on the costs of jobs from higher-priority tasks.
  Local Lemma job_cost_and_ohep_workload_indep2 :
    indep2 𝓒 𝓦.
  Proof.
    set (Rc := [seq
                  mkRvar
                  (restrict μ (ξpart◁{ξ}))
                  (fun ω ⇒ (j, job_cost j ω, job_task j, D (job_task j)))
               | j <- [::j]]
).
    set (Rz := [seq
                  mkRvar
                  (restrict μ (ξpart◁{ξ}))
                  (fun ω ⇒ (j, job_cost j ω, job_task j, D (job_task j)))
               | j <- rem j (index_enum Job) ]
        ).
    have [Fc EQc] :
      ∃ (F : seq _ → _), ∀ ω, rvar_comp (rvar_list Rc) F ω = 𝓒 ω.
    { ∃ (fun xs ⇒ sumn (map (fun '(j, c, tsk, D) ⇒ odflt 0%nat c) xs)).
      by unfold rvar_comp, "\o" ⇒ // ⇒ ωo ⇒ //=; rewrite addn0.
    }
    have [Fz EQz] :
      ∃ (F : seq _ → _), ∀ ω,
        (restrict μ (ξpart◁{ξ})) ω > 0 →
        rvar_comp (rvar_list Rz) F ω = 𝓦 ω.
    { ∃ (fun xs ⇒
           \sum_(tsko <- ts | hep_task tsko tsk && (tsko != tsk))
            \sum_(j <- map (fun '(j, c, _, _) ⇒ j)
                          (filter (fun '(j, c, tskoo, D) ⇒
                                     (is_some (job_arrival j ω) )
                                     && (t - D ≤ odflt0 (job_arrival j) ω < t + Δ)%nat
                                     && (tskoo == tsko))
                                  xs
                          )
                 | true)
            (sumn (
                 map (fun '(j, c, tsk, D) ⇒ odflt 0%nat c)
                     (filter (fun '(jo, c, tskoo, D) ⇒ (pred1 j jo) && (tskoo == tsko)) xs)
        ))).
      move ⇒ // ⇒ ωo POSo ⇒ //=.
      apply congr_big ⇒ // ⇒ tsko /andP [HEP NEQ].
      rewrite [RHS](@eq_bigl _ _ _ _ _ _ (fun j ⇒ job_of_task tsko j && job_of_task tsko j) );
        last by intros jo; destruct (job_of_task tsko).
      rewrite big_mkcondr //= -[RHS]big_filter; erewrite perm_big.
      { apply congr_big; [reflexivity | done | ].
        rewrite -map_comp ⇒ jo _.
        rewrite filter_map -map_comp sumnE big_map_id big_filter big_mkcondr //=.
        rewrite rem_filter; last by apply index_enum_uniq.
        rewrite big_filter_cond big_mkcondl big_pred1_eq //=.
        unfold job_of_task; destruct (job_task jo == _ ) eqn:TSK, (jo != _ ) eqn:NEQ2 ⇒ //; rewrite TSK ⇒ //.
        move: NEQ2 TSK (H_job_of_task) ⇒ /eqP EQ /eqP TSK /eqP EQ2; subst.
        by rewrite eq_refl in NEQ.
      }
      { apply/allP ⇒ s IN2; rewrite -map_comp filter_map -map_comp //=.
        rewrite !count_uniq_mem; first last.
        { rewrite map_inj_uniq //.
          by apply filter_uniq, rem_uniq, index_enum_uniq. }
        { apply filter_uniq, bigcat_nat_uniq.
          { by intros g; apply arr_seq_uniq. }
          intros jo t1 t2 INa INb.
          apply H_arrivals_consistent in INa.
          apply H_arrivals_consistent in INb.
          by rewrite INa in INb; inversion INb.
        }
        clear IN2; apply/eqP; destruct (s \in _ ) eqn:EQ.
        { symmetry; rewrite mem_filter.
          unfold "\o" in EQ; simpl in EQ.
          move: EQ ⇒ /mapP [jo INo EQ]; subst jo.
          move: INo; rewrite mem_filter //= ⇒ /andP [/andP [/andP [SOME NEQ2] TSK] _].
          apply/eqP; rewrite eqb1; apply/andP; split ⇒ //.
          apply mem_bigcat with (x := odflt0 (job_arrival s) ω).
          rewrite mem_index_iota; first by move : TSK ⇒ /eqP TSK; subst tsko.
          destruct (job_arrival s ω) eqn:EQ; last by rewrite EQ in SOME.
          rewrite //= EQ; apply H_arrivals_consistent.
          inversion INωξ as [IN]; eapply pmf_restricted_pred in POSo.
          move: POSo ⇒ /eqP POSo; rewrite -POSo in IN; rewrite -EQ.
          by apply eq_arr_seq_impl_eq_job_arrival; move: IN ⇒ /eqP →.
        }
        { symmetry; apply/eqP; rewrite eqb0; apply/negP ⇒ INO.
          move: INO; rewrite mem_filter ⇒ /andP [TSK INO].
          apply mem_bigcat_nat_exists in INO; move: INO ⇒ [to [INO NEQ2]].
          move: EQ ⇒ /neqP EQ; apply: EQ; rewrite eqbF_neg negb_involutive.
          apply/mapP; ∃ s ⇒ //.
          have SO : job_arrival s ω = Some to.
          { inversion INωξ as [IN]; move: IN ⇒ /eqP INω.
            apply pmf_restricted_pred in POSo; move: POSo ⇒ /eqP POSo; rewrite -INω in POSo.
            erewrite eq_arr_seq_impl_eq_job_arrival.
            { by apply H_arrivals_consistent in INO; erewrite INO. }
            { by intros; rewrite POSo. }
          }
          rewrite mem_filter.
          apply/andP; split; last first.
          { apply in_neq_impl_rem_in; first by apply mem_index_enum.
            apply/negP ⇒ /eqP EQ. subst s.
            move: (H_job_of_task) TSK ⇒ /eqP EQ /eqP EQ2.
            by move: NEQ; rewrite -EQ -EQ2 eq_refl.
          }
          apply/andP; split ⇒ //.
          move: TSK ⇒ /eqP TSK; subst.
          by apply/andP; split; rewrite SO.
        }
      }
    }
    eapply indep2_fn_ext with (X1 := rvar_list Rc) (f1 := Fc) (Y1 := rvar_list Rz) (f2 := Fz).
    { by intros; apply EQc. }
    { by apply EQz. }
    { apply: indep_cat_indep2_list; rewrite -map_cat; apply indep_subset with (ys := index_enum Job).
      { by clear; move ⇒ s _ ; apply mem_index_enum. }
      { erewrite perm_uniq; last first.
        { by rewrite perm_sym; apply perm_to_rem, mem_index_enum. }
        { by apply index_enum_uniq. }
      }
      { by apply index_enum_uniq. }
      { apply indep_pair_const_r, indep_pair_const_r, indep_pair_swap, indep_pair_const_r.
        by apply: H_job_costs_cond_independent; eauto 1.
      }
    }
  Qed.

  Corollary job_cost_and_ohep_workload_independent :
    ∀ (c w : work),
      ℙ<μ>{[ (𝓒 ⟨=⟩ c) ∩ (𝓦 ⟨=⟩ w) | ξpart◁{ξ} ]}
      = ℙ<μ>{[ 𝓒 ⟨=⟩ c | ξpart◁{ξ} ]} × ℙ<μ>{[ 𝓦 ⟨=⟩ w | ξpart◁{ξ} ]}.
  Proof.
    by intros; apply job_cost_and_ohep_workload_indep2.
  Qed.

End JobCostWorkloadIndependent.