Library prosa.classic.model.arrival.basic.arrival_sequence
Require Import prosa.classic.util.all prosa.classic.model.arrival.basic.task prosa.classic.model.time.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module ArrivalSequence.
Export Time.
Section ArrivalSequenceDef.
Variable Job: eqType.
Definition arrival_sequence := time → seq Job.
End ArrivalSequenceDef.
Section JobProperties.
Context {Job: eqType}.
Variable arr_seq: arrival_sequence Job.
Definition jobs_arriving_at (t: time) := arr_seq t.
Definition arrives_at (j: Job) (t: time) := j \in jobs_arriving_at t.
Definition arrives_in (j: Job) := ∃ t, j \in jobs_arriving_at t.
End JobProperties.
Section ArrivalSequenceProperties.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable arr_seq: arrival_sequence Job.
Definition arrival_times_are_consistent :=
∀ j t,
arrives_at arr_seq j t → job_arrival j = t.
Definition arrival_sequence_is_a_set := ∀ t, uniq (jobs_arriving_at arr_seq t).
End ArrivalSequenceProperties.
Section PropertiesOfArrivalTime.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable j: Job.
Definition has_arrived (t: time) := job_arrival j ≤ t.
Definition arrived_before (t: time) := job_arrival j < t.
Definition arrived_between (t1 t2: time) := t1 ≤ job_arrival j < t2.
End PropertiesOfArrivalTime.
Section ArrivalSequencePrefix.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable arr_seq: arrival_sequence Job.
Definition jobs_arrived_between (t1 t2: time) :=
\cat_(t1 ≤ t < t2) jobs_arriving_at arr_seq t.
Definition jobs_arrived_up_to (t: time) := jobs_arrived_between 0 t.+1.
Definition jobs_arrived_before (t: time) := jobs_arrived_between 0 t.
Section Lemmas.
Section Basic.
Lemma job_arrived_between_cat:
∀ t1 t t2,
t1 ≤ t →
t ≤ t2 →
jobs_arrived_between t1 t2 = jobs_arrived_between t1 t ++ jobs_arrived_between t t2.
Lemma jobs_arrived_between_mem_cat:
∀ j t1 t t2,
t1 ≤ t →
t ≤ t2 →
j \in jobs_arrived_between t1 t2 =
(j \in jobs_arrived_between t1 t ++ jobs_arrived_between t t2).
Lemma jobs_arrived_between_sub:
∀ j t1 t1' t2 t2',
t1' ≤ t1 →
t2 ≤ t2' →
j \in jobs_arrived_between t1 t2 →
j \in jobs_arrived_between t1' t2'.
End Basic.
Section ArrivalTimes.
Hypothesis H_arrival_times_are_consistent:
arrival_times_are_consistent job_arrival arr_seq.
Lemma in_arrivals_implies_arrived:
∀ j t1 t2,
j \in jobs_arrived_between t1 t2 →
arrives_in arr_seq j.
Lemma in_arrivals_implies_arrived_between:
∀ j t1 t2,
j \in jobs_arrived_between t1 t2 →
arrived_between job_arrival j t1 t2.
Lemma in_arrivals_implies_arrived_before:
∀ j t,
j \in jobs_arrived_before t →
arrived_before job_arrival j t.
Lemma arrived_between_implies_in_arrivals:
∀ j t1 t2,
arrives_in arr_seq j →
arrived_between job_arrival j t1 t2 →
j \in jobs_arrived_between t1 t2.
Lemma arrivals_uniq :
arrival_sequence_is_a_set arr_seq →
∀ t1 t2, uniq (jobs_arrived_between t1 t2).
End ArrivalTimes.
End Lemmas.
End ArrivalSequencePrefix.
End ArrivalSequence.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module ArrivalSequence.
Export Time.
Section ArrivalSequenceDef.
Variable Job: eqType.
Definition arrival_sequence := time → seq Job.
End ArrivalSequenceDef.
Section JobProperties.
Context {Job: eqType}.
Variable arr_seq: arrival_sequence Job.
Definition jobs_arriving_at (t: time) := arr_seq t.
Definition arrives_at (j: Job) (t: time) := j \in jobs_arriving_at t.
Definition arrives_in (j: Job) := ∃ t, j \in jobs_arriving_at t.
End JobProperties.
Section ArrivalSequenceProperties.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable arr_seq: arrival_sequence Job.
Definition arrival_times_are_consistent :=
∀ j t,
arrives_at arr_seq j t → job_arrival j = t.
Definition arrival_sequence_is_a_set := ∀ t, uniq (jobs_arriving_at arr_seq t).
End ArrivalSequenceProperties.
Section PropertiesOfArrivalTime.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable j: Job.
Definition has_arrived (t: time) := job_arrival j ≤ t.
Definition arrived_before (t: time) := job_arrival j < t.
Definition arrived_between (t1 t2: time) := t1 ≤ job_arrival j < t2.
End PropertiesOfArrivalTime.
Section ArrivalSequencePrefix.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable arr_seq: arrival_sequence Job.
Definition jobs_arrived_between (t1 t2: time) :=
\cat_(t1 ≤ t < t2) jobs_arriving_at arr_seq t.
Definition jobs_arrived_up_to (t: time) := jobs_arrived_between 0 t.+1.
Definition jobs_arrived_before (t: time) := jobs_arrived_between 0 t.
Section Lemmas.
Section Basic.
Lemma job_arrived_between_cat:
∀ t1 t t2,
t1 ≤ t →
t ≤ t2 →
jobs_arrived_between t1 t2 = jobs_arrived_between t1 t ++ jobs_arrived_between t t2.
Lemma jobs_arrived_between_mem_cat:
∀ j t1 t t2,
t1 ≤ t →
t ≤ t2 →
j \in jobs_arrived_between t1 t2 =
(j \in jobs_arrived_between t1 t ++ jobs_arrived_between t t2).
Lemma jobs_arrived_between_sub:
∀ j t1 t1' t2 t2',
t1' ≤ t1 →
t2 ≤ t2' →
j \in jobs_arrived_between t1 t2 →
j \in jobs_arrived_between t1' t2'.
End Basic.
Section ArrivalTimes.
Hypothesis H_arrival_times_are_consistent:
arrival_times_are_consistent job_arrival arr_seq.
Lemma in_arrivals_implies_arrived:
∀ j t1 t2,
j \in jobs_arrived_between t1 t2 →
arrives_in arr_seq j.
Lemma in_arrivals_implies_arrived_between:
∀ j t1 t2,
j \in jobs_arrived_between t1 t2 →
arrived_between job_arrival j t1 t2.
Lemma in_arrivals_implies_arrived_before:
∀ j t,
j \in jobs_arrived_before t →
arrived_before job_arrival j t.
Lemma arrived_between_implies_in_arrivals:
∀ j t1 t2,
arrives_in arr_seq j →
arrived_between job_arrival j t1 t2 →
j \in jobs_arrived_between t1 t2.
Lemma arrivals_uniq :
arrival_sequence_is_a_set arr_seq →
∀ t1 t2, uniq (jobs_arrived_between t1 t2).
End ArrivalTimes.
End Lemmas.
End ArrivalSequencePrefix.
End ArrivalSequence.