Library probsa.rt.analysis.independent.task_workload

From probsa.rt.model Require Export events workload.

Section PrTaskWorkloadIndependence.

  Context {Ω} {μ : measure Ω}.

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

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

  Variable ts : seq Task.
  Hypothesis H_ts_uniq : uniq ts.
  Hypothesis H_jobs_from_ts : ∀ (j : Job), job_task j \in ts.

  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

  Hypothesis H_arrival_sequence_uniq : pr_arrival_sequence_uniq.
  Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.

  Let ξpart := partition_on_ξ μ : Ω_partition.
  Hypothesis job_costs_cond_independent :
    ∀ (ξ : I ξpart) `{!PosProb μ (ξpart◁{ξ})},
      independent
        [seq mkRvar (restrict μ (ξpart◁{ξ})) (job_cost j) | j <- index_enum Job].

  Variable ξ : I ξpart.
  Context {ρ : PosProb μ (ξpart◁{ξ})}.

  Variable (t1 t2 : Task → instant).

  Let pr_task_workload (tsk : Task) :=
    mkRvar _ (pr_workload_of_task tsk (t1 tsk) (t2 tsk))
    : rvar (restrict μ (ξpart◁{ξ})) [eqType of work].

  Lemma pr_task_workload_independence :
    independent [seq pr_task_workload tsk | tsk <- ts].
  Proof.
    have [ω INωξ] : ∃ ω, ξpart◁{ξ} ω.
    { move: (ρ) ⇒ POS.
      apply pr_pos_inv in POS.
      move: POS ⇒ [ω [IN _]].
      by ∃ ω; apply IN.
    }
    set (F xs :=
           (\sum_(j <-
                    map (fun '(j, _, _, _) ⇒ j)
                        (filter (fun '(j, _, t1, t2) ⇒
                                   (is_some (job_arrival j ω) )
                                   && (t1 ≤ odflt0 (job_arrival j) ω < t2)) xs
                        )
                 | true)
             (sumn (map (fun '(_, c, _, _) ⇒ c) (filter (fun '(jo, _, _, _) ⇒ pred1 j jo ) xs)))
           )%nat
        ).
    set (f tsk ω j := (j, odflt0 (job_cost j) ω, t1 tsk, t2 tsk ) ).
    set (R :=
           fun tsk ⇒
             mkRvar (restrict μ (ξpart◁{ξ}))
                    (fun ω ⇒
                       map (f tsk ω) (filter (job_of_task tsk) (index_enum Job))
                    )
        ).
    apply: indep_irr; last first.
    { apply: (@indep_comp _ (restrict μ (ξpart◁{ξ})) _ _ R _ F ts).
      apply (@independent_flatten _ (restrict μ (ξpart◁{ξ})) _ _ _ f ts).
      rewrite allpairs_rvar; eapply indep_perm_eq.
      { apply perm_eq_allpairs_flatten with (F0 := job_task) ⇒ //.
        { by apply index_enum_uniq. }
        { by intros j IN; rewrite /job_of_task. }
        { by move⇒ tsk1 tsk2 j _ /eqP <- /eqP <-. }
      }
      rewrite -map_comp.
      apply: indep_pair_const_r; apply: indep_pair_const_r.
      apply indep_pair_swap, indep_pair_const_r.
      apply: (@indep_comp _ (restrict μ (ξpart◁{ξ})) _ _ (fun j ⇒ mkRvar _ (job_cost j))).
      apply job_costs_cond_independent.
    }
    { clear tsk H_tsk_in_ts ⇒ tsk ωo IN POSo; unfold F.
      rewrite [RHS](@eq_bigl _ _ _ _ _ _ (fun j ⇒ job_of_task tsk j && job_of_task tsk j) );
        last by intros j; destruct job_of_task.
      rewrite big_mkcondr //= -[RHS]big_filter.
      erewrite perm_big.
      { apply congr_big; [reflexivity | done | move ⇒ jo _].
        rewrite filter_map -map_comp -filter_predI sumnE big_map_id big_filter.
        by rewrite big_mkcondr big_pred1_eq //=.
      }
      { apply/allP ⇒ j IN2.
        rewrite filter_map -map_comp -filter_predI //= !count_uniq_mem; first last.
        { by rewrite map_inj_uniq //; apply filter_uniq, index_enum_uniq. }
        { apply filter_uniq, bigcat_nat_uniq.
          { by intros s; apply H_arrival_sequence_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 (j \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 NEQ] TSK] _].
            apply/eqP; rewrite eqb1; apply/andP; split ⇒ //.
            apply mem_bigcat with (x := odflt0 (job_arrival j) ω); first by rewrite mem_index_iota.
            destruct (job_arrival j ω) eqn:EQ; last by rewrite EQ in SOME.
            rewrite //= EQ; apply H_arrivals_consistent.
            clear IN; inversion INωξ as [IN].
            eapply pmf_restricted_pred in POSo; move: POSo ⇒ /eqP POSo; rewrite -POSo in IN.
            rewrite -EQ; apply eq_arr_seq_impl_eq_job_arrival ⇒ to.
            by move: IN ⇒ /eqP →.
          }
          { symmetry; apply/eqP; rewrite eqb0; apply/negP ⇒ INO.
            move: EQ ⇒ /neqP EQ; apply: EQ; rewrite eqbF_neg negb_involutive.
            move: INO; rewrite mem_filter ⇒ /andP [TSK INO].
            apply mem_bigcat_nat_exists in INO; move: INO ⇒ [to [INO NEQ]].
            apply H_arrivals_consistent in INO; apply/mapP.
            ∃ j ⇒ //.
            have SO : job_arrival j ω = Some to.
            { clear IN; inversion INωξ as [IN]; move: IN ⇒ /eqP INω.
              apply pmf_restricted_pred in POSo; move: POSo ⇒ /eqP POSo; rewrite -INω in POSo.
              by erewrite eq_arr_seq_impl_eq_job_arrival; [erewrite INO | intros; rewrite POSo].
            }
            rewrite mem_filter; apply/andP; split; last by apply mem_index_enum.
            by apply/andP; split ⇒ //; apply/andP; split; rewrite SO.
          }
        }
      }
    }
  Qed.

End PrTaskWorkloadIndependence.