# Library prosa.implementation.facts.extrapolated_arrival_curve

In this file, we prove basic properties of the arrival-curve prefix and the extrapolated_arrival_curve function.
Section BasicFacts.

We show that the relation ltn_steps is transitive.
Lemma ltn_steps_is_transitive :
transitive ltn_steps.
Proof.
movea b c /andP [FSTab SNDab] /andP [FSTbc SNDbc].
by apply /andP; split; lia.
Qed.

Next, we show that the relation leq_steps is reflexive...
Lemma leq_steps_is_reflexive :
reflexive leq_steps.
Proof.
move⇒ [l r].
rewrite /leq_steps.
by apply /andP; split.
Qed.

... and transitive.
Lemma leq_steps_is_transitive :
transitive leq_steps.
Proof.
movea b c /andP [FSTab SNDab] /andP [FSTbc SNDbc].
by apply /andP; split; lia.
Qed.

End BasicFacts.

In the following section, we prove a few properties of arrival-curve prefixes assuming that there are no infinite arrivals and that the list of steps is sorted according to the leq_steps relation.
Consider an arbitrary leq-sorted arrival-curve prefix without infinite arrivals.
We prove that value_at is monotone with respect to the relation .
Lemma value_at_monotone :
monotone leq (value_at ac_prefix).
Proof.
intros t1 t2 LE; clear H_no_inf_arrivals.
unfold sorted_leq_steps, value_at, step_at, steps_of in ×.
destruct ac_prefix as [h steps]; simpl.
have GenLem:
t__d1 v__d1 t__d2 v__d2,
v__d1 v__d2
all (leq_steps (t__d1, v__d1)) steps
all (leq_steps (t__d2, v__d2)) steps
snd (last (t__d1, v__d1) [seq step <- steps | fst step t1]) snd (last (t__d2, v__d2) [seq step <- steps | fst step t2]).
{ have steps_sorted := H_sorted_leq; clear H_sorted_leq.
elim: steps steps_sorted ⇒ [//|[t__c v__c] steps IHsteps] steps_sorted.
simpl; intros *; moveLEv /andP [LTN1 /allP ALL1] /andP [LTN2 /allP ALL2].
move: (steps_sorted); rewrite //= (@path_sorted_inE _ predT leq_steps); first last.
{ by apply/allP. }
{ by intros ? ? ? _ _ _; apply leq_steps_is_transitive. }
move ⇒ /andP [ALL SORT].
destruct (leqP (fst (t__c, v__c)) t1) as [R1 | R1], (leqP (fst (t__c, v__c)) t2) as [R2 | R2]; simpl in ×.
{ by rewrite R1 R2 //=; apply: IHsteps. }
{ lia. }
{ rewrite ltnNge -eqbF_neg in R1; move: R1 ⇒ /eqP ->; rewrite R2 //=; apply IHsteps ⇒ //.
- by move: LTN1; rewrite /leq_steps ⇒ /andP //= [_ LEc].
- by apply/allP.
}
{ rewrite ltnNge -eqbF_neg in R1; move: R1 ⇒ /eqP →.
rewrite ltnNge -eqbF_neg in R2; move: R2 ⇒ /eqP →.
by apply IHsteps ⇒ //; apply/allP.
}
}
by apply: GenLem ⇒ [//||]; apply/allP; intros x _; rewrite /leq_steps //=.
Qed.

Next, we prove a correctness claim stating that if value_at makes a step at time instant t + ε (that is, value_at t < value_at (t + ε)), then steps_of ac_prefix contains a step (t + ε, v) for some v.
Lemma value_at_change_is_in_steps_of :
t,
value_at ac_prefix t < value_at ac_prefix (t + ε)
v, (t + ε, v) \in steps_of ac_prefix.
Proof.
movet LT /=.
unfold value_at, step_at in LT.
destruct ac_prefix as [h2 steps]; simpl in LT.
rewrite [in X in _ < X](sorted_split _ _ fst t) /= in LT.
{ rewrite [in X in _ ++ X](eq_filter (a2 := fun xfst x == t + ε)) in LT; last first.
{ by move⇒ [a b] /=; lia. }
{ destruct ([seq x <- steps | fst x == t + ε]) as [|p l] eqn:LST ⇒ //=.
{ rewrite [in X in X ++ _](eq_filter (a2 := fun xfst x t)) in LT; last first.
{ clear; intros [a b]; simpl.
destruct (leqP a t).
- by rewrite Bool.andb_true_r; apply/eqP; lia.
- by rewrite Bool.andb_false_r.
}
{ by rewrite cats0 ltnn in LT. }
}
{ have: p \in [seq x <- steps | x.1 == t + 1]
move⇒ {LT} {LST}; move: p ⇒ //= [t_c v_c].
by rewrite mem_filter ⇒ //= /andP [/eqP ->].
}
}
}
{ move: (H_sorted_leq); clear H_sorted_leq; rewrite /sorted_leq_steps //= ⇒ SORT; clear H_no_inf_arrivals.
elim: steps SORT ⇒ [//|a steps IHsteps] /= SORT.
move: SORT; rewrite path_sortedE; auto using leq_steps_is_transitive; move ⇒ /andP [LE SORT].
apply IHsteps in SORT.
rewrite path_sortedE; last by intros ? ? ? LE1 LE2; lia.
apply/andP; split⇒ [|//].
apply/allP; intros [x y] IN.
by move: LE ⇒ /allP LE; specialize (LE _ IN); move: LE ⇒ /andP [LT _].
}
Qed.

End ArrivalCurvePrefixSortedLeq.

(* In the next section, we make the stronger assumption that
arrival-curve prefixes are sorted according to the ltn_steps
relation. *)

Section ArrivalCurvePrefixSortedLtn.

Consider an arbitrary ltn-sorted arrival-curve prefix without infinite arrivals.
Variable ac_prefix : ArrivalCurvePrefix.
Hypothesis H_sorted_ltn : sorted_ltn_steps ac_prefix. (* Stronger assumption. *)
Hypothesis H_no_inf_arrivals : no_inf_arrivals ac_prefix.

First, we show that an ltn-sorted arrival-curve prefix is an leq-sorted arrival-curve prefix.
Lemma sorted_ltn_steps_imply_sorted_leq_steps_steps :
sorted_leq_steps ac_prefix.
Proof.
destruct ac_prefix as [d l]; unfold sorted_leq_steps, sorted_ltn_steps in *; simpl in ×.
clear H_no_inf_arrivals d.
destruct l ⇒ [//|]; simpl in ×.
eapply sub_path; last by apply H_sorted_ltn.
intros [a1 b1] [a2 b2] LT.
by unfold ltn_steps, leq_steps in *; simpl in *; lia.
Qed.

Next, we show that step_at 0 is equal to (0, 0).
Lemma step_at_0_is_00 :
step_at ac_prefix 0 = (0, 0).
Proof.
unfold step_at; destruct ac_prefix as [h [ | [t v] steps]] ⇒ [//|].
have TR := ltn_steps_is_transitive.
move: (H_sorted_ltn); clear H_sorted_ltn; rewrite /sorted_ltn_steps //= path_sortedE // ⇒ /andP [ALL LT].
have EM : [seq step <- steps | fst step 0] = [::].
{ apply filter_in_pred0; intros [t' v'] IN.
move: ALL ⇒ /allP ALL; specialize (ALL _ IN); simpl in ALL.
by rewrite -ltnNge //=; move: ALL; rewrite /ltn_steps //= ⇒ /andP [T _ ]; lia. }
rewrite EM; destruct (posnP t) as [Z | POS].
{ subst t; simpl.
move: H_no_inf_arrivals; rewrite /no_inf_arrivals /value_at /step_at //= EM //=.
by move ⇒ /eqP EQ; subst v. }
{ by rewrite leqNgt POS //=. }
Qed.

We show that functions steps_of and step_at are consistent. That is, if a pair (t, v) is in steps of ac_prefix, then step_at t is equal to (t, v).
Lemma step_at_agrees_with_steps_of :
t v, (t, v) \in steps_of ac_prefix step_at ac_prefix t = (t, v).
Proof.
case: ac_prefix H_sorted_ltn ⇒ [h steps] + //= ? ? IN.
move: IN ⇒ /in_cat //= [steps__l [steps__r ->]] /sorted_cat //=; case ⇒ //= [|_ +]; first by apply ltn_steps_is_transitive.
rewrite /step_at filter_cat last_cat (nonnil_last _ _ (0,0)); last by rewrite //= leqnn.
rewrite //= path_sortedE; auto using ltn_steps_is_transitive; rewrite //= leqnn ⇒ /andP [ALL SORT].
replace (filter _ _ ) with (@nil (nat × nat)) ⇒ [//|].
rewrite filter_in_pred0 // ⇒ x IN; rewrite -ltnNge.
by move: ALL ⇒ /allP ALL; move: (ALL _ IN); rewrite /ltn_steps //= ⇒ /andP [LT _ ].
Qed.

End ArrivalCurvePrefixSortedLtn.

In this section, we prove a few basic properties of extrapolated_arrival_curve function, such as (1) monotonicity of extrapolated_arrival_curve or (2) implications of the fact that extrapolated_arrival_curve makes a step at time t + ε.
Consider an arbitrary leq-sorted arrival-curve prefix without infinite arrivals.
Let h denote the horizon of ac_prefix ...
Let h := horizon_of ac_prefix.

... and prefix be shorthand for value_at ac_prefix.
Let prefix := value_at ac_prefix.

We show that extrapolated_arrival_curve is monotone.
Lemma extrapolated_arrival_curve_is_monotone :
monotone leq (extrapolated_arrival_curve ac_prefix).
Proof.
intros t1 t2 LE; unfold extrapolated_arrival_curve.
replace (horizon_of _) with h ⇒ [|//].
move: LE; rewrite leq_eqVlt ⇒ /orP [/eqP EQ | LTs].
{ by subst t2. }
{ have ALT : (t1 %/ h == t2 %/ h) (t1 %/ h < t2 %/ h).
{ by apply/orP; rewrite -leq_eqVlt; apply leq_div2r, ltnW. }
move: ALT ⇒ [/eqP EQ | LT].
{ rewrite EQ leq_add2l; apply value_at_monotone ⇒ //.
by apply eqdivn_leqmodn; lia.
}
{ have EQ: k, t1 + k = t2 k > 0.
{ (t2 - t1); split; lia. }
destruct EQ as [k [EQ POS]]; subst t2; clear LTs.
rewrite divnD//.
destruct (leqP h k) as [LEk|LTk].
{ eapply leq_trans; last by apply leq_addr.
move: LEk; rewrite leq_eqVlt ⇒ /orP [/eqP EQk | LTk].
{ by subst; rewrite divnn POS mul1n; apply value_at_monotone, ltnW, ltn_pmod. }
{ rewrite -[value_at _ (t1 %% h)]mul1n; apply leq_mul.
- by rewrite divn_gt0; [apply: ltnW|].
- by apply value_at_monotone, ltnW, ltn_pmod.
}
}
{ rewrite divn_small // mul0n add0n.
rewrite lt0bF; rewrite F; clear F.
rewrite mul1n; eapply leq_trans; last by apply leq_addr.
by apply value_at_monotone, ltnW, ltn_pmod.
}
}
}
Qed.

Finally, we show that if extrapolated_arrival_curve t extrapolated_arrival_curve (t + ε), then either (1) t + ε divides h or (2) prefix (t mod h) < prefix ((t + ε) mod h).
Lemma extrapolated_arrival_curve_change :
t,
extrapolated_arrival_curve ac_prefix t != extrapolated_arrival_curve ac_prefix (t + ε)
(* 1 *) t %/ h < (t + ε) %/ h
(* 2 *) t %/ h = (t + ε) %/ h prefix (t %% h) < prefix ((t + ε) %% h).
Proof.
intros t NEQ.
have LT := ltn_neqAle (extrapolated_arrival_curve ac_prefix t) (extrapolated_arrival_curve ac_prefix (t + ε)).
rewrite NEQ in LT; rewrite extrapolated_arrival_curve_is_monotone in LT; last by apply leq_addr.
clear NEQ; simpl in LT.
unfold extrapolated_arrival_curve in LT.
replace (horizon_of _) with h in LT ⇒ [|//].
have AF : s1 s2 m x y,
s1 s2
m × s1 + x < m × s2 + y
s1 < s2 s1 = s2 x < y.
{ clear; intros s1 s2 m x y LEs LT.
move: LEs; rewrite leq_eqVlt ⇒ /orP [/eqP EQ | LTs].
{ by subst s2; rename s1 into s; right; split; [|lia]. }
{ by left. }
}
apply AF with (m := prefix h).
{ by apply leq_div2r, leq_addr. }
{ by rewrite ![prefix _ × _]mulnC; apply LT. }
Qed.

End ExtrapolatedArrivalCurve.