# Library prosa.analysis.facts.hyperperiod

In this file we prove some simple properties of hyperperiods of periodic tasks.
Section Hyperperiod.

Consider any type of periodic tasks, ...

... any task set ts, ...

Hypothesis H_tsk_in_ts: tsk \in ts.

(k : nat),
hyperperiod ts = k × task_period tsk.
Proof. by apply/dvdnP; apply lcm_seq_is_mult_of_all_ints, map_f, H_tsk_in_ts. Qed.

End Hyperperiod.

In this section we show a property of hyperperiod in context of task sets with valid periods.
Consider any type of periodic tasks ...

... and any task set ts ...

... such that all tasks in ts have valid periods.
Hypothesis H_valid_periods: valid_periods ts.

We show that the hyperperiod of task set ts is positive.
Lemma valid_periods_imply_pos_hp:
hyperperiod ts > 0.
Proof.
apply all_pos_implies_lcml_pos.
moveb /mapP [x IN EQ]; subst b.
now apply H_valid_periods.
Qed.

End ValidPeriodsImplyPositiveHP.

In this section we prove some lemmas about the hyperperiod in context of the periodic model.
Section PeriodicLemmas.

Consider any type of tasks, ...

... any type of jobs, ...
Context {Job : JobType}.
Context `{JobArrival Job}.

... and a consistent arrival sequence with non-duplicate arrivals.
Consider a task set ts such that all tasks in ts have valid periods.
Hypothesis H_valid_periods: valid_periods ts.

Let tsk be any periodic task in ts with a valid offset and period.
Hypothesis H_valid_offset: valid_offset arr_seq tsk.
Hypothesis H_valid_period: valid_period tsk.

Assume we have an infinite sequence of jobs in the arrival sequence.
Let O_max denote the maximum task offset in ts and let HP denote the hyperperiod of all tasks in ts.
Let HP := hyperperiod ts.

We show that the job corresponding to any job j1 in any other hyperperiod is of the same task as j1.
j1 j2,
Proof.
movej1 j2.
(starting_instant_of_hyperperiod ts (job_arrival j2) + HP)).
set IND := (job_index_in_hyperperiod ts arr_seq j1 (starting_instant_of_hyperperiod ts (job_arrival j1)) (job_task j1)).
have SIZE_G : size ARRIVALS IND job_task (nth j1 ARRIVALS IND) = job_task j1 by intro SG; rewrite nth_default.
case: (boolP (size ARRIVALS == IND)) ⇒ [/eqP EQ|NEQ]; first by apply SIZE_G; lia.
move : NEQ; rewrite neq_ltn; move ⇒ /orP [LT | G]; first by apply SIZE_G; lia.
set jb := nth j1 ARRIVALS IND.
have JOB_IN : jb \in ARRIVALS by apply mem_nth.
rewrite /ARRIVALS /task_arrivals_between mem_filter in JOB_IN.
now move : JOB_IN ⇒ /andP [/eqP TSK JB_IN].
Qed.

We show that if a job j lies in the hyperperiod starting at instant t then j arrives in the interval `[t, t + HP)`.
Lemma all_jobs_arrive_within_hyperperiod:
j t,
j \in jobs_in_hyperperiod ts arr_seq t tsk
t job_arrival j < t + HP.
Proof.
intros × JB_IN_HP.
rewrite mem_filter in JB_IN_HP.
move : JB_IN_HP ⇒ /andP [/eqP TSK JB_IN]; apply mem_bigcat_nat_exists in JB_IN.
destruct JB_IN as [i [JB_IN INEQ]].
apply job_arrival_at in JB_IN ⇒ //.
by rewrite JB_IN.
Qed.

We show that the number of jobs in a hyperperiod starting at n1 × HP + O_max is the same as the number of jobs in a hyperperiod starting at n2 × HP + O_max given that n1 is less than or equal to n2.
Lemma eq_size_hyp_lt:
n1 n2,
n1 n2
size (jobs_in_hyperperiod ts arr_seq (n1 × HP + O_max) tsk) =
size (jobs_in_hyperperiod ts arr_seq (n2 × HP + O_max) tsk).
Proof.
moven1 n2 N1_LT.
have → : n2 × HP + O_max = n1 × HP + O_max + (n2 - n1) × HP.
{ by rewrite -[in LHS](subnKC N1_LT) mulnDl addnAC. }
rewrite [in X in _ = size (_ (n1 × HP + O_max + _ × X) tsk)]HYP.
erewrite big_sum_eq_in_eq_sized_intervals ⇒ //; intros g G_LT.
have OFF_G : task_offset tsk O_max by apply max_offset_g.
have FG : v b n, v + b + n = v + n + b by intros *; lia.
erewrite eq_size_of_task_arrivals_seperated_by_period ⇒ //; last lia.
by rewrite FG.
Qed.

We generalize the above lemma by lifting the condition on n1 and n2.
Lemma eq_size_of_arrivals_in_hyperperiod:
n1 n2,
size (jobs_in_hyperperiod ts arr_seq (n1 × HP + O_max) tsk) =
size (jobs_in_hyperperiod ts arr_seq (n2 × HP + O_max) tsk).
Proof.
moven1 n2.
case : (boolP (n1 == n2)) ⇒ [/eqP EQ | NEQ]; first by rewrite EQ.
move : NEQ; rewrite neq_ltn; move ⇒ /orP [LT | LT].
+ by apply eq_size_hyp_lt ⇒ //; lia.
+ move : (eq_size_hyp_lt n2 n1) ⇒ EQ_S.
by feed_n 1 EQ_S ⇒ //; lia.
Qed.

Consider any two jobs j1 and j2 that stem from the arrival sequence arr_seq such that j1 is of task tsk.
Variable j1 : Job.
Variable j2 : Job.
Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.

Assume that both j1 and j2 arrive after O_max.
We show that any job j that arrives in task arrivals in the same hyperperiod as j2 also arrives in task arrivals up to job_arrival j2 + HP.
j,
j \in jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP × HP + O_max) tsk
j \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP).
Proof.
intros j J_IN.
set jobs_in_hp := (jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP × HP + O_max) tsk).
move : (J_IN) ⇒ J_ARR; apply all_jobs_arrive_within_hyperperiod in J_IN.
move : J_ARR ⇒ /andP [/eqP TSK' NTH_IN].
by apply in_arrivals_implies_arrived in NTH_IN.
apply mem_bigcat_nat_exists in NTH_IN.
apply /andP; split ⇒ //.
rewrite ltnS.
apply leq_trans with (n := (job_arrival j2 - O_max) %/ HP × HP + O_max + HP); first by lia.
have O_M : (job_arrival j2 - O_max) %/ HP × HP job_arrival j2 - O_max by apply leq_trunc_div.
have ARR_G : job_arrival j2 O_max by [].
lia.
Qed.

We show that job j1 arrives in its own hyperperiod.
Lemma job_in_own_hp:
j1 \in jobs_in_hyperperiod ts arr_seq ((job_arrival j1 - O_max) %/ HP × HP + O_max) tsk.
Proof.
apply /andP; split.
+ rewrite addnC -leq_subRL ⇒ //.
by apply leq_trunc_div.
+ specialize (div_floor_add_g (job_arrival j1 - O_max) HP) ⇒ AB.
feed_n 1 AB; first by apply valid_periods_imply_pos_hp ⇒ //.
rewrite ltn_subLR // in AB.
by rewrite -/(HP); lia.
Qed.

We show that the corresponding_job_in_hyperperiod of j1 in j2's hyperperiod arrives in task arrivals up to job_arrival j2 + HP.
Finally, we show that the corresponding_job_in_hyperperiod of j1 in j2's hyperperiod arrives in the arrival sequence arr_seq.
Lemma corresponding_job_arrives:
arrives_in arr_seq (corresponding_job_in_hyperperiod ts arr_seq j1 (starting_instant_of_corresponding_hyperperiod ts j2) tsk).
Proof.
move : ARR_G ⇒ /andP [/eqP TSK' NTH_IN].
by apply in_arrivals_implies_arrived in NTH_IN.
Qed.

End PeriodicLemmas.