Built with
Alectryon , running Coq+SerAPI v8.20.0+0.20.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.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted. [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Serlib plugin: coq-paramcoq.plugin is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted. [Loading ML file paramcoq.cmxs (using legacy method) ... done ] Notations "[ coqeal _ of _ ]" defined at level 0
and "[ TASK id: _ cost: _ deadline: _ arrival: _ priority: _ ]"
defined at level 6 have incompatible prefixes.
One of them will likely not work.
[notation-incompatible-prefix,parsing,default] Notations "[ coqeal _ of _ ]" defined at level 0
and "[ PERIODIC-TASK id: _ cost: _ deadline: _ period: _ priority: _ ]"
defined at level 6 have incompatible prefixes.
One of them will likely not work.
[notation-incompatible-prefix,parsing,default] Notations "[ coqeal _ of _ ]" defined at level 0
and "[ SPORADIC-TASK id: _ cost: _ deadline: _ separation: _ priority: _ ]"
defined at level 6 have incompatible prefixes.
One of them will likely not work.
[notation-incompatible-prefix,parsing,default] Notations "[ coqeal _ of _ ]" defined at level 0
and "[ CURVE horizon: _ steps: _ ]" defined at level 6
have incompatible prefixes.
One of them will likely not work.
[notation-incompatible-prefix,parsing,default] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
(** In this section, we prove some properties that every valid
arrival curve prefix entails. *)
Section ValidArrivalCurvePrefixFacts .
(** Consider a task set with valid arrivals [ts], ... *)
Variable ts : seq Task.
Hypothesis H_valid_task_set : task_set_with_valid_arrivals ts.
(** ... and a task [tsk] belonging to [ts] with positive cost and
non-zero arrival bound. *)
Variable tsk : Task.
Hypothesis H_positive_cost : 0 < task_cost tsk.
Hypothesis H_tsk_in_ts : tsk \in ts.
Hypothesis H_positive_step : fst (head (0 ,0 ) (steps_of (get_arrival_curve_prefix tsk))) > 0 .
(** First, we show that the arrival curve prefix of [tsk] is valid. *)
Lemma has_valid_arrival_curve_prefix_tsk :
has_valid_arrival_curve_prefix tsk.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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1
has_valid_arrival_curve_prefix tsk
Proof .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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1
has_valid_arrival_curve_prefix tsk
move : (H_valid_task_set tsk H_tsk_in_ts); rewrite /valid_arrivals => VALID.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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 VALID : match task_arrival tsk with
| Periodic p => 0 < p
| Sporadic m => 0 < m
| ArrivalPrefix emax_vec =>
valid_arrival_curve_prefix_dec emax_vec
end
has_valid_arrival_curve_prefix tsk
destruct (arrival_cases tsk) as [[p EQ] | [[m EQ] | [evec EQ]]].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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 VALID : match task_arrival tsk with
| Periodic p => 0 < p
| Sporadic m => 0 < m
| ArrivalPrefix emax_vec =>
valid_arrival_curve_prefix_dec emax_vec
end p : nat EQ : task_arrival tsk = Periodic p
has_valid_arrival_curve_prefix tsk
all : rewrite /has_valid_arrival_curve_prefix /max_arrivals /MaxArrivals /ConcreteMaxArrivals /get_arrival_curve_prefix EQ //=.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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 VALID : match task_arrival tsk with
| Periodic p => 0 < p
| Sporadic m => 0 < m
| ArrivalPrefix emax_vec =>
valid_arrival_curve_prefix_dec emax_vec
end p : nat EQ : task_arrival tsk = Periodic p
exists ac_prefix_vec : ArrivalCurvePrefix,
inter_arrival_to_prefix p = ac_prefix_vec /\
valid_arrival_curve_prefix ac_prefix_vec
all : rewrite EQ in VALID.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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 p : nat EQ : task_arrival tsk = Periodic p VALID : 0 < p
exists ac_prefix_vec : ArrivalCurvePrefix,
inter_arrival_to_prefix p = ac_prefix_vec /\
valid_arrival_curve_prefix ac_prefix_vec
{ 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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 p : nat EQ : task_arrival tsk = Periodic p VALID : 0 < p
exists ac_prefix_vec : ArrivalCurvePrefix,
inter_arrival_to_prefix p = ac_prefix_vec /\
valid_arrival_curve_prefix ac_prefix_vec
exists (inter_arrival_to_prefix p ).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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 p : nat EQ : task_arrival tsk = Periodic p VALID : 0 < p
inter_arrival_to_prefix p = inter_arrival_to_prefix p /\
valid_arrival_curve_prefix (inter_arrival_to_prefix p)
split ;[|split ;[|split ;[|split ;[|split ]]]] => //=.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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 p : nat EQ : task_arrival tsk = Periodic p VALID : 0 < p
large_horizon (inter_arrival_to_prefix p)
move => s.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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 p : nat EQ : task_arrival tsk = Periodic p VALID : 0 < ps : Datatypes_nat__canonical__eqtype_Equality
s \in time_steps_of (inter_arrival_to_prefix p) ->
s <= horizon_of (inter_arrival_to_prefix p)
by rewrite /large_horizon in_cons => /orP [|] /eqP. } 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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 m : nat EQ : task_arrival tsk = Sporadic m VALID : 0 < m
exists ac_prefix_vec : ArrivalCurvePrefix,
inter_arrival_to_prefix m = ac_prefix_vec /\
valid_arrival_curve_prefix ac_prefix_vec
{ 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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 m : nat EQ : task_arrival tsk = Sporadic m VALID : 0 < m
exists ac_prefix_vec : ArrivalCurvePrefix,
inter_arrival_to_prefix m = ac_prefix_vec /\
valid_arrival_curve_prefix ac_prefix_vec
exists (inter_arrival_to_prefix m ).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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 m : nat EQ : task_arrival tsk = Sporadic m VALID : 0 < m
inter_arrival_to_prefix m = inter_arrival_to_prefix m /\
valid_arrival_curve_prefix (inter_arrival_to_prefix m)
split ;[|split ;[|split ;[|split ;[|split ]]]] => //=.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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 m : nat EQ : task_arrival tsk = Sporadic m VALID : 0 < m
large_horizon (inter_arrival_to_prefix m)
move => s.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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 m : nat EQ : task_arrival tsk = Sporadic m VALID : 0 < ms : Datatypes_nat__canonical__eqtype_Equality
s \in time_steps_of (inter_arrival_to_prefix m) ->
s <= horizon_of (inter_arrival_to_prefix m)
by rewrite /large_horizon in_cons => /orP [|] /eqP. } 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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 evec : ArrivalCurvePrefix EQ : task_arrival tsk = ArrivalPrefix evec VALID : valid_arrival_curve_prefix_dec evec
exists ac_prefix_vec : ArrivalCurvePrefix,
evec = ac_prefix_vec /\
valid_arrival_curve_prefix ac_prefix_vec
{ 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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 evec : ArrivalCurvePrefix EQ : task_arrival tsk = ArrivalPrefix evec VALID : valid_arrival_curve_prefix_dec evec
exists ac_prefix_vec : ArrivalCurvePrefix,
evec = ac_prefix_vec /\
valid_arrival_curve_prefix ac_prefix_vec
by exists evec ; split => //; apply /valid_arrival_curve_prefix_P. }
Qed .
(** Next, we show that each time step of the arrival curve prefix must be
positive. *)
Lemma steps_are_positive_if_first_step_is_positive :
forall st ,
st \in get_time_steps_of_task tsk -> st > 0 .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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1
forall st : Datatypes_nat__canonical__eqtype_Equality,
st \in get_time_steps_of_task tsk -> 0 < st
Proof .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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1
forall st : Datatypes_nat__canonical__eqtype_Equality,
st \in get_time_steps_of_task tsk -> 0 < st
intros st IN; unfold get_time_steps_of_task in *.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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 st : Datatypes_nat__canonical__eqtype_Equality IN : st
\in time_steps_of
(get_arrival_curve_prefix tsk)
0 < st
move : (H_valid_task_set) => VAL; specialize (VAL _ H_tsk_in_ts).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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 st : Datatypes_nat__canonical__eqtype_Equality IN : st
\in time_steps_of
(get_arrival_curve_prefix tsk) VAL : valid_arrivals tsk
0 < st
unfold valid_arrivals in VAL; unfold get_arrival_curve_prefix in *.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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
match task_arrival tsk with
| Periodic p =>
inter_arrival_to_prefix p
| Sporadic m =>
inter_arrival_to_prefix m
| ArrivalPrefix steps => steps
end )).1 st : Datatypes_nat__canonical__eqtype_Equality IN : st
\in time_steps_of
match task_arrival tsk with
| Periodic p => inter_arrival_to_prefix p
| Sporadic m => inter_arrival_to_prefix m
| ArrivalPrefix steps => steps
end VAL : match task_arrival tsk with
| Periodic p => 0 < p
| Sporadic m => 0 < m
| ArrivalPrefix emax_vec =>
valid_arrival_curve_prefix_dec emax_vec
end
0 < st
destruct (task_arrival tsk) as [a|a|a].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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(inter_arrival_to_prefix a))).1 st : Datatypes_nat__canonical__eqtype_Equality IN : st \in time_steps_of (inter_arrival_to_prefix a) VAL : 0 < a
0 < st
{ 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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(inter_arrival_to_prefix a))).1 st : Datatypes_nat__canonical__eqtype_Equality IN : st \in time_steps_of (inter_arrival_to_prefix a) VAL : 0 < a
0 < st
by unfold inter_arrival_to_prefix, time_steps_of in *; simpl in IN;
move : IN; rewrite mem_seq1 => /eqP EQ; subst . } 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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(inter_arrival_to_prefix a))).1 st : Datatypes_nat__canonical__eqtype_Equality IN : st \in time_steps_of (inter_arrival_to_prefix a) VAL : 0 < a
0 < st
{ 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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(inter_arrival_to_prefix a))).1 st : Datatypes_nat__canonical__eqtype_Equality IN : st \in time_steps_of (inter_arrival_to_prefix a) VAL : 0 < a
0 < st
by unfold inter_arrival_to_prefix, time_steps_of in *; simpl in IN;
move : IN; rewrite mem_seq1 => /eqP EQ; subst . } 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 : ArrivalCurvePrefix H_positive_step : 0 < (head (0 , 0 ) (steps_of a)).1 st : Datatypes_nat__canonical__eqtype_Equality IN : st \in time_steps_of a VAL : valid_arrival_curve_prefix_dec a
0 < st
{ 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 : ArrivalCurvePrefix H_positive_step : 0 < (head (0 , 0 ) (steps_of a)).1 st : Datatypes_nat__canonical__eqtype_Equality IN : st \in time_steps_of a VAL : valid_arrival_curve_prefix_dec a
0 < st
destruct a as [h [ | st0 sts]]; first by done .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 h : duration st0 : (duration * nat)%type sts : seq (duration * nat) H_positive_step : 0 <
(head (0 , 0 )
(steps_of (h, st0 :: sts))).1 st : Datatypes_nat__canonical__eqtype_Equality IN : st \in time_steps_of (h, st0 :: sts) VAL : valid_arrival_curve_prefix_dec (h, st0 :: sts)
0 < st
move : IN => /mapP [[t v] IN EQ]; simpl in *; subst st.ts : seq concrete_task H_valid_task_set : task_set_with_valid_arrivals ts tsk : concrete_task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts h : duration st0 : (duration * nat)%type sts : seq (duration * nat) H_positive_step : 0 < st0.1 VAL : valid_arrival_curve_prefix_dec (h, st0 :: sts) t, v : nat IN : (t, v) \in st0 :: sts
0 < t
move : IN; rewrite in_cons => /orP [/eqP EQ | IN]; first by subst .ts : seq concrete_task H_valid_task_set : task_set_with_valid_arrivals ts tsk : concrete_task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts h : duration st0 : (duration * nat)%type sts : seq (duration * nat) H_positive_step : 0 < st0.1 VAL : valid_arrival_curve_prefix_dec (h, st0 :: sts) t, v : nat IN : (t, v) \in sts
0 < t
move : VAL => /valid_arrival_curve_prefix_P VAL.ts : seq concrete_task H_valid_task_set : task_set_with_valid_arrivals ts tsk : concrete_task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts h : duration st0 : (duration * nat)%type sts : seq (duration * nat) H_positive_step : 0 < st0.1 t, v : nat IN : (t, v) \in sts VAL : valid_arrival_curve_prefix (h, st0 :: sts)
0 < t
destruct VAL as [_ [_ [_ [_ SORT]]]].ts : seq concrete_task H_valid_task_set : task_set_with_valid_arrivals ts tsk : concrete_task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts h : duration st0 : (duration * nat)%type sts : seq (duration * nat) H_positive_step : 0 < st0.1 t, v : nat IN : (t, v) \in sts SORT : sorted_ltn_steps (h, st0 :: sts)
0 < t
unfold sorted_ltn_steps in *; simpl in *.ts : seq concrete_task H_valid_task_set : task_set_with_valid_arrivals ts tsk : concrete_task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts h : duration st0 : (duration * nat)%type sts : seq (duration * nat) H_positive_step : 0 < st0.1 t, v : nat IN : (t, v) \in sts SORT : path ltn_steps st0 sts
0 < t
rewrite (@path_sorted_inE _ predT) in SORT; last apply all_predT.ts : seq concrete_task H_valid_task_set : task_set_with_valid_arrivals ts tsk : concrete_task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts h : duration st0 : (duration * nat)%type sts : seq (duration * nat) H_positive_step : 0 < st0.1 t, v : nat IN : (t, v) \in sts SORT : all (ltn_steps st0) sts && sorted ltn_steps sts
0 < t
+ ts : seq concrete_task H_valid_task_set : task_set_with_valid_arrivals ts tsk : concrete_task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts h : duration st0 : (duration * nat)%type sts : seq (duration * nat) H_positive_step : 0 < st0.1 t, v : nat IN : (t, v) \in sts SORT : all (ltn_steps st0) sts && sorted ltn_steps sts
0 < t
move : SORT => /andP [/allP ALL _].ts : seq concrete_task H_valid_task_set : task_set_with_valid_arrivals ts tsk : concrete_task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts h : duration st0 : (duration * nat)%type sts : seq (duration * nat) H_positive_step : 0 < st0.1 t, v : nat IN : (t, v) \in sts ALL : {in sts,
forall
x : Datatypes_prod__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality
Datatypes_nat__canonical__eqtype_Equality,
ltn_steps st0 x}
0 < t
specialize (ALL (t,v) IN); move : ALL.ts : seq concrete_task H_valid_task_set : task_set_with_valid_arrivals ts tsk : concrete_task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts h : duration st0 : (duration * nat)%type sts : seq (duration * nat) H_positive_step : 0 < st0.1 t, v : nat IN : (t, v) \in sts
ltn_steps st0 (t, v) -> 0 < t
destruct st0; simpl in *.ts : seq concrete_task H_valid_task_set : task_set_with_valid_arrivals ts tsk : concrete_task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts h, d : duration n : nat sts : seq (duration * nat) H_positive_step : 0 < dt, v : nat IN : (t, v) \in sts
ltn_steps (d, n) (t, v) -> 0 < t
by move => /andP //= => [[LT1 LT2]]; lia .
+ ts : seq concrete_task H_valid_task_set : task_set_with_valid_arrivals ts tsk : concrete_task H_positive_cost : 0 < task_cost tskH_tsk_in_ts : tsk \in ts h : duration st0 : (duration * nat)%type sts : seq (duration * nat) H_positive_step : 0 < st0.1 t, v : nat IN : (t, v) \in sts
{in predT & &, transitive (T:=nat * nat) ltn_steps}
by intros ? ? ? _ _ _; apply ltn_steps_is_transitive. }
Qed .
(** Next, we show that even shifting the time steps by a positive
offset, they remain positive. *)
Lemma nonshifted_offsets_are_positive :
forall A offs ,
A \in repeat_steps_with_offset tsk offs -> A > 0 .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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1
forall (A : Datatypes_nat__canonical__eqtype_Equality)
(offs : seq nat),
A \in repeat_steps_with_offset tsk offs -> 0 < A
Proof .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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1
forall (A : Datatypes_nat__canonical__eqtype_Equality)
(offs : seq nat),
A \in repeat_steps_with_offset tsk offs -> 0 < A
intros A offs IN.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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 A : Datatypes_nat__canonical__eqtype_Equality offs : seq nat IN : A \in repeat_steps_with_offset tsk offs
0 < A
move : IN => /flatten_mapP [o INo IN].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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 A : Datatypes_nat__canonical__eqtype_Equality offs : seq nat o : Datatypes_nat__canonical__eqtype_Equality INo : o \in offs IN : A \in time_steps_with_offset tsk o
0 < A
move : IN => /mapP [st IN EQ]; subst A.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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 offs : seq nat o : Datatypes_nat__canonical__eqtype_Equality INo : o \in offs st : Datatypes_nat__canonical__eqtype_Equality IN : st \in get_time_steps_of_task tsk
0 < st + o
rewrite addn_gt0; apply /orP; left .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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 offs : seq nat o : Datatypes_nat__canonical__eqtype_Equality INo : o \in offs st : Datatypes_nat__canonical__eqtype_Equality IN : st \in get_time_steps_of_task tsk
0 < st
by apply steps_are_positive_if_first_step_is_positive.
Qed .
(** Finally, we show that the time steps are strictly increasing. *)
Lemma time_steps_sorted :
sorted ltn (get_time_steps_of_task tsk).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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1
sorted ltn (get_time_steps_of_task tsk)
Proof .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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1
sorted ltn (get_time_steps_of_task tsk)
move : (H_valid_task_set) => VALID; rewrite /get_time_steps_of_task.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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 VALID : task_set_with_valid_arrivals ts
sorted ltn
(time_steps_of (get_arrival_curve_prefix tsk))
move : (has_valid_arrival_curve_prefix_tsk) => [arrival_curve_prefix [EQ [POSh [LARGEh [NOINF [BUR SORT]]]]]].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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 VALID : task_set_with_valid_arrivals 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
sorted ltn
(time_steps_of (get_arrival_curve_prefix tsk))
rewrite EQ.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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 VALID : task_set_with_valid_arrivals 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
sorted ltn (time_steps_of arrival_curve_prefix)
eapply (homo_sorted _ _ SORT).
Unshelve .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 H_positive_step : 0 <
(head (0 , 0 )
(steps_of
(get_arrival_curve_prefix tsk))).1 VALID : task_set_with_valid_arrivals 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
{homo fst : x y / ltn_steps x y >-> ltn x y}
by move => x y; rewrite /ltn_steps => /andP[LT _].
Qed .
End ValidArrivalCurvePrefixFacts .