Library prosa.analysis.facts.periodic.arrival_times
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.periodic.max_inter_arrival.
Require Export prosa.analysis.facts.model.offset.
Require Export prosa.analysis.facts.periodic.sporadic.
In this module, we'll prove the known arrival
times of jobs that stem from periodic tasks.
Consider periodic tasks with an offset ...
... and any type of jobs associated with these tasks.
Consider any unique arrival sequence with consistent arrivals ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq 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.
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:
∀ 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 668)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
induction n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 673)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 676) is:
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = succn n ->
job_arrival j = task_offset tsk + succn n * task_period tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 673)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 680)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 690)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
apply first_job_arrival with (arr_seq0 := arr_seq) (tsk0 := job_task j) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 676)
subgoal 1 (ID 676) is:
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = succn n ->
job_arrival j = task_offset tsk + succn n * task_period tsk
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 676)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 = succn n ->
job_arrival j = task_offset tsk + succn n * task_period tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 676)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 = succn n ->
job_arrival j = task_offset tsk + succn n * task_period tsk
----------------------------------------------------------------------------- *)
intros j ARR TSK_IN JB_INDEX.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 708)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
j : Job
ARR : arrives_in arr_seq j
TSK_IN : job_task j = tsk
JB_INDEX : job_index arr_seq j = succn n
============================
job_arrival j = task_offset tsk + succn n * task_period tsk
----------------------------------------------------------------------------- *)
move : (H_task_respects_periodic_model j ARR) ⇒ PREV_JOB.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 710)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
j : Job
ARR : arrives_in arr_seq j
TSK_IN : job_task j = tsk
JB_INDEX : job_index arr_seq j = succn n
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 + succn n * task_period tsk
----------------------------------------------------------------------------- *)
feed_n 2 PREV_JOB ⇒ //; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 722)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
j : Job
ARR : arrives_in arr_seq j
TSK_IN : job_task j = tsk
JB_INDEX : job_index arr_seq j = succn n
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 + succn n * task_period tsk
----------------------------------------------------------------------------- *)
move : PREV_JOB ⇒ [pj [ARR' [IND [TSK ARRIVAL]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1886)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
j : Job
ARR : arrives_in arr_seq j
TSK_IN : job_task j = tsk
JB_INDEX : job_index arr_seq j = succn n
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 + succn n * task_period tsk
----------------------------------------------------------------------------- *)
specialize (IHn pj); feed_n 3 IHn ⇒ //; first by rewrite IND JB_INDEX; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1906)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 = succn n
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 + succn n * task_period tsk
----------------------------------------------------------------------------- *)
rewrite ARRIVAL IHn; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 668)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
induction n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 673)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 676) is:
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = succn n ->
job_arrival j = task_offset tsk + succn n * task_period tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 673)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 680)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 690)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
apply first_job_arrival with (arr_seq0 := arr_seq) (tsk0 := job_task j) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 676)
subgoal 1 (ID 676) is:
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_index arr_seq j = succn n ->
job_arrival j = task_offset tsk + succn n * task_period tsk
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 676)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 = succn n ->
job_arrival j = task_offset tsk + succn n * task_period tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 676)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 = succn n ->
job_arrival j = task_offset tsk + succn n * task_period tsk
----------------------------------------------------------------------------- *)
intros j ARR TSK_IN JB_INDEX.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 708)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
j : Job
ARR : arrives_in arr_seq j
TSK_IN : job_task j = tsk
JB_INDEX : job_index arr_seq j = succn n
============================
job_arrival j = task_offset tsk + succn n * task_period tsk
----------------------------------------------------------------------------- *)
move : (H_task_respects_periodic_model j ARR) ⇒ PREV_JOB.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 710)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
j : Job
ARR : arrives_in arr_seq j
TSK_IN : job_task j = tsk
JB_INDEX : job_index arr_seq j = succn n
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 + succn n * task_period tsk
----------------------------------------------------------------------------- *)
feed_n 2 PREV_JOB ⇒ //; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 722)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
j : Job
ARR : arrives_in arr_seq j
TSK_IN : job_task j = tsk
JB_INDEX : job_index arr_seq j = succn n
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 + succn n * task_period tsk
----------------------------------------------------------------------------- *)
move : PREV_JOB ⇒ [pj [ARR' [IND [TSK ARRIVAL]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1886)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
j : Job
ARR : arrives_in arr_seq j
TSK_IN : job_task j = tsk
JB_INDEX : job_index arr_seq j = succn n
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 + succn n * task_period tsk
----------------------------------------------------------------------------- *)
specialize (IHn pj); feed_n 3 IHn ⇒ //; first by rewrite IND JB_INDEX; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1906)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 = succn n
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 + succn n * task_period tsk
----------------------------------------------------------------------------- *)
rewrite ARRIVAL IHn; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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:
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
∃ n, job_arrival j = task_offset tsk + n × task_period tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 686)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
intros × ARR TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 689)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
∃ (job_index arr_seq j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 695)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 702)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now feed_n 3 J_ARR ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
∃ n, job_arrival j = task_offset tsk + n × task_period tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 686)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
intros × ARR TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 689)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
∃ (job_index arr_seq j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 695)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 702)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
----------------------------------------------------------------------------- *)
now feed_n 3 J_ARR ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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:
∀ 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 709)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
have F : task_period tsk > 0 by auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 714)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 719)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 722) is:
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j = task_offset tsk + succn n * task_period tsk ->
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
+ intros × ARR_J TSK ARR.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 726)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
j : 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
subgoal 2 (ID 722) is:
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j = task_offset tsk + succn n * task_period tsk ->
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]] ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 742)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
j : 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 = succn m
============================
job_index arr_seq j = 0
subgoal 2 (ID 722) is:
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j = task_offset tsk + succn n * task_period tsk ->
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
now apply periodic_arrival_times in SUCC ⇒ //; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 722)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
n : 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 + succn n * task_period tsk ->
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
+ intros × ARR_J TSK ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1053)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
n : 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
j : Job
ARR_J : arrives_in arr_seq j
TSK : job_task j = tsk
ARR : job_arrival j = task_offset tsk + succn n * task_period tsk
============================
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
specialize (H_task_respects_periodic_model j); feed_n 3 H_task_respects_periodic_model ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1062)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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
ARR_J : arrives_in arr_seq j
TSK : job_task j = tsk
ARR : job_arrival j = task_offset tsk + succn n * task_period tsk
============================
0 < job_index arr_seq j
subgoal 2 (ID 1073) is:
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1062)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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
ARR_J : arrives_in arr_seq j
TSK : job_task j = tsk
ARR : job_arrival j = task_offset tsk + succn n * task_period tsk
============================
0 < job_index arr_seq j
----------------------------------------------------------------------------- *)
rewrite lt0n; apply /eqP; intro EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1160)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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
ARR_J : arrives_in arr_seq j
TSK : job_task j = tsk
ARR : job_arrival j = task_offset tsk + succn n * task_period tsk
EQ : job_index arr_seq j = 0
============================
False
----------------------------------------------------------------------------- *)
apply first_job_arrival with (tsk0 := tsk) in EQ ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1166)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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
ARR_J : arrives_in arr_seq j
TSK : job_task j = tsk
ARR : job_arrival j = task_offset tsk + succn n * task_period tsk
EQ : job_arrival j = task_offset tsk
============================
False
----------------------------------------------------------------------------- *)
now rewrite EQ in ARR; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1073)
subgoal 1 (ID 1073) is:
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1073)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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
ARR_J : arrives_in arr_seq j
TSK : job_task j = tsk
ARR : job_arrival j = task_offset tsk + succn n * task_period tsk
============================
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
move : H_task_respects_periodic_model ⇒ [j' [ARR' [IND' [TSK' ARRIVAL']]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2623)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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
ARR_J : arrives_in arr_seq j
TSK : job_task j = tsk
ARR : job_arrival j = task_offset tsk + succn n * 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 = succn n
----------------------------------------------------------------------------- *)
specialize (IHn j'); feed_n 3 IHn ⇒ //; first by rewrite ARR in ARRIVAL'; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2643)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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 + succn n * 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 = succn n
----------------------------------------------------------------------------- *)
rewrite IHn in IND'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3209)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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 + succn n * 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 = succn n
----------------------------------------------------------------------------- *)
destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]]; last by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3220)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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 + succn n * 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 = succn n
----------------------------------------------------------------------------- *)
apply first_job_arrival with (tsk0 := tsk) in Z ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3570)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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 + succn n * 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_arrival j = task_offset tsk
============================
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
now rewrite Z in ARR; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PeriodicArrivalTimes.
∀ 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 709)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
have F : task_period tsk > 0 by auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 714)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 719)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
subgoal 2 (ID 722) is:
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j = task_offset tsk + succn n * task_period tsk ->
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
+ intros × ARR_J TSK ARR.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 726)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
j : 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
subgoal 2 (ID 722) is:
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j = task_offset tsk + succn n * task_period tsk ->
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]] ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 742)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
j : 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 = succn m
============================
job_index arr_seq j = 0
subgoal 2 (ID 722) is:
forall j : Job,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j = task_offset tsk + succn n * task_period tsk ->
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
now apply periodic_arrival_times in SUCC ⇒ //; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 722)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
n : 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 + succn n * task_period tsk ->
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
+ intros × ARR_J TSK ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1053)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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
n : 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
j : Job
ARR_J : arrives_in arr_seq j
TSK : job_task j = tsk
ARR : job_arrival j = task_offset tsk + succn n * task_period tsk
============================
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
specialize (H_task_respects_periodic_model j); feed_n 3 H_task_respects_periodic_model ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1062)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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
ARR_J : arrives_in arr_seq j
TSK : job_task j = tsk
ARR : job_arrival j = task_offset tsk + succn n * task_period tsk
============================
0 < job_index arr_seq j
subgoal 2 (ID 1073) is:
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1062)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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
ARR_J : arrives_in arr_seq j
TSK : job_task j = tsk
ARR : job_arrival j = task_offset tsk + succn n * task_period tsk
============================
0 < job_index arr_seq j
----------------------------------------------------------------------------- *)
rewrite lt0n; apply /eqP; intro EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1160)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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
ARR_J : arrives_in arr_seq j
TSK : job_task j = tsk
ARR : job_arrival j = task_offset tsk + succn n * task_period tsk
EQ : job_index arr_seq j = 0
============================
False
----------------------------------------------------------------------------- *)
apply first_job_arrival with (tsk0 := tsk) in EQ ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1166)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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
ARR_J : arrives_in arr_seq j
TSK : job_task j = tsk
ARR : job_arrival j = task_offset tsk + succn n * task_period tsk
EQ : job_arrival j = task_offset tsk
============================
False
----------------------------------------------------------------------------- *)
now rewrite EQ in ARR; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1073)
subgoal 1 (ID 1073) is:
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1073)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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
ARR_J : arrives_in arr_seq j
TSK : job_task j = tsk
ARR : job_arrival j = task_offset tsk + succn n * task_period tsk
============================
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
move : H_task_respects_periodic_model ⇒ [j' [ARR' [IND' [TSK' ARRIVAL']]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2623)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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
ARR_J : arrives_in arr_seq j
TSK : job_task j = tsk
ARR : job_arrival j = task_offset tsk + succn n * 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 = succn n
----------------------------------------------------------------------------- *)
specialize (IHn j'); feed_n 3 IHn ⇒ //; first by rewrite ARR in ARRIVAL'; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2643)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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 + succn n * 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 = succn n
----------------------------------------------------------------------------- *)
rewrite IHn in IND'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3209)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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 + succn n * 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 = succn n
----------------------------------------------------------------------------- *)
destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]]; last by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3220)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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 + succn n * 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 = succn n
----------------------------------------------------------------------------- *)
apply first_job_arrival with (tsk0 := tsk) in Z ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3570)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq 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 tsk
F : 0 < task_period tsk
n : 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 + succn n * 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_arrival j = task_offset tsk
============================
job_index arr_seq j = succn n
----------------------------------------------------------------------------- *)
now rewrite Z in ARR; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PeriodicArrivalTimes.