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. It is required by coq-proba library that codomain is an eqType; however, an arrival sequence is a function, which means that there is no decidable equality defined on schedules. Similarly to pr_schedule, we resolve this issue using classical logic. However, unlike the pr_schedule, Coq is able to derive eqType automatically due to the simpler definition of an arrival sequence.

Additional Definitions

job_arrival → pr_arrival_sequence for Job : Finite

If Job is a finType, one can derive a probabilistic arrival sequence from JobArrivalRV.

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.

Lemmas