# Library prosa.implementation.facts.maximal_arrival_sequence

Recall that, given an arrival curve max_arrivals and a job-generating function generate_jobs_at, the function concrete_arrival_sequence generates an arrival sequence. In this section, we prove a few properties of this function.
Consider any type of tasks ...

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

Hypothesis H_ts_uniq : uniq ts.

Let max_arrivals be a family of valid arrival curves, i.e., for any task tsk in ts, max_arrival tsk is (1) an arrival bound of tsk, and (2) it is a monotonic function that equals 0 for the empty interval delta = 0.
Further assume we are given a function that generates the required number of jobs of a given task at a given instant of time.
First, we assume that generate_jobs_at tsk n t generates n jobs.
Hypothesis H_job_generation_valid_number:
(tsk : Task) (n : nat) (t : instant), tsk \in ts size (generate_jobs_at tsk n t) = n.

Second, we assume that generate_jobs_at tsk n t generates jobs of task tsk that arrive at time t.
Finally, we assume that all jobs generated by generate_jobs_at are unique.
Assuming such a well-behaved "constructor" generate_jobs_at, we prove a few validity claims about an arrival sequence generated by concrete_arrival_sequence.
Section ValidityClaims.

We start by showing that the obtained arrival sequence is a set.
Lemma arr_seq_is_a_set :
arrival_sequence_uniq (concrete_arrival_sequence generate_jobs_at ts).
Proof.
movet.
move: (H_jobs_unique t t.+1).
by rewrite /arrivals_between big_nat1.
Qed.

Next, we show that all jobs in the arrival sequence come from ts.
Proof.
movej [t /mem_bigcat_exists [tsk [TSK_IN IN]]].
move: (H_job_generation_valid_jobs tsk _ _ _ IN) ⇒ [JOB_TASK _].
Qed.

Further, we note that the jobs in the arrival sequence have consistent arrival times.
Lemma arrival_times_are_consistent :
consistent_arrival_times (concrete_arrival_sequence generate_jobs_at ts).
Proof.
movej t /mem_bigcat_exists [tsk [TSK_IN IN]].
by move: (H_job_generation_valid_jobs tsk _ _ _ IN) ⇒ [_ [JOB_ARR _]].
Qed.

Lastly, we observe that the jobs in the arrival sequence have valid job costs.
Lemma concrete_valid_job_cost :
arrivals_have_valid_job_costs (concrete_arrival_sequence generate_jobs_at ts).
Proof.
movej [t /mem_bigcat_exists [tsk [TSK_IN IN]]].
move: (H_job_generation_valid_jobs tsk _ _ _ IN) ⇒ [JOB_TASK [_ JOB_COST]].
Qed.

End ValidityClaims.

In this section, we prove a series of facts regarding the maximal arrival sequence, leading up to the main theorem that all arrival-curve constraints are respected.
Section Facts.

Let tsk be any task in ts that is to be analyzed.
Hypothesis H_tsk_in_ts : tsk \in ts.

First, we show that the arrivals at time t are indeed generated by generate_jobs_at applied at time t.
t,
task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t
= generate_jobs_at tsk (max_arrivals_at tsk t) t.
Proof.
movet.
rewrite /task_arrivals_at bigcat_filter_eq_filter_bigcat bigcat_seq_uniqK // ⇒ tsk0 j INj.
apply H_job_generation_valid_jobs in INj.
by destruct INj.
Qed.

Next, we show that the number of arrivals at time t always matches max_arrivals_at applied at time t.
t,
size (task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t)
= max_arrivals_at tsk t.
Proof. by movet; rewrite task_arrivals_at_eq_generate_jobs_at. Qed.

We then generalize the previous result to an arbitrary interval `[t1,t2)`.
We further show that, starting from an empty prefix and applying extend_arrival_prefix t times, we end up with a prefix of size t...
Lemma extend_horizon_size :
t,
size (iter t (extend_arrival_prefix tsk) [::]) = t.
Proof. by elim⇒ // t IHt; rewrite size_cat IHt //=; lia. Qed.

...and that the arrival sequence prefix up to an arbitrary horizon t is a sequence of t+1 elements.
Lemma prefix_up_to_size :
t,
size (maximal_arrival_prefix tsk t) = t.+1.
Proof.
by elim⇒ // t IHt; rewrite /maximal_arrival_prefix /extend_arrival_prefix size_cat IHt //=; lia.
Qed.

Next, we prove prefix inclusion for maximal_arrival_prefix when the horizon is expanded by one...
Lemma n_arrivals_at_prefix_inclusion1 :
t h,
t h
nth 0 (maximal_arrival_prefix tsk h) t
= nth 0 (maximal_arrival_prefix tsk h.+1) t.
Proof.
movet h LEQ.
rewrite /maximal_arrival_prefix //= {3}/extend_arrival_prefix nth_cat prefix_up_to_size.
by case: (ltnP t h.+1); lia.
Qed.

...and we generalize the previous result to two arbitrary horizons h1 h2.
Lemma n_arrivals_at_prefix_inclusion :
t h1 h2,
t h1 h2
nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t.
Proof.
movet h1 h2 /andP[LEQh1 LEQh2].
elim: h2 LEQh2 ⇒ [|h2 IHh2] LEQh2; [by have → : h1 = 0; lia |].
rewrite leq_eqVlt in LEQh2.
move: LEQh2 ⇒ /orP [/eqP EQ | LT]; first by rewrite EQ.
feed IHh2; first by lia.
rewrite -n_arrivals_at_prefix_inclusion1 //.
by lia.
Qed.

Next, we prove that, for any positive time instant t, max_arrivals_at indeed matches the arrivals of next_max_arrival applied at t-1.
Lemma max_arrivals_at_next_max_arrivals_eq:
t,
0 < t
max_arrivals_at tsk t
= next_max_arrival tsk (maximal_arrival_prefix tsk t.-1).
Proof.
movet GT0.
move: prefix_up_to_size; rewrite /maximal_arrival_prefixPUS.
rewrite /max_arrivals_at /maximal_arrival_prefix {1}/extend_arrival_prefix nth_cat extend_horizon_size //= ltnn //= subnn //=.
by destruct t.
Qed.

Given a time instant t and and interval Δ, we show that max_arrivals_at applied at time t is always less-or-equal to max_arrivals applied to Δ+1, even when each value of max_arrivals_at in the interval `[t-Δ, t)` is subtracted from it.
Lemma n_arrivals_at_leq :
t Δ,
Δ t
max_arrivals_at tsk t
max_arrivals tsk Δ.+1 - \sum_(t - Δ i < t) max_arrivals_at tsk i.
Proof.
movet Δ LEQ.
move: (H_valid_arrival_curve tsk H_tsk_in_ts) ⇒ [ZERO MONO].
destruct t as [|t].
{ rewrite unlock //= subn0.
rewrite /max_arrivals_at /maximal_arrival_prefix /extend_arrival_prefix
/next_max_arrival //= /suffix_sum subn0 unlock subn0.
by apply MONO. }
{ rewrite max_arrivals_at_next_max_arrivals_eq; last by done.
rewrite /next_max_arrival /jobs_remaining prefix_up_to_size.
simpl (t.+1.-1).
destruct supremum eqn:SUP; last by move:(supremum_none _ _ SUP); rewrite map_cons.
eapply (supremum_spec _ leqnn leq_total leq_trans _ _ SUP).
rewrite /suffix_sum prefix_up_to_size /max_arrivals_at.
have → : \sum_(t.+1 - Δ i < t.+1) nth 0 (maximal_arrival_prefix tsk i) i =
\sum_(t.+1 - Δ i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i.
{ apply eq_big_nati RANGE.
by apply n_arrivals_at_prefix_inclusion; lia. }
set f := fun xmax_arrivals _ x.+1 - \sum_(t.+1-x i < t.+1) nth 0 (maximal_arrival_prefix _ t) i.
have→ : max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i = f Δ by done.
apply map_f.
by rewrite mem_iota; lia. }
Qed.

End Facts.

Finally, we prove our main result, that is, the proposed maximal arrival sequence instantiation indeed respects all arrival-curve constraints.
Theorem concrete_is_arrival_curve :
Proof.
movetsk IN t1 t LEQ.
set Δ := t - t1.
replace t1 with (t-Δ); last by lia.
have LEQd: Δ t by lia.
generalize Δ LEQd; clear LEQ Δ LEQd.
elim: t ⇒ [|t IHt] Δ LEQ.
{ rewrite sub0n.
by vm_compute; rewrite unlock. }
destruct Δ as [|Δ]; first by rewrite /index_iota subnn; vm_compute; rewrite unlock.
rewrite subSS.
specialize (IHt Δ).
feed IHt; first by lia.
rewrite big_nat_recr //=; last by lia.
rewrite -leq_subRL; first apply n_arrivals_at_leq; try lia.
move: (H_valid_arrival_curve tsk IN) ⇒ [ZERO MONO].
apply (leq_trans IHt).
by apply MONO. }
Qed.

End MaximalArrivalSequence.