Library probsa.rt.behavior.arrival_sequence
From prosa Require Export util.all.
From prosa Require Export behavior.all.
From prosa Require Export model.task.concept.
From probsa.util Require Export boolp.
From probsa.rt.behavior Require Export job.
From prosa Require Export behavior.all.
From prosa Require Export model.task.concept.
From probsa.util Require Export boolp.
From probsa.rt.behavior Require Export job.
Probabilistic Arrival Sequence
Arrival sequence is a function that maps a time instant to a sequence of jobs that arrive at this time instant. A probabilistic arrival sequence is a random variable with a codomain in arrival sequences.
Definition pr_arrival_sequence {Ω} (μ : measure Ω) (Job : JobType) : Type :=
rvar μ [eqType of {classic (arrival_sequence Job)}].
rvar μ [eqType of {classic (arrival_sequence Job)}].
job_arrival → pr_arrival_sequence for Job : Finite
If Job is a finType, one can derive a probabilistic arrival sequence from JobArrivalRV.
Section ArrSeqForFinTypeJobs.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}.
The set of jobs that arrive at a time instant t in a scenario
ω is simply j <- Job | job_arrival j ω = t. Note that since
the number of jobs is finite, we can just check every single job
if it arrives at time t in a scenario ω.
Due to the fact that arrival_sequence is an arrow type
(instant → seq Job), Coq cannot automatically derive the right
type. Therefore, we need to steer Coq's coercion and type
systems towards the right type via annotation B :=
Equality.clone _ _. This technicality does not change the
intuitive meaning; therefore, we do not explain it here. An
interested reader can inspect the resulting term using commands
Set Printing All and Print arr_seq.
Definition arr_seq : pr_arrival_sequence μ Job :=
mkRvar _ (B := Equality.clone _ _)
(fun ω t ⇒
[seq j <- index_enum Job |
if job_arrival j ω is Some ta
then t == ta
else false
]
).
End ArrSeqForFinTypeJobs.
Section PrArrivalsBetween.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Let ξ : pr_arrival_sequence μ Job := arr_seq.
Definition pr_arrivals_between (t1 t2 : instant) : rvar μ [eqType of seq Job] :=
mkRvar μ (fun ω ⇒ arrivals_between (ξ ω) t1 t2).
Definition pr_arrivals_task_between (tsk : Task) (t1 t2 : instant) : rvar μ [eqType of seq Job] :=
mkRvar μ (fun ω ⇒ [seq j <- pr_arrivals_between t1 t2 ω | job_of_task tsk j]).
End PrArrivalsBetween.
Section ConsistentDef.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}.
Definition arr_seq_job_arrival_consistent :=
∀ (j : Job) (ω : Ω) (t : instant),
job_arrival j ω = Some t ↔ j \in arr_seq ω t.
End ConsistentDef.
Section ArrSeqAndJobArrivalAgree.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}.
Local Remark cons_elim :
∀ {T} (x y : T) (xs ys : seq T),
x::xs = y::ys → x = y ∧ xs = ys.
Proof. by move ⇒ ? ? ? ? ?; case. Qed.
Local Remark filter_eq_cons_sat :
∀ {T} (x : T) (xs ys : seq T) (P : pred T),
x :: xs = [seq e <- ys | P e] → P x.
Proof.
intros × EQ.
induction ys; first by done.
case_eq (P a) ⇒ [Pa| Pa]; rewrite //= Pa in EQ.
- by apply cons_elim in EQ; destruct EQ; subst a.
- by apply IHys in EQ.
Qed.
Local Remark filter_cons_eq :
∀ {T} (x : T) (xs : seq T) (P1 P2 : T → bool),
[seq e <- x::xs | P1 e ] = [seq e <- x::xs | P2 e ] →
(P1 x = P2 x) ∧ [seq e <- xs | P1 e ] = [seq e <- xs | P2 e ].
Proof.
intros × EQ.
destruct P1 eqn:P1x, P2 eqn:P2x; rewrite //= P1x P2x in EQ; try done.
- by split; last (apply cons_elim in EQ; apply EQ).
- by apply filter_eq_cons_sat in EQ; rewrite EQ in P2x.
- by apply esym, filter_eq_cons_sat in EQ; rewrite EQ in P1x.
Qed.
Lemma eq_arr_seq_impl_eq_job_arrival :
∀ (j : Job) (ω ω' : Ω),
(∀ t, arr_seq ω t = arr_seq ω' t) →
job_arrival j ω = job_arrival j ω'.
Proof.
rewrite /arr_seq ⇒ j ω ω' EQ.
set (js := index_enum Job) in ×.
have IN : j \in js by apply mem_index_enum.
induction js; first by done.
move: IN; rewrite in_cons ⇒ /orP [/eqP E | IN]; [subst a; clear IHjs | ].
{ destruct (job_arrival j ω) as [t1|] eqn:JAω.
{ specialize (EQ t1); unfold rvar_fun in ×.
apply filter_cons_eq in EQ; destruct EQ as [EQUIV EQ].
destruct (job_arrival _ ) as [job_arrival1 ].
rewrite JAω eq_refl in EQUIV; destruct (job_arrival1 ω'); last by done.
by move: EQUIV ⇒ /eqP; rewrite eq_sym eqb_id ⇒ /eqP →. }
{ destruct (job_arrival j ω') as [t2|] eqn:JAω'; last by done.
specialize (EQ t2); unfold rvar_fun in ×.
apply filter_cons_eq in EQ; destruct EQ as [EQUIV EQ].
destruct (job_arrival _ ) as [job_arrival1 ].
by rewrite JAω' eq_refl JAω in EQUIV.
}
}
{ apply IHjs; last by done.
intros t; specialize (EQ t); unfold rvar_fun in ×.
by apply filter_cons_eq in EQ; destruct EQ as [_ EQ]; apply EQ.
}
Qed.
End ArrSeqAndJobArrivalAgree.
Section ArrSeqUniq.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Let ξ : pr_arrival_sequence μ Job := arr_seq.
Lemma arr_seq_uniq :
∀ t ω, uniq (ξ t ω).
Proof.
by intros *; rewrite filter_uniq // index_enum_uniq.
Qed.
End ArrSeqUniq.
Section Consistent.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Lemma arr_seq_consistent :
arr_seq_job_arrival_consistent.
Proof.
intros ? ? ?; split; [intros EQ | ].
{ by rewrite mem_filter EQ eq_refl andTb mem_index_enum. }
{ rewrite mem_filter ⇒ /andP [MA IN].
destruct (job_arrival j ω) eqn:ARR; last by done.
by move: MA ⇒ /eqP EQ; subst.
}
Qed.
Lemma pr_consistent_arrival_times :
∀ (ω : Ω),
@consistent_arrival_times
Job
(fun j ⇒ odflt0 (job_arrival j) ω)
(arr_seq ω).
Proof.
intros ? ? ?; unfold arrives_at, arrivals_at ⇒ ARR.
apply arr_seq_consistent in ARR.
by rewrite /prosa.behavior.job.job_arrival //= ARR.
Qed.
End Consistent.
Global Opaque arr_seq arrival_sequence.
mkRvar _ (B := Equality.clone _ _)
(fun ω t ⇒
[seq j <- index_enum Job |
if job_arrival j ω is Some ta
then t == ta
else false
]
).
End ArrSeqForFinTypeJobs.
Section PrArrivalsBetween.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Let ξ : pr_arrival_sequence μ Job := arr_seq.
Definition pr_arrivals_between (t1 t2 : instant) : rvar μ [eqType of seq Job] :=
mkRvar μ (fun ω ⇒ arrivals_between (ξ ω) t1 t2).
Definition pr_arrivals_task_between (tsk : Task) (t1 t2 : instant) : rvar μ [eqType of seq Job] :=
mkRvar μ (fun ω ⇒ [seq j <- pr_arrivals_between t1 t2 ω | job_of_task tsk j]).
End PrArrivalsBetween.
Section ConsistentDef.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}.
Definition arr_seq_job_arrival_consistent :=
∀ (j : Job) (ω : Ω) (t : instant),
job_arrival j ω = Some t ↔ j \in arr_seq ω t.
End ConsistentDef.
Section ArrSeqAndJobArrivalAgree.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}.
Local Remark cons_elim :
∀ {T} (x y : T) (xs ys : seq T),
x::xs = y::ys → x = y ∧ xs = ys.
Proof. by move ⇒ ? ? ? ? ?; case. Qed.
Local Remark filter_eq_cons_sat :
∀ {T} (x : T) (xs ys : seq T) (P : pred T),
x :: xs = [seq e <- ys | P e] → P x.
Proof.
intros × EQ.
induction ys; first by done.
case_eq (P a) ⇒ [Pa| Pa]; rewrite //= Pa in EQ.
- by apply cons_elim in EQ; destruct EQ; subst a.
- by apply IHys in EQ.
Qed.
Local Remark filter_cons_eq :
∀ {T} (x : T) (xs : seq T) (P1 P2 : T → bool),
[seq e <- x::xs | P1 e ] = [seq e <- x::xs | P2 e ] →
(P1 x = P2 x) ∧ [seq e <- xs | P1 e ] = [seq e <- xs | P2 e ].
Proof.
intros × EQ.
destruct P1 eqn:P1x, P2 eqn:P2x; rewrite //= P1x P2x in EQ; try done.
- by split; last (apply cons_elim in EQ; apply EQ).
- by apply filter_eq_cons_sat in EQ; rewrite EQ in P2x.
- by apply esym, filter_eq_cons_sat in EQ; rewrite EQ in P1x.
Qed.
Lemma eq_arr_seq_impl_eq_job_arrival :
∀ (j : Job) (ω ω' : Ω),
(∀ t, arr_seq ω t = arr_seq ω' t) →
job_arrival j ω = job_arrival j ω'.
Proof.
rewrite /arr_seq ⇒ j ω ω' EQ.
set (js := index_enum Job) in ×.
have IN : j \in js by apply mem_index_enum.
induction js; first by done.
move: IN; rewrite in_cons ⇒ /orP [/eqP E | IN]; [subst a; clear IHjs | ].
{ destruct (job_arrival j ω) as [t1|] eqn:JAω.
{ specialize (EQ t1); unfold rvar_fun in ×.
apply filter_cons_eq in EQ; destruct EQ as [EQUIV EQ].
destruct (job_arrival _ ) as [job_arrival1 ].
rewrite JAω eq_refl in EQUIV; destruct (job_arrival1 ω'); last by done.
by move: EQUIV ⇒ /eqP; rewrite eq_sym eqb_id ⇒ /eqP →. }
{ destruct (job_arrival j ω') as [t2|] eqn:JAω'; last by done.
specialize (EQ t2); unfold rvar_fun in ×.
apply filter_cons_eq in EQ; destruct EQ as [EQUIV EQ].
destruct (job_arrival _ ) as [job_arrival1 ].
by rewrite JAω' eq_refl JAω in EQUIV.
}
}
{ apply IHjs; last by done.
intros t; specialize (EQ t); unfold rvar_fun in ×.
by apply filter_cons_eq in EQ; destruct EQ as [_ EQ]; apply EQ.
}
Qed.
End ArrSeqAndJobArrivalAgree.
Section ArrSeqUniq.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Let ξ : pr_arrival_sequence μ Job := arr_seq.
Lemma arr_seq_uniq :
∀ t ω, uniq (ξ t ω).
Proof.
by intros *; rewrite filter_uniq // index_enum_uniq.
Qed.
End ArrSeqUniq.
Section Consistent.
Context {Ω} {μ : measure Ω}.
Context {Task : TaskType}.
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Lemma arr_seq_consistent :
arr_seq_job_arrival_consistent.
Proof.
intros ? ? ?; split; [intros EQ | ].
{ by rewrite mem_filter EQ eq_refl andTb mem_index_enum. }
{ rewrite mem_filter ⇒ /andP [MA IN].
destruct (job_arrival j ω) eqn:ARR; last by done.
by move: MA ⇒ /eqP EQ; subst.
}
Qed.
Lemma pr_consistent_arrival_times :
∀ (ω : Ω),
@consistent_arrival_times
Job
(fun j ⇒ odflt0 (job_arrival j) ω)
(arr_seq ω).
Proof.
intros ? ? ?; unfold arrives_at, arrivals_at ⇒ ARR.
apply arr_seq_consistent in ARR.
by rewrite /prosa.behavior.job.job_arrival //= ARR.
Qed.
End Consistent.
Global Opaque arr_seq arrival_sequence.