Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.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 .
Require Export prosa.behavior.time .
Require Export prosa.util.all .[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.implementation.definitions.extrapolated_arrival_curve.
(** 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
have steps_sorted := H_sorted_leq; clear H_sorted_leq.ac_prefix : ArrivalCurvePrefix h : duration steps : seq (duration * nat) t1, t2 : nat LE : t1 <= t2 steps_sorted : 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
elim : steps steps_sorted => [//|[t__c v__c] steps IHsteps] steps_sorted.ac_prefix : ArrivalCurvePrefix h : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : sorted leq_steps
(h, (t__c, v__c) :: steps).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 : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : sorted leq_steps
(h, (t__c, v__c) :: steps).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 : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall
x : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality,
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 : (steps_sorted); rewrite //= (@path_sorted_inE _ predT leq_steps); first last .ac_prefix : ArrivalCurvePrefix h : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : sorted leq_steps
(h, (t__c, v__c) :: steps).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 : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall
x : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality,
leq_steps (t__d2, v__d2) x}
all predT ((t__c, v__c) :: steps)
{ ac_prefix : ArrivalCurvePrefix h : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : sorted leq_steps
(h, (t__c, v__c) :: steps).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 : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall
x : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality,
leq_steps (t__d2, v__d2) x}
all predT ((t__c, v__c) :: steps)
by apply /allP. } ac_prefix : ArrivalCurvePrefix h : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : sorted leq_steps
(h, (t__c, v__c) :: steps).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 : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall
x : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality,
leq_steps (t__d2, v__d2) x}
{in predT & &, transitive (T:=nat * nat) leq_steps}
{ ac_prefix : ArrivalCurvePrefix h : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : sorted leq_steps
(h, (t__c, v__c) :: steps).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 : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall
x : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality,
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 : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : sorted leq_steps
(h, (t__c, v__c) :: steps).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 : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall
x : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality,
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 : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : sorted leq_steps
(h, (t__c, v__c) :: steps).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 : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality,
leq_steps (t__d1, v__d1) x} LTN2 : leq_steps (t__d2, v__d2) (t__c, v__c) ALL2 : {in steps,
forall
x : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality,
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 : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : path leq_steps (t__c, v__c) steps 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 : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : path leq_steps (t__c, v__c) steps 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
by rewrite R1 R2 //=; apply : IHsteps. } ac_prefix : ArrivalCurvePrefix h : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : path leq_steps (t__c, v__c) steps 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 : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : path leq_steps (t__c, v__c) steps 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
lia . } ac_prefix : ArrivalCurvePrefix h : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : path leq_steps (t__c, v__c) steps 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 : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : path leq_steps (t__c, v__c) steps 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 => //.ac_prefix : ArrivalCurvePrefix h : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : path leq_steps (t__c, v__c) steps 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 : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : path leq_steps (t__c, v__c) steps 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 : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : path leq_steps (t__c, v__c) steps 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 : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : path leq_steps (t__c, v__c) steps 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 : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : path leq_steps (t__c, v__c) steps 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 : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : path leq_steps (t__c, v__c) steps 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 : duration t1, t2 : nat LE : t1 <= t2 t__c : duration v__c : nat steps : seq (duration * nat) 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 steps_sorted : path leq_steps (t__c, v__c) steps 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
by apply IHsteps => //; 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
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 :
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 + 1 ) ->
exists v : Datatypes_nat__canonical__eqtype_Equality,
(t + 1 , 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 + 1 ) ->
exists v : Datatypes_nat__canonical__eqtype_Equality,
(t + 1 , v) \in steps_of ac_prefix
move => t 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 + 1 )
exists v : nat, (t + 1 , 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 + 1 ]).2
exists v : nat, (t + 1 , 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 + 1 ]).2
exists v : nat, (t + 1 , 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 + 1 & x.1 <= t] ++
[seq x <- steps | x.1 <= t + 1 & t < x.1 ])).2
exists v : nat, (t + 1 , 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 + 1 & x.1 <= t] ++
[seq x <- steps | x.1 <= t + 1 & t < x.1 ])).2
exists v : nat, (t + 1 , 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 : nat * nat => (x.1 <= t + 1 ) && (t < x.1 )) =1
(fun
x : Datatypes_nat__canonical__eqtype_Equality * nat
=> x.1 == t + 1 )
{ 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 : nat * nat => (x.1 <= t + 1 ) && (t < x.1 )) =1
(fun
x : Datatypes_nat__canonical__eqtype_Equality * nat
=> x.1 == t + 1 )
by move => [a b] /=; lia . } 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 + 1 & x.1 <= t] ++
[seq x <- steps | x.1 == t + 1 ])).2
exists v : nat, (t + 1 , 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 + 1 & x.1 <= t] ++
[seq x <- steps | x.1 == t + 1 ])).2
exists v : nat, (t + 1 , v) \in steps_of (h2, steps)
destruct ([seq x <- steps | fst x == t + ε]) as [|p l] 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 LST : [seq x <- steps | x.1 == t + 1 ] = [::] LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
[::])).2
exists v : nat, (t + 1 , v) \in 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 + 1 ] = [::] LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
[::])).2
exists v : nat, (t + 1 , v) \in 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 + 1 ] = [::]
(fun x : nat * nat => (x.1 <= t + 1 ) && (x.1 <= t)) =1
(fun x : nat * nat => 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 + 1 ] = [::]
(fun x : nat * nat => (x.1 <= t + 1 ) && (x.1 <= t)) =1
(fun x : nat * nat => x.1 <= t)
clear ; intros [a b]; simpl .t : duration a, b : nat
(a <= t + 1 ) && (a <= t) = (a <= t)
destruct (leqP a t).t : duration a, b : nat i : a <= t
(a <= t + 1 ) && true = true
- t : duration a, b : nat i : a <= t
(a <= t + 1 ) && true = true
by rewrite Bool.andb_true_r; apply /eqP; lia .
- t : duration a, b : nat i : t < a
(a <= t + 1 ) && 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 + 1 ] = [::] LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t] ++ [::])).2
exists v : nat, (t + 1 , v) \in 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 + 1 ] = [::] LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t] ++ [::])).2
exists v : nat, (t + 1 , v) \in 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 p : (Datatypes_nat__canonical__eqtype_Equality * nat)%type l : seq
(Datatypes_nat__canonical__eqtype_Equality * nat) LST : [seq x <- steps | x.1 == t + 1 ] = p :: l LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
p :: l)).2
exists v : nat, (t + 1 , v) \in 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 p : (Datatypes_nat__canonical__eqtype_Equality * nat)%type l : seq
(Datatypes_nat__canonical__eqtype_Equality * nat) LST : [seq x <- steps | x.1 == t + 1 ] = p :: l LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
p :: l)).2
exists v : nat, (t + 1 , v) \in steps
have : p \in [seq x <- steps | x.1 == t + 1 ]
by rewrite LST; apply : mem_head.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 p : (Datatypes_nat__canonical__eqtype_Equality * nat)%type l : seq
(Datatypes_nat__canonical__eqtype_Equality * nat) LST : [seq x <- steps | x.1 == t + 1 ] = p :: l LT : (last (0 , 0 ) [seq step <- steps | step.1 <= t]).2 <
(last (0 , 0 )
([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
p :: l)).2
p \in [seq x <- steps | x.1 == t + 1 ] ->
exists v : nat, (t + 1 , v) \in steps
move => {LT} {LST}; move : p => //= [t_c 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 l : seq
(Datatypes_nat__canonical__eqtype_Equality * nat) t_c, v_c : nat
(t_c, v_c) \in [seq x <- steps | x.1 == t + 1 ] ->
exists v : nat, (t + 1 , v) \in steps
by rewrite mem_filter => //= /andP [/eqP ->].
}
}
} 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 : nat * nat => 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 : nat * nat => 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
elim : steps SORT => [//|a steps IHsteps] /= SORT.ac_prefix : ArrivalCurvePrefix h2, t : duration a : (duration * nat)%type steps : seq (duration * nat) IHsteps : sorted leq_steps steps ->
sorted (fun x y : nat * nat => x.1 <= y.1 )
steps SORT : path leq_steps a 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, t : duration a : (duration * nat)%type steps : seq (duration * nat) 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, t : duration a : (duration * nat)%type steps : seq (duration * nat) 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, t : duration a : (duration * nat)%type steps : seq (duration * nat) 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 => [|//].ac_prefix : ArrivalCurvePrefix h2, t : duration a : (duration * nat)%type steps : seq (duration * nat) 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, t : duration a : (duration * nat)%type steps : seq (duration * nat) 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 : Datatypes_nat__canonical__eqtype_Equality 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 as [d l]; 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 *.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]] => [//|].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' : Datatypes_nat__canonical__eqtype_Equality 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' : Datatypes_nat__canonical__eqtype_Equality 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 : Datatypes_nat__canonical__eqtype_Equality,
(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 : Datatypes_nat__canonical__eqtype_Equality,
(t, v) \in steps_of ac_prefix ->
step_at ac_prefix t = (t, v)
case : ac_prefix H_sorted_ltn => [h steps] + //= ? ? IN.ac_prefix : ArrivalCurvePrefix H_sorted_ltn : sorted_ltn_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix h : duration steps : seq (duration * nat) _t_, _v_ : nat IN : (_t_, _v_) \in steps
sorted_ltn_steps (h, steps) ->
step_at (h, steps) _t_ = (_t_, _v_)
move : IN => /in_cat //= [steps__l [steps__r ->]] /sorted_cat //=; case => //= [|_ +]; first by apply ltn_steps_is_transitive.ac_prefix : ArrivalCurvePrefix H_sorted_ltn : sorted_ltn_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix h : duration steps : seq (duration * nat) _t_, _v_ : nat steps__l, steps__r : seq (nat * nat)
path ltn_steps (_t_, _v_) steps__r ->
step_at (h, steps__l ++ (_t_, _v_) :: steps__r) _t_ =
(_t_, _v_)
rewrite /step_at filter_cat last_cat (nonnil_last _ _ (0 ,0 )); last by rewrite //= leqnn.ac_prefix : ArrivalCurvePrefix H_sorted_ltn : sorted_ltn_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix h : duration steps : seq (duration * nat) _t_, _v_ : nat steps__l, steps__r : seq (nat * nat)
path ltn_steps (_t_, _v_) steps__r ->
last (0 , 0 )
[seq step <- (_t_, _v_) :: steps__r | step.1 <= _t_] =
(_t_, _v_)
rewrite //= path_sortedE; auto using ltn_steps_is_transitive; rewrite //= leqnn => /andP [ALL SORT].ac_prefix : ArrivalCurvePrefix H_sorted_ltn : sorted_ltn_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix h : duration steps : seq (duration * nat) _t_, _v_ : nat steps__l, steps__r : seq (nat * nat) 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_)
replace (filter _ _ ) with (@nil (nat * nat)) => [//|].ac_prefix : ArrivalCurvePrefix H_sorted_ltn : sorted_ltn_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix h : duration steps : seq (duration * nat) _t_, _v_ : nat steps__l, steps__r : seq (nat * nat) ALL : all (ltn_steps (_t_, _v_)) steps__rSORT : sorted ltn_steps steps__r
[::] = [seq step <- steps__r | step.1 <= _t_]
rewrite filter_in_pred0 // => x IN; rewrite -ltnNge.ac_prefix : ArrivalCurvePrefix H_sorted_ltn : sorted_ltn_steps ac_prefix H_no_inf_arrivals : no_inf_arrivals ac_prefix h : duration steps : seq (duration * nat) _t_, _v_ : nat steps__l, steps__r : seq (nat * nat) ALL : all (ltn_steps (_t_, _v_)) steps__rSORT : sorted ltn_steps steps__r x : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality IN : x \in steps__r
_t_ < x.1
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 + ε]. *)
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 => [|//].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//.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
- 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
by rewrite divn_gt0; [apply : 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, 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 + 1 ) ->
t %/ h < (t + 1 ) %/ h \/
t %/ h = (t + 1 ) %/ h /\
prefix (t %% h) < prefix ((t + 1 ) %% 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 + 1 ) ->
t %/ h < (t + 1 ) %/ h \/
t %/ h = (t + 1 ) %/ h /\
prefix (t %% h) < prefix ((t + 1 ) %% 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 + 1 )
t %/ h < (t + 1 ) %/ h \/
t %/ h = (t + 1 ) %/ h /\
prefix (t %% h) < prefix ((t + 1 ) %% 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 + 1 ) LT : (extrapolated_arrival_curve ac_prefix t <
extrapolated_arrival_curve ac_prefix (t + 1 )) =
(extrapolated_arrival_curve ac_prefix t
!= extrapolated_arrival_curve ac_prefix (t + 1 )) &&
(extrapolated_arrival_curve ac_prefix t <=
extrapolated_arrival_curve ac_prefix (t + 1 ))
t %/ h < (t + 1 ) %/ h \/
t %/ h = (t + 1 ) %/ h /\
prefix (t %% h) < prefix ((t + 1 ) %% 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 + 1 ) LT : (extrapolated_arrival_curve ac_prefix t <
extrapolated_arrival_curve ac_prefix (t + 1 )) =
true && true
t %/ h < (t + 1 ) %/ h \/
t %/ h = (t + 1 ) %/ h /\
prefix (t %% h) < prefix ((t + 1 ) %% 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 + 1 )) =
true
t %/ h < (t + 1 ) %/ h \/
t %/ h = (t + 1 ) %/ h /\
prefix (t %% h) < prefix ((t + 1 ) %% 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 + 1 ) %/ horizon_of ac_prefix *
value_at ac_prefix (horizon_of ac_prefix) +
value_at ac_prefix
((t + 1 ) %% horizon_of ac_prefix)) = true
t %/ h < (t + 1 ) %/ h \/
t %/ h = (t + 1 ) %/ h /\
prefix (t %% h) < prefix ((t + 1 ) %% h)
replace (horizon_of _) with h 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 %/ h * value_at ac_prefix h +
value_at ac_prefix (t %% h) <
(t + 1 ) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + 1 ) %% h)) = true
t %/ h < (t + 1 ) %/ h \/
t %/ h = (t + 1 ) %/ h /\
prefix (t %% h) < prefix ((t + 1 ) %% 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 + 1 ) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + 1 ) %% 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 + 1 ) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + 1 ) %% 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 s1 s2 m x y 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 ; [|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 + 1 ) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + 1 ) %% 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 + 1 ) %/ h \/
t %/ h = (t + 1 ) %/ h /\
prefix (t %% h) < prefix ((t + 1 ) %% 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 + 1 ) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + 1 ) %% 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 + 1 ) %/ 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 + 1 ) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + 1 ) %% 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 + 1 ) %/ 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 + 1 ) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + 1 ) %% 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 + 1 ) %/ h) + prefix ((t + 1 ) %% 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 + 1 ) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t + 1 ) %% 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 + 1 ) %/ h) + prefix ((t + 1 ) %% h)
by rewrite ![prefix _ * _]mulnC; apply LT. }
Qed .
End ExtrapolatedArrivalCurve .