Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
From mathcomp Require Export ssreflect ssrbool eqtype ssrnat div seq path fintype bigop.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.behavior.time .
Require Export prosa.util.all .Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.implementation.definitions.extrapolated_arrival_curve.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** In this file, we prove basic properties of the arrival-curve
prefix and the [extrapolated_arrival_curve] function. *)
(** We start with basic facts about the relations [ltn_steps] and [leq_steps]. *)
Section BasicFacts .
(** We show that the relation [ltn_steps] is transitive. *)
Lemma ltn_steps_is_transitive :
transitive ltn_steps.transitive (T:=nat * nat) ltn_steps
Proof .transitive (T:=nat * nat) ltn_steps
move => a b c /andP [FSTab SNDab] /andP [FSTbc SNDbc].a, b, c : (nat * nat)%type FSTab : b.1 < a.1 SNDab : b.2 < a.2 FSTbc : a.1 < c.1 SNDbc : a.2 < c.2
ltn_steps b c
by apply /andP; split ; lia .
Qed .
(** Next, we show that the relation [leq_steps] is reflexive... *)
Lemma leq_steps_is_reflexive :
reflexive leq_steps.reflexive (T:=nat * nat) leq_steps
Proof .reflexive (T:=nat * nat) leq_steps
move => [l r].l, r : nat
leq_steps (l, r) (l, r)
rewrite /leq_steps.l, r : nat
((l, r).1 <= (l, r).1 ) && ((l, r).2 <= (l, r).2 )
by apply /andP; split .
Qed .
(** ... and transitive. *)
Lemma leq_steps_is_transitive :
transitive leq_steps.transitive (T:=nat * nat) leq_steps
Proof .transitive (T:=nat * nat) leq_steps
move => a b c /andP [FSTab SNDab] /andP [FSTbc SNDbc].a, b, c : (nat * nat)%type FSTab : b.1 <= a.1 SNDab : b.2 <= a.2 FSTbc : a.1 <= c.1 SNDbc : a.2 <= c.2
leq_steps b c
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. *)
Section ArrivalCurvePrefixSortedLeq .
(** Consider an arbitrary [leq]-sorted arrival-curve prefix without
infinite arrivals. *)
Variable ac_prefix : ArrivalCurvePrefix.
Hypothesis H_sorted_leq : sorted_leq_steps ac_prefix.
Hypothesis H_no_inf_arrivals : no_inf_arrivals ac_prefix.
(** We prove that [value_at] is monotone with respect to the relation [<=]. *)
Lemma value_at_monotone :
monotone leq (value_at ac_prefix).ac_prefix : ArrivalCurvePrefix H_sorted_leq : sorted_leq_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix
monotone leq (value_at ac_prefix)
Proof .ac_prefix : ArrivalCurvePrefix H_sorted_leq : sorted_leq_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix
monotone leq (value_at ac_prefix)
intros t1 t2 LE; clear H_no_inf_arrivals.ac_prefix : ArrivalCurvePrefix H_sorted_leq : sorted_leq_steps ac_prefix t1, t2 : nat LE : t1 <= t2
value_at ac_prefix t1 <= value_at ac_prefix t2
unfold sorted_leq_steps, value_at, step_at, steps_of in *.ac_prefix : ArrivalCurvePrefix H_sorted_leq : sorted leq_steps ac_prefix.2 t1, t2 : nat LE : t1 <= t2
(last (0 , 0 ) [seq step <- ac_prefix.2 | step.1 <= t1]).2 <=
(last (0 , 0 ) [seq step <- ac_prefix.2 | step.1 <= t2]).2
destruct ac_prefix as [h steps]; simpl .ac_prefix : ArrivalCurvePrefix h : duration steps : seq (duration * nat) H_sorted_leq : sorted leq_steps (h, steps).2 t1, t2 : nat LE : t1 <= t2
(last (0 , 0 ) [seq step <- steps | step.1 <= t1]).2 <=
(last (0 , 0 ) [seq step <- steps | step.1 <= t2]).2
have GenLem:
forall 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]).ac_prefix : ArrivalCurvePrefix h : duration steps : seq (duration * nat) H_sorted_leq : sorted leq_steps (h, steps).2 t1, t2 : nat LE : t1 <= t2
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2
{ ac_prefix : ArrivalCurvePrefix h : duration steps : seq (duration * nat) H_sorted_leq : sorted leq_steps (h, steps).2 t1, t2 : nat LE : t1 <= t2
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2
induction steps as [ | [t__c v__c] steps]; first by done .ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : sorted leq_steps
(h, (t__c, v__c) :: steps).2 t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) ((t__c, v__c) :: steps) ->
all (leq_steps (t__d2, v__d2)) ((t__c, v__c) :: steps) ->
(last (t__d1, v__d1)
[seq step <- (t__c, v__c) :: steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- (t__c, v__c) :: steps | step.1 <= t2]).2
simpl ; intros *; move => LEv /andP [LTN1 /allP ALL1] /andP [LTN2 /allP ALL2].ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : sorted leq_steps
(h, (t__c, v__c) :: steps).2 t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : prod_eqType nat_eqType nat_eqType,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : prod_eqType nat_eqType nat_eqType,
leq_steps (t__d2, v__d2) x}
(last (t__d1, v__d1)
(if t__c <= t1
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t1]
else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
(if t__c <= t2
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t2]
else [seq step <- steps | step.1 <= t2])).2
move : (H_sorted_leq); rewrite //= (@path_sorted_inE _ predT leq_steps); first last .ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : sorted leq_steps
(h, (t__c, v__c) :: steps).2 t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : prod_eqType nat_eqType nat_eqType,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : prod_eqType nat_eqType nat_eqType,
leq_steps (t__d2, v__d2) x}
all predT ((t__c, v__c) :: steps)
{ ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : sorted leq_steps
(h, (t__c, v__c) :: steps).2 t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : prod_eqType nat_eqType nat_eqType,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : prod_eqType nat_eqType nat_eqType,
leq_steps (t__d2, v__d2) x}
all predT ((t__c, v__c) :: steps)
by apply /allP. } ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : sorted leq_steps
(h, (t__c, v__c) :: steps).2 t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : prod_eqType nat_eqType nat_eqType,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : prod_eqType nat_eqType nat_eqType,
leq_steps (t__d2, v__d2) x}
{in predT & &, transitive (T:=nat * nat) leq_steps}
{ ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : sorted leq_steps
(h, (t__c, v__c) :: steps).2 t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : prod_eqType nat_eqType nat_eqType,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : prod_eqType nat_eqType nat_eqType,
leq_steps (t__d2, v__d2) x}
{in predT & &, transitive (T:=nat * nat) leq_steps}
by intros ? ? ? _ _ _; apply leq_steps_is_transitive. } ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : sorted leq_steps
(h, (t__c, v__c) :: steps).2 t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : prod_eqType nat_eqType nat_eqType,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : prod_eqType nat_eqType nat_eqType,
leq_steps (t__d2, v__d2) x}
all (leq_steps (t__c, v__c)) steps &&
sorted leq_steps steps ->
(last (t__d1, v__d1)
(if t__c <= t1
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t1]
else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
(if t__c <= t2
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t2]
else [seq step <- steps | step.1 <= t2])).2
move => /andP [ALL SORT].ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : sorted leq_steps
(h, (t__c, v__c) :: steps).2 t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : prod_eqType nat_eqType nat_eqType,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : prod_eqType nat_eqType nat_eqType,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps
(last (t__d1, v__d1)
(if t__c <= t1
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t1]
else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
(if t__c <= t2
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t2]
else [seq step <- steps | step.1 <= t2])).2
destruct (leqP (fst (t__c, v__c)) t1) as [R1 | R1], (leqP (fst (t__c, v__c)) t2) as [R2 | R2]; simpl in *.ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps R1 : t__c <= t1 R2 : t__c <= t2
(last (t__d1, v__d1)
(if t__c <= t1
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t1]
else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
(if t__c <= t2
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t2]
else [seq step <- steps | step.1 <= t2])).2
{ ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps R1 : t__c <= t1 R2 : t__c <= t2
(last (t__d1, v__d1)
(if t__c <= t1
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t1]
else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
(if t__c <= t2
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t2]
else [seq step <- steps | step.1 <= t2])).2
rewrite R1 R2 //=; apply IHsteps; try done . } ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps R1 : t__c <= t1 R2 : t2 < t__c
(last (t__d1, v__d1)
(if t__c <= t1
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t1]
else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
(if t__c <= t2
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t2]
else [seq step <- steps | step.1 <= t2])).2
{ ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps R1 : t__c <= t1 R2 : t2 < t__c
(last (t__d1, v__d1)
(if t__c <= t1
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t1]
else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
(if t__c <= t2
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t2]
else [seq step <- steps | step.1 <= t2])).2
by lia . } ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps R1 : t1 < t__c R2 : t__c <= t2
(last (t__d1, v__d1)
(if t__c <= t1
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t1]
else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
(if t__c <= t2
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t2]
else [seq step <- steps | step.1 <= t2])).2
{ ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps R1 : t1 < t__c R2 : t__c <= t2
(last (t__d1, v__d1)
(if t__c <= t1
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t1]
else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
(if t__c <= t2
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t2]
else [seq step <- steps | step.1 <= t2])).2
rewrite ltnNge -eqbF_neg in R1; move : R1 => /eqP ->; rewrite R2 //=; apply IHsteps; try done .ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps R2 : t__c <= t2
v__d1 <= v__c
- ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps R2 : t__c <= t2
v__d1 <= v__c
by move : LTN1; rewrite /leq_steps => /andP //= [_ LEc].ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps R2 : t__c <= t2
all (leq_steps (t__d1, v__d1)) steps
- ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps R2 : t__c <= t2
all (leq_steps (t__d1, v__d1)) steps
by apply /allP.
} ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps R1 : t1 < t__c R2 : t2 < t__c
(last (t__d1, v__d1)
(if t__c <= t1
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t1]
else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
(if t__c <= t2
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t2]
else [seq step <- steps | step.1 <= t2])).2
{ ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps R1 : t1 < t__c R2 : t2 < t__c
(last (t__d1, v__d1)
(if t__c <= t1
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t1]
else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
(if t__c <= t2
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t2]
else [seq step <- steps | step.1 <= t2])).2
rewrite ltnNge -eqbF_neg in R1; move : R1 => /eqP ->.ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps R2 : t2 < t__c
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
(if t__c <= t2
then
(t__c, v__c)
:: [seq step <- steps | step.1 <= t2]
else [seq step <- steps | step.1 <= t2])).2
rewrite ltnNge -eqbF_neg in R2; move : R2 => /eqP ->.ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2
apply IHsteps; try done .ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps
all (leq_steps (t__d1, v__d1)) steps
- ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps
all (leq_steps (t__d1, v__d1)) steps
by apply /allP.ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps
all (leq_steps (t__d2, v__d2)) steps
- ac_prefix : ArrivalCurvePrefix h, t__c : duration v__c : nat steps : seq (duration * nat) H_sorted_leq : path leq_steps (t__c, v__c) steps t1, t2 : nat LE : t1 <= t2 IHsteps : sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2 t__d1, v__d1, t__d2, v__d2 : nat LEv : v__d1 <= v__d2 LTN1 : leq_steps (t__d1, v__d1) (t__c, v__c) ALL1 : {in steps,
forall x : nat * nat,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall x : nat * nat,
leq_steps (t__d2, v__d2) x} ALL : all (leq_steps (t__c, v__c)) stepsSORT : sorted leq_steps steps
all (leq_steps (t__d2, v__d2)) steps
by apply /allP.
}
} ac_prefix : ArrivalCurvePrefix h : duration steps : seq (duration * nat) H_sorted_leq : sorted leq_steps (h, steps).2 t1, t2 : nat LE : t1 <= t2 GenLem : forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2
(last (0 , 0 ) [seq step <- steps | step.1 <= t1]).2 <=
(last (0 , 0 ) [seq step <- steps | step.1 <= t2]).2
apply GenLem; first by done .ac_prefix : ArrivalCurvePrefix h : duration steps : seq (duration * nat) H_sorted_leq : sorted leq_steps (h, steps).2 t1, t2 : nat LE : t1 <= t2 GenLem : forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
[seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
[seq step <- steps | step.1 <= t2]).2
all (leq_steps (0 , 0 )) steps
all : by 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 :
forall t ,
value_at ac_prefix t < value_at ac_prefix (t + ε) ->
exists v , (t + ε, v) \in steps_of ac_prefix.ac_prefix : ArrivalCurvePrefix H_sorted_leq : sorted_leq_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix
forall t : duration,
value_at ac_prefix t < value_at ac_prefix (t + ε) ->
exists v : nat_eqType,
(t + ε, v) \in steps_of ac_prefix
Proof .ac_prefix : ArrivalCurvePrefix H_sorted_leq : sorted_leq_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix
forall t : duration,
value_at ac_prefix t < value_at ac_prefix (t + ε) ->
exists v : nat_eqType,
(t + ε, v) \in steps_of ac_prefix
intros ? LT.ac_prefix : ArrivalCurvePrefix H_sorted_leq : sorted_leq_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix t : duration LT : value_at ac_prefix t < value_at ac_prefix (t + ε)
exists v : nat_eqType,
(t + ε, v) \in steps_of ac_prefix
unfold value_at, step_at in LT.ac_prefix : ArrivalCurvePrefix H_sorted_leq : sorted_leq_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix t : duration LT : (last (0 , 0 )
[seq step <- steps_of ac_prefix | step.1 <= t]).2 <
(last (0 , 0 )
[seq step <- steps_of ac_prefix
| step.1 <= t + ε]).2
exists v : nat_eqType,
(t + ε, v) \in steps_of ac_prefix
destruct ac_prefix as [h2 steps]; simpl in LT.ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
[seq step <- steps | step.1 <= t + ε]).2
exists v : nat_eqType,
(t + ε, v) \in steps_of (h2, steps)
rewrite [in X in _ < X](sorted_split _ _ fst t) in LT.ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++
[seq x <- steps | x.1 <= t + ε & t < x.1 ])).2
exists v : nat_eqType,
(t + ε, v) \in steps_of (h2, steps)
{ ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++
[seq x <- steps | x.1 <= t + ε & t < x.1 ])).2
exists v : nat_eqType,
(t + ε, v) \in steps_of (h2, steps)
rewrite [in X in _ ++ X](eq_filter (a2 := fun x => fst x == t + ε)) in LT; last first .ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration
(fun x : prod_eqType nat_eqType nat_eqType =>
(x.1 <= t + ε) && (t < x.1 )) =1
(fun x : nat_eqType * nat_eqType => x.1 == t + ε)
{ ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration
(fun x : prod_eqType nat_eqType nat_eqType =>
(x.1 <= t + ε) && (t < x.1 )) =1
(fun x : nat_eqType * nat_eqType => x.1 == t + ε)
by intros [a b]; simpl ; rewrite -addn1 /ε eqn_leq. } ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++
[seq x <- steps | x.1 == t + ε])).2
exists v : nat_eqType,
(t + ε, v) \in steps_of (h2, steps)
{ ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++
[seq x <- steps | x.1 == t + ε])).2
exists v : nat_eqType,
(t + ε, v) \in steps_of (h2, steps)
destruct ([seq x <- steps | fst x == t + ε]) eqn :LST.ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++
[seq x <- steps | x.1 == t + ε])).2 LST : [seq x <- steps | x.1 == t + ε] = [::]
exists v : nat_eqType,
(t + ε, v) \in steps_of (h2, steps)
{ ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++
[seq x <- steps | x.1 == t + ε])).2 LST : [seq x <- steps | x.1 == t + ε] = [::]
exists v : nat_eqType,
(t + ε, v) \in steps_of (h2, steps)
rewrite LST in LT.ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LST : [seq x <- steps | x.1 == t + ε] = [::] LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++
[::])).2
exists v : nat_eqType,
(t + ε, v) \in steps_of (h2, steps)
rewrite [in X in X ++ _](eq_filter (a2 := fun x => fst x <= t)) in LT; last first .ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LST : [seq x <- steps | x.1 == t + ε] = [::]
(fun x : prod_eqType nat_eqType nat_eqType =>
(x.1 <= t + ε) && (x.1 <= t)) =1
(fun x : nat * nat_eqType => x.1 <= t)
{ ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LST : [seq x <- steps | x.1 == t + ε] = [::]
(fun x : prod_eqType nat_eqType nat_eqType =>
(x.1 <= t + ε) && (x.1 <= t)) =1
(fun x : nat * nat_eqType => x.1 <= t)
clear ; intros [a b]; simpl .t : duration a : nat b : nat_eqType
(a <= t + ε) && (a <= t) = (a <= t)
destruct (leqP a t).t : duration a : nat b : nat_eqType i : a <= t
(a <= t + ε) && true = true
- t : duration a : nat b : nat_eqType i : a <= t
(a <= t + ε) && true = true
by rewrite Bool.andb_true_r; apply /eqP; lia .t : duration a : nat b : nat_eqType i : t < a
(a <= t + ε) && false = false
- t : duration a : nat b : nat_eqType i : t < a
(a <= t + ε) && false = false
by rewrite Bool.andb_false_r.
} ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LST : [seq x <- steps | x.1 == t + ε] = [::] LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t] ++ [::])).2
exists v : nat_eqType,
(t + ε, v) \in steps_of (h2, steps)
{ ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LST : [seq x <- steps | x.1 == t + ε] = [::] LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t] ++ [::])).2
exists v : nat_eqType,
(t + ε, v) \in steps_of (h2, steps)
by rewrite cats0 ltnn in LT. }
} ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++
[seq x <- steps | x.1 == t + ε])).2 p : (nat_eqType * nat)%type l : seq (nat_eqType * nat) LST : [seq x <- steps | x.1 == t + ε] = p :: l
exists v : nat_eqType,
(t + ε, v) \in steps_of (h2, steps)
{ ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++
[seq x <- steps | x.1 == t + ε])).2 p : (nat_eqType * nat)%type l : seq (nat_eqType * nat) LST : [seq x <- steps | x.1 == t + ε] = p :: l
exists v : nat_eqType,
(t + ε, v) \in steps_of (h2, steps)
destruct p as [t__c v__c]; exists v__c .ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++
[seq x <- steps | x.1 == t + ε])).2 t__c : nat_eqType v__c : nat l : seq (nat_eqType * nat) LST : [seq x <- steps | x.1 == t + ε] =
(t__c, v__c) :: l
(t + ε, v__c) \in steps_of (h2, steps)
rewrite /steps_of //=; symmetry in LST.ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++
[seq x <- steps | x.1 == t + ε])).2 t__c : nat_eqType v__c : nat l : seq (nat_eqType * nat) LST : (t__c, v__c) :: l =
[seq x <- steps | x.1 == t + ε]
(t + ε, v__c) \in steps
apply mem_head_impl in LST.ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++
[seq x <- steps | x.1 == t + ε])).2 t__c : nat_eqType v__c : nat l : seq (nat_eqType * nat) LST : (t__c, v__c) \in [seq x <- steps | x.1 == t + ε]
(t + ε, v__c) \in steps
by move : LST; rewrite mem_filter //= => /andP [/eqP -> IN].
}
}
} ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration
sorted
(fun x y : prod_eqType nat_eqType nat_eqType =>
x.1 <= y.1 ) steps
{ ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) H_sorted_leq : sorted_leq_steps (h2, steps) H_no_inf_arrivals : no_inf_arrivals (h2, steps) t : duration
sorted
(fun x y : prod_eqType nat_eqType nat_eqType =>
x.1 <= y.1 ) steps
move : (H_sorted_leq); clear H_sorted_leq; rewrite /sorted_leq_steps //= => SORT; clear H_no_inf_arrivals.ac_prefix : ArrivalCurvePrefix h2 : duration steps : seq (duration * nat) t : duration SORT : sorted leq_steps steps
sorted (fun x y : nat * nat => x.1 <= y.1 ) steps
induction steps; [by done | simpl in *].ac_prefix : ArrivalCurvePrefix h2 : duration a : (duration * nat)%type steps : seq (duration * nat) t : duration SORT : path leq_steps a steps IHsteps : sorted leq_steps steps ->
sorted (fun x y : nat * nat => x.1 <= y.1 )
steps
path (fun x y : nat * nat => x.1 <= y.1 ) a steps
move : SORT; rewrite path_sortedE; auto using leq_steps_is_transitive; move => /andP [LE SORT].ac_prefix : ArrivalCurvePrefix h2 : duration a : (duration * nat)%type steps : seq (duration * nat) t : duration IHsteps : sorted leq_steps steps ->
sorted (fun x y : nat * nat => x.1 <= y.1 )
steps LE : all (leq_steps a) stepsSORT : sorted leq_steps steps
path (fun x y : nat * nat => x.1 <= y.1 ) a steps
apply IHsteps in SORT.ac_prefix : ArrivalCurvePrefix h2 : duration a : (duration * nat)%type steps : seq (duration * nat) t : duration IHsteps : sorted leq_steps steps ->
sorted (fun x y : nat * nat => x.1 <= y.1 )
steps LE : all (leq_steps a) stepsSORT : sorted (fun x y : nat * nat => x.1 <= y.1 )
steps
path (fun x y : nat * nat => x.1 <= y.1 ) a steps
rewrite path_sortedE; last by intros ? ? ? LE1 LE2; lia .ac_prefix : ArrivalCurvePrefix h2 : duration a : (duration * nat)%type steps : seq (duration * nat) t : duration IHsteps : sorted leq_steps steps ->
sorted (fun x y : nat * nat => x.1 <= y.1 )
steps LE : all (leq_steps a) stepsSORT : sorted (fun x y : nat * nat => x.1 <= y.1 )
steps
all (fun y : nat * nat => a.1 <= y.1 ) steps &&
sorted (fun x y : nat * nat => x.1 <= y.1 ) steps
apply /andP; split ; last by done .ac_prefix : ArrivalCurvePrefix h2 : duration a : (duration * nat)%type steps : seq (duration * nat) t : duration IHsteps : sorted leq_steps steps ->
sorted (fun x y : nat * nat => x.1 <= y.1 )
steps LE : all (leq_steps a) stepsSORT : sorted (fun x y : nat * nat => x.1 <= y.1 )
steps
all (fun y : nat * nat => a.1 <= y.1 ) steps
apply /allP; intros [x y] IN.ac_prefix : ArrivalCurvePrefix h2 : duration a : (duration * nat)%type steps : seq (duration * nat) t : duration IHsteps : sorted leq_steps steps ->
sorted (fun x y : nat * nat => x.1 <= y.1 )
steps LE : all (leq_steps a) stepsSORT : sorted (fun x y : nat * nat => x.1 <= y.1 )
steps x, y : nat_eqType IN : (x, y) \in steps
a.1 <= (x, y).1
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.ac_prefix : ArrivalCurvePrefix H_sorted_ltn : sorted_ltn_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix
sorted_leq_steps ac_prefix
Proof .ac_prefix : ArrivalCurvePrefix H_sorted_ltn : sorted_ltn_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix
sorted_leq_steps ac_prefix
destruct ac_prefix; unfold sorted_leq_steps, sorted_ltn_steps in *; simpl in *.ac_prefix : ArrivalCurvePrefix d : duration l : seq (duration * nat) H_sorted_ltn : sorted ltn_steps l H_no_inf_arrivals : no_inf_arrivals (d, l)
sorted leq_steps l
clear H_no_inf_arrivals d.ac_prefix : ArrivalCurvePrefix l : seq (duration * nat) H_sorted_ltn : sorted ltn_steps l
sorted leq_steps l
destruct l; simpl in *; first by done .ac_prefix : ArrivalCurvePrefix p : (duration * nat)%type l : seq (duration * nat) H_sorted_ltn : path ltn_steps p l
path leq_steps p l
eapply sub_path; last by apply H_sorted_ltn.ac_prefix : ArrivalCurvePrefix p : (duration * nat)%type l : seq (duration * nat) H_sorted_ltn : path ltn_steps p l
subrel (T:=nat * nat) ltn_steps leq_steps
intros [a1 b1] [a2 b2] LT.ac_prefix : ArrivalCurvePrefix p : (duration * nat)%type l : seq (duration * nat) H_sorted_ltn : path ltn_steps p l a1, b1, a2, b2 : nat LT : ltn_steps (a1, b1) (a2, b2)
leq_steps (a1, b1) (a2, b2)
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 ).ac_prefix : ArrivalCurvePrefix H_sorted_ltn : sorted_ltn_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix
step_at ac_prefix 0 = (0 , 0 )
Proof .ac_prefix : ArrivalCurvePrefix H_sorted_ltn : sorted_ltn_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix
step_at ac_prefix 0 = (0 , 0 )
unfold step_at; destruct ac_prefix as [h [ | [t v] steps]]; first by done .ac_prefix : ArrivalCurvePrefix h, t : duration v : nat steps : seq (duration * nat) H_sorted_ltn : sorted_ltn_steps (h, (t, v) :: steps) H_no_inf_arrivals : no_inf_arrivals
(h, (t, v) :: steps)
last (0 , 0 )
[seq step <- steps_of (h, (t, v) :: steps)
| step.1 <= 0 ] = (0 , 0 )
have TR := ltn_steps_is_transitive.ac_prefix : ArrivalCurvePrefix h, t : duration v : nat steps : seq (duration * nat) H_sorted_ltn : sorted_ltn_steps (h, (t, v) :: steps) H_no_inf_arrivals : no_inf_arrivals
(h, (t, v) :: steps) TR : transitive (T:=nat * nat) ltn_steps
last (0 , 0 )
[seq step <- steps_of (h, (t, v) :: steps)
| step.1 <= 0 ] = (0 , 0 )
move : (H_sorted_ltn); clear H_sorted_ltn; rewrite /sorted_ltn_steps //= path_sortedE // => /andP [ALL LT].ac_prefix : ArrivalCurvePrefix h, t : duration v : nat steps : seq (duration * nat) H_no_inf_arrivals : no_inf_arrivals
(h, (t, v) :: steps) TR : transitive (T:=nat * nat) ltn_steps ALL : all (ltn_steps (t, v)) stepsLT : sorted ltn_steps steps
last (0 , 0 )
(if t <= 0
then (t, v) :: [seq step <- steps | step.1 <= 0 ]
else [seq step <- steps | step.1 <= 0 ]) = (0 , 0 )
have EM : [seq step <- steps | fst step <= 0 ] = [::].ac_prefix : ArrivalCurvePrefix h, t : duration v : nat steps : seq (duration * nat) H_no_inf_arrivals : no_inf_arrivals
(h, (t, v) :: steps) TR : transitive (T:=nat * nat) ltn_steps ALL : all (ltn_steps (t, v)) stepsLT : sorted ltn_steps steps
[seq step <- steps | step.1 <= 0 ] = [::]
{ ac_prefix : ArrivalCurvePrefix h, t : duration v : nat steps : seq (duration * nat) H_no_inf_arrivals : no_inf_arrivals
(h, (t, v) :: steps) TR : transitive (T:=nat * nat) ltn_steps ALL : all (ltn_steps (t, v)) stepsLT : sorted ltn_steps steps
[seq step <- steps | step.1 <= 0 ] = [::]
apply filter_in_pred0; intros [t' v'] IN.ac_prefix : ArrivalCurvePrefix h, t : duration v : nat steps : seq (duration * nat) H_no_inf_arrivals : no_inf_arrivals
(h, (t, v) :: steps) TR : transitive (T:=nat * nat) ltn_steps ALL : all (ltn_steps (t, v)) stepsLT : sorted ltn_steps steps t', v' : nat_eqType IN : (t', v') \in steps
~~ ((t', v').1 <= 0 )
move : ALL => /allP ALL; specialize (ALL _ IN); simpl in ALL.ac_prefix : ArrivalCurvePrefix h, t : duration v : nat steps : seq (duration * nat) H_no_inf_arrivals : no_inf_arrivals
(h, (t, v) :: steps) TR : transitive (T:=nat * nat) ltn_steps LT : sorted ltn_steps steps t', v' : nat_eqType IN : (t', v') \in steps ALL : ltn_steps (t, v) (t', v')
~~ ((t', v').1 <= 0 )
by rewrite -ltnNge //=; move : ALL; rewrite /ltn_steps //= => /andP [T _ ]; lia . } ac_prefix : ArrivalCurvePrefix h, t : duration v : nat steps : seq (duration * nat) H_no_inf_arrivals : no_inf_arrivals
(h, (t, v) :: steps) TR : transitive (T:=nat * nat) ltn_steps ALL : all (ltn_steps (t, v)) stepsLT : sorted ltn_steps steps EM : [seq step <- steps | step.1 <= 0 ] = [::]
last (0 , 0 )
(if t <= 0
then (t, v) :: [seq step <- steps | step.1 <= 0 ]
else [seq step <- steps | step.1 <= 0 ]) = (0 , 0 )
rewrite EM; destruct (posnP t) as [Z | POS].ac_prefix : ArrivalCurvePrefix h, t : duration v : nat steps : seq (duration * nat) H_no_inf_arrivals : no_inf_arrivals
(h, (t, v) :: steps) TR : transitive (T:=nat * nat) ltn_steps ALL : all (ltn_steps (t, v)) stepsLT : sorted ltn_steps steps EM : [seq step <- steps | step.1 <= 0 ] = [::] Z : t = 0
last (0 , 0 ) (if t <= 0 then [:: (t, v)] else [::]) =
(0 , 0 )
{ ac_prefix : ArrivalCurvePrefix h, t : duration v : nat steps : seq (duration * nat) H_no_inf_arrivals : no_inf_arrivals
(h, (t, v) :: steps) TR : transitive (T:=nat * nat) ltn_steps ALL : all (ltn_steps (t, v)) stepsLT : sorted ltn_steps steps EM : [seq step <- steps | step.1 <= 0 ] = [::] Z : t = 0
last (0 , 0 ) (if t <= 0 then [:: (t, v)] else [::]) =
(0 , 0 )
subst t; simpl .ac_prefix : ArrivalCurvePrefix h : duration v : nat steps : seq (duration * nat) H_no_inf_arrivals : no_inf_arrivals
(h, (0 , v) :: steps) TR : transitive (T:=nat * nat) ltn_steps ALL : all (ltn_steps (0 , v)) stepsLT : sorted ltn_steps steps EM : [seq step <- steps | step.1 <= 0 ] = [::]
(0 , v) = (0 , 0 )
move : H_no_inf_arrivals; rewrite /no_inf_arrivals /value_at /step_at //= EM //=.ac_prefix : ArrivalCurvePrefix h : duration v : nat steps : seq (duration * nat) H_no_inf_arrivals : no_inf_arrivals
(h, (0 , v) :: steps) TR : transitive (T:=nat * nat) ltn_steps ALL : all (ltn_steps (0 , v)) stepsLT : sorted ltn_steps steps EM : [seq step <- steps | step.1 <= 0 ] = [::]
v == 0 -> (0 , v) = (0 , 0 )
by move => /eqP EQ; subst v. } ac_prefix : ArrivalCurvePrefix h, t : duration v : nat steps : seq (duration * nat) H_no_inf_arrivals : no_inf_arrivals
(h, (t, v) :: steps) TR : transitive (T:=nat * nat) ltn_steps ALL : all (ltn_steps (t, v)) stepsLT : sorted ltn_steps steps EM : [seq step <- steps | step.1 <= 0 ] = [::] POS : 0 < t
last (0 , 0 ) (if t <= 0 then [:: (t, v)] else [::]) =
(0 , 0 )
{ ac_prefix : ArrivalCurvePrefix h, t : duration v : nat steps : seq (duration * nat) H_no_inf_arrivals : no_inf_arrivals
(h, (t, v) :: steps) TR : transitive (T:=nat * nat) ltn_steps ALL : all (ltn_steps (t, v)) stepsLT : sorted ltn_steps steps EM : [seq step <- steps | step.1 <= 0 ] = [::] POS : 0 < t
last (0 , 0 ) (if t <= 0 then [:: (t, v)] else [::]) =
(0 , 0 )
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 :
forall t v , (t, v) \in steps_of ac_prefix -> step_at ac_prefix t = (t, v).ac_prefix : ArrivalCurvePrefix H_sorted_ltn : sorted_ltn_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix
forall t v : nat_eqType,
(t, v) \in steps_of ac_prefix ->
step_at ac_prefix t = (t, v)
Proof .ac_prefix : ArrivalCurvePrefix H_sorted_ltn : sorted_ltn_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix
forall t v : nat_eqType,
(t, v) \in steps_of ac_prefix ->
step_at ac_prefix t = (t, v)
intros * IN; destruct ac_prefix as [h steps].ac_prefix : ArrivalCurvePrefix h : duration steps : seq (duration * nat) H_sorted_ltn : sorted_ltn_steps (h, steps) H_no_inf_arrivals : no_inf_arrivals (h, steps) t, v : nat_eqType IN : (t, v) \in steps_of (h, steps)
step_at (h, steps) t = (t, v)
unfold step_at; simpl in *.ac_prefix : ArrivalCurvePrefix h : duration steps : seq (duration * nat) H_sorted_ltn : sorted_ltn_steps (h, steps) H_no_inf_arrivals : no_inf_arrivals (h, steps) t, v : nat IN : (t, v) \in steps
last (0 , 0 ) [seq step <- steps | step.1 <= t] = (t, v)
apply in_cat in IN; move : IN => [steps__l [steps__r EQ]]; subst steps.ac_prefix : ArrivalCurvePrefix h : duration t, v : nat steps__l, steps__r : seq (prod_eqType nat_eqType nat_eqType) H_no_inf_arrivals : no_inf_arrivals
(h,
steps__l ++
[:: (t, v)] ++ steps__r) H_sorted_ltn : sorted_ltn_steps
(h,
steps__l ++ [:: (t, v)] ++ steps__r)
last (0 , 0 )
[seq step <- steps__l ++ [:: (t, v)] ++ steps__r
| step.1 <= t] = (t, v)
apply sorted_cat in H_sorted_ltn; destruct H_sorted_ltn; clear H_sorted_ltn; last by apply ltn_steps_is_transitive.ac_prefix : ArrivalCurvePrefix h : duration t, v : nat steps__l, steps__r : seq (prod_eqType nat_eqType nat_eqType) H_no_inf_arrivals : no_inf_arrivals
(h,
steps__l ++
[:: (t, v)] ++ steps__r) H : sorted ltn_steps steps__l H0 : sorted ltn_steps ([:: (t, v)] ++ steps__r)
last (0 , 0 )
[seq step <- steps__l ++ [:: (t, v)] ++ steps__r
| step.1 <= t] = (t, v)
rewrite filter_cat last_cat (nonnil_last _ _ (0 ,0 )); last by rewrite //= leqnn.ac_prefix : ArrivalCurvePrefix h : duration t, v : nat steps__l, steps__r : seq (prod_eqType nat_eqType nat_eqType) H_no_inf_arrivals : no_inf_arrivals
(h,
steps__l ++
[:: (t, v)] ++ steps__r) H : sorted ltn_steps steps__l H0 : sorted ltn_steps ([:: (t, v)] ++ steps__r)
last (0 , 0 )
[seq step <- [:: (t, v)] ++ steps__r | step.1 <= t] =
(t, v)
move : H0; rewrite //= path_sortedE; auto using ltn_steps_is_transitive; rewrite //= leqnn => /andP [ALL SORT].ac_prefix : ArrivalCurvePrefix h : duration t, v : nat steps__l, steps__r : seq (prod_eqType nat_eqType nat_eqType) H_no_inf_arrivals : no_inf_arrivals
(h,
steps__l ++
[:: (t, v)] ++ steps__r) H : sorted ltn_steps steps__l ALL : all (ltn_steps (t, v)) steps__rSORT : sorted ltn_steps steps__r
last (0 , 0 )
((t, v) :: [seq step <- steps__r | step.1 <= t]) =
(t, v)
simpl ; replace (filter _ _ ) with (@nil (nat * nat)); first by done .ac_prefix : ArrivalCurvePrefix h : duration t, v : nat steps__l, steps__r : seq (prod_eqType nat_eqType nat_eqType) H_no_inf_arrivals : no_inf_arrivals
(h,
steps__l ++
[:: (t, v)] ++ steps__r) H : sorted ltn_steps steps__l ALL : all (ltn_steps (t, v)) steps__rSORT : sorted ltn_steps steps__r
[::] = [seq step <- steps__r | step.1 <= t]
symmetry ; apply filter_in_pred0; intros x IN; rewrite -ltnNge.ac_prefix : ArrivalCurvePrefix h : duration t, v : nat steps__l, steps__r : seq (prod_eqType nat_eqType nat_eqType) H_no_inf_arrivals : no_inf_arrivals
(h,
steps__l ++
[:: (t, v)] ++ steps__r) H : sorted ltn_steps steps__l ALL : all (ltn_steps (t, v)) steps__rSORT : sorted ltn_steps steps__r x : prod_eqType nat_eqType nat_eqType IN : x \in steps__r
t < x.1
by move : ALL => /allP ALL; specialize (ALL _ IN); move : ALL; 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 + ε]. *)
Section ExtrapolatedArrivalCurve .
(** Consider an arbitrary [leq]-sorted arrival-curve prefix without infinite arrivals. *)
Variable ac_prefix : ArrivalCurvePrefix.
Hypothesis H_positive : positive_horizon ac_prefix.
Hypothesis H_sorted_leq : sorted_leq_steps ac_prefix.
(** 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).ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat
monotone leq (extrapolated_arrival_curve ac_prefix)
Proof .ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat
monotone leq (extrapolated_arrival_curve ac_prefix)
intros t1 t2 LE; unfold extrapolated_arrival_curve.ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat LE : t1 <= t2
t1 %/ horizon_of ac_prefix *
value_at ac_prefix (horizon_of ac_prefix) +
value_at ac_prefix (t1 %% horizon_of ac_prefix) <=
t2 %/ horizon_of ac_prefix *
value_at ac_prefix (horizon_of ac_prefix) +
value_at ac_prefix (t2 %% horizon_of ac_prefix)
replace (horizon_of _) with h; last by done .ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat LE : t1 <= t2
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
move : LE; rewrite leq_eqVlt => /orP [/eqP EQ | LTs].ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat EQ : t1 = t2
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
{ ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat EQ : t1 = t2
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
by subst t2. } ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat LTs : t1 < t2
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
{ ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat LTs : t1 < t2
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
have ALT : (t1 %/ h == t2 %/ h) \/ (t1 %/ h < t2 %/ h).ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat LTs : t1 < t2
t1 %/ h == t2 %/ h \/ t1 %/ h < t2 %/ h
{ ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat LTs : t1 < t2
t1 %/ h == t2 %/ h \/ t1 %/ h < t2 %/ h
by apply /orP; rewrite -leq_eqVlt; apply leq_div2r, ltnW. } ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat LTs : t1 < t2 ALT : t1 %/ h == t2 %/ h \/ t1 %/ h < t2 %/ h
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
move : ALT => [/eqP EQ | LT].ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat LTs : t1 < t2 EQ : t1 %/ h = t2 %/ h
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
{ ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat LTs : t1 < t2 EQ : t1 %/ h = t2 %/ h
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
rewrite EQ leq_add2l; apply value_at_monotone => //.ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat LTs : t1 < t2 EQ : t1 %/ h = t2 %/ h
t1 %% h <= t2 %% h
by apply eqdivn_leqmodn; lia .
} ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat LTs : t1 < t2 LT : t1 %/ h < t2 %/ h
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
{ ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat LTs : t1 < t2 LT : t1 %/ h < t2 %/ h
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
have EQ: exists k , t1 + k = t2 /\ k > 0 .ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat LTs : t1 < t2 LT : t1 %/ h < t2 %/ h
exists k : nat, t1 + k = t2 /\ 0 < k
{ ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat LTs : t1 < t2 LT : t1 %/ h < t2 %/ h
exists k : nat, t1 + k = t2 /\ 0 < k
exists (t2 - t1); split ; lia . } ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, t2 : nat LTs : t1 < t2 LT : t1 %/ h < t2 %/ h EQ : exists k : nat, t1 + k = t2 /\ 0 < k
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
destruct EQ as [k [EQ POS]]; subst t2; clear LTs.ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat LT : t1 %/ h < (t1 + k) %/ h POS : 0 < k
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
(t1 + k) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t1 + k) %% h)
rewrite divnD; last by done .ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat LT : t1 %/ h < (t1 + k) %/ h POS : 0 < k
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
(t1 %/ h + k %/ h + (h <= t1 %% h + k %% h)) *
value_at ac_prefix h +
value_at ac_prefix ((t1 + k) %% h)
rewrite !mulnDl -!addnA leq_add2l.ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat LT : t1 %/ h < (t1 + k) %/ h POS : 0 < k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h +
((h <= t1 %% h + k %% h) * value_at ac_prefix h +
value_at ac_prefix ((t1 + k) %% h))
destruct (leqP h k) as [LEk|LTk].ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat LT : t1 %/ h < (t1 + k) %/ h POS : 0 < kLEk : h <= k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h +
((h <= t1 %% h + k %% h) * value_at ac_prefix h +
value_at ac_prefix ((t1 + k) %% h))
{ ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat LT : t1 %/ h < (t1 + k) %/ h POS : 0 < kLEk : h <= k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h +
((h <= t1 %% h + k %% h) * value_at ac_prefix h +
value_at ac_prefix ((t1 + k) %% h))
eapply leq_trans; last by apply leq_addr.ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat LT : t1 %/ h < (t1 + k) %/ h POS : 0 < kLEk : h <= k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h
move : LEk; rewrite leq_eqVlt => /orP [/eqP EQk | LTk].ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat LT : t1 %/ h < (t1 + k) %/ h POS : 0 < kEQk : h = k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h
{ ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat LT : t1 %/ h < (t1 + k) %/ h POS : 0 < kEQk : h = k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h
by subst ; rewrite divnn POS mul1n; apply value_at_monotone, ltnW, ltn_pmod. } ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat LT : t1 %/ h < (t1 + k) %/ h POS : 0 < kLTk : h < k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h
{ ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat LT : t1 %/ h < (t1 + k) %/ h POS : 0 < kLTk : h < k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h
rewrite -[value_at _ (t1 %% h)]mul1n; apply leq_mul.ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat LT : t1 %/ h < (t1 + k) %/ h POS : 0 < kLTk : h < k
0 < k %/ h
rewrite divn_gt0; [by apply ltnW | by done ].ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat LT : t1 %/ h < (t1 + k) %/ h POS : 0 < kLTk : h < k
value_at ac_prefix (t1 %% h) <= value_at ac_prefix h
by apply value_at_monotone, ltnW, ltn_pmod.
}
} ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat LT : t1 %/ h < (t1 + k) %/ h POS : 0 < kLTk : k < h
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h +
((h <= t1 %% h + k %% h) * value_at ac_prefix h +
value_at ac_prefix ((t1 + k) %% h))
{ ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat LT : t1 %/ h < (t1 + k) %/ h POS : 0 < kLTk : k < h
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h +
((h <= t1 %% h + k %% h) * value_at ac_prefix h +
value_at ac_prefix ((t1 + k) %% h))
rewrite divn_small // mul0n add0n.ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat LT : t1 %/ h < (t1 + k) %/ h POS : 0 < kLTk : k < h
value_at ac_prefix (t1 %% h) <=
(h <= t1 %% h + k %% h) * value_at ac_prefix h +
value_at ac_prefix ((t1 + k) %% h)
rewrite divnD // in LT; move : LT; rewrite -addnA -addn1 leq_add2l divn_small // add0n.ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat POS : 0 < kLTk : k < h
0 < (h <= t1 %% h + k %% h) ->
value_at ac_prefix (t1 %% h) <=
(h <= t1 %% h + k %% h) * value_at ac_prefix h +
value_at ac_prefix ((t1 + k) %% h)
rewrite lt0b => F; rewrite F; clear F.ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat POS : 0 < kLTk : k < h
value_at ac_prefix (t1 %% h) <=
true * value_at ac_prefix h +
value_at ac_prefix ((t1 + k) %% h)
rewrite mul1n; eapply leq_trans; last by apply leq_addr.ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t1, k : nat POS : 0 < kLTk : k < h
value_at ac_prefix (t1 %% h) <= value_at ac_prefix h
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 :
forall 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).ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat
forall t : duration,
extrapolated_arrival_curve ac_prefix t
!= extrapolated_arrival_curve ac_prefix (t + ε) ->
t %/ h < (t + ε) %/ h \/
t %/ h = (t + ε) %/ h /\
prefix (t %% h) < prefix ((t + ε) %% h)
Proof .ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat
forall t : duration,
extrapolated_arrival_curve ac_prefix t
!= extrapolated_arrival_curve ac_prefix (t + ε) ->
t %/ h < (t + ε) %/ h \/
t %/ h = (t + ε) %/ h /\
prefix (t %% h) < prefix ((t + ε) %% h)
intros t NEQ.ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t : duration NEQ : extrapolated_arrival_curve ac_prefix t
!= extrapolated_arrival_curve ac_prefix (t + ε)
t %/ h < (t + ε) %/ h \/
t %/ h = (t + ε) %/ h /\
prefix (t %% h) < prefix ((t + ε) %% h)
have LT := ltn_neqAle (extrapolated_arrival_curve ac_prefix t) (extrapolated_arrival_curve ac_prefix (t + ε)).ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t : duration NEQ : extrapolated_arrival_curve ac_prefix t
!= extrapolated_arrival_curve ac_prefix (t + ε) LT : (extrapolated_arrival_curve ac_prefix t <
extrapolated_arrival_curve ac_prefix (t + ε)) =
(extrapolated_arrival_curve ac_prefix t
!= extrapolated_arrival_curve ac_prefix (t + ε)) &&
(extrapolated_arrival_curve ac_prefix t <=
extrapolated_arrival_curve ac_prefix (t + ε))
t %/ h < (t + ε) %/ h \/
t %/ h = (t + ε) %/ h /\
prefix (t %% h) < prefix ((t + ε) %% h)
rewrite NEQ in LT; rewrite extrapolated_arrival_curve_is_monotone in LT; last by apply leq_addr.ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t : duration NEQ : extrapolated_arrival_curve ac_prefix t
!= extrapolated_arrival_curve ac_prefix (t + ε) LT : (extrapolated_arrival_curve ac_prefix t <
extrapolated_arrival_curve ac_prefix (t + ε)) =
true && true
t %/ h < (t + ε) %/ h \/
t %/ h = (t + ε) %/ h /\
prefix (t %% h) < prefix ((t + ε) %% h)
clear NEQ; simpl in LT.ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t : duration LT : (extrapolated_arrival_curve ac_prefix t <
extrapolated_arrival_curve ac_prefix (t + ε)) =
true
t %/ h < (t + ε) %/ h \/
t %/ h = (t + ε) %/ h /\
prefix (t %% h) < prefix ((t + ε) %% h)
unfold extrapolated_arrival_curve in LT.ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t : duration LT : (t %/ horizon_of ac_prefix *
value_at ac_prefix (horizon_of ac_prefix) +
value_at ac_prefix (t %% horizon_of ac_prefix) <
(t + ε) %/ horizon_of ac_prefix *
value_at ac_prefix (horizon_of ac_prefix) +
value_at ac_prefix
((t + ε) %% horizon_of ac_prefix)) = true
t %/ h < (t + ε) %/ h \/
t %/ h = (t + ε) %/ h /\
prefix (t %% h) < prefix ((t + ε) %% h)
replace (horizon_of _) with h in LT; last by done .ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t : duration LT : (t %/ h * value_at ac_prefix h +
value_at ac_prefix (t %% h) <
(t + ε) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + ε) %% h)) = true
t %/ h < (t + ε) %/ h \/
t %/ h = (t + ε) %/ h /\
prefix (t %% h) < prefix ((t + ε) %% h)
have AF : forall s1 s2 m x y ,
s1 <= s2 ->
m * s1 + x < m * s2 + y ->
s1 < s2 \/ s1 = s2 /\ x < y.ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t : duration LT : (t %/ h * value_at ac_prefix h +
value_at ac_prefix (t %% h) <
(t + ε) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + ε) %% h)) = true
forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y -> s1 < s2 \/ s1 = s2 /\ x < y
{ ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t : duration LT : (t %/ h * value_at ac_prefix h +
value_at ac_prefix (t %% h) <
(t + ε) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + ε) %% h)) = true
forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y -> s1 < s2 \/ s1 = s2 /\ x < y
clear ; intros * LEs LT.s1, s2, m, x, y : nat LEs : s1 <= s2 LT : m * s1 + x < m * s2 + y
s1 < s2 \/ s1 = s2 /\ x < y
move : LEs; rewrite leq_eqVlt => /orP [/eqP EQ | LTs].s1, s2, m, x, y : nat LT : m * s1 + x < m * s2 + y EQ : s1 = s2
s1 < s2 \/ s1 = s2 /\ x < y
{ s1, s2, m, x, y : nat LT : m * s1 + x < m * s2 + y EQ : s1 = s2
s1 < s2 \/ s1 = s2 /\ x < y
by subst s2; rename s1 into s; right ; split ; [ done | lia ]. } s1, s2, m, x, y : nat LT : m * s1 + x < m * s2 + y LTs : s1 < s2
s1 < s2 \/ s1 = s2 /\ x < y
{ s1, s2, m, x, y : nat LT : m * s1 + x < m * s2 + y LTs : s1 < s2
s1 < s2 \/ s1 = s2 /\ x < y
by left . }
} ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t : duration LT : (t %/ h * value_at ac_prefix h +
value_at ac_prefix (t %% h) <
(t + ε) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + ε) %% h)) = true AF : forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y ->
s1 < s2 \/ s1 = s2 /\ x < y
t %/ h < (t + ε) %/ h \/
t %/ h = (t + ε) %/ h /\
prefix (t %% h) < prefix ((t + ε) %% h)
apply AF with (m := prefix h).ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t : duration LT : (t %/ h * value_at ac_prefix h +
value_at ac_prefix (t %% h) <
(t + ε) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + ε) %% h)) = true AF : forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y ->
s1 < s2 \/ s1 = s2 /\ x < y
t %/ h <= (t + ε) %/ h
{ ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t : duration LT : (t %/ h * value_at ac_prefix h +
value_at ac_prefix (t %% h) <
(t + ε) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + ε) %% h)) = true AF : forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y ->
s1 < s2 \/ s1 = s2 /\ x < y
t %/ h <= (t + ε) %/ h
by apply leq_div2r, leq_addr. } ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t : duration LT : (t %/ h * value_at ac_prefix h +
value_at ac_prefix (t %% h) <
(t + ε) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + ε) %% h)) = true AF : forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y ->
s1 < s2 \/ s1 = s2 /\ x < y
prefix h * (t %/ h) + prefix (t %% h) <
prefix h * ((t + ε) %/ h) + prefix ((t + ε) %% h)
{ ac_prefix : ArrivalCurvePrefix H_positive : positive_horizon ac_prefix H_sorted_leq : sorted_leq_steps ac_prefix h := horizon_of ac_prefix : duration prefix := value_at ac_prefix : duration -> nat t : duration LT : (t %/ h * value_at ac_prefix h +
value_at ac_prefix (t %% h) <
(t + ε) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + ε) %% h)) = true AF : forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y ->
s1 < s2 \/ s1 = s2 /\ x < y
prefix h * (t %/ h) + prefix (t %% h) <
prefix h * ((t + ε) %/ h) + prefix ((t + ε) %% h)
by rewrite ![prefix _ * _]mulnC; apply LT. }
Qed .
End ExtrapolatedArrivalCurve .