Library prosa.analysis.facts.periodic.arrival_separation
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.periodic.sporadic.
Require Export prosa.analysis.facts.sporadic.
In this section we show that the separation between job
arrivals of a periodic task is some multiple of their
corresponding task's period.
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_arrseq: arrival_sequence_uniq arr_seq.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
... and any task [tsk] that is to be analyzed.
Assume all tasks have a valid period and respect the periodic task model.
Hypothesis H_periodic_model: respects_periodic_task_model arr_seq tsk.
Hypothesis H_valid_period: valid_period tsk.
Hypothesis H_valid_period: valid_period tsk.
In this section we show that two consecutive jobs of a periodic
task have their arrival times separated by their task's
period.
Consider any two _consecutive_ jobs [j1] and [j2] of task [tsk].
Variable j1 : Job.
Variable j2 : Job.
Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
Hypothesis H_j1_of_task: job_task j1 = tsk.
Hypothesis H_j2_of_task: job_task j2 = tsk.
Hypothesis H_consecutive_jobs: job_index arr_seq j2 = job_index arr_seq j1 + 1.
Variable j2 : Job.
Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
Hypothesis H_j1_of_task: job_task j1 = tsk.
Hypothesis H_j2_of_task: job_task j2 = tsk.
Hypothesis H_consecutive_jobs: job_index arr_seq j2 = job_index arr_seq j1 + 1.
We show that if job [j1] and [j2] are consecutive jobs with [j2]
arriving after [j1], then their arrival times are separated by
their task's period.
Lemma consecutive_job_separation:
job_arrival j2 = job_arrival j1 + task_period tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 372)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
============================
job_arrival j2 = job_arrival j1 + task_period tsk
----------------------------------------------------------------------------- *)
Proof.
move : (H_periodic_model j2) ⇒ PERIODIC.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 374)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
PERIODIC : arrives_in arr_seq j2 ->
0 < job_index arr_seq j2 ->
job_task j2 = tsk ->
exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j2 - 1 /\
job_task j' = tsk /\
job_arrival j2 = job_arrival j' + task_period tsk
============================
job_arrival j2 = job_arrival j1 + task_period tsk
----------------------------------------------------------------------------- *)
feed_n 3 PERIODIC ⇒ //; first by rewrite H_consecutive_jobs; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 392)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
PERIODIC : exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j2 - 1 /\
job_task j' = tsk /\
job_arrival j2 = job_arrival j' + task_period tsk
============================
job_arrival j2 = job_arrival j1 + task_period tsk
----------------------------------------------------------------------------- *)
move : PERIODIC ⇒ [pj' [ARR_IN_PJ' [INDPJ'J' [TSKPJ' ARRPJ']]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1060)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
pj' : Job
ARR_IN_PJ' : arrives_in arr_seq pj'
INDPJ'J' : job_index arr_seq pj' = job_index arr_seq j2 - 1
TSKPJ' : job_task pj' = tsk
ARRPJ' : job_arrival j2 = job_arrival pj' + task_period tsk
============================
job_arrival j2 = job_arrival j1 + task_period tsk
----------------------------------------------------------------------------- *)
rewrite H_consecutive_jobs addnK in INDPJ'J'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1099)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
pj' : Job
ARR_IN_PJ' : arrives_in arr_seq pj'
TSKPJ' : job_task pj' = tsk
ARRPJ' : job_arrival j2 = job_arrival pj' + task_period tsk
INDPJ'J' : job_index arr_seq pj' = job_index arr_seq j1
============================
job_arrival j2 = job_arrival j1 + task_period tsk
----------------------------------------------------------------------------- *)
apply equal_index_implies_equal_jobs in INDPJ'J' ⇒ //; last by rewrite TSKPJ'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1104)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
pj' : Job
ARR_IN_PJ' : arrives_in arr_seq pj'
TSKPJ' : job_task pj' = tsk
ARRPJ' : job_arrival j2 = job_arrival pj' + task_period tsk
INDPJ'J' : pj' = j1
============================
job_arrival j2 = job_arrival j1 + task_period tsk
----------------------------------------------------------------------------- *)
now rewrite INDPJ'J' in ARRPJ'; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ConsecutiveJobSeparation.
job_arrival j2 = job_arrival j1 + task_period tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 372)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
============================
job_arrival j2 = job_arrival j1 + task_period tsk
----------------------------------------------------------------------------- *)
Proof.
move : (H_periodic_model j2) ⇒ PERIODIC.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 374)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
PERIODIC : arrives_in arr_seq j2 ->
0 < job_index arr_seq j2 ->
job_task j2 = tsk ->
exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j2 - 1 /\
job_task j' = tsk /\
job_arrival j2 = job_arrival j' + task_period tsk
============================
job_arrival j2 = job_arrival j1 + task_period tsk
----------------------------------------------------------------------------- *)
feed_n 3 PERIODIC ⇒ //; first by rewrite H_consecutive_jobs; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 392)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
PERIODIC : exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j2 - 1 /\
job_task j' = tsk /\
job_arrival j2 = job_arrival j' + task_period tsk
============================
job_arrival j2 = job_arrival j1 + task_period tsk
----------------------------------------------------------------------------- *)
move : PERIODIC ⇒ [pj' [ARR_IN_PJ' [INDPJ'J' [TSKPJ' ARRPJ']]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1060)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
pj' : Job
ARR_IN_PJ' : arrives_in arr_seq pj'
INDPJ'J' : job_index arr_seq pj' = job_index arr_seq j2 - 1
TSKPJ' : job_task pj' = tsk
ARRPJ' : job_arrival j2 = job_arrival pj' + task_period tsk
============================
job_arrival j2 = job_arrival j1 + task_period tsk
----------------------------------------------------------------------------- *)
rewrite H_consecutive_jobs addnK in INDPJ'J'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1099)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
pj' : Job
ARR_IN_PJ' : arrives_in arr_seq pj'
TSKPJ' : job_task pj' = tsk
ARRPJ' : job_arrival j2 = job_arrival pj' + task_period tsk
INDPJ'J' : job_index arr_seq pj' = job_index arr_seq j1
============================
job_arrival j2 = job_arrival j1 + task_period tsk
----------------------------------------------------------------------------- *)
apply equal_index_implies_equal_jobs in INDPJ'J' ⇒ //; last by rewrite TSKPJ'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1104)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1
pj' : Job
ARR_IN_PJ' : arrives_in arr_seq pj'
TSKPJ' : job_task pj' = tsk
ARRPJ' : job_arrival j2 = job_arrival pj' + task_period tsk
INDPJ'J' : pj' = j1
============================
job_arrival j2 = job_arrival j1 + task_period tsk
----------------------------------------------------------------------------- *)
now rewrite INDPJ'J' in ARRPJ'; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ConsecutiveJobSeparation.
In this section we show that for two unequal jobs of a task,
there exists a non-zero multiple of their task's period which separates
their arrival times.
Consider any two _consecutive_ jobs [j1] and [j2] of task [tsk]
that stem from the arrival sequence.
Variable j1 j2 : Job.
Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
Hypothesis H_j1_of_task: job_task j1 = tsk.
Hypothesis H_j2_of_task: job_task j2 = tsk.
Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
Hypothesis H_j1_of_task: job_task j1 = tsk.
Hypothesis H_j2_of_task: job_task j2 = tsk.
We'll assume that job [j1] arrives before [j2] and that
their indices differ by an integer [k].
Variable k : nat.
Hypothesis H_index_difference_k: job_index arr_seq j1 + k = job_index arr_seq j2 .
Hypothesis H_job_arrival_lt: job_arrival j1 < job_arrival j2.
Hypothesis H_index_difference_k: job_index arr_seq j1 + k = job_index arr_seq j2 .
Hypothesis H_job_arrival_lt: job_arrival j1 < job_arrival j2.
We prove that arrival of unequal jobs of a task [tsk] are
separated by a non-zero multiple of [task_period tsk] provided
their index differs by a number [k].
Lemma job_arrival_separation_when_index_diff_is_k:
∃ n,
n > 0 ∧
job_arrival j2 = job_arrival j1 + n × task_period tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 378)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
k : nat
H_index_difference_k : job_index arr_seq j1 + k = job_index arr_seq j2
H_job_arrival_lt : job_arrival j1 < job_arrival j2
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
Proof.
move: j1 j2 H_j1_of_task H_j2_of_task H_index_difference_k H_job_arrival_lt H_j2_from_arr_seq H_j1_from_arr_seq;
clear H_index_difference_k H_job_arrival_lt H_j2_from_arr_seq H_j1_from_arr_seq H_j1_of_task H_j2_of_task j1 j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 387)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
============================
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + k = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
move: k ⇒ s.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 389)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
============================
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
induction s.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 393)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
============================
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
subgoal 2 (ID 396) is:
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 393)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
============================
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
intros j1 j2 TSKj1 TSKj2 STEP LT ARRj1 ARRj2; exfalso.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 405)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + 0 = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj1 : arrives_in arr_seq j2
ARRj2 : arrives_in arr_seq j1
============================
False
----------------------------------------------------------------------------- *)
specialize (earlier_arrival_implies_lower_index arr_seq H_consistent_arrivals j1 j2) ⇒ LT_IND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 412)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + 0 = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj1 : arrives_in arr_seq j2
ARRj2 : arrives_in arr_seq j1
LT_IND : arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = job_task j2 ->
job_arrival j1 < job_arrival j2 ->
job_index arr_seq j1 < job_index arr_seq j2
============================
False
----------------------------------------------------------------------------- *)
feed_n 4 LT_IND ⇒ //; first by rewrite TSKj2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 436)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + 0 = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj1 : arrives_in arr_seq j2
ARRj2 : arrives_in arr_seq j1
LT_IND : job_index arr_seq j1 < job_index arr_seq j2
============================
False
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
subgoal 1 (ID 396) is:
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
============================
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
============================
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
intros j1 j2 TSKj1 TSKj2 STEP LT ARRj2 ARRj1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 679)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn s = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
specialize (exists_jobs_before_j
arr_seq H_consistent_arrivals H_uniq_arrseq j2 ARRj2 (job_index arr_seq j2 - s)) ⇒ BEFORE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 690)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn s = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
BEFORE : job_index arr_seq j2 - s < job_index arr_seq j2 ->
exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j2 - s
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
destruct s.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 707)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + 1 = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
BEFORE : job_index arr_seq j2 - 0 < job_index arr_seq j2 ->
exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j2 - 0
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
subgoal 2 (ID 714) is:
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
- ∃ 1; repeat split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 719)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + 1 = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
BEFORE : job_index arr_seq j2 - 0 < job_index arr_seq j2 ->
exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j2 - 0
============================
job_arrival j2 = job_arrival j1 + 1 * task_period tsk
subgoal 2 (ID 714) is:
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
now rewrite (consecutive_job_separation j1) //; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 714)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
BEFORE : job_index arr_seq j2 - succn s < job_index arr_seq j2 ->
exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j2 - succn s
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
- feed BEFORE; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1751)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
BEFORE : exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j2 - succn s
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
move : BEFORE ⇒ [nj [NEQNJ [TSKNJ [ARRNJ INDNJ]]]]; rewrite TSKj2 in TSKNJ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2838)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
nj : Job
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
specialize (IHs nj j2); feed_n 6 IHs ⇒ //; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2859)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj : Job
IHs : job_arrival nj < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq nj ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival nj + n * task_period tsk
j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
============================
job_arrival nj < job_arrival j2
subgoal 2 (ID 2876) is:
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2859)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj : Job
IHs : job_arrival nj < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq nj ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival nj + n * task_period tsk
j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
============================
job_arrival nj < job_arrival j2
----------------------------------------------------------------------------- *)
now apply (lower_index_implies_earlier_arrival _ H_consistent_arrivals H_uniq_arrseq tsk);
auto with basic_facts; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2876)
subgoal 1 (ID 2876) is:
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2876)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj : Job
IHs : exists n : nat,
0 < n /\ job_arrival j2 = job_arrival nj + n * task_period tsk
j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
move : IHs ⇒ [n [NZN ARRJ'NJ]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 5209)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
ARRJ'NJ : job_arrival j2 = job_arrival nj + n * task_period tsk
============================
exists n0 : nat,
0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk
----------------------------------------------------------------------------- *)
move: (H_periodic_model nj) ⇒ PERIODIC; feed_n 3 PERIODIC ⇒ //; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 5229)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
ARRJ'NJ : job_arrival j2 = job_arrival nj + n * task_period tsk
PERIODIC : exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq nj - 1 /\
job_task j' = tsk /\
job_arrival nj = job_arrival j' + task_period tsk
============================
exists n0 : nat,
0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk
----------------------------------------------------------------------------- *)
move : PERIODIC ⇒ [sj [ARR_IN_SJ [INDSJ [TSKSJ ARRSJ]]]]; rewrite ARRSJ in ARRJ'NJ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 7339)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
sj : Job
ARR_IN_SJ : arrives_in arr_seq sj
INDSJ : job_index arr_seq sj = job_index arr_seq nj - 1
TSKSJ : job_task sj = tsk
ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
ARRJ'NJ : job_arrival j2 =
job_arrival sj + task_period tsk + n * task_period tsk
============================
exists n0 : nat,
0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk
----------------------------------------------------------------------------- *)
have INDJ : (job_index arr_seq j1 = job_index arr_seq j2 - s.+2) by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 7888)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
sj : Job
ARR_IN_SJ : arrives_in arr_seq sj
INDSJ : job_index arr_seq sj = job_index arr_seq nj - 1
TSKSJ : job_task sj = tsk
ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
ARRJ'NJ : job_arrival j2 =
job_arrival sj + task_period tsk + n * task_period tsk
INDJ : job_index arr_seq j1 = job_index arr_seq j2 - succn (succn s)
============================
exists n0 : nat,
0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk
----------------------------------------------------------------------------- *)
rewrite INDNJ -subnDA addn1 -INDJ in INDSJ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 7942)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
sj : Job
ARR_IN_SJ : arrives_in arr_seq sj
TSKSJ : job_task sj = tsk
ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
ARRJ'NJ : job_arrival j2 =
job_arrival sj + task_period tsk + n * task_period tsk
INDJ : job_index arr_seq j1 = job_index arr_seq j2 - succn (succn s)
INDSJ : job_index arr_seq sj = job_index arr_seq j1
============================
exists n0 : nat,
0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk
----------------------------------------------------------------------------- *)
apply equal_index_implies_equal_jobs in INDSJ ⇒ //; last by rewrite TSKj1 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 7947)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
sj : Job
ARR_IN_SJ : arrives_in arr_seq sj
TSKSJ : job_task sj = tsk
ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
ARRJ'NJ : job_arrival j2 =
job_arrival sj + task_period tsk + n * task_period tsk
INDJ : job_index arr_seq j1 = job_index arr_seq j2 - succn (succn s)
INDSJ : sj = j1
============================
exists n0 : nat,
0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk
----------------------------------------------------------------------------- *)
∃ (n.+1); split; try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 8011)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
sj : Job
ARR_IN_SJ : arrives_in arr_seq sj
TSKSJ : job_task sj = tsk
ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
ARRJ'NJ : job_arrival j2 =
job_arrival sj + task_period tsk + n * task_period tsk
INDJ : job_index arr_seq j1 = job_index arr_seq j2 - succn (succn s)
INDSJ : sj = j1
============================
job_arrival j2 = job_arrival j1 + succn n * task_period tsk
----------------------------------------------------------------------------- *)
rewrite INDSJ in ARRJ'NJ; rewrite mulSnr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 9130)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
sj : Job
ARR_IN_SJ : arrives_in arr_seq sj
TSKSJ : job_task sj = tsk
ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
INDJ : job_index arr_seq j1 = job_index arr_seq j2 - succn (succn s)
INDSJ : sj = j1
ARRJ'NJ : job_arrival j2 =
job_arrival j1 + task_period tsk + n * task_period tsk
============================
job_arrival j2 = job_arrival j1 + (n * task_period tsk + task_period tsk)
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ArrivalSeparationWithGivenIndexDifference.
∃ n,
n > 0 ∧
job_arrival j2 = job_arrival j1 + n × task_period tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 378)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
k : nat
H_index_difference_k : job_index arr_seq j1 + k = job_index arr_seq j2
H_job_arrival_lt : job_arrival j1 < job_arrival j2
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
Proof.
move: j1 j2 H_j1_of_task H_j2_of_task H_index_difference_k H_job_arrival_lt H_j2_from_arr_seq H_j1_from_arr_seq;
clear H_index_difference_k H_job_arrival_lt H_j2_from_arr_seq H_j1_from_arr_seq H_j1_of_task H_j2_of_task j1 j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 387)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
============================
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + k = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
move: k ⇒ s.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 389)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
============================
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
induction s.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 393)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
============================
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
subgoal 2 (ID 396) is:
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 393)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
============================
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
intros j1 j2 TSKj1 TSKj2 STEP LT ARRj1 ARRj2; exfalso.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 405)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + 0 = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj1 : arrives_in arr_seq j2
ARRj2 : arrives_in arr_seq j1
============================
False
----------------------------------------------------------------------------- *)
specialize (earlier_arrival_implies_lower_index arr_seq H_consistent_arrivals j1 j2) ⇒ LT_IND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 412)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + 0 = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj1 : arrives_in arr_seq j2
ARRj2 : arrives_in arr_seq j1
LT_IND : arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = job_task j2 ->
job_arrival j1 < job_arrival j2 ->
job_index arr_seq j1 < job_index arr_seq j2
============================
False
----------------------------------------------------------------------------- *)
feed_n 4 LT_IND ⇒ //; first by rewrite TSKj2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 436)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + 0 = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj1 : arrives_in arr_seq j2
ARRj2 : arrives_in arr_seq j1
LT_IND : job_index arr_seq j1 < job_index arr_seq j2
============================
False
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
subgoal 1 (ID 396) is:
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
============================
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
============================
forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
intros j1 j2 TSKj1 TSKj2 STEP LT ARRj2 ARRj1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 679)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn s = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
specialize (exists_jobs_before_j
arr_seq H_consistent_arrivals H_uniq_arrseq j2 ARRj2 (job_index arr_seq j2 - s)) ⇒ BEFORE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 690)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn s = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
BEFORE : job_index arr_seq j2 - s < job_index arr_seq j2 ->
exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j2 - s
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
destruct s.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 707)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + 1 = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
BEFORE : job_index arr_seq j2 - 0 < job_index arr_seq j2 ->
exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j2 - 0
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
subgoal 2 (ID 714) is:
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
- ∃ 1; repeat split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 719)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + 0 = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + 1 = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
BEFORE : job_index arr_seq j2 - 0 < job_index arr_seq j2 ->
exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j2 - 0
============================
job_arrival j2 = job_arrival j1 + 1 * task_period tsk
subgoal 2 (ID 714) is:
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
now rewrite (consecutive_job_separation j1) //; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 714)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
BEFORE : job_index arr_seq j2 - succn s < job_index arr_seq j2 ->
exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j2 - succn s
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
- feed BEFORE; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1751)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
BEFORE : exists j' : Job,
j2 <> j' /\
job_task j' = job_task j2 /\
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq j2 - succn s
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
move : BEFORE ⇒ [nj [NEQNJ [TSKNJ [ARRNJ INDNJ]]]]; rewrite TSKj2 in TSKNJ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2838)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
IHs : forall j1 j2 : Job,
job_task j1 = tsk ->
job_task j2 = tsk ->
job_index arr_seq j1 + succn s = job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq j1 ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
j1, j2 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
nj : Job
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
specialize (IHs nj j2); feed_n 6 IHs ⇒ //; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2859)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj : Job
IHs : job_arrival nj < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq nj ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival nj + n * task_period tsk
j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
============================
job_arrival nj < job_arrival j2
subgoal 2 (ID 2876) is:
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2859)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj : Job
IHs : job_arrival nj < job_arrival j2 ->
arrives_in arr_seq j2 ->
arrives_in arr_seq nj ->
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival nj + n * task_period tsk
j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
============================
job_arrival nj < job_arrival j2
----------------------------------------------------------------------------- *)
now apply (lower_index_implies_earlier_arrival _ H_consistent_arrivals H_uniq_arrseq tsk);
auto with basic_facts; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2876)
subgoal 1 (ID 2876) is:
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2876)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj : Job
IHs : exists n : nat,
0 < n /\ job_arrival j2 = job_arrival nj + n * task_period tsk
j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
move : IHs ⇒ [n [NZN ARRJ'NJ]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 5209)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
ARRJ'NJ : job_arrival j2 = job_arrival nj + n * task_period tsk
============================
exists n0 : nat,
0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk
----------------------------------------------------------------------------- *)
move: (H_periodic_model nj) ⇒ PERIODIC; feed_n 3 PERIODIC ⇒ //; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 5229)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
ARRJ'NJ : job_arrival j2 = job_arrival nj + n * task_period tsk
PERIODIC : exists j' : Job,
arrives_in arr_seq j' /\
job_index arr_seq j' = job_index arr_seq nj - 1 /\
job_task j' = tsk /\
job_arrival nj = job_arrival j' + task_period tsk
============================
exists n0 : nat,
0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk
----------------------------------------------------------------------------- *)
move : PERIODIC ⇒ [sj [ARR_IN_SJ [INDSJ [TSKSJ ARRSJ]]]]; rewrite ARRSJ in ARRJ'NJ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 7339)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
sj : Job
ARR_IN_SJ : arrives_in arr_seq sj
INDSJ : job_index arr_seq sj = job_index arr_seq nj - 1
TSKSJ : job_task sj = tsk
ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
ARRJ'NJ : job_arrival j2 =
job_arrival sj + task_period tsk + n * task_period tsk
============================
exists n0 : nat,
0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk
----------------------------------------------------------------------------- *)
have INDJ : (job_index arr_seq j1 = job_index arr_seq j2 - s.+2) by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 7888)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
sj : Job
ARR_IN_SJ : arrives_in arr_seq sj
INDSJ : job_index arr_seq sj = job_index arr_seq nj - 1
TSKSJ : job_task sj = tsk
ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
ARRJ'NJ : job_arrival j2 =
job_arrival sj + task_period tsk + n * task_period tsk
INDJ : job_index arr_seq j1 = job_index arr_seq j2 - succn (succn s)
============================
exists n0 : nat,
0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk
----------------------------------------------------------------------------- *)
rewrite INDNJ -subnDA addn1 -INDJ in INDSJ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 7942)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
sj : Job
ARR_IN_SJ : arrives_in arr_seq sj
TSKSJ : job_task sj = tsk
ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
ARRJ'NJ : job_arrival j2 =
job_arrival sj + task_period tsk + n * task_period tsk
INDJ : job_index arr_seq j1 = job_index arr_seq j2 - succn (succn s)
INDSJ : job_index arr_seq sj = job_index arr_seq j1
============================
exists n0 : nat,
0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk
----------------------------------------------------------------------------- *)
apply equal_index_implies_equal_jobs in INDSJ ⇒ //; last by rewrite TSKj1 ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 7947)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
sj : Job
ARR_IN_SJ : arrives_in arr_seq sj
TSKSJ : job_task sj = tsk
ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
ARRJ'NJ : job_arrival j2 =
job_arrival sj + task_period tsk + n * task_period tsk
INDJ : job_index arr_seq j1 = job_index arr_seq j2 - succn (succn s)
INDSJ : sj = j1
============================
exists n0 : nat,
0 < n0 /\ job_arrival j2 = job_arrival j1 + n0 * task_period tsk
----------------------------------------------------------------------------- *)
∃ (n.+1); split; try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 8011)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
sj : Job
ARR_IN_SJ : arrives_in arr_seq sj
TSKSJ : job_task sj = tsk
ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
ARRJ'NJ : job_arrival j2 =
job_arrival sj + task_period tsk + n * task_period tsk
INDJ : job_index arr_seq j1 = job_index arr_seq j2 - succn (succn s)
INDSJ : sj = j1
============================
job_arrival j2 = job_arrival j1 + succn n * task_period tsk
----------------------------------------------------------------------------- *)
rewrite INDSJ in ARRJ'NJ; rewrite mulSnr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 9130)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
k, s : nat
j2, nj, j1 : Job
TSKj1 : job_task j1 = tsk
TSKj2 : job_task j2 = tsk
STEP : job_index arr_seq j1 + succn (succn s) = job_index arr_seq j2
LT : job_arrival j1 < job_arrival j2
ARRj2 : arrives_in arr_seq j2
ARRj1 : arrives_in arr_seq j1
NEQNJ : j2 <> nj
ARRNJ : arrives_in arr_seq nj
INDNJ : job_index arr_seq nj = job_index arr_seq j2 - succn s
TSKNJ : job_task nj = tsk
n : nat
NZN : 0 < n
sj : Job
ARR_IN_SJ : arrives_in arr_seq sj
TSKSJ : job_task sj = tsk
ARRSJ : job_arrival nj = job_arrival sj + task_period tsk
INDJ : job_index arr_seq j1 = job_index arr_seq j2 - succn (succn s)
INDSJ : sj = j1
ARRJ'NJ : job_arrival j2 =
job_arrival j1 + task_period tsk + n * task_period tsk
============================
job_arrival j2 = job_arrival j1 + (n * task_period tsk + task_period tsk)
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ArrivalSeparationWithGivenIndexDifference.
Consider any two _distinct_ jobs [j1] and [j2] of task [tsk]
that stem from the arrival sequence.
Variable j1 j2 : Job.
Hypothesis H_j1_neq_j2: j1 ≠ j2.
Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
Hypothesis H_j1_of_task: job_task j1 = tsk.
Hypothesis H_j2_of_task: job_task j2 = tsk.
Hypothesis H_j1_neq_j2: j1 ≠ j2.
Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
Hypothesis H_j1_of_task: job_task j1 = tsk.
Hypothesis H_j2_of_task: job_task j2 = tsk.
Without loss of generality, we assume that
job [j1] arrives before job [j2].
We generalize the above lemma to show that any two unequal
jobs of task [tsk] are separated by a non-zero multiple
of [task_period tsk].
Lemma job_sep_periodic:
∃ n,
n > 0 ∧
job_arrival j2 = job_arrival j1 + n × task_period tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 370)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
Proof.
apply job_arrival_separation_when_index_diff_is_k with (k := (job_index arr_seq j2 - job_index arr_seq j1)); try done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 383)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
============================
job_index arr_seq j1 + (job_index arr_seq j2 - job_index arr_seq j1) =
job_index arr_seq j2
subgoal 2 (ID 384) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
- apply subnKC.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 431)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
============================
job_index arr_seq j1 <= job_index arr_seq j2
subgoal 2 (ID 384) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
move_neq_up IND.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 459)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
IND : job_index arr_seq j2 < job_index arr_seq j1
============================
False
subgoal 2 (ID 384) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
eapply lower_index_implies_earlier_arrival in IND; eauto with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 467)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
IND : job_arrival j2 < job_arrival j1
============================
False
subgoal 2 (ID 384) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
now move_neq_down IND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 384)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
============================
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
- case: (boolP (job_index arr_seq j1 == job_index arr_seq j2)) ⇒ [/eqP EQ_IND|NEQ_IND].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 912)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
EQ_IND : job_index arr_seq j1 = job_index arr_seq j2
============================
job_arrival j1 < job_arrival j2
subgoal 2 (ID 911) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
+ now apply equal_index_implies_equal_jobs in EQ_IND ⇒ //; rewrite H_j1_of_task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 911)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
NEQ_IND : job_index arr_seq j1 != job_index arr_seq j2
============================
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
+ move: NEQ_IND; rewrite neq_ltn ⇒ /orP [LT|LT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1020)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
LT : job_index arr_seq j1 < job_index arr_seq j2
============================
job_arrival j1 < job_arrival j2
subgoal 2 (ID 1021) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
× now eapply (lower_index_implies_earlier_arrival) in LT; eauto with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1021)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
LT : job_index arr_seq j2 < job_index arr_seq j1
============================
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
× eapply (lower_index_implies_earlier_arrival) in LT; eauto with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1124)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
LT : job_arrival j2 < job_arrival j1
============================
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
now move_neq_down LT.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End JobArrivalSeparation.
∃ n,
n > 0 ∧
job_arrival j2 = job_arrival j1 + n × task_period tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 370)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
============================
exists n : nat,
0 < n /\ job_arrival j2 = job_arrival j1 + n * task_period tsk
----------------------------------------------------------------------------- *)
Proof.
apply job_arrival_separation_when_index_diff_is_k with (k := (job_index arr_seq j2 - job_index arr_seq j1)); try done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 383)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
============================
job_index arr_seq j1 + (job_index arr_seq j2 - job_index arr_seq j1) =
job_index arr_seq j2
subgoal 2 (ID 384) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
- apply subnKC.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 431)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
============================
job_index arr_seq j1 <= job_index arr_seq j2
subgoal 2 (ID 384) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
move_neq_up IND.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 459)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
IND : job_index arr_seq j2 < job_index arr_seq j1
============================
False
subgoal 2 (ID 384) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
eapply lower_index_implies_earlier_arrival in IND; eauto with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 467)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
IND : job_arrival j2 < job_arrival j1
============================
False
subgoal 2 (ID 384) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
now move_neq_down IND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 384)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
============================
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
- case: (boolP (job_index arr_seq j1 == job_index arr_seq j2)) ⇒ [/eqP EQ_IND|NEQ_IND].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 912)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
EQ_IND : job_index arr_seq j1 = job_index arr_seq j2
============================
job_arrival j1 < job_arrival j2
subgoal 2 (ID 911) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
+ now apply equal_index_implies_equal_jobs in EQ_IND ⇒ //; rewrite H_j1_of_task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 911)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
NEQ_IND : job_index arr_seq j1 != job_index arr_seq j2
============================
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
+ move: NEQ_IND; rewrite neq_ltn ⇒ /orP [LT|LT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1020)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
LT : job_index arr_seq j1 < job_index arr_seq j2
============================
job_arrival j1 < job_arrival j2
subgoal 2 (ID 1021) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
× now eapply (lower_index_implies_earlier_arrival) in LT; eauto with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1021)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
LT : job_index arr_seq j2 < job_index arr_seq j1
============================
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
× eapply (lower_index_implies_earlier_arrival) in LT; eauto with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1124)
Task : TaskType
H : PeriodicModel Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arrseq : arrival_sequence_uniq arr_seq
tsk : Task
H_periodic_model : respects_periodic_task_model arr_seq tsk
H_valid_period : valid_period tsk
j1, j2 : Job
H_j1_neq_j2 : j1 <> j2
H_j1_from_arr_seq : arrives_in arr_seq j1
H_j2_from_arr_seq : arrives_in arr_seq j2
H_j1_of_task : job_task j1 = tsk
H_j2_of_task : job_task j2 = tsk
H_j1_before_j2 : job_arrival j1 <= job_arrival j2
LT : job_arrival j2 < job_arrival j1
============================
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
now move_neq_down LT.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End JobArrivalSeparation.