Library probsa.rt.model.events
From prosa Require Export util.all.
From prosa Require Export behavior.all.
From probsa.util Require Export boolp.
From probsa.probability Require Export partition.
From probsa.rt.behavior Require Export job arrival_sequence.
From mathcomp Require Import finfun.
From prosa Require Export behavior.all.
From probsa.util Require Export boolp.
From probsa.probability Require Export partition.
From probsa.rt.behavior Require Export job arrival_sequence.
From mathcomp Require Import finfun.
Fixed Arrival Sequence
Given a probability space (Ω,μ) and a job type Job, function ξ_fix returns an event E ⊆ Ω in which the arrival-sequence random variable ξ_pr is equal to some fixed (deterministic) arrival sequence ξ.
Definition ξ_fix {Ω} {μ : measure Ω} {Job : JobType}
(ξ_pr : pr_arrival_sequence μ Job) (ξ : arrival_sequence Job) : pred Ω :=
fun ω : Ω ⇒ ξ_pr ω == ξ.
(ξ_pr : pr_arrival_sequence μ Job) (ξ : arrival_sequence Job) : pred Ω :=
fun ω : Ω ⇒ ξ_pr ω == ξ.
Fixed Job Costs
Given a probability space (Ω, μ), an assignment of costs 𝗖 to jobs, and a set of jobs jobs, the term 𝓒_fix 𝗖 jobs denotes an event E ⊆ Ω where the costs of jobs in jobs agree with the assignment of 𝗖.
Definition 𝓒_fix {Ω} {μ : measure Ω} {Job : JobType} {job_cost : JobCostRV Job Ω μ}
(𝗖 : Job → option work) (jobs : seq Job) : pred Ω :=
fun ω : Ω ⇒ all (fun j : Job ⇒ sample_costs ω j == 𝗖 j) jobs.
(𝗖 : Job → option work) (jobs : seq Job) : pred Ω :=
fun ω : Ω ⇒ all (fun j : Job ⇒ sample_costs ω j == 𝗖 j) jobs.
Partitions
In addition to the aforementioned straightforward events, one can construct partitions over arrival sequences and sequences of job costs of a fixed set of jobs.Partition on Arrival Sequences
In this section, we define a construction for a partition S of a sample space on arrival sequences. Each event S◁{ξ} of the partition is an event with a fixed arrival sequence ξ.
Section ArrivalsPartition.
Context {Ω} (μ : measure Ω).
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}.
Context {Ω} (μ : measure Ω).
Context {Job : finType}
{job_arrival : JobArrivalRV Job Ω μ}.
Program Definition partition_on_ξ : @Ω_partition Ω μ :=
{|
I := [countType of imgT arr_seq];
p := fun ξ ω ⇒ arr_seq ω == sval ξ
|}.
Next Obligation.
by rewrite /sval //=; unshelve eexists;
first (apply exist with (x := arr_seq ω); rewrite unfold_in; apply/exCP; ∃ ω).
Qed.
Next Obligation.
move: i j H H0 ⇒ [ξ1 IN1] [ξ2 IN2] ⇒ //=.
move ⇒ /eqP EQ1 /eqP EQ2; subst.
by f_equal; apply classical_proof_irrelevance.
Qed.
End ArrivalsPartition.
{|
I := [countType of imgT arr_seq];
p := fun ξ ω ⇒ arr_seq ω == sval ξ
|}.
Next Obligation.
by rewrite /sval //=; unshelve eexists;
first (apply exist with (x := arr_seq ω); rewrite unfold_in; apply/exCP; ∃ ω).
Qed.
Next Obligation.
move: i j H H0 ⇒ [ξ1 IN1] [ξ2 IN2] ⇒ //=.
move ⇒ /eqP EQ1 /eqP EQ2; subst.
by f_equal; apply classical_proof_irrelevance.
Qed.
End ArrivalsPartition.
Partition on Job Costs
In this section, we define a construction for a partition {S_i} of a sample space on (1) costs of a single job and (2) costs of a finite set of jobs.
Section CostPartition.
Context {Ω} (μ : measure Ω).
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}.
Context {Ω} (μ : measure Ω).
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}.
Consider a job j. First, we define a partition S of Ω into
events where the job cost of j is fixed. We define index of
the partition as all job costs None, Some 0, Some 1, .... In
other words, an event S◁{Some 2} contains ωs such that
job_cost j ω = Some 2.
Program Definition partition_on_𝓒 (j : Job) : @Ω_partition Ω μ :=
{|
I := [countType of option nat];
p := fun (c : option work) (ω : Ω) ⇒ job_cost j ω == c
|}.
Next Obligation.
eexists; apply/eqP; reflexivity.
Qed.
Next Obligation.
by move: H H0 ⇒ /eqP → /eqP →.
Qed.
{|
I := [countType of option nat];
p := fun (c : option work) (ω : Ω) ⇒ job_cost j ω == c
|}.
Next Obligation.
eexists; apply/eqP; reflexivity.
Qed.
Next Obligation.
by move: H H0 ⇒ /eqP → /eqP →.
Qed.
Consider a set of jobs jobs. We define a partition of Ω into
events where job costs of these jobs are fixed. Index of the
partition is all functions that map a job from jobs to its
cost (i.e., [jobs] → option work).
Program Definition partition_on_𝓒s (jobs : seq Job) : @Ω_partition Ω μ :=
{|
I := [countType of { ffun (seq_sub jobs) → [countType of option work] }];
p := fun 𝓒 ω ⇒ [∀ j : seq_sub jobs, 𝓒 j == job_cost (ssval j) ω]
|}.
Next Obligation.
rename H into POS.
∃ (FinfunOf (Phant (seq_sub (T:=Job) jobs → option nat))
(finfun.finfun_rec
(aT:=seq_sub_finType (T:=Job) jobs)
(rT:=fun⇒ option nat)
(λ x : seq_sub_finType (T:=Job) jobs,
match x with
| {| ssval := j |} ⇒ job_cost j ω
end)
(enum (seq_sub_finType (T:=Job) jobs)))
).
apply/forallP ⇒ [[j IN]].
simpl; set s := enum _; set s_x : mem_seq s _ := mem_enum _ _.
elim: s s_x ⇒ //= x1 s IHs; case: eqP ⇒ [|_]; [case: x1 / | apply: IHs].
by move ⇒ _.
Qed.
Next Obligation.
rename i into f1, j into f2; apply ffunP ⇒ j.
move: H H0 ⇒ /forallP ALL1 /forallP ALL2.
by move: (ALL1 j) (ALL2 j) ⇒ /eqP → /eqP →.
Qed.
End CostPartition.
{|
I := [countType of { ffun (seq_sub jobs) → [countType of option work] }];
p := fun 𝓒 ω ⇒ [∀ j : seq_sub jobs, 𝓒 j == job_cost (ssval j) ω]
|}.
Next Obligation.
rename H into POS.
∃ (FinfunOf (Phant (seq_sub (T:=Job) jobs → option nat))
(finfun.finfun_rec
(aT:=seq_sub_finType (T:=Job) jobs)
(rT:=fun⇒ option nat)
(λ x : seq_sub_finType (T:=Job) jobs,
match x with
| {| ssval := j |} ⇒ job_cost j ω
end)
(enum (seq_sub_finType (T:=Job) jobs)))
).
apply/forallP ⇒ [[j IN]].
simpl; set s := enum _; set s_x : mem_seq s _ := mem_enum _ _.
elim: s s_x ⇒ //= x1 s IHs; case: eqP ⇒ [|_]; [case: x1 / | apply: IHs].
by move ⇒ _.
Qed.
Next Obligation.
rename i into f1, j into f2; apply ffunP ⇒ j.
move: H H0 ⇒ /forallP ALL1 /forallP ALL2.
by move: (ALL1 j) (ALL2 j) ⇒ /eqP → /eqP →.
Qed.
End CostPartition.