# Library prosa.implementation.refinements.arrival_curve_prefix

In this section, we prove some properties that every valid arrival curve prefix entails.
Consider a task set with valid arrivals ts, ...

... and a task tsk belonging to ts with positive cost and non-zero arrival bound.
Hypothesis H_positive_cost : 0 < task_cost tsk.
Hypothesis H_tsk_in_ts : tsk \in ts.
Hypothesis H_positive_step : fst (head (0,0) (steps_of (get_arrival_curve_prefix tsk))) > 0.

First, we show that the arrival curve prefix of tsk is valid.
Lemma has_valid_arrival_curve_prefix_tsk :
has_valid_arrival_curve_prefix tsk.
Proof.
move: (H_valid_task_set tsk H_tsk_in_ts); rewrite /valid_arrivalsVALID.
destruct (arrival_cases tsk) as [[p EQ] | [[m EQ] | [evec EQ]]].
all: rewrite /has_valid_arrival_curve_prefix /max_arrivals /MaxArrivals /ConcreteMaxArrivals /get_arrival_curve_prefix EQ //=.
all: rewrite EQ in VALID.
{ (inter_arrival_to_prefix p).
split;[|split;[|split;[|split;[|split]]]] ⇒ //=.
moves.
rewrite /large_horizon in_cons ⇒ /orP [|] ⇒ /eqP EQs //=.
by subst s; rewrite //=; lia. }
{ (inter_arrival_to_prefix m).
split;[|split;[|split;[|split;[|split]]]] ⇒ //=.
moves.
rewrite /large_horizon in_cons ⇒ /orP [|] ⇒ /eqP EQs //=.
by subst s; rewrite //=; lia. }
{ by evec; split ⇒ //; apply /valid_arrival_curve_prefix_P. }
Qed.

Next, we show that each time step of the arrival curve prefix must be positive.
Lemma steps_are_positive_if_first_step_is_positive :
st,
st \in get_time_steps_of_task tsk st > 0.
Proof.
intros st IN; unfold get_time_steps_of_task in ×.
move: (H_valid_task_set) ⇒ VAL; specialize (VAL _ H_tsk_in_ts).
unfold valid_arrivals in VAL; unfold get_arrival_curve_prefix in ×.
{ by unfold inter_arrival_to_prefix, time_steps_of in *; simpl in IN;
move: IN; rewrite mem_seq1 ⇒ /eqP EQ; subst. }
{ by unfold inter_arrival_to_prefix, time_steps_of in *; simpl in IN;
move: IN; rewrite mem_seq1 ⇒ /eqP EQ; subst. }
{ destruct a as [h [ | st0 sts]]; first by done.
move: IN ⇒ /mapP [[t v] IN EQ]; simpl in *; subst st.
move: IN; rewrite in_cons ⇒ /orP [/eqP EQ | IN]; first by subst.
move: VAL ⇒ /valid_arrival_curve_prefix_P VAL.
destruct VAL as [_ [_ [_ [_ SORT]]]].
unfold sorted_ltn_steps in *; simpl in ×.
rewrite (@path_sorted_inE _ predT) in SORT; last apply all_predT.
+ move: SORT ⇒ /andP [/allP ALL _].
specialize (ALL (t,v) IN); move: ALL.
destruct st0; simpl in ×.
by move ⇒ /andP //= ⇒ [[LT1 LT2]]; lia.
+ by intros ? ? ? _ _ _; apply ltn_steps_is_transitive. }
Qed.

Next, we show that even shifting the time steps by a positive offset, they remain positive.
Lemma nonshifted_offsets_are_positive :
A offs,
A \in repeat_steps_with_offset tsk offs A > 0.
Proof.
intros × IN.
move: IN ⇒ /flatten_mapP [o INo IN].
move: IN ⇒ /mapP [st IN EQ]; subst A.
by apply steps_are_positive_if_first_step_is_positive.
Qed.

Finally, we show that the time steps are strictly increasing.
Lemma time_steps_sorted :