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.model.task.arrival.periodic_as_sporadic.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.analysis.facts.periodic.max_inter_arrival.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.facts.model.offset.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** In this module, we'll prove the known arrival
times of jobs that stem from periodic tasks. *)
Section PeriodicArrivalTimes .
(** Consider periodic tasks with an offset ... *)
Context {Task : TaskType}.
Context `{TaskOffset Task}.
Context `{PeriodicModel Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
(** Consider any unique arrival sequence with consistent arrivals ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and any periodic task [tsk] with a valid offset and period. *)
Variable tsk : Task.
Hypothesis H_valid_offset : valid_offset arr_seq tsk.
Hypothesis H_valid_period : valid_period tsk.
Hypothesis H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk.
(** We show that the nth job [j] of task [tsk]
arrives at the instant [task_offset tsk + n * task_period tsk]. *)
Lemma periodic_arrival_times :
forall n (j : Job),
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = n ->
job_arrival j = task_offset tsk + n * task_period tsk.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk
forall (n : nat) (j : Job),
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = n ->
job_arrival j = task_offset tsk + n * task_period tsk
Proof .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk
forall (n : nat) (j : Job),
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = n ->
job_arrival j = task_offset tsk + n * task_period tsk
induction n.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = 0 ->
job_arrival j = task_offset tsk + 0 * task_period tsk
{ Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = 0 ->
job_arrival j = task_offset tsk + 0 * task_period tsk
intros j ARR TSK_IN ZINDEX.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk j : Job ARR : arrives_in arr_seq j TSK_IN : job_task j = tsk ZINDEX : job_index arr_seq j = 0
job_arrival j = task_offset tsk + 0 * task_period tsk
rewrite mul0n addn0.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk j : Job ARR : arrives_in arr_seq j TSK_IN : job_task j = tsk ZINDEX : job_index arr_seq j = 0
job_arrival j = task_offset tsk
exact : first_job_arrival ZINDEX.
} Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk n : nat IHn : forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = n ->
job_arrival j =
task_offset tsk + n * task_period tsk
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = n.+1 ->
job_arrival j =
task_offset tsk + n.+1 * task_period tsk
{ Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk n : nat IHn : forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = n ->
job_arrival j =
task_offset tsk + n * task_period tsk
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = n.+1 ->
job_arrival j =
task_offset tsk + n.+1 * task_period tsk
intros j ARR TSK_IN JB_INDEX.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk n : nat IHn : forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = n ->
job_arrival j =
task_offset tsk + n * task_period tskj : Job ARR : arrives_in arr_seq j TSK_IN : job_task j = tsk JB_INDEX : job_index arr_seq j = n.+1
job_arrival j =
task_offset tsk + n.+1 * task_period tsk
move : (H_task_respects_periodic_model j ARR) => PREV_JOB.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk n : nat IHn : forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = n ->
job_arrival j =
task_offset tsk + n * task_period tskj : Job ARR : arrives_in arr_seq j TSK_IN : job_task j = tsk JB_INDEX : job_index arr_seq j = n.+1 PREV_JOB : 0 < job_index arr_seq j ->
job_task j = tsk ->
exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' =
job_index arr_seq j - 1 /\
job_task j' = tsk /\
job_arrival j =
job_arrival j' + task_period tsk
job_arrival j =
task_offset tsk + n.+1 * task_period tsk
feed_n 2 PREV_JOB => //; first by lia . Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk n : nat IHn : forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = n ->
job_arrival j =
task_offset tsk + n * task_period tskj : Job ARR : arrives_in arr_seq j TSK_IN : job_task j = tsk JB_INDEX : job_index arr_seq j = n.+1 PREV_JOB : exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' =
job_index arr_seq j - 1 /\
job_task j' = tsk /\
job_arrival j =
job_arrival j' + task_period tsk
job_arrival j =
task_offset tsk + n.+1 * task_period tsk
move : PREV_JOB => [pj [ARR' [IND [TSK ARRIVAL]]]].Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk n : nat IHn : forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = n ->
job_arrival j =
task_offset tsk + n * task_period tskj : Job ARR : arrives_in arr_seq j TSK_IN : job_task j = tsk JB_INDEX : job_index arr_seq j = n.+1 pj : Job ARR' : arrives_in arr_seq pj IND : job_index arr_seq pj = job_index arr_seq j - 1 TSK : job_task pj = tsk ARRIVAL : job_arrival j =
job_arrival pj + task_period tsk
job_arrival j =
task_offset tsk + n.+1 * task_period tsk
specialize (IHn pj); feed_n 3 IHn => //; first by rewrite IND JB_INDEX; lia .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk n : nat pj : Job IHn : job_arrival pj =
task_offset tsk + n * task_period tsk j : Job ARR : arrives_in arr_seq j TSK_IN : job_task j = tsk JB_INDEX : job_index arr_seq j = n.+1 ARR' : arrives_in arr_seq pj IND : job_index arr_seq pj = job_index arr_seq j - 1 TSK : job_task pj = tsk ARRIVAL : job_arrival j =
job_arrival pj + task_period tsk
job_arrival j =
task_offset tsk + n.+1 * task_period tsk
rewrite ARRIVAL IHn; lia .
}
Qed .
(** We show that for every job [j] of task [tsk] there exists a number
[n] such that [j] arrives at the instant [task_offset tsk + n * task_period tsk]. *)
Lemma job_arrival_times :
forall j ,
arrives_in arr_seq j ->
job_task j = tsk ->
exists n , job_arrival j = task_offset tsk + n * task_period tsk.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
exists n : nat,
job_arrival j =
task_offset tsk + n * task_period tsk
Proof .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
exists n : nat,
job_arrival j =
task_offset tsk + n * task_period tsk
intros * ARR TSK.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk j : Job ARR : arrives_in arr_seq j TSK : job_task j = tsk
exists n : nat,
job_arrival j =
task_offset tsk + n * task_period tsk
exists (job_index arr_seq j ).Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk j : Job ARR : arrives_in arr_seq j TSK : job_task j = tsk
job_arrival j =
task_offset tsk +
job_index arr_seq j * task_period tsk
specialize (periodic_arrival_times (job_index arr_seq j) j) => J_ARR.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk j : Job ARR : arrives_in arr_seq j TSK : job_task j = tsk J_ARR : arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = job_index arr_seq j ->
job_arrival j =
task_offset tsk +
job_index arr_seq j * task_period tsk
job_arrival j =
task_offset tsk +
job_index arr_seq j * task_period tsk
by feed_n 3 J_ARR => //.
Qed .
(** If a job [j] of task [tsk] arrives at [task_offset tsk + n * task_period tsk]
then the [job_index] of [j] is equal to [n]. *)
Lemma job_arr_index :
forall n j ,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j = task_offset tsk + n * task_period tsk ->
job_index arr_seq j = n.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk
forall (n : nat) (j : Job),
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j = task_offset tsk + n * task_period tsk ->
job_index arr_seq j = n
Proof .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk
forall (n : nat) (j : Job),
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j = task_offset tsk + n * task_period tsk ->
job_index arr_seq j = n
have F : task_period tsk > 0 by auto .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk F : 0 < task_period tsk
forall (n : nat) (j : Job),
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j = task_offset tsk + n * task_period tsk ->
job_index arr_seq j = n
induction n.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk F : 0 < task_period tsk
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j = task_offset tsk + 0 * task_period tsk ->
job_index arr_seq j = 0
+ Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk F : 0 < task_period tsk
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j = task_offset tsk + 0 * task_period tsk ->
job_index arr_seq j = 0
intros * ARR_J TSK ARR.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk F : 0 < task_period tskj : Job ARR_J : arrives_in arr_seq j TSK : job_task j = tsk ARR : job_arrival j =
task_offset tsk + 0 * task_period tsk
job_index arr_seq j = 0
destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]] => //.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk F : 0 < task_period tskj : Job ARR_J : arrives_in arr_seq j TSK : job_task j = tsk ARR : job_arrival j =
task_offset tsk + 0 * task_period tsk m : nat SUCC : job_index arr_seq j = m.+1
job_index arr_seq j = 0
by apply periodic_arrival_times in SUCC => //; lia .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk F : 0 < task_period tskn : nat IHn : forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j =
task_offset tsk + n * task_period tsk ->
job_index arr_seq j = n
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j =
task_offset tsk + n.+1 * task_period tsk ->
job_index arr_seq j = n.+1
+ Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk F : 0 < task_period tskn : nat IHn : forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j =
task_offset tsk + n * task_period tsk ->
job_index arr_seq j = n
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j =
task_offset tsk + n.+1 * task_period tsk ->
job_index arr_seq j = n.+1
intros * ARR_J TSK ARR.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk H_task_respects_periodic_model : respects_periodic_task_model
arr_seq tsk F : 0 < task_period tskn : nat IHn : forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j =
task_offset tsk + n * task_period tsk ->
job_index arr_seq j = nj : Job ARR_J : arrives_in arr_seq j TSK : job_task j = tsk ARR : job_arrival j =
task_offset tsk + n.+1 * task_period tsk
job_index arr_seq j = n.+1
specialize (H_task_respects_periodic_model j); feed_n 3 H_task_respects_periodic_model => //.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk j : Job H_task_respects_periodic_model : 0 <
job_index arr_seq j ->
job_task j = tsk ->
exists j' : Job,
arrives_in arr_seq
j' /\
job_index arr_seq
j' =
job_index arr_seq j -
1 /\
job_task j' = tsk /\
job_arrival j =
job_arrival j' +
task_period tskF : 0 < task_period tskn : nat IHn : forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j =
task_offset tsk + n * task_period tsk ->
job_index arr_seq j = nARR_J : arrives_in arr_seq j TSK : job_task j = tsk ARR : job_arrival j =
task_offset tsk + n.+1 * task_period tsk
0 < job_index arr_seq j
{ Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk j : Job H_task_respects_periodic_model : 0 <
job_index arr_seq j ->
job_task j = tsk ->
exists j' : Job,
arrives_in arr_seq
j' /\
job_index arr_seq
j' =
job_index arr_seq j -
1 /\
job_task j' = tsk /\
job_arrival j =
job_arrival j' +
task_period tskF : 0 < task_period tskn : nat IHn : forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j =
task_offset tsk + n * task_period tsk ->
job_index arr_seq j = nARR_J : arrives_in arr_seq j TSK : job_task j = tsk ARR : job_arrival j =
task_offset tsk + n.+1 * task_period tsk
0 < job_index arr_seq j
rewrite lt0n; apply /eqP; intro EQ.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk j : Job H_task_respects_periodic_model : 0 <
job_index arr_seq j ->
job_task j = tsk ->
exists j' : Job,
arrives_in arr_seq
j' /\
job_index arr_seq
j' =
job_index arr_seq j -
1 /\
job_task j' = tsk /\
job_arrival j =
job_arrival j' +
task_period tskF : 0 < task_period tskn : nat IHn : forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j =
task_offset tsk + n * task_period tsk ->
job_index arr_seq j = nARR_J : arrives_in arr_seq j TSK : job_task j = tsk ARR : job_arrival j =
task_offset tsk + n.+1 * task_period tsk EQ : job_index arr_seq j = 0
False
apply (first_job_arrival _ H_valid_arrival_sequence tsk) in EQ => //.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk j : Job H_task_respects_periodic_model : 0 <
job_index arr_seq j ->
job_task j = tsk ->
exists j' : Job,
arrives_in arr_seq
j' /\
job_index arr_seq
j' =
job_index arr_seq j -
1 /\
job_task j' = tsk /\
job_arrival j =
job_arrival j' +
task_period tskF : 0 < task_period tskn : nat IHn : forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j =
task_offset tsk + n * task_period tsk ->
job_index arr_seq j = nARR_J : arrives_in arr_seq j TSK : job_task j = tsk ARR : job_arrival j =
task_offset tsk + n.+1 * task_period tsk EQ : job_arrival j = task_offset tsk
False
by rewrite EQ in ARR; lia .
} Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk j : Job H_task_respects_periodic_model : exists j' : Job,
arrives_in arr_seq
j' /\
job_index arr_seq
j' =
job_index arr_seq j -
1 /\
job_task j' = tsk /\
job_arrival j =
job_arrival j' +
task_period tskF : 0 < task_period tskn : nat IHn : forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j =
task_offset tsk + n * task_period tsk ->
job_index arr_seq j = nARR_J : arrives_in arr_seq j TSK : job_task j = tsk ARR : job_arrival j =
task_offset tsk + n.+1 * task_period tsk
job_index arr_seq j = n.+1
move : H_task_respects_periodic_model => [j' [ARR' [IND' [TSK' ARRIVAL']]]].Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk j : Job H_task_respects_periodic_model : exists j' : Job,
arrives_in arr_seq
j' /\
job_index arr_seq
j' =
job_index arr_seq j -
1 /\
job_task j' = tsk /\
job_arrival j =
job_arrival j' +
task_period tskF : 0 < task_period tskn : nat IHn : forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j =
task_offset tsk + n * task_period tsk ->
job_index arr_seq j = nARR_J : arrives_in arr_seq j TSK : job_task j = tsk ARR : job_arrival j =
task_offset tsk + n.+1 * task_period tsk j' : Job ARR' : arrives_in arr_seq j' IND' : job_index arr_seq j' = job_index arr_seq j - 1 TSK' : job_task j' = tsk ARRIVAL' : job_arrival j =
job_arrival j' + task_period tsk
job_index arr_seq j = n.+1
specialize (IHn j'); feed_n 3 IHn => //; first by rewrite ARR in ARRIVAL'; lia .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk j : Job H_task_respects_periodic_model : exists j' : Job,
arrives_in arr_seq
j' /\
job_index arr_seq
j' =
job_index arr_seq j -
1 /\
job_task j' = tsk /\
job_arrival j =
job_arrival j' +
task_period tskF : 0 < task_period tskn : nat j' : Job IHn : job_index arr_seq j' = n ARR_J : arrives_in arr_seq j TSK : job_task j = tsk ARR : job_arrival j =
task_offset tsk + n.+1 * task_period tsk ARR' : arrives_in arr_seq j' IND' : job_index arr_seq j' = job_index arr_seq j - 1 TSK' : job_task j' = tsk ARRIVAL' : job_arrival j =
job_arrival j' + task_period tsk
job_index arr_seq j = n.+1
rewrite IHn in IND'.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk j : Job H_task_respects_periodic_model : exists j' : Job,
arrives_in arr_seq
j' /\
job_index arr_seq
j' =
job_index arr_seq j -
1 /\
job_task j' = tsk /\
job_arrival j =
job_arrival j' +
task_period tskF : 0 < task_period tskn : nat j' : Job IHn : job_index arr_seq j' = n ARR_J : arrives_in arr_seq j TSK : job_task j = tsk ARR : job_arrival j =
task_offset tsk + n.+1 * task_period tsk ARR' : arrives_in arr_seq j' TSK' : job_task j' = tsk ARRIVAL' : job_arrival j =
job_arrival j' + task_period tsk IND' : n = job_index arr_seq j - 1
job_index arr_seq j = n.+1
destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]]; last by lia .Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk j : Job H_task_respects_periodic_model : exists j' : Job,
arrives_in arr_seq
j' /\
job_index arr_seq
j' =
job_index arr_seq j -
1 /\
job_task j' = tsk /\
job_arrival j =
job_arrival j' +
task_period tskF : 0 < task_period tskn : nat j' : Job IHn : job_index arr_seq j' = n ARR_J : arrives_in arr_seq j TSK : job_task j = tsk ARR : job_arrival j =
task_offset tsk + n.+1 * task_period tsk ARR' : arrives_in arr_seq j' TSK' : job_task j' = tsk ARRIVAL' : job_arrival j =
job_arrival j' + task_period tsk IND' : n = job_index arr_seq j - 1 Z : job_index arr_seq j = 0
job_index arr_seq j = n.+1
rewrite (first_job_arrival arr_seq _ tsk)// in ARR.Task : TaskType H : TaskOffset Task H0 : PeriodicModel Task Job : JobType H1 : JobTask Job Task H2 : JobArrival Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq tsk : Task H_valid_offset : valid_offset arr_seq tsk H_valid_period : valid_period tsk j : Job H_task_respects_periodic_model : exists j' : Job,
arrives_in arr_seq
j' /\
job_index arr_seq
j' =
job_index arr_seq j -
1 /\
job_task j' = tsk /\
job_arrival j =
job_arrival j' +
task_period tskF : 0 < task_period tskn : nat j' : Job IHn : job_index arr_seq j' = n ARR_J : arrives_in arr_seq j TSK : job_task j = tsk ARR' : arrives_in arr_seq j' TSK' : job_task j' = tsk ARRIVAL' : job_arrival j =
job_arrival j' + task_period tsk IND' : n = job_index arr_seq j - 1 Z : job_index arr_seq j = 0 ARR : task_offset tsk =
task_offset tsk + n.+1 * task_period tsk
job_index arr_seq j = n.+1
by lia .
Qed .
End PeriodicArrivalTimes .