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.
Proof.
unfold jobs_arrived_between; intros t1 t t2 GE LE.
by rewrite (@big_cat_nat _ _ _ t).
Qed.
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).
Proof.
by intros j t1 t t2 GE LE; rewrite (job_arrived_between_cat _ t).
Qed.
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'.
Proof.
intros j t1 t1' t2 t2' GE1 LE2 IN.
move: (leq_total t1 t2) ⇒ /orP [BEFORE | AFTER];
last by rewrite /jobs_arrived_between big_geq // in IN.
rewrite /jobs_arrived_between.
rewrite → big_cat_nat with (n := t1); [simpl | by done | by apply: (leq_trans BEFORE)].
rewrite mem_cat; apply/orP; right.
rewrite → big_cat_nat with (n := t2); [simpl | by done | by done].
by rewrite mem_cat; apply/orP; left.
Qed.
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.
Proof.
rename H_arrival_times_are_consistent into CONS.
intros j t1 t2 IN.
apply mem_bigcat_nat_exists in IN.
move: IN ⇒ [arr [IN _]].
by ∃ arr.
Qed.
Lemma in_arrivals_implies_arrived_between:
∀ j t1 t2,
j \in jobs_arrived_between t1 t2 →
arrived_between job_arrival j t1 t2.
Proof.
rename H_arrival_times_are_consistent into CONS.
intros j t1 t2 IN.
apply mem_bigcat_nat_exists in IN.
move: IN ⇒ [t0 [IN /= LT]].
by apply CONS in IN; rewrite /arrived_between IN.
Qed.
Lemma in_arrivals_implies_arrived_before:
∀ j t,
j \in jobs_arrived_before t →
arrived_before job_arrival j t.
Proof.
intros j t IN.
suff: arrived_between job_arrival j 0 t by rewrite /arrived_between /=.
by apply in_arrivals_implies_arrived_between.
Qed.
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.
Proof.
rename H_arrival_times_are_consistent into CONS.
move ⇒ j t1 t2 [a_j ARRj] BEFORE.
have SAME := ARRj; apply CONS in SAME; subst a_j.
by apply mem_bigcat_nat with (j := (job_arrival j)).
Qed.
Lemma arrivals_uniq :
arrival_sequence_is_a_set arr_seq →
∀ t1 t2, uniq (jobs_arrived_between t1 t2).
Proof.
rename H_arrival_times_are_consistent into CONS.
unfold jobs_arrived_up_to; intros SET t1 t2.
apply bigcat_nat_uniq; first by done.
intros x t t' IN1 IN2.
by apply CONS in IN1; apply CONS in IN2; subst.
Qed.
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.
Proof.
unfold jobs_arrived_between; intros t1 t t2 GE LE.
by rewrite (@big_cat_nat _ _ _ t).
Qed.
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).
Proof.
by intros j t1 t t2 GE LE; rewrite (job_arrived_between_cat _ t).
Qed.
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'.
Proof.
intros j t1 t1' t2 t2' GE1 LE2 IN.
move: (leq_total t1 t2) ⇒ /orP [BEFORE | AFTER];
last by rewrite /jobs_arrived_between big_geq // in IN.
rewrite /jobs_arrived_between.
rewrite → big_cat_nat with (n := t1); [simpl | by done | by apply: (leq_trans BEFORE)].
rewrite mem_cat; apply/orP; right.
rewrite → big_cat_nat with (n := t2); [simpl | by done | by done].
by rewrite mem_cat; apply/orP; left.
Qed.
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.
Proof.
rename H_arrival_times_are_consistent into CONS.
intros j t1 t2 IN.
apply mem_bigcat_nat_exists in IN.
move: IN ⇒ [arr [IN _]].
by ∃ arr.
Qed.
Lemma in_arrivals_implies_arrived_between:
∀ j t1 t2,
j \in jobs_arrived_between t1 t2 →
arrived_between job_arrival j t1 t2.
Proof.
rename H_arrival_times_are_consistent into CONS.
intros j t1 t2 IN.
apply mem_bigcat_nat_exists in IN.
move: IN ⇒ [t0 [IN /= LT]].
by apply CONS in IN; rewrite /arrived_between IN.
Qed.
Lemma in_arrivals_implies_arrived_before:
∀ j t,
j \in jobs_arrived_before t →
arrived_before job_arrival j t.
Proof.
intros j t IN.
suff: arrived_between job_arrival j 0 t by rewrite /arrived_between /=.
by apply in_arrivals_implies_arrived_between.
Qed.
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.
Proof.
rename H_arrival_times_are_consistent into CONS.
move ⇒ j t1 t2 [a_j ARRj] BEFORE.
have SAME := ARRj; apply CONS in SAME; subst a_j.
by apply mem_bigcat_nat with (j := (job_arrival j)).
Qed.
Lemma arrivals_uniq :
arrival_sequence_is_a_set arr_seq →
∀ t1 t2, uniq (jobs_arrived_between t1 t2).
Proof.
rename H_arrival_times_are_consistent into CONS.
unfold jobs_arrived_up_to; intros SET t1 t2.
apply bigcat_nat_uniq; first by done.
intros x t t' IN1 IN2.
by apply CONS in IN1; apply CONS in IN2; subst.
Qed.
End ArrivalTimes.
End Lemmas.
End ArrivalSequencePrefix.
End ArrivalSequence.