Library probsa.rt.analysis.arrivals

From prosa.model Require Import task.arrival.curves.
From prosa.analysis Require Export facts.behavior.arrivals.

From probsa.probability Require Export law_of_total_prob.
From probsa.rt.model Require Export events.

Local Open Scope nat_scope.

Section PrArrivalLemmas.

Consider a system that is described by a sample space Ω and a probability measure μ.

Variables (Ω : _) (μ : measure Ω).

Consider any type of tasks and their jobs.

  Context {Task : TaskType}
          {α : MaxArrivals Task}.

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

Consider an arbitrary task set ts...

Variable ts : seq Task.

... and a task tsk ∈ ts.

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

Let ξpart denote a partition of Ω into sets corresponding to different arrival sequences...

Let ξpart := partition_on_ξ μ : Ω_partition.

... and let ξ denote a positive-probability element of such a partition.

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

  Lemma pr_arrivals_between_eq :
    ∀ (t1 t2 : instant) (ω1 ω2 : Ω),
      ξpart ◁{ξ } ω1 →
      ξpart ◁{ξ } ω2 →
      pr_arrivals_between t1 t2 ω1 = pr_arrivals_between t1 t2 ω2.
  Proof.
    intros × INω1 INω2.
    inversion INω1 as [EQ1]; move: EQ1 ⇒ /eqP EQ1.
    inversion INω2 as [EQ2]; move: EQ2 ⇒ /eqP EQ2.
    rewrite -EQ1 in EQ2; rewrite /pr_arrivals_between //=.
    by f_equal; symmetry.
  Qed.

  Lemma pr_arrivals_task_between_eq :
    ∀ (t1 t2 : instant) (ω1 ω2 : Ω),
      ξpart ◁{ξ } ω1 →
      ξpart ◁{ξ } ω2 →
      pr_arrivals_task_between tsk t1 t2 ω1 = pr_arrivals_task_between tsk t1 t2 ω2.
  Proof.
    intros × INω1 INω2.
    rewrite /pr_arrivals_task_between //=.
    by f_equal; apply pr_arrivals_between_eq.
  Qed.

  Lemma pr_arrivals_between_fixed_in_partition :
    ∀ (t1 t2 : instant),
    ∃ (jobs : seq Job ), ∀ (ω : Ω),
      ξpart ◁{ξ } ω →
      [seq x <- arrivals_between (arr_seq ω) t1 t2 | job_of_task tsk x] = jobs.
  Proof.
    intros × ; apply pr_pos_inv in ρ; destruct ρ as [ω [IN _]].
    ∃ ([seq j <- arrivals_between (arr_seq ω) t1 t2 | job_of_task tsk j]).
    by intros ω' IN'; f_equal; apply pr_arrivals_between_eq.
  Qed.

  Hypothesis H_respects_arrival_curve :
    ∀ ω, taskset_respects_max_arrivals (arr_seq ω) ts.

  Hypothesis H_valid_arrival_curve :
    valid_taskset_arrival_curve ts α.

  Lemma pr_arrivals_task_between_respect_arrival_curve :
    ∀ (t1 t2 : instant) (ω : Ω),
      size (pr_arrivals_task_between tsk t1 t2 ω) ≤ α tsk (t2 - t1).
  Proof.
    intros.
    have [LE|LE] := leqP t1 t2; last first.
    { apply leq_trans with 0%nat ⇒ //.
      by rewrite leqn0 size_eq0 /pr_arrivals_task_between //=
                 arrivals_between_geq // ltnW.
    }
    { apply: leq_trans; last first.
      { by apply (H_respects_arrival_curve ω tsk H_tsk_in_ts t1 t2) ⇒ //. }
      { by done. }
    }
  Qed.

  Corollary pr_arrivals_task_between_respect_arrival_curve_mid :
    ∀ (t1 t2 A : instant) (ω : Ω),
      size (pr_arrivals_task_between tsk (A - t1) (A + t2) ω) ≤ α tsk (t1 + t2).
  Proof.
    intros; apply: leq_trans; first by apply pr_arrivals_task_between_respect_arrival_curve.
    apply H_valid_arrival_curve ⇒ //.
    have [LE|LE] := leqP A t1.
    { move: (LE); rewrite -subn_eq0 ⇒ /eqP →.
      by rewrite subn0 leq_add2r. }
    { rewrite subnBA; last by apply ltnW.
      by rewrite -addnA addKn addnC. }
  Qed.

End PrArrivalLemmas.