In this file we prove some properties concerning the size of task arrivals in context of the periodic model.

Consider any type of 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.
We show that if an instant t is not an "arrival time" for task tsk then task_arrivals_at arr_seq tsk t is an empty sequence.
t,
task_arrivals_at arr_seq tsk t = [::].
Proof.
movet T.
have EMPT_OR_EXISTS : xs, xs = [::] a, a \in xs.
{ movet0; elim⇒ [|a xs IHxs]; first by left.
right; a.
}
destruct (EMPT_OR_EXISTS Job (task_arrivals_at arr_seq tsk t)) as [EMPT | [a A_IN]] ⇒ //.
rewrite /task_arrivals_at mem_filter in A_IN; move : A_IN ⇒ /andP [/eqP TSK A_ARR].
move : H_valid_arrival_sequence ⇒ [CONSISTENT UNIQ].
move : (A_ARR) ⇒ A_IN; apply CONSISTENT in A_IN.
rewrite -A_IN in T; rewrite /arrivals_at in A_ARR.
apply in_arrseq_implies_arrives in A_ARR.
have EXISTS_N : n, job_arrival a = task_offset tsk + n × task_period tsk.
exact: (job_arrival_times arr_seq).
move : EXISTS_N ⇒ [n A_ARRIVAL].
by move : (T n) ⇒ T1.
Qed.

We show that at any instant t, at most one job of task tsk can arrive (i.e. size of task_arrivals_at arr_seq tsk t is at most one).
t,
size (task_arrivals_at arr_seq tsk t) = 0
size (task_arrivals_at arr_seq tsk t) = 1.
Proof.
intro t.
case: (ltngtP (size (task_arrivals_at arr_seq tsk t)) 1) ⇒ [LT|GT|EQ]; try by auto.
destruct (size (task_arrivals_at arr_seq tsk t)); now left.
specialize (exists_two (task_arrivals_at arr_seq tsk t)) ⇒ EXISTS_TWO.
move : H_valid_arrival_sequence ⇒ [CONSISTENT UNIQ].
destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by [] | by apply filter_uniq | ].
rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.
move: A_IN B_IN ⇒ /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].
move: (ARRA); move: (ARRB); rewrite /arrivals_atA_IN B_IN.
apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
have EQ_ARR_A : (job_arrival a = t) by [].
have EQ_ARR_B : (job_arrival b = t) by [].
specialize (SPO a b); feed_n 6 SPO ⇒ //; first lia.
rewrite EQ_ARR_A EQ_ARR_B in SPO.
have POS : task_period tsk > 0 by [].
lia.
Qed.

We show that the size of task arrivals (strictly) between two consecutive arrival times is zero.
n,
size (task_arrivals_between arr_seq tsk l r) = 0.
Proof.
intros n l r; rewrite /l /r.
rewrite size_of_task_arrivals_between big_nat_eq0 ⇒ //; intros t INEQ.
rewrite task_arrivals_size_at_non_arrival ⇒ //; intros n1 EQ.
rewrite EQ in INEQ.
move : INEQ ⇒ /andP [INEQ1 INEQ2].
move : INEQ1 INEQ2 ⇒ /andP [A B] /andP [C D].
by lia.
Qed.

In this section we show some properties of task arrivals in case of an infinite sequence of jobs.
Assume that we have an infinite sequence of jobs.
Hypothesis H_infinite_jobs : infinite_jobs arr_seq.

We show that for any number n, there exists a job j of task tsk such that job_index of j is equal to n and j arrives at task_offset tsk + n × task_period tsk.
Lemma jobs_exists_later:
n,
j,
arrives_in arr_seq j
job_index arr_seq j = n.
Proof.
moven.
destruct (H_infinite_jobs tsk n) as [j [ARR [TSK IND]]].
j; repeat split ⇒ //.
exact: (periodic_arrival_times arr_seq).
Qed.

We show that the size of task arrivals at any arrival time is equal to one.
n,
size (task_arrivals_at arr_seq tsk l) = 1.
Proof.
intros n l; rewrite /l.
move : (jobs_exists_later n) ⇒ [j' [ARR [TSK [ARRIVAL IND]]]].
arr_seq H_valid_arrival_sequence tsk) in ARR ⇒ //.
by rewrite -ARRIVAL ARR.
Qed.

We show that the size of task arrivals up to task_offset tsk is equal to one.
Proof.
feed_n 2 CAT ⇒ //; rewrite CAT size_cat.
have Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0.
{ rewrite size_of_task_arrivals_between big_nat_eq0 ⇒ //; intros t T_EQ.
rewrite task_arrivals_size_at_non_arrival ⇒ //; intros n EQ.
by lia.
}
by rewrite mul0n addn0 in AT_SIZE.
Qed.

We show that for any number n, the number of jobs released by task tsk up to task_offset tsk + n × task_period tsk is equal to n + 1.
n,
size (task_arrivals_up_to arr_seq tsk l) = n + 1.
Proof.
elim⇒ [|n IHn].
intros l r.
feed_n 1 CAT; first by lia.
rewrite CAT size_cat IHn.
feed_n 2 S_CAT; try by lia.
by apply /andP; split ⇒ //.
}
rewrite S_CAT size_cat /task_arrivals_between /arrivals_between big_nat1.
by lia.
Qed.

We show that the number of jobs released by task tsk at any instant t and t + n × task_period tsk is the same for any number n.
n t,
size (task_arrivals_at arr_seq tsk t) =
Proof.
moven t o_le_t.
have [tmo_eq0|tmo_neq0] :=