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 .
Require Export prosa.implementation.refinements.arrival_curve_prefix.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]
(** In this section, we provide definitions and lemmas to show
Abstract RTA' s search space can be rewritten in an equivalent,
computation-oriented way. *)
Section FastSearchSpaceComputation .
(** Let L be a constant which bounds any busy interval of task [tsk]. *)
Variable L : duration.
(** Consider a task set [ts] with valid arrivals... *)
Variable ts : seq Task.
Hypothesis H_valid_task_set : task_set_with_valid_arrivals ts.
(** ... and a task [tsk] of [ts] with positive cost. *)
Variable tsk : Task.
Hypothesis H_positive_cost : 0 < task_cost tsk.
Hypothesis H_tsk_in_ts : tsk \in ts.
Section Definitions .
(** We generically define the search space for fixed-priority tasks in
the interval <<[l,r)>> by repeating the time steps of the task
in the interval <<[l*h,r*h)>>. *)
Definition search_space_arrival_curve_prefix_FP_h (tsk : Task) l r :=
let h := get_horizon_of_task tsk in
let offsets := map (muln h) (iota l r) in
let arrival_curve_prefix_offsets := repeat_steps_with_offset tsk offsets in
map predn arrival_curve_prefix_offsets.
(** By using the above definition, we give a concrete definition of
the search space for fixed-priority tasks. *)
Definition search_space_arrival_curve_prefix_FP (tsk : Task) L :=
let h := get_horizon_of_task tsk in
search_space_arrival_curve_prefix_FP_h (tsk : Task) 0 (L %/h).+1 .
End Definitions .
Section Facts .
(** We begin by showing that either each time step of an arrival curve prefix
is either strictly less than the horizon, or it is the horizon. *)
Lemma steps_lt_horizon_last_eq_horizon :
(forall s , s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk) \/
(last0 (get_time_steps_of_task tsk) = get_horizon_of_task tsk).L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts
(forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tsk) \/
last0 (get_time_steps_of_task tsk) =
get_horizon_of_task tsk
Proof .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts
(forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tsk) \/
last0 (get_time_steps_of_task tsk) =
get_horizon_of_task tsk
move : (has_valid_arrival_curve_prefix_tsk _ H_valid_task_set _ H_tsk_in_ts).L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts
has_valid_arrival_curve_prefix tsk ->
(forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tsk) \/
last0 (get_time_steps_of_task tsk) =
get_horizon_of_task tsk
move => [arrival_curve_prefix [EQ [POSh [LARGEh [NOINF [BUR SORT]]]]]].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix
(forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tsk) \/
last0 (get_time_steps_of_task tsk) =
get_horizon_of_task tsk
destruct (ltngtP (last0 (get_time_steps_of_task tsk)) (get_horizon_of_task tsk))
as [GT1 | LT1 | EQ1]; last by right .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix GT1 : last0 (get_time_steps_of_task tsk) <
get_horizon_of_task tsk
(forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tsk) \/
last0 (get_time_steps_of_task tsk) =
get_horizon_of_task tsk
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix GT1 : last0 (get_time_steps_of_task tsk) <
get_horizon_of_task tsk
(forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tsk) \/
last0 (get_time_steps_of_task tsk) =
get_horizon_of_task tsk
left .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix GT1 : last0 (get_time_steps_of_task tsk) <
get_horizon_of_task tsk
forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tsk
move => step IN.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix GT1 : last0 (get_time_steps_of_task tsk) <
get_horizon_of_task tsk step : nat_eqType IN : step \in get_time_steps_of_task tsk
step < get_horizon_of_task tsk
apply leq_ltn_trans with (n:=last0 (get_time_steps_of_task tsk)) => //.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix GT1 : last0 (get_time_steps_of_task tsk) <
get_horizon_of_task tsk step : nat_eqType IN : step \in get_time_steps_of_task tsk
step <= last0 (get_time_steps_of_task tsk)
move : (time_steps_sorted ts H_valid_task_set tsk H_tsk_in_ts).L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix GT1 : last0 (get_time_steps_of_task tsk) <
get_horizon_of_task tsk step : nat_eqType IN : step \in get_time_steps_of_task tsk
sorted ltn (get_time_steps_of_task tsk) ->
step <= last0 (get_time_steps_of_task tsk)
rewrite ltn_sorted_uniq_leq => /andP [TS_UNIQ TS_SORT].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix GT1 : last0 (get_time_steps_of_task tsk) <
get_horizon_of_task tsk step : nat_eqType IN : step \in get_time_steps_of_task tsk TS_UNIQ : uniq (get_time_steps_of_task tsk) TS_SORT : sorted leq (get_time_steps_of_task tsk)
step <= last0 (get_time_steps_of_task tsk)
apply (sorted_leq_index leq_trans leqnn TS_SORT step _ IN) => //=.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix GT1 : last0 (get_time_steps_of_task tsk) <
get_horizon_of_task tsk step : nat_eqType IN : step \in get_time_steps_of_task tsk TS_UNIQ : uniq (get_time_steps_of_task tsk) TS_SORT : sorted leq (get_time_steps_of_task tsk)
last0 (get_time_steps_of_task tsk)
\in get_time_steps_of_task tsk
- L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix GT1 : last0 (get_time_steps_of_task tsk) <
get_horizon_of_task tsk step : nat_eqType IN : step \in get_time_steps_of_task tsk TS_UNIQ : uniq (get_time_steps_of_task tsk) TS_SORT : sorted leq (get_time_steps_of_task tsk)
last0 (get_time_steps_of_task tsk)
\in get_time_steps_of_task tsk
by destruct get_time_steps_of_task; last by rewrite /last0 //=; apply mem_last.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix GT1 : last0 (get_time_steps_of_task tsk) <
get_horizon_of_task tsk step : nat_eqType IN : step \in get_time_steps_of_task tsk TS_UNIQ : uniq (get_time_steps_of_task tsk) TS_SORT : sorted leq (get_time_steps_of_task tsk)
index step (get_time_steps_of_task tsk) <=
index (last0 (get_time_steps_of_task tsk))
(get_time_steps_of_task tsk)
- L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix GT1 : last0 (get_time_steps_of_task tsk) <
get_horizon_of_task tsk step : nat_eqType IN : step \in get_time_steps_of_task tsk TS_UNIQ : uniq (get_time_steps_of_task tsk) TS_SORT : sorted leq (get_time_steps_of_task tsk)
index step (get_time_steps_of_task tsk) <=
index (last0 (get_time_steps_of_task tsk))
(get_time_steps_of_task tsk)
destruct get_time_steps_of_task; rewrite //= -index_mem in IN.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix d : duration l : seq duration GT1 : last0 (d :: l) < get_horizon_of_task tsk step : nat_eqType TS_UNIQ : uniq (d :: l) TS_SORT : sorted leq (d :: l) IN : index step (d :: l) < size (d :: l)
index step (d :: l) <= index (last0 (d :: l)) (d :: l)
by rewrite /last0; simpl (last 0 _); rewrite index_last. } L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix LT1 : get_horizon_of_task tsk <
last0 (get_time_steps_of_task tsk)
(forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tsk) \/
last0 (get_time_steps_of_task tsk) =
get_horizon_of_task tsk
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix LT1 : get_horizon_of_task tsk <
last0 (get_time_steps_of_task tsk)
(forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tsk) \/
last0 (get_time_steps_of_task tsk) =
get_horizon_of_task tsk
exfalso . (* h is at least the last step *) L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix LT1 : get_horizon_of_task tsk <
last0 (get_time_steps_of_task tsk)
False
destruct get_time_steps_of_task eqn :TS => //.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix d : duration l : seq duration TS : get_time_steps_of_task tsk = d :: l LT1 : get_horizon_of_task tsk < last0 (d :: l)
False
have IN: last0 (d::l) \in d::l by rewrite /last0 //=; apply mem_last.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : large_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix d : duration l : seq duration TS : get_time_steps_of_task tsk = d :: l LT1 : get_horizon_of_task tsk < last0 (d :: l) IN : last0 (d :: l) \in d :: l
False
unfold large_horizon, get_time_steps_of_task in *.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix LARGEh : forall s : nat_eqType,
s \in time_steps_of arrival_curve_prefix ->
s <= horizon_of arrival_curve_prefixNOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix d : duration l : seq duration TS : time_steps_of (get_arrival_curve_prefix tsk) =
d :: l LT1 : get_horizon_of_task tsk < last0 (d :: l) IN : last0 (d :: l) \in d :: l
False
rewrite EQ in TS; rewrite TS in LARGEh.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix d : duration l : seq duration LT1 : get_horizon_of_task tsk < last0 (d :: l) IN : last0 (d :: l) \in d :: l TS : time_steps_of arrival_curve_prefix = d :: l LARGEh : forall s : nat_eqType,
s \in d :: l ->
s <= horizon_of arrival_curve_prefix
False
apply LARGEh in IN.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts arrival_curve_prefix : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk =
arrival_curve_prefix POSh : positive_horizon arrival_curve_prefix NOINF : no_inf_arrivals arrival_curve_prefix BUR : specified_bursts arrival_curve_prefix SORT : sorted_ltn_steps arrival_curve_prefix d : duration l : seq duration LT1 : get_horizon_of_task tsk < last0 (d :: l) IN : last0 (d :: l) <= horizon_of arrival_curve_prefix TS : time_steps_of arrival_curve_prefix = d :: l LARGEh : forall s : nat_eqType,
s \in d :: l ->
s <= horizon_of arrival_curve_prefix
False
by rewrite /get_horizon_of_task EQ in LT1; lia . }
Qed .
(** Next, we show that for each offset [A] in the search space for fixed-priority
tasks, either (1) [A+ε] is zero or a multiple of the horizon, offset by
one of the time steps of the arrival curve prefix, or (2) [A+ε] is
exactly a multiple of the horizon. *)
Lemma structure_of_correct_search_space :
forall A ,
A < L ->
task_rbf tsk A != task_rbf tsk (A + ε) ->
(exists i t ,
i < (L %/ get_horizon_of_task tsk).+1
/\ (t \in get_time_steps_of_task tsk)
/\ A + ε = i * get_horizon_of_task tsk + t )
\/ (exists i ,
i < (L %/ get_horizon_of_task tsk).+1
/\ A + ε = i * get_horizon_of_task tsk).L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts
forall A : nat,
A < L ->
task_rbf tsk A != task_rbf tsk (A + ε) ->
(exists (i : nat) (t : nat_eqType),
i < (L %/ get_horizon_of_task tsk).+1 /\
t \in get_time_steps_of_task tsk /\
A + ε = i * get_horizon_of_task tsk + t) \/
(exists i : nat,
i < (L %/ get_horizon_of_task tsk).+1 /\
A + ε = i * get_horizon_of_task tsk)
Proof .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts
forall A : nat,
A < L ->
task_rbf tsk A != task_rbf tsk (A + ε) ->
(exists (i : nat) (t : nat_eqType),
i < (L %/ get_horizon_of_task tsk).+1 /\
t \in get_time_steps_of_task tsk /\
A + ε = i * get_horizon_of_task tsk + t) \/
(exists i : nat,
i < (L %/ get_horizon_of_task tsk).+1 /\
A + ε = i * get_horizon_of_task tsk)
move : (has_valid_arrival_curve_prefix_tsk ts H_valid_task_set tsk H_tsk_in_ts).L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts
has_valid_arrival_curve_prefix tsk ->
forall A : nat,
A < L ->
task_rbf tsk A != task_rbf tsk (A + ε) ->
(exists (i : nat) (t : nat_eqType),
i < (L %/ get_horizon_of_task tsk).+1 /\
t \in get_time_steps_of_task tsk /\
A + ε = i * get_horizon_of_task tsk + t) \/
(exists i : nat,
i < (L %/ get_horizon_of_task tsk).+1 /\
A + ε = i * get_horizon_of_task tsk)
move => [evec [EQ [POSh [LARGEh [NOINF [BUR SORT]]]]]] A LT_L NEQ.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : task_rbf tsk A != task_rbf tsk (A + ε)
(exists (i : nat) (t : nat_eqType),
i < (L %/ get_horizon_of_task tsk).+1 /\
t \in get_time_steps_of_task tsk /\
A + ε = i * get_horizon_of_task tsk + t) \/
(exists i : nat,
i < (L %/ get_horizon_of_task tsk).+1 /\
A + ε = i * get_horizon_of_task tsk)
rewrite eqn_pmul2l // /max_arrivals /MaxArrivals /ConcreteMaxArrivals
/concrete_max_arrivals EQ in NEQ.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε)
(exists (i : nat) (t : nat_eqType),
i < (L %/ get_horizon_of_task tsk).+1 /\
t \in get_time_steps_of_task tsk /\
A + ε = i * get_horizon_of_task tsk + t) \/
(exists i : nat,
i < (L %/ get_horizon_of_task tsk).+1 /\
A + ε = i * get_horizon_of_task tsk)
rewrite /get_horizon_of_task EQ.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε)
(exists (i : nat) (t : nat_eqType),
i < (L %/ horizon_of evec).+1 /\
t \in get_time_steps_of_task tsk /\
A + ε = i * horizon_of evec + t) \/
(exists i : nat,
i < (L %/ horizon_of evec).+1 /\
A + ε = i * horizon_of evec)
move : (sorted_ltn_steps_imply_sorted_leq_steps_steps _ SORT NOINF) => SORT_LEQ.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec
(exists (i : nat) (t : nat_eqType),
i < (L %/ horizon_of evec).+1 /\
t \in get_time_steps_of_task tsk /\
A + ε = i * horizon_of evec + t) \/
(exists i : nat,
i < (L %/ horizon_of evec).+1 /\
A + ε = i * horizon_of evec)
unfold positive_horizon in *; set (h := horizon_of evec) in *.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec
(exists (i : nat) (t : nat_eqType),
i < (L %/ h).+1 /\
t \in get_time_steps_of_task tsk /\
A + ε = i * h + t) \/
(exists i : nat, i < (L %/ h).+1 /\ A + ε = i * h)
move : (extrapolated_arrival_curve_change evec POSh SORT_LEQ A NEQ) => [LT|[EQdiv LTe]].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec LT : A %/ horizon_of evec < (A + ε) %/ horizon_of evec
(exists (i : nat) (t : nat_eqType),
i < (L %/ h).+1 /\
t \in get_time_steps_of_task tsk /\
A + ε = i * h + t) \/
(exists i : nat, i < (L %/ h).+1 /\ A + ε = i * h)
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec LT : A %/ horizon_of evec < (A + ε) %/ horizon_of evec
(exists (i : nat) (t : nat_eqType),
i < (L %/ h).+1 /\
t \in get_time_steps_of_task tsk /\
A + ε = i * h + t) \/
(exists i : nat, i < (L %/ h).+1 /\ A + ε = i * h)
right .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec LT : A %/ horizon_of evec < (A + ε) %/ horizon_of evec
exists i : nat, i < (L %/ h).+1 /\ A + ε = i * h
exists ((A+ε) %/ h); split ; first by rewrite ltnS leq_div2r // /ε; lia .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec LT : A %/ horizon_of evec < (A + ε) %/ horizon_of evec
A + ε = (A + ε) %/ h * h
by symmetry ; apply /eqP; rewrite -dvdn_eq; by apply ltdivn_dvdn. } L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec)
(exists (i : nat) (t : nat_eqType),
i < (L %/ h).+1 /\
t \in get_time_steps_of_task tsk /\
A + ε = i * h + t) \/
(exists i : nat, i < (L %/ h).+1 /\ A + ε = i * h)
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec)
(exists (i : nat) (t : nat_eqType),
i < (L %/ h).+1 /\
t \in get_time_steps_of_task tsk /\
A + ε = i * h + t) \/
(exists i : nat, i < (L %/ h).+1 /\ A + ε = i * h)
left .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec)
exists (i : nat) (t : nat_eqType),
i < (L %/ h).+1 /\
t \in get_time_steps_of_task tsk /\
A + ε = i * h + t
exists ((A + ε) %/ h), (step_at evec ((A + ε) %% h)).1 ; split ; last split .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec)
(A + ε) %/ h < (L %/ h).+1
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec)
(A + ε) %/ h < (L %/ h).+1
by rewrite addn1 ltnS; apply leq_div2r. } L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec)
(step_at evec ((A + ε) %% h)).1
\in get_time_steps_of_task tsk
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec)
(step_at evec ((A + ε) %% h)).1
\in get_time_steps_of_task tsk
rewrite /get_time_steps_of_task EQ.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec)
(step_at evec ((A + ε) %% h)).1 \in time_steps_of evec
have -> := @map_f _ _ fst (steps_of _) (last (0 , 0 ) [seq s <- _ | s.1 <= (A+ε)%%h])=> //.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec)
last (0 , 0 )
[seq s <- steps_of evec | s.1 <= (A + ε) %% h]
\in steps_of evec
have EQeps: (A + ε) %% h = A %% h + ε by apply addn1_modn_commute.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec) EQeps : (A + ε) %% h = A %% h + ε
last (0 , 0 )
[seq s <- steps_of evec | s.1 <= (A + ε) %% h]
\in steps_of evec
rewrite EQeps in LTe.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec EQeps : (A + ε) %% h = A %% h + ε LTe : value_at evec (A %% horizon_of evec) <
value_at evec (A %% h + ε)
last (0 , 0 )
[seq s <- steps_of evec | s.1 <= (A + ε) %% h]
\in steps_of evec
move : (value_at_change_is_in_steps_of _ SORT_LEQ NOINF _ LTe) => [v IN].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec EQeps : (A + ε) %% h = A %% h + ε LTe : value_at evec (A %% horizon_of evec) <
value_at evec (A %% h + ε) v : nat_eqType IN : (A %% horizon_of evec + ε, v) \in steps_of evec
last (0 , 0 )
[seq s <- steps_of evec | s.1 <= (A + ε) %% h]
\in steps_of evec
rewrite -EQeps in IN; apply filter_last_mem; apply /hasP.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec EQeps : (A + ε) %% h = A %% h + ε LTe : value_at evec (A %% horizon_of evec) <
value_at evec (A %% h + ε) v : nat_eqType IN : ((A + ε) %% h, v) \in steps_of evec
exists2 x : prod_eqType nat_eqType nat_eqType,
x \in steps_of evec & x.1 <= (A + ε) %% h
by exists ((A+ε) %% h, v). } L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec)
A + ε =
(A + ε) %/ h * h + (step_at evec ((A + ε) %% h)).1
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec)
A + ε =
(A + ε) %/ h * h + (step_at evec ((A + ε) %% h)).1
case (extrapolated_arrival_curve_change _ POSh SORT_LEQ _ NEQ) as [EQs|[EQs LT]].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec) EQs : A %/ horizon_of evec <
(A + ε) %/ horizon_of evec
A + ε =
(A + ε) %/ h * h + (step_at evec ((A + ε) %% h)).1
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec) EQs : A %/ horizon_of evec <
(A + ε) %/ horizon_of evec
A + ε =
(A + ε) %/ h * h + (step_at evec ((A + ε) %% h)).1
apply ltdivn_dvdn in EQs; move : EQs => /dvdnP [k EQs]; rewrite EQs.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec) k : nat EQs : A + 1 = k * horizon_of evec
k * horizon_of evec =
(k * horizon_of evec) %/ h * h +
(step_at evec ((k * horizon_of evec) %% h)).1
by rewrite modnMl step_at_0_is_00; [rewrite addn0 mulnK | apply SORT |]. } L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec) EQs : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LT : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec)
A + ε =
(A + ε) %/ h * h + (step_at evec ((A + ε) %% h)).1
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LTe : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec) EQs : A %/ horizon_of evec =
(A + ε) %/ horizon_of evec LT : value_at evec (A %% horizon_of evec) <
value_at evec ((A + ε) %% horizon_of evec)
A + ε =
(A + ε) %/ h * h + (step_at evec ((A + ε) %% h)).1
subst h; unfold ε in *; set (h := horizon_of evec) in *.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + 1 ) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ h = (A + 1 ) %/ h LTe : value_at evec (A %% h) <
value_at evec ((A + 1 ) %% h) EQs : A %/ h = (A + 1 ) %/ h LT : value_at evec (A %% h) <
value_at evec ((A + 1 ) %% h)
A + 1 =
(A + 1 ) %/ h * h + (step_at evec ((A + 1 ) %% h)).1
rewrite {1 }[_ + _](divn_eq _ h).L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + 1 ) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ h = (A + 1 ) %/ h LTe : value_at evec (A %% h) <
value_at evec ((A + 1 ) %% h) EQs : A %/ h = (A + 1 ) %/ h LT : value_at evec (A %% h) <
value_at evec ((A + 1 ) %% h)
(A + 1 ) %/ h * h + (A + 1 ) %% h =
(A + 1 ) %/ h * h + (step_at evec ((A + 1 ) %% h)).1
apply /eqP; rewrite eqn_add2l; apply /eqP.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + 1 ) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ h = (A + 1 ) %/ h LTe : value_at evec (A %% h) <
value_at evec ((A + 1 ) %% h) EQs : A %/ h = (A + 1 ) %/ h LT : value_at evec (A %% h) <
value_at evec ((A + 1 ) %% h)
(A + 1 ) %% h = (step_at evec ((A + 1 ) %% h)).1
rewrite modnD //= [h <= _]leqNgt addmod_le_mod //= subn0 in LT.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + 1 ) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ h = (A + 1 ) %/ h LTe : value_at evec (A %% h) <
value_at evec ((A + 1 ) %% h) EQs : A %/ h = (A + 1 ) %/ h LT : value_at evec (A %% h) <
value_at evec (A %% h + 1 %% h)
(A + 1 ) %% h = (step_at evec ((A + 1 ) %% h)).1
have EQ1: 1 %%h= 1 by apply modn_small; case h as [|[|h]]; rewrite //= in EQs; lia .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + 1 ) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ h = (A + 1 ) %/ h LTe : value_at evec (A %% h) <
value_at evec ((A + 1 ) %% h) EQs : A %/ h = (A + 1 ) %/ h LT : value_at evec (A %% h) <
value_at evec (A %% h + 1 %% h) EQ1 : 1 %% h = 1
(A + 1 ) %% h = (step_at evec ((A + 1 ) %% h)).1
rewrite EQ1 in LT; apply value_at_change_is_in_steps_of in LT => //.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + 1 ) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ h = (A + 1 ) %/ h LTe : value_at evec (A %% h) <
value_at evec ((A + 1 ) %% h) EQs : A %/ h = (A + 1 ) %/ h EQ1 : 1 %% h = 1 LT : exists v : nat_eqType,
(A %% h + ε, v) \in steps_of evec
(A + 1 ) %% h = (step_at evec ((A + 1 ) %% h)).1
case LT as [v IN].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + 1 ) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ h = (A + 1 ) %/ h LTe : value_at evec (A %% h) <
value_at evec ((A + 1 ) %% h) EQs : A %/ h = (A + 1 ) %/ h EQ1 : 1 %% h = 1 v : nat_eqType IN : (A %% h + ε, v) \in steps_of evec
(A + 1 ) %% h = (step_at evec ((A + 1 ) %% h)).1
rewrite modnD //= [h <= _]leqNgt addmod_le_mod //=.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + 1 ) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ h = (A + 1 ) %/ h LTe : value_at evec (A %% h) <
value_at evec ((A + 1 ) %% h) EQs : A %/ h = (A + 1 ) %/ h EQ1 : 1 %% h = 1 v : nat_eqType IN : (A %% h + ε, v) \in steps_of evec
A %% h + 1 %% h - 0 * h =
(step_at evec (A %% h + 1 %% h - 0 * h)).1
apply step_at_agrees_with_steps_of in IN => //.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EQ : get_arrival_curve_prefix tsk = evec h := horizon_of evec : duration POSh : 0 < hLARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT_L : A < L NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + 1 ) SORT_LEQ : sorted_leq_steps evec EQdiv : A %/ h = (A + 1 ) %/ h LTe : value_at evec (A %% h) <
value_at evec ((A + 1 ) %% h) EQs : A %/ h = (A + 1 ) %/ h EQ1 : 1 %% h = 1 v : nat_eqType IN : step_at evec (A %% h + ε) = (A %% h + ε, v)
A %% h + 1 %% h - 0 * h =
(step_at evec (A %% h + 1 %% h - 0 * h)).1
by rewrite subn0 !EQ1 IN. } } }
Qed .
(** Conversely, every multiple of the horizon that is strictly less than [L] is contained
in the search space for fixed-priority tasks... *)
Lemma multiple_of_horizon_in_approx_ss :
forall A ,
A < L ->
get_horizon_of_task tsk %| A ->
A \in search_space_arrival_curve_prefix_FP tsk L.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts
forall A : nat,
A < L ->
get_horizon_of_task tsk %| A ->
A \in search_space_arrival_curve_prefix_FP tsk L
Proof .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts
forall A : nat,
A < L ->
get_horizon_of_task tsk %| A ->
A \in search_space_arrival_curve_prefix_FP tsk L
move : (has_valid_arrival_curve_prefix_tsk ts H_valid_task_set tsk H_tsk_in_ts) => [evec [EMAX VALID]].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec VALID : valid_arrival_curve_prefix evec
forall A : nat,
A < L ->
get_horizon_of_task tsk %| A ->
A \in search_space_arrival_curve_prefix_FP tsk L
intros * LT DIV; rewrite /search_space_arrival_curve_prefix_FP.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec VALID : valid_arrival_curve_prefix evec A : nat LT : A < L DIV : get_horizon_of_task tsk %| A
A
\in search_space_arrival_curve_prefix_FP_h tsk 0
(L %/ get_horizon_of_task tsk).+1
destruct VALID as [POSh [LARGEh [NOINF [BUR SORT]]]].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT : A < L DIV : get_horizon_of_task tsk %| A
A
\in search_space_arrival_curve_prefix_FP_h tsk 0
(L %/ get_horizon_of_task tsk).+1
replace A with (A + ε - ε); last by lia .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT : A < L DIV : get_horizon_of_task tsk %| A
A + ε - ε
\in search_space_arrival_curve_prefix_FP_h tsk 0
(L %/ get_horizon_of_task tsk).+1
rewrite subn1; apply map_f.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT : A < L DIV : get_horizon_of_task tsk %| A
A + ε
\in repeat_steps_with_offset tsk
[seq get_horizon_of_task tsk * i
| i <- iota 0
(L %/ get_horizon_of_task tsk).+1 ]
set (h := get_horizon_of_task tsk) in *.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT : A < L h := get_horizon_of_task tsk : duration DIV : h %| A
A + ε
\in repeat_steps_with_offset tsk
[seq h * i | i <- iota 0 (L %/ h).+1 ]
rewrite /repeat_steps_with_offset; apply /flatten_mapP.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LT : A < L h := get_horizon_of_task tsk : duration DIV : h %| A
exists2 x : nat_eqType,
x \in [seq h * i | i <- iota 0 (L %/ h).+1 ] &
A + ε \in time_steps_with_offset tsk x
move : DIV => /dvdnP [k DIV]; subst A.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec h := get_horizon_of_task tsk : duration k : nat LT : k * h < L
exists2 x : nat_eqType,
x \in [seq h * i | i <- iota 0 (L %/ h).+1 ] &
k * h + ε \in time_steps_with_offset tsk x
exists (k * h).L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec h := get_horizon_of_task tsk : duration k : nat LT : k * h < L
k * h \in [seq h * i | i <- iota 0 (L %/ h).+1 ]
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec h := get_horizon_of_task tsk : duration k : nat LT : k * h < L
k * h \in [seq h * i | i <- iota 0 (L %/ h).+1 ]
rewrite mulnC; apply map_f.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec h := get_horizon_of_task tsk : duration k : nat LT : k * h < L
k \in iota 0 (L %/ h).+1
rewrite mem_iota; apply /andP; split ; first by apply leq0n.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec h := get_horizon_of_task tsk : duration k : nat LT : k * h < L
k < 0 + (L %/ h).+1
rewrite add0n ltnS leq_divRL //; first by lia .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec h := get_horizon_of_task tsk : duration k : nat LT : k * h < L
0 < h
rewrite /specified_bursts in BUR.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec SORT : sorted_ltn_steps evec h := get_horizon_of_task tsk : duration k : nat LT : k * h < L BUR : ε \in time_steps_of evec
0 < h
by rewrite /h /get_horizon_of_task EMAX. } L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec h := get_horizon_of_task tsk : duration k : nat LT : k * h < L
k * h + ε \in time_steps_with_offset tsk (k * h)
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec h := get_horizon_of_task tsk : duration k : nat LT : k * h < L
k * h + ε \in time_steps_with_offset tsk (k * h)
rewrite /time_steps_with_offset addnC.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec h := get_horizon_of_task tsk : duration k : nat LT : k * h < L
ε + k * h
\in [seq t + k * h
| t <- get_time_steps_of_task tsk]
have MFF := map_f (fun t0 => t0 + k * h); apply : MFF.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec h := get_horizon_of_task tsk : duration k : nat LT : k * h < L
ε \in get_time_steps_of_task tsk
by rewrite /get_time_steps_of_task EMAX; apply BUR. }
Qed .
(** ... and every [A] for which [A+ε] is a multiple of the horizon offset by a
time step of the arrival curve prefix is also in the search space for
fixed-priority tasks. *)
Lemma steps_in_approx_ss :
forall i t A ,
i < (L %/ get_horizon_of_task tsk).+1 ->
(t \in get_time_steps_of_task tsk) ->
A + ε = i * get_horizon_of_task tsk + t ->
A \in search_space_arrival_curve_prefix_FP tsk L.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts
forall (i : nat) (t : nat_eqType) (A : nat),
i < (L %/ get_horizon_of_task tsk).+1 ->
t \in get_time_steps_of_task tsk ->
A + ε = i * get_horizon_of_task tsk + t ->
A \in search_space_arrival_curve_prefix_FP tsk L
Proof .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts
forall (i : nat) (t : nat_eqType) (A : nat),
i < (L %/ get_horizon_of_task tsk).+1 ->
t \in get_time_steps_of_task tsk ->
A + ε = i * get_horizon_of_task tsk + t ->
A \in search_space_arrival_curve_prefix_FP tsk L
move : (H_valid_task_set) => VALID; intros * LT IN EQ; rewrite /search_space_arrival_curve_prefix_FP.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts VALID : task_set_with_valid_arrivals ts i : nat t : nat_eqType A : nat LT : i < (L %/ get_horizon_of_task tsk).+1 IN : t \in get_time_steps_of_task tsk EQ : A + ε = i * get_horizon_of_task tsk + t
A
\in search_space_arrival_curve_prefix_FP_h tsk 0
(L %/ get_horizon_of_task tsk).+1
replace A with (A + ε - ε); last by lia .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts VALID : task_set_with_valid_arrivals ts i : nat t : nat_eqType A : nat LT : i < (L %/ get_horizon_of_task tsk).+1 IN : t \in get_time_steps_of_task tsk EQ : A + ε = i * get_horizon_of_task tsk + t
A + ε - ε
\in search_space_arrival_curve_prefix_FP_h tsk 0
(L %/ get_horizon_of_task tsk).+1
rewrite subn1; apply map_f.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts VALID : task_set_with_valid_arrivals ts i : nat t : nat_eqType A : nat LT : i < (L %/ get_horizon_of_task tsk).+1 IN : t \in get_time_steps_of_task tsk EQ : A + ε = i * get_horizon_of_task tsk + t
A + ε
\in repeat_steps_with_offset tsk
[seq get_horizon_of_task tsk * i
| i <- iota 0
(L %/ get_horizon_of_task tsk).+1 ]
set (h := get_horizon_of_task tsk) in *.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts VALID : task_set_with_valid_arrivals ts i : nat t : nat_eqType A : nat h := get_horizon_of_task tsk : duration LT : i < (L %/ h).+1 IN : t \in get_time_steps_of_task tsk EQ : A + ε = i * h + t
A + ε
\in repeat_steps_with_offset tsk
[seq h * i | i <- iota 0 (L %/ h).+1 ]
rewrite /repeat_steps_with_offset; apply /flatten_mapP.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts VALID : task_set_with_valid_arrivals ts i : nat t : nat_eqType A : nat h := get_horizon_of_task tsk : duration LT : i < (L %/ h).+1 IN : t \in get_time_steps_of_task tsk EQ : A + ε = i * h + t
exists2 x : nat_eqType,
x \in [seq h * i | i <- iota 0 (L %/ h).+1 ] &
A + ε \in time_steps_with_offset tsk x
exists (i * h); first by rewrite mulnC; apply map_f; rewrite mem_iota; lia .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts VALID : task_set_with_valid_arrivals ts i : nat t : nat_eqType A : nat h := get_horizon_of_task tsk : duration LT : i < (L %/ h).+1 IN : t \in get_time_steps_of_task tsk EQ : A + ε = i * h + t
A + ε \in time_steps_with_offset tsk (i * h)
unfold time_steps_with_offset.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts VALID : task_set_with_valid_arrivals ts i : nat t : nat_eqType A : nat h := get_horizon_of_task tsk : duration LT : i < (L %/ h).+1 IN : t \in get_time_steps_of_task tsk EQ : A + ε = i * h + t
A + ε
\in [seq t + i * h
| t <- get_time_steps_of_task tsk]
rewrite EQ addnC.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts VALID : task_set_with_valid_arrivals ts i : nat t : nat_eqType A : nat h := get_horizon_of_task tsk : duration LT : i < (L %/ h).+1 IN : t \in get_time_steps_of_task tsk EQ : A + ε = i * h + t
t + i * h
\in [seq t + i * h
| t <- get_time_steps_of_task tsk]
by apply (map_f (fun t0 => t0 + i * h) IN).
Qed .
(** Next, we show that if the horizon of the arrival curve prefix divides [A+ε],
then [A] is not contained in the search space for fixed-priority tasks. *)
Lemma constant_max_arrivals :
forall A ,
(forall s , s \in get_time_steps_of_task tsk -> s < get_horizon_of_task tsk) ->
get_horizon_of_task tsk %| (A + ε) ->
max_arrivals tsk A = max_arrivals tsk (A + ε).L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts
forall A : nat,
(forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tsk) ->
get_horizon_of_task tsk %| A + ε ->
max_arrivals tsk A = max_arrivals tsk (A + ε)
Proof .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts
forall A : nat,
(forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tsk) ->
get_horizon_of_task tsk %| A + ε ->
max_arrivals tsk A = max_arrivals tsk (A + ε)
move : (has_valid_arrival_curve_prefix_tsk ts H_valid_task_set tsk H_tsk_in_ts).L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts
has_valid_arrival_curve_prefix tsk ->
forall A : nat,
(forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tsk) ->
get_horizon_of_task tsk %| A + ε ->
max_arrivals tsk A = max_arrivals tsk (A + ε)
move => [evec [EMAX [POSh [LARGEh [NOINF [BUR SORT]]]]]] A LTH DIV.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskDIV : get_horizon_of_task tsk %| A + ε
max_arrivals tsk A = max_arrivals tsk (A + ε)
rewrite /max_arrivals /ConcreteMaxArrivals /concrete_max_arrivals EMAX.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskDIV : get_horizon_of_task tsk %| A + ε
extrapolated_arrival_curve evec A =
extrapolated_arrival_curve evec (A + ε)
rewrite /get_horizon_of_task EMAX in DIV; move : (DIV) => /eqP MOD0.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskDIV : horizon_of evec %| A + ε MOD0 : (A + ε) %% horizon_of evec = 0
extrapolated_arrival_curve evec A =
extrapolated_arrival_curve evec (A + ε)
rewrite /extrapolated_arrival_curve.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskDIV : horizon_of evec %| A + ε MOD0 : (A + ε) %% horizon_of evec = 0
A %/ horizon_of evec * value_at evec (horizon_of evec) +
value_at evec (A %% horizon_of evec) =
(A + ε) %/ horizon_of evec *
value_at evec (horizon_of evec) +
value_at evec ((A + ε) %% horizon_of evec)
set (h := horizon_of evec) in *; set (vec := value_at evec) in *.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat
A %/ h * vec h + vec (A %% h) =
(A + ε) %/ h * vec h + vec ((A + ε) %% h)
destruct (ltngtP 1 h) as [GT1|LT1|EQ1].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < h
A %/ h * vec h + vec (A %% h) =
(A + ε) %/ h * vec h + vec ((A + ε) %% h)
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < h
A %/ h * vec h + vec (A %% h) =
(A + ε) %/ h * vec h + vec ((A + ε) %% h)
move : NOINF => /eqP NOINF.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < hNOINF : value_at evec 0 = 0
A %/ h * vec h + vec (A %% h) =
(A + ε) %/ h * vec h + vec ((A + ε) %% h)
rewrite MOD0 {4 }/vec NOINF addn0.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < hNOINF : value_at evec 0 = 0
A %/ h * vec h + vec (A %% h) = (A + ε) %/ h * vec h
have -> : vec (A %% h) = vec h.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < hNOINF : value_at evec 0 = 0
vec (A %% h) = vec h
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < hNOINF : value_at evec 0 = 0
vec (A %% h) = vec h
rewrite /vec /value_at.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < hNOINF : value_at evec 0 = 0
(step_at evec (A %% h)).2 = (step_at evec h).2
have -> : ((step_at evec (A %% h)) = (step_at evec h)) => //.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < hNOINF : value_at evec 0 = 0
step_at evec (A %% h) = step_at evec h
rewrite (pred_Sn A) -addn1 modn_pred; [|repeat destruct h=> //|lia ].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < hNOINF : value_at evec 0 = 0
step_at evec
(if h %| A + 1 then h.-1 else ((A + 1 ) %% h).-1 ) =
step_at evec h
rewrite /step_at DIV.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < hNOINF : value_at evec 0 = 0
last (0 , 0 )
[seq step <- steps_of evec | step.1 <= h.-1 ] =
last (0 , 0 ) [seq step <- steps_of evec | step.1 <= h]
have -> : [seq step <- steps_of evec | step.1 <= h] = steps_of evec.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < hNOINF : value_at evec 0 = 0
[seq step <- steps_of evec | step.1 <= h] =
steps_of evec
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < hNOINF : value_at evec 0 = 0
[seq step <- steps_of evec | step.1 <= h] =
steps_of evec
apply /all_filterP /allP => [step IN]; apply ltnW; subst h.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskDIV : horizon_of evec %| A + ε MOD0 : (A + ε) %% horizon_of evec = 0 vec := value_at evec : duration -> nat GT1 : 1 < horizon_of evecNOINF : value_at evec 0 = 0 step : prod_eqType nat_eqType nat_eqType IN : step \in steps_of evec
step.1 < horizon_of evec
move : LTH; rewrite /get_horizon_of_task EMAX => -> //.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat DIV : horizon_of evec %| A + ε MOD0 : (A + ε) %% horizon_of evec = 0 vec := value_at evec : duration -> nat GT1 : 1 < horizon_of evecNOINF : value_at evec 0 = 0 step : prod_eqType nat_eqType nat_eqType IN : step \in steps_of evec
step.1 \in get_time_steps_of_task tsk
rewrite /get_time_steps_of_task EMAX.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat DIV : horizon_of evec %| A + ε MOD0 : (A + ε) %% horizon_of evec = 0 vec := value_at evec : duration -> nat GT1 : 1 < horizon_of evecNOINF : value_at evec 0 = 0 step : prod_eqType nat_eqType nat_eqType IN : step \in steps_of evec
step.1 \in time_steps_of evec
by apply (map_f fst). } L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < hNOINF : value_at evec 0 = 0
last (0 , 0 )
[seq step <- steps_of evec | step.1 <= h.-1 ] =
last (0 , 0 ) (steps_of evec)
have -> : [seq step <- steps_of evec | step.1 <= h.-1 ] = steps_of evec => //.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < hNOINF : value_at evec 0 = 0
[seq step <- steps_of evec | step.1 <= h.-1 ] =
steps_of evec
apply /all_filterP /allP => [step IN]; subst h.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskDIV : horizon_of evec %| A + ε MOD0 : (A + ε) %% horizon_of evec = 0 vec := value_at evec : duration -> nat GT1 : 1 < horizon_of evecNOINF : value_at evec 0 = 0 step : prod_eqType nat_eqType nat_eqType IN : step \in steps_of evec
step.1 <= (horizon_of evec).-1
move : LTH; rewrite /get_horizon_of_task EMAX => VALID.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat DIV : horizon_of evec %| A + ε MOD0 : (A + ε) %% horizon_of evec = 0 vec := value_at evec : duration -> nat GT1 : 1 < horizon_of evecNOINF : value_at evec 0 = 0 step : prod_eqType nat_eqType nat_eqType IN : step \in steps_of evec VALID : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < horizon_of evec
step.1 <= (horizon_of evec).-1
specialize (VALID step.1 ).L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat DIV : horizon_of evec %| A + ε MOD0 : (A + ε) %% horizon_of evec = 0 vec := value_at evec : duration -> nat GT1 : 1 < horizon_of evecNOINF : value_at evec 0 = 0 step : prod_eqType nat_eqType nat_eqType IN : step \in steps_of evec VALID : step.1 \in get_time_steps_of_task tsk ->
step.1 < horizon_of evec
step.1 <= (horizon_of evec).-1
feed VALID; first by rewrite /get_time_steps_of_task EMAX; apply (map_f fst). L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat DIV : horizon_of evec %| A + ε MOD0 : (A + ε) %% horizon_of evec = 0 vec := value_at evec : duration -> nat GT1 : 1 < horizon_of evecNOINF : value_at evec 0 = 0 step : prod_eqType nat_eqType nat_eqType IN : step \in steps_of evec VALID : step.1 < horizon_of evec
step.1 <= (horizon_of evec).-1
by destruct (horizon_of evec). } L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < hNOINF : value_at evec 0 = 0
A %/ h * vec h + vec h = (A + ε) %/ h * vec h
rewrite -mulSnr {1 }(pred_Sn A) divn_pred -(addn1 A) DIV subn1 prednK //=.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < hNOINF : value_at evec 0 = 0
0 < (A + 1 ) %/ h
move : DIV => /dvdnP [k EQk]; rewrite EQk.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat GT1 : 1 < hNOINF : value_at evec 0 = 0 k : nat EQk : A + ε = k * h
0 < (k * h) %/ h
by destruct k;[rewrite /ε in EQk; lia | rewrite mulnK]. } L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat LT1 : h < 1
A %/ h * vec h + vec (A %% h) =
(A + ε) %/ h * vec h + vec ((A + ε) %% h)
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat LT1 : h < 1
A %/ h * vec h + vec (A %% h) =
(A + ε) %/ h * vec h + vec ((A + ε) %% h)
replace h with 0 ; rewrite /positive_horizon in POSh; lia . } L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat EQ1 : 1 = h
A %/ h * vec h + vec (A %% h) =
(A + ε) %/ h * vec h + vec ((A + ε) %% h)
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat EQ1 : 1 = h
A %/ h * vec h + vec (A %% h) =
(A + ε) %/ h * vec h + vec ((A + ε) %% h)
exfalso .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat LTH : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskh := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat EQ1 : 1 = h
False
rewrite /get_time_steps_of_task EMAX in LTH.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat h := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat EQ1 : 1 = hLTH : forall s : nat_eqType,
s \in time_steps_of evec ->
s < get_horizon_of_task tsk
False
specialize (LTH _ BUR).L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat h := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat EQ1 : 1 = hLTH : ε < get_horizon_of_task tsk
False
move : LTH; rewrite ltnNge => /negP CONTR; apply : CONTR.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts evec : ArrivalCurvePrefix EMAX : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec A : nat h := horizon_of evec : duration DIV : h %| A + ε MOD0 : (A + ε) %% h = 0 vec := value_at evec : duration -> nat EQ1 : 1 = h
get_horizon_of_task tsk <= ε
by unfold h in *; rewrite /get_horizon_of_task EMAX -EQ1. }
Qed .
(** Finally, we show that steps in the request-bound function correspond to
points in the search space for fixed-priority tasks. *)
Lemma task_search_space_subset :
forall A ,
A < L ->
task_rbf tsk A != task_rbf tsk (A + ε) ->
A \in search_space_arrival_curve_prefix_FP tsk L.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts
forall A : nat,
A < L ->
task_rbf tsk A != task_rbf tsk (A + ε) ->
A \in search_space_arrival_curve_prefix_FP tsk L
Proof .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts
forall A : nat,
A < L ->
task_rbf tsk A != task_rbf tsk (A + ε) ->
A \in search_space_arrival_curve_prefix_FP tsk L
intros A LT_L IN.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε)
A \in search_space_arrival_curve_prefix_FP tsk L
destruct (get_horizon_of_task tsk %|A) eqn :DIV;
first by apply multiple_of_horizon_in_approx_ss.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) DIV : (get_horizon_of_task tsk %| A) = false
A \in search_space_arrival_curve_prefix_FP tsk L
move : (structure_of_correct_search_space _ LT_L IN).L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) DIV : (get_horizon_of_task tsk %| A) = false
(exists (i : nat) (t : nat_eqType),
i < (L %/ get_horizon_of_task tsk).+1 /\
t \in get_time_steps_of_task tsk /\
A + ε = i * get_horizon_of_task tsk + t) \/
(exists i : nat,
i < (L %/ get_horizon_of_task tsk).+1 /\
A + ε = i * get_horizon_of_task tsk) ->
A \in search_space_arrival_curve_prefix_FP tsk L
move => [[i [t [LT [INt EQ]]]] | [i [LT EQ]]]; first by eapply steps_in_approx_ss; eauto .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk
A \in search_space_arrival_curve_prefix_FP tsk L
destruct (steps_lt_horizon_last_eq_horizon) as [LTh | EQh].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk LTh : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tsk
A \in search_space_arrival_curve_prefix_FP tsk L
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk LTh : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tsk
A \in search_space_arrival_curve_prefix_FP tsk L
exfalso . (* Can't be in search space if h > last step *) L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk LTh : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tsk
False
move : (H_valid_task_set) => VALID; specialize (VALID _ H_tsk_in_ts).L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk LTh : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskVALID : valid_arrivals tsk
False
move : (has_valid_arrival_curve_prefix_tsk ts H_valid_task_set tsk H_tsk_in_ts).L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk LTh : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskVALID : valid_arrivals tsk
has_valid_arrival_curve_prefix tsk -> False
move => [evec [EMAXeq [POSh [LARGEh [NOINF [BUR SORT]]]]]].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk LTh : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskVALID : valid_arrivals tsk evec : ArrivalCurvePrefix EMAXeq : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec
False
rewrite /task_rbf /task_request_bound_function /max_arrivals
/MaxArrivals /ConcreteMaxArrivals /concrete_max_arrivals
EMAXeq eqn_mul2l negb_or in IN.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk LTh : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskVALID : valid_arrivals tsk evec : ArrivalCurvePrefix EMAXeq : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec IN : (concept.task_cost tsk != 0 ) &&
(extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε))
False
move : IN => /andP [_ NEQ].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk LTh : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskVALID : valid_arrivals tsk evec : ArrivalCurvePrefix EMAXeq : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε)
False
move : (sorted_ltn_steps_imply_sorted_leq_steps_steps _ SORT NOINF) => SORT_LEQ.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk LTh : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskVALID : valid_arrivals tsk evec : ArrivalCurvePrefix EMAXeq : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec
False
move : (constant_max_arrivals A LTh) => EQmax.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk LTh : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskVALID : valid_arrivals tsk evec : ArrivalCurvePrefix EMAXeq : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQmax : get_horizon_of_task tsk %| A + ε ->
max_arrivals tsk A = max_arrivals tsk (A + ε)
False
feed EQmax; first by rewrite EQ; apply dvdn_mull, dvdnn. L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk LTh : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskVALID : valid_arrivals tsk evec : ArrivalCurvePrefix EMAXeq : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQmax : max_arrivals tsk A = max_arrivals tsk (A + ε)
False
rewrite /max_arrivals /MaxArrivals /ConcreteMaxArrivals
/concrete_max_arrivals EMAXeq in EQmax.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk LTh : forall s : nat_eqType,
s \in get_time_steps_of_task tsk ->
s < get_horizon_of_task tskVALID : valid_arrivals tsk evec : ArrivalCurvePrefix EMAXeq : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec NEQ : extrapolated_arrival_curve evec A
!= extrapolated_arrival_curve evec (A + ε) SORT_LEQ : sorted_leq_steps evec EQmax : extrapolated_arrival_curve evec A =
extrapolated_arrival_curve evec (A + ε)
False
by rewrite EQmax in NEQ; move : NEQ => /eqP. } L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk EQh : last0 (get_time_steps_of_task tsk) =
get_horizon_of_task tsk
A \in search_space_arrival_curve_prefix_FP tsk L
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk EQh : last0 (get_time_steps_of_task tsk) =
get_horizon_of_task tsk
A \in search_space_arrival_curve_prefix_FP tsk L
replace A with (A + ε - ε); last by lia .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk EQh : last0 (get_time_steps_of_task tsk) =
get_horizon_of_task tsk
A + ε - ε
\in search_space_arrival_curve_prefix_FP tsk L
rewrite subn1; apply map_f; rewrite EQ.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) DIV : (get_horizon_of_task tsk %| A) = false i : nat LT : i < (L %/ get_horizon_of_task tsk).+1 EQ : A + ε = i * get_horizon_of_task tsk EQh : last0 (get_time_steps_of_task tsk) =
get_horizon_of_task tsk
i * get_horizon_of_task tsk
\in repeat_steps_with_offset tsk
[seq get_horizon_of_task tsk * i
| i <- iota 0
(L %/ get_horizon_of_task tsk).+1 ]
set (h := get_horizon_of_task tsk) in *.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) h := get_horizon_of_task tsk : duration DIV : (h %| A) = false i : nat LT : i < (L %/ h).+1 EQ : A + ε = i * h EQh : last0 (get_time_steps_of_task tsk) = h
i * h
\in repeat_steps_with_offset tsk
[seq h * i | i <- iota 0 (L %/ h).+1 ]
apply /flatten_mapP; exists ((i-1 )*h); first by rewrite mulnC map_f // mem_iota; lia .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) h := get_horizon_of_task tsk : duration DIV : (h %| A) = false i : nat LT : i < (L %/ h).+1 EQ : A + ε = i * h EQh : last0 (get_time_steps_of_task tsk) = h
i * h \in time_steps_with_offset tsk ((i - 1 ) * h)
replace (i * h) with (h + (i - 1 ) * h); last first .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) h := get_horizon_of_task tsk : duration DIV : (h %| A) = false i : nat LT : i < (L %/ h).+1 EQ : A + ε = i * h EQh : last0 (get_time_steps_of_task tsk) = h
h + (i - 1 ) * h = i * h
{ L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) h := get_horizon_of_task tsk : duration DIV : (h %| A) = false i : nat LT : i < (L %/ h).+1 EQ : A + ε = i * h EQh : last0 (get_time_steps_of_task tsk) = h
h + (i - 1 ) * h = i * h
destruct (posnP i) as [Z|POS]; first by subst i; rewrite /ε in EQ; lia .L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) h := get_horizon_of_task tsk : duration DIV : (h %| A) = false i : nat LT : i < (L %/ h).+1 EQ : A + ε = i * h EQh : last0 (get_time_steps_of_task tsk) = h POS : 0 < i
h + (i - 1 ) * h = i * h
by rewrite mulnBl mul1n; apply subnKC, leq_pmull. } L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) h := get_horizon_of_task tsk : duration DIV : (h %| A) = false i : nat LT : i < (L %/ h).+1 EQ : A + ε = i * h EQh : last0 (get_time_steps_of_task tsk) = h
h + (i - 1 ) * h
\in time_steps_with_offset tsk ((i - 1 ) * h)
have MFF := map_f (fun t0 => t0 + (i - 1 ) * h); apply : MFF.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) h := get_horizon_of_task tsk : duration DIV : (h %| A) = false i : nat LT : i < (L %/ h).+1 EQ : A + ε = i * h EQh : last0 (get_time_steps_of_task tsk) = h
h \in get_time_steps_of_task tsk
rewrite -EQh.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) h := get_horizon_of_task tsk : duration DIV : (h %| A) = false i : nat LT : i < (L %/ h).+1 EQ : A + ε = i * h EQh : last0 (get_time_steps_of_task tsk) = h
last0 (get_time_steps_of_task tsk)
\in get_time_steps_of_task tsk
move : (has_valid_arrival_curve_prefix_tsk ts H_valid_task_set tsk H_tsk_in_ts).L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) h := get_horizon_of_task tsk : duration DIV : (h %| A) = false i : nat LT : i < (L %/ h).+1 EQ : A + ε = i * h EQh : last0 (get_time_steps_of_task tsk) = h
has_valid_arrival_curve_prefix tsk ->
last0 (get_time_steps_of_task tsk)
\in get_time_steps_of_task tsk
move => [evec [EMAXeq [POSh [LARGEh [NOINF [BUR SORT]]]]]].L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) h := get_horizon_of_task tsk : duration DIV : (h %| A) = false i : nat LT : i < (L %/ h).+1 EQ : A + ε = i * h EQh : last0 (get_time_steps_of_task tsk) = h evec : ArrivalCurvePrefix EMAXeq : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : specified_bursts evec SORT : sorted_ltn_steps evec
last0 (get_time_steps_of_task tsk)
\in get_time_steps_of_task tsk
rewrite /get_time_steps_of_task EMAXeq; unfold specified_bursts in *.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) h := get_horizon_of_task tsk : duration DIV : (h %| A) = false i : nat LT : i < (L %/ h).+1 EQ : A + ε = i * h EQh : last0 (get_time_steps_of_task tsk) = h evec : ArrivalCurvePrefix EMAXeq : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec BUR : ε \in time_steps_of evec SORT : sorted_ltn_steps evec
last0 (time_steps_of evec) \in time_steps_of evec
destruct (time_steps_of evec) => //=.L : duration ts : seq Task H_valid_task_set : task_set_with_valid_arrivals ts tsk : Task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts A : nat LT_L : A < L IN : task_rbf tsk A != task_rbf tsk (A + ε) h := get_horizon_of_task tsk : duration DIV : (h %| A) = false i : nat LT : i < (L %/ h).+1 EQ : A + ε = i * h EQh : last0 (get_time_steps_of_task tsk) = h evec : ArrivalCurvePrefix EMAXeq : get_arrival_curve_prefix tsk = evec POSh : positive_horizon evec LARGEh : large_horizon evec NOINF : no_inf_arrivals evec d : duration l : seq duration BUR : ε \in d :: l SORT : sorted_ltn_steps evec
last0 (d :: l) \in d :: l
by rewrite /last0 //=; apply mem_last. }
Qed .
End Facts .
End FastSearchSpaceComputation .