Library prosa.classic.model.arrival.jitter.arrival_sequence
Require Import prosa.classic.util.all prosa.classic.model.arrival.basic.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module ArrivalSequenceWithJitter.
Export ArrivalSequence.
Section ActualArrival.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_jitter: Job → time.
Variable j: Job.
Definition actual_arrival := job_arrival j + job_jitter j.
Definition jitter_has_passed (t: time) := actual_arrival ≤ t.
Definition actual_arrival_before (t: time) := actual_arrival < t.
Definition actual_arrival_between (t1 t2: time) :=
t1 ≤ actual_arrival < t2.
End ActualArrival.
Section ArrivingJobs.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_jitter: Job → time.
Variable arr_seq: arrival_sequence Job.
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
Let actual_job_arrival_between := actual_arrival_between job_arrival job_jitter.
Let actual_job_arrival_before := actual_arrival_before job_arrival job_jitter.
Let arrivals_before := jobs_arrived_before arr_seq.
Definition actual_arrivals_between (t1 t2: time) :=
[seq j <- arrivals_before t2 | t1 ≤ actual_job_arrival j < t2].
Definition actual_arrivals_up_to (t: time) := actual_arrivals_between 0 t.+1.
Definition actual_arrivals_before (t: time) := actual_arrivals_between 0 t.
Section Lemmas.
Hypothesis H_arrival_times_are_consistent:
arrival_times_are_consistent job_arrival arr_seq.
Section Basic.
Lemma actual_arrivals_between_mem_cat:
∀ j t1 t t2,
t1 ≤ t →
t ≤ t2 →
j \in actual_arrivals_between t1 t2 =
(j \in actual_arrivals_between t1 t ++ actual_arrivals_between t t2).
Lemma actual_arrivals_between_sub:
∀ j t1 t1' t2 t2',
t1' ≤ t1 →
t2 ≤ t2' →
j \in actual_arrivals_between t1 t2 →
j \in actual_arrivals_between t1' t2'.
End Basic.
Section ArrivalTimes.
Lemma in_actual_arrivals_between_implies_arrived:
∀ j t1 t2,
j \in actual_arrivals_between t1 t2 →
arrives_in arr_seq j.
Lemma in_actual_arrivals_before_implies_arrived:
∀ j t,
j \in actual_arrivals_before t →
arrives_in arr_seq j.
Lemma in_actual_arrivals_implies_arrived_before:
∀ j t,
j \in actual_arrivals_before t →
actual_job_arrival_before j t.
Lemma in_actual_arrivals_implies_arrived_between:
∀ j t1 t2,
j \in actual_arrivals_between t1 t2 →
actual_job_arrival_between j t1 t2.
Lemma arrived_between_implies_in_actual_arrivals:
∀ j t1 t2,
arrives_in arr_seq j →
actual_job_arrival_between j t1 t2 →
j \in actual_arrivals_between t1 t2.
Lemma actual_arrivals_uniq :
arrival_sequence_is_a_set arr_seq →
∀ t1 t2, uniq (actual_arrivals_between t1 t2).
End ArrivalTimes.
End Lemmas.
End ArrivingJobs.
End ArrivalSequenceWithJitter.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module ArrivalSequenceWithJitter.
Export ArrivalSequence.
Section ActualArrival.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_jitter: Job → time.
Variable j: Job.
Definition actual_arrival := job_arrival j + job_jitter j.
Definition jitter_has_passed (t: time) := actual_arrival ≤ t.
Definition actual_arrival_before (t: time) := actual_arrival < t.
Definition actual_arrival_between (t1 t2: time) :=
t1 ≤ actual_arrival < t2.
End ActualArrival.
Section ArrivingJobs.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_jitter: Job → time.
Variable arr_seq: arrival_sequence Job.
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
Let actual_job_arrival_between := actual_arrival_between job_arrival job_jitter.
Let actual_job_arrival_before := actual_arrival_before job_arrival job_jitter.
Let arrivals_before := jobs_arrived_before arr_seq.
Definition actual_arrivals_between (t1 t2: time) :=
[seq j <- arrivals_before t2 | t1 ≤ actual_job_arrival j < t2].
Definition actual_arrivals_up_to (t: time) := actual_arrivals_between 0 t.+1.
Definition actual_arrivals_before (t: time) := actual_arrivals_between 0 t.
Section Lemmas.
Hypothesis H_arrival_times_are_consistent:
arrival_times_are_consistent job_arrival arr_seq.
Section Basic.
Lemma actual_arrivals_between_mem_cat:
∀ j t1 t t2,
t1 ≤ t →
t ≤ t2 →
j \in actual_arrivals_between t1 t2 =
(j \in actual_arrivals_between t1 t ++ actual_arrivals_between t t2).
Lemma actual_arrivals_between_sub:
∀ j t1 t1' t2 t2',
t1' ≤ t1 →
t2 ≤ t2' →
j \in actual_arrivals_between t1 t2 →
j \in actual_arrivals_between t1' t2'.
End Basic.
Section ArrivalTimes.
Lemma in_actual_arrivals_between_implies_arrived:
∀ j t1 t2,
j \in actual_arrivals_between t1 t2 →
arrives_in arr_seq j.
Lemma in_actual_arrivals_before_implies_arrived:
∀ j t,
j \in actual_arrivals_before t →
arrives_in arr_seq j.
Lemma in_actual_arrivals_implies_arrived_before:
∀ j t,
j \in actual_arrivals_before t →
actual_job_arrival_before j t.
Lemma in_actual_arrivals_implies_arrived_between:
∀ j t1 t2,
j \in actual_arrivals_between t1 t2 →
actual_job_arrival_between j t1 t2.
Lemma arrived_between_implies_in_actual_arrivals:
∀ j t1 t2,
arrives_in arr_seq j →
actual_job_arrival_between j t1 t2 →
j \in actual_arrivals_between t1 t2.
Lemma actual_arrivals_uniq :
arrival_sequence_is_a_set arr_seq →
∀ t1 t2, uniq (actual_arrivals_between t1 t2).
End ArrivalTimes.
End Lemmas.
End ArrivingJobs.
End ArrivalSequenceWithJitter.