# Library prosa.analysis.facts.periodic.arrival_times

In this module, we'll prove the known arrival times of jobs that stem from periodic tasks.
Consider periodic tasks with an offset ...

... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobArrival Job}.

Consider any unique arrival sequence with consistent arrivals ...
... and any periodic task tsk with a valid offset and period.
Variable tsk : Task.
Hypothesis H_valid_offset: valid_offset arr_seq tsk.
Hypothesis H_valid_period: valid_period tsk.

We show that the nth job j of task tsk arrives at the instant task_offset tsk + n × task_period tsk.
Lemma periodic_arrival_times:
n (j : Job),
arrives_in arr_seq j
job_task j = tsk
job_index arr_seq j = n
job_arrival j = task_offset tsk + n × task_period tsk.
Proof.
elim⇒ [|n IHn].
{ intros j ARR TSK_IN ZINDEX.
exact: first_job_arrival ZINDEX.
}
{ intros j ARR TSK_IN JB_INDEX.
move : (H_task_respects_periodic_model j ARR) ⇒ PREV_JOB.
feed_n 2 PREV_JOB ⇒ //.
move : PREV_JOB ⇒ [pj [ARR' [IND [TSK ARRIVAL]]]].
specialize (IHn pj); feed_n 3 IHn ⇒ //; first by rewrite IND JB_INDEX; lia.
rewrite ARRIVAL IHn; lia.
}
Qed.

We show that for every job j of task tsk there exists a number n such that j arrives at the instant task_offset tsk + n × task_period tsk.
Lemma job_arrival_times:
j,
arrives_in arr_seq j
job_task j = tsk
n, job_arrival j = task_offset tsk + n × task_period tsk.
Proof.
movej ARR TSK.
(job_index arr_seq j).
specialize (periodic_arrival_times (job_index arr_seq j) j) ⇒ J_ARR.
by feed_n 3 J_ARR ⇒ //.
Qed.

If a job j of task tsk arrives at task_offset tsk + n × task_period tsk then the job_index of j is equal to n.
Lemma job_arr_index:
n j,
arrives_in arr_seq j
job_task j = tsk
job_arrival j = task_offset tsk + n × task_period tsk
job_index arr_seq j = n.
Proof.
have F : task_period tsk > 0 by auto.
elim⇒ [|n IHn].
+ movej ARR_J TSK ARR.
destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]] ⇒ //.
by apply periodic_arrival_times in SUCC ⇒ //; lia.
+ movej ARR_J TSK ARR.
specialize (H_task_respects_periodic_model j); feed_n 3 H_task_respects_periodic_model ⇒ //.
{ rewrite lt0n; apply /eqP; intro EQ.
apply (first_job_arrival _ H_valid_arrival_sequence tsk) in EQ ⇒ //.
by rewrite EQ in ARR; lia.
}
move : H_task_respects_periodic_model ⇒ [j' [ARR' [IND' [TSK' ARRIVAL']]]].
specialize (IHn j'); feed_n 3 IHn ⇒ //; first by rewrite ARR in ARRIVAL'; lia.
rewrite IHn in IND'.
destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]]; last by lia.
rewrite (first_job_arrival arr_seq _ tsk)// in ARR.
lia.
Qed.

End PeriodicArrivalTimes.