Library prosa.analysis.facts.sporadic
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.task.arrival.periodic.
Require Export prosa.analysis.facts.job_index.
The Sporadic Model
Consider sporadic tasks with an offset ...
Context {Task : TaskType}.
Context `{TaskOffset Task}.
Context `{TaskMaxInterArrival Task}.
Context `{SporadicModel Task}.
Context `{TaskOffset Task}.
Context `{TaskMaxInterArrival Task}.
Context `{SporadicModel Task}.
... 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 sporadic task [tsk] that is to be analyzed.
Variable tsk : Task.
Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
Consider any two jobs from the arrival sequence that stem
from task [tsk].
Variable j1 : Job.
Variable j2 : Job.
Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
Hypothesis H_j1_task: job_task j1 = tsk.
Hypothesis H_j2_task: job_task j2 = tsk.
Variable j2 : Job.
Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
Hypothesis H_j1_task: job_task j1 = tsk.
Hypothesis H_j2_task: job_task j2 = tsk.
We first show that for any two jobs [j1] and [j2], [j2] arrives after [j1]
provided [job_index] of [j2] strictly exceeds the [job_index] of [j1].
Lemma lower_index_implies_earlier_arrival:
job_index arr_seq j1 < job_index arr_seq j2 →
job_arrival j1 < job_arrival j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 366)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
job_index arr_seq j1 < job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
Proof.
intro IND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 367)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
============================
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
move: (H_sporadic_model j1 j2) ⇒ SPORADIC; feed_n 6 SPORADIC ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 370)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
SPORADIC : j1 <> j2 ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = tsk ->
job_task j2 = tsk ->
job_arrival j1 <= job_arrival j2 ->
job_arrival j1 + task_min_inter_arrival_time tsk <=
job_arrival j2
============================
j1 <> j2
subgoal 2 (ID 400) is:
job_arrival j1 <= job_arrival j2
subgoal 3 (ID 405) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
- rewrite → diff_jobs_iff_diff_indices ⇒ //; auto.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 491)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
SPORADIC : j1 <> j2 ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = tsk ->
job_task j2 = tsk ->
job_arrival j1 <= job_arrival j2 ->
job_arrival j1 + task_min_inter_arrival_time tsk <=
job_arrival j2
============================
job_index arr_seq j1 <> job_index arr_seq j2
subgoal 2 (ID 497) is:
job_task j1 = job_task j2
subgoal 3 (ID 400) is:
job_arrival j1 <= job_arrival j2
subgoal 4 (ID 405) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
+ now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 497)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
SPORADIC : j1 <> j2 ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = tsk ->
job_task j2 = tsk ->
job_arrival j1 <= job_arrival j2 ->
job_arrival j1 + task_min_inter_arrival_time tsk <=
job_arrival j2
============================
job_task j1 = job_task j2
subgoal 2 (ID 400) is:
job_arrival j1 <= job_arrival j2
subgoal 3 (ID 405) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
+ now rewrite H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 400)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
SPORADIC : job_arrival j1 <= job_arrival j2 ->
job_arrival j1 + task_min_inter_arrival_time tsk <=
job_arrival j2
============================
job_arrival j1 <= job_arrival j2
subgoal 2 (ID 405) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
- apply (index_lte_implies_arrival_lte arr_seq); try auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1427)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
SPORADIC : job_arrival j1 <= job_arrival j2 ->
job_arrival j1 + task_min_inter_arrival_time tsk <=
job_arrival j2
============================
job_task j2 = job_task j1
subgoal 2 (ID 405) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
now rewrite H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 405)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
SPORADIC : job_arrival j1 + task_min_inter_arrival_time tsk <=
job_arrival j2
============================
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
- have POS_IA : task_min_inter_arrival_time tsk > 0 by auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1437)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
SPORADIC : job_arrival j1 + task_min_inter_arrival_time tsk <=
job_arrival j2
POS_IA : 0 < task_min_inter_arrival_time tsk
============================
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End SporadicModelIndexLemmas.
job_index arr_seq j1 < job_index arr_seq j2 →
job_arrival j1 < job_arrival j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 366)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
job_index arr_seq j1 < job_index arr_seq j2 ->
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
Proof.
intro IND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 367)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
============================
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
move: (H_sporadic_model j1 j2) ⇒ SPORADIC; feed_n 6 SPORADIC ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 370)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
SPORADIC : j1 <> j2 ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = tsk ->
job_task j2 = tsk ->
job_arrival j1 <= job_arrival j2 ->
job_arrival j1 + task_min_inter_arrival_time tsk <=
job_arrival j2
============================
j1 <> j2
subgoal 2 (ID 400) is:
job_arrival j1 <= job_arrival j2
subgoal 3 (ID 405) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
- rewrite → diff_jobs_iff_diff_indices ⇒ //; auto.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 491)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
SPORADIC : j1 <> j2 ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = tsk ->
job_task j2 = tsk ->
job_arrival j1 <= job_arrival j2 ->
job_arrival j1 + task_min_inter_arrival_time tsk <=
job_arrival j2
============================
job_index arr_seq j1 <> job_index arr_seq j2
subgoal 2 (ID 497) is:
job_task j1 = job_task j2
subgoal 3 (ID 400) is:
job_arrival j1 <= job_arrival j2
subgoal 4 (ID 405) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
+ now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 497)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
SPORADIC : j1 <> j2 ->
arrives_in arr_seq j1 ->
arrives_in arr_seq j2 ->
job_task j1 = tsk ->
job_task j2 = tsk ->
job_arrival j1 <= job_arrival j2 ->
job_arrival j1 + task_min_inter_arrival_time tsk <=
job_arrival j2
============================
job_task j1 = job_task j2
subgoal 2 (ID 400) is:
job_arrival j1 <= job_arrival j2
subgoal 3 (ID 405) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
+ now rewrite H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 400)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
SPORADIC : job_arrival j1 <= job_arrival j2 ->
job_arrival j1 + task_min_inter_arrival_time tsk <=
job_arrival j2
============================
job_arrival j1 <= job_arrival j2
subgoal 2 (ID 405) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
- apply (index_lte_implies_arrival_lte arr_seq); try auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1427)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
SPORADIC : job_arrival j1 <= job_arrival j2 ->
job_arrival j1 + task_min_inter_arrival_time tsk <=
job_arrival j2
============================
job_task j2 = job_task j1
subgoal 2 (ID 405) is:
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
now rewrite H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 405)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
SPORADIC : job_arrival j1 + task_min_inter_arrival_time tsk <=
job_arrival j2
============================
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
- have POS_IA : task_min_inter_arrival_time tsk > 0 by auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1437)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : job_index arr_seq j1 < job_index arr_seq j2
SPORADIC : job_arrival j1 + task_min_inter_arrival_time tsk <=
job_arrival j2
POS_IA : 0 < task_min_inter_arrival_time tsk
============================
job_arrival j1 < job_arrival j2
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End SporadicModelIndexLemmas.
Consider sporadic tasks with an offset ...
Context {Task : TaskType}.
Context `{TaskOffset Task}.
Context `{TaskMaxInterArrival Task}.
Context `{SporadicModel Task}.
Context `{TaskOffset Task}.
Context `{TaskMaxInterArrival Task}.
Context `{SporadicModel Task}.
... 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 sporadic task [tsk] that is to be analyzed.
Variable tsk : Task.
Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
Consider any two jobs from the arrival sequence that stem
from task [tsk].
Variable j1 : Job.
Variable j2 : Job.
Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
Hypothesis H_j1_task: job_task j1 = tsk.
Hypothesis H_j2_task: job_task j2 = tsk.
Variable j2 : Job.
Hypothesis H_j1_from_arrseq: arrives_in arr_seq j1.
Hypothesis H_j2_from_arrseq: arrives_in arr_seq j2.
Hypothesis H_j1_task: job_task j1 = tsk.
Hypothesis H_j2_task: job_task j2 = tsk.
We observe that distinct jobs cannot have equal arrival times.
Lemma uneq_job_uneq_arr:
j1 ≠ j2 →
job_arrival j1 ≠ job_arrival j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 362)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
j1 <> j2 -> job_arrival j1 <> job_arrival j2
----------------------------------------------------------------------------- *)
Proof.
intros UNEQ EQ_ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 365)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
UNEQ : j1 <> j2
EQ_ARR : job_arrival j1 = job_arrival j2
============================
False
----------------------------------------------------------------------------- *)
rewrite → diff_jobs_iff_diff_indices in UNEQ ⇒ //; auto; last by rewrite H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 382)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
EQ_ARR : job_arrival j1 = job_arrival j2
UNEQ : job_index arr_seq j1 <> job_index arr_seq j2
============================
False
----------------------------------------------------------------------------- *)
move /neqP: UNEQ; rewrite neq_ltn ⇒ /orP [LT|LT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 625)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
EQ_ARR : job_arrival j1 = job_arrival j2
LT : job_index arr_seq j1 < job_index arr_seq j2
============================
False
subgoal 2 (ID 626) is:
False
----------------------------------------------------------------------------- *)
all: now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT ⇒ //; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
j1 ≠ j2 →
job_arrival j1 ≠ job_arrival j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 362)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
j1 <> j2 -> job_arrival j1 <> job_arrival j2
----------------------------------------------------------------------------- *)
Proof.
intros UNEQ EQ_ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 365)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
UNEQ : j1 <> j2
EQ_ARR : job_arrival j1 = job_arrival j2
============================
False
----------------------------------------------------------------------------- *)
rewrite → diff_jobs_iff_diff_indices in UNEQ ⇒ //; auto; last by rewrite H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 382)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
EQ_ARR : job_arrival j1 = job_arrival j2
UNEQ : job_index arr_seq j1 <> job_index arr_seq j2
============================
False
----------------------------------------------------------------------------- *)
move /neqP: UNEQ; rewrite neq_ltn ⇒ /orP [LT|LT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 625)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
EQ_ARR : job_arrival j1 = job_arrival j2
LT : job_index arr_seq j1 < job_index arr_seq j2
============================
False
subgoal 2 (ID 626) is:
False
----------------------------------------------------------------------------- *)
all: now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT ⇒ //; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We prove a stronger version of the above lemma by showing
that jobs [j1] and [j2] are equal if and only if they arrive at the
same time.
Lemma same_jobs_iff_same_arr:
j1 = j2 ↔
job_arrival j1 = job_arrival j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 371)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
j1 = j2 <-> job_arrival j1 = job_arrival j2
----------------------------------------------------------------------------- *)
Proof.
split; first by apply congr1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 374)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
job_arrival j1 = job_arrival j2 -> j1 = j2
----------------------------------------------------------------------------- *)
intro EQ_ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 375)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
EQ_ARR : job_arrival j1 = job_arrival j2
============================
j1 = j2
----------------------------------------------------------------------------- *)
case: (boolP (j1 == j2)) ⇒ [/eqP EQ | /eqP NEQ]; first by auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 463)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
EQ_ARR : job_arrival j1 = job_arrival j2
NEQ : j1 <> j2
============================
j1 = j2
----------------------------------------------------------------------------- *)
rewrite → diff_jobs_iff_diff_indices in NEQ ⇒ //; auto; last by rewrite H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 480)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
EQ_ARR : job_arrival j1 = job_arrival j2
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
============================
j1 = j2
----------------------------------------------------------------------------- *)
move /neqP: NEQ; rewrite neq_ltn ⇒ /orP [LT|LT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 706)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
EQ_ARR : job_arrival j1 = job_arrival j2
LT : job_index arr_seq j1 < job_index arr_seq j2
============================
j1 = j2
subgoal 2 (ID 707) is:
j1 = j2
----------------------------------------------------------------------------- *)
all: now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT ⇒ //; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End DifferentJobsImplyDifferentArrivalTimes.
j1 = j2 ↔
job_arrival j1 = job_arrival j2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 371)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
j1 = j2 <-> job_arrival j1 = job_arrival j2
----------------------------------------------------------------------------- *)
Proof.
split; first by apply congr1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 374)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
job_arrival j1 = job_arrival j2 -> j1 = j2
----------------------------------------------------------------------------- *)
intro EQ_ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 375)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
EQ_ARR : job_arrival j1 = job_arrival j2
============================
j1 = j2
----------------------------------------------------------------------------- *)
case: (boolP (j1 == j2)) ⇒ [/eqP EQ | /eqP NEQ]; first by auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 463)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
EQ_ARR : job_arrival j1 = job_arrival j2
NEQ : j1 <> j2
============================
j1 = j2
----------------------------------------------------------------------------- *)
rewrite → diff_jobs_iff_diff_indices in NEQ ⇒ //; auto; last by rewrite H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 480)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
EQ_ARR : job_arrival j1 = job_arrival j2
NEQ : job_index arr_seq j1 <> job_index arr_seq j2
============================
j1 = j2
----------------------------------------------------------------------------- *)
move /neqP: NEQ; rewrite neq_ltn ⇒ /orP [LT|LT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 706)
Task : TaskType
H : TaskOffset Task
H0 : TaskMaxInterArrival Task
H1 : SporadicModel Task
Job : JobType
H2 : JobTask Job Task
H3 : 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_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
j1, j2 : Job
H_j1_from_arrseq : arrives_in arr_seq j1
H_j2_from_arrseq : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
EQ_ARR : job_arrival j1 = job_arrival j2
LT : job_index arr_seq j1 < job_index arr_seq j2
============================
j1 = j2
subgoal 2 (ID 707) is:
j1 = j2
----------------------------------------------------------------------------- *)
all: now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT ⇒ //; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End DifferentJobsImplyDifferentArrivalTimes.
In this section we prove a few properties regarding task arrivals
in context of the sporadic task model.
Consider sporadic tasks with an offset ...
Context {Task : TaskType}.
Context `{TaskOffset Task}.
Context `{SporadicModel Task}.
Context `{TaskMaxInterArrival Task}.
Context `{TaskOffset Task}.
Context `{SporadicModel Task}.
Context `{TaskMaxInterArrival Task}.
... and any type of jobs associated with these tasks.
Consider any unique arrival sequence with consistent arrivals, ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
... and any sporadic task [tsk] to be analyzed.
Assume all tasks have valid minimum inter-arrival times, valid offsets, and respect the
sporadic task model.
Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
Hypothesis H_valid_offset: valid_offset arr_seq tsk.
Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
Hypothesis H_valid_offset: valid_offset arr_seq tsk.
Consider any two jobs from the arrival sequence that stem
from task [tsk].
Variable j1 j2 : Job.
Hypothesis H_j1_from_arrival_sequence: arrives_in arr_seq j1.
Hypothesis H_j2_from_arrival_sequence: arrives_in arr_seq j2.
Hypothesis H_j1_task: job_task j1 = tsk.
Hypothesis H_j2_task: job_task j2 = tsk.
Hypothesis H_j1_from_arrival_sequence: arrives_in arr_seq j1.
Hypothesis H_j2_from_arrival_sequence: arrives_in arr_seq j2.
Hypothesis H_j1_task: job_task j1 = tsk.
Hypothesis H_j2_task: job_task j2 = tsk.
We show that a sporadic task with valid min inter-arrival time cannot
have more than one job arriving at any time.
Lemma size_task_arrivals_at_leq_one:
(∃ j,
size (task_arrivals_at_job_arrival arr_seq j) > 1 ∧
respects_sporadic_task_model arr_seq (job_task j) ∧
valid_task_min_inter_arrival_time (job_task j)) →
False.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 379)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
(exists j : Job,
1 < size (task_arrivals_at_job_arrival arr_seq j) /\
respects_sporadic_task_model arr_seq (job_task j) /\
valid_task_min_inter_arrival_time (job_task j)) -> False
----------------------------------------------------------------------------- *)
Proof.
move ⇒ [j [SIZE_G [PERIODIC VALID_TMIA]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 410)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
============================
False
----------------------------------------------------------------------------- *)
specialize (exists_two Job (task_arrivals_at_job_arrival arr_seq j)) ⇒ EXISTS_TWO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 417)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
EXISTS_TWO : 1 < size (task_arrivals_at_job_arrival arr_seq j) ->
uniq (task_arrivals_at_job_arrival arr_seq j) ->
exists a b : Job,
a <> b /\
a \in task_arrivals_at_job_arrival arr_seq j /\
b \in task_arrivals_at_job_arrival arr_seq j
============================
False
----------------------------------------------------------------------------- *)
destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by done | by apply filter_uniq | ].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 442)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : a <> b
A_IN : a \in task_arrivals_at_job_arrival arr_seq j
B_IN : b \in task_arrivals_at_job_arrival arr_seq j
============================
False
----------------------------------------------------------------------------- *)
rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 527)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : a <> b
A_IN : (job_task a == job_task j) &&
(a \in arrivals_at arr_seq (job_arrival j))
B_IN : (job_task b == job_task j) &&
(b \in arrivals_at arr_seq (job_arrival j))
============================
False
----------------------------------------------------------------------------- *)
move: A_IN B_IN ⇒ /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 674)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : a <> b
TSKA : job_task a = job_task j
ARRA : a \in arrivals_at arr_seq (job_arrival j)
TSKB : job_task b = job_task j
ARRB : b \in arrivals_at arr_seq (job_arrival j)
============================
False
----------------------------------------------------------------------------- *)
move: (ARRA); move: (ARRB); rewrite /arrivals_at ⇒ A_IN B_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 681)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : a <> b
TSKA : job_task a = job_task j
ARRA : a \in arrivals_at arr_seq (job_arrival j)
TSKB : job_task b = job_task j
ARRB : b \in arrivals_at arr_seq (job_arrival j)
A_IN : b \in arr_seq (job_arrival j)
B_IN : a \in arr_seq (job_arrival j)
============================
False
----------------------------------------------------------------------------- *)
apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 686)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : a <> b
TSKA : job_task a = job_task j
ARRA : a \in arrivals_at arr_seq (job_arrival j)
TSKB : job_task b = job_task j
ARRB : b \in arrivals_at arr_seq (job_arrival j)
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
============================
False
----------------------------------------------------------------------------- *)
have EQ_ARR_A : (job_arrival a = job_arrival j) by apply H_consistent_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 697)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : a <> b
TSKA : job_task a = job_task j
ARRA : a \in arrivals_at arr_seq (job_arrival j)
TSKB : job_task b = job_task j
ARRB : b \in arrivals_at arr_seq (job_arrival j)
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
EQ_ARR_A : job_arrival a = job_arrival j
============================
False
----------------------------------------------------------------------------- *)
have EQ_ARR_B : (job_arrival b = job_arrival j) by apply H_consistent_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 707)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : a <> b
TSKA : job_task a = job_task j
ARRA : a \in arrivals_at arr_seq (job_arrival j)
TSKB : job_task b = job_task j
ARRB : b \in arrivals_at arr_seq (job_arrival j)
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
EQ_ARR_A : job_arrival a = job_arrival j
EQ_ARR_B : job_arrival b = job_arrival j
============================
False
----------------------------------------------------------------------------- *)
apply uneq_job_uneq_arr with (arr_seq0 := arr_seq) (tsk0 := job_task j) in NEQ ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 716)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : job_arrival a <> job_arrival b
TSKA : job_task a = job_task j
ARRA : a \in arrivals_at arr_seq (job_arrival j)
TSKB : job_task b = job_task j
ARRB : b \in arrivals_at arr_seq (job_arrival j)
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
EQ_ARR_A : job_arrival a = job_arrival j
EQ_ARR_B : job_arrival b = job_arrival j
============================
False
----------------------------------------------------------------------------- *)
now rewrite EQ_ARR_A EQ_ARR_B in NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(∃ j,
size (task_arrivals_at_job_arrival arr_seq j) > 1 ∧
respects_sporadic_task_model arr_seq (job_task j) ∧
valid_task_min_inter_arrival_time (job_task j)) →
False.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 379)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
(exists j : Job,
1 < size (task_arrivals_at_job_arrival arr_seq j) /\
respects_sporadic_task_model arr_seq (job_task j) /\
valid_task_min_inter_arrival_time (job_task j)) -> False
----------------------------------------------------------------------------- *)
Proof.
move ⇒ [j [SIZE_G [PERIODIC VALID_TMIA]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 410)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
============================
False
----------------------------------------------------------------------------- *)
specialize (exists_two Job (task_arrivals_at_job_arrival arr_seq j)) ⇒ EXISTS_TWO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 417)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
EXISTS_TWO : 1 < size (task_arrivals_at_job_arrival arr_seq j) ->
uniq (task_arrivals_at_job_arrival arr_seq j) ->
exists a b : Job,
a <> b /\
a \in task_arrivals_at_job_arrival arr_seq j /\
b \in task_arrivals_at_job_arrival arr_seq j
============================
False
----------------------------------------------------------------------------- *)
destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by done | by apply filter_uniq | ].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 442)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : a <> b
A_IN : a \in task_arrivals_at_job_arrival arr_seq j
B_IN : b \in task_arrivals_at_job_arrival arr_seq j
============================
False
----------------------------------------------------------------------------- *)
rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 527)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : a <> b
A_IN : (job_task a == job_task j) &&
(a \in arrivals_at arr_seq (job_arrival j))
B_IN : (job_task b == job_task j) &&
(b \in arrivals_at arr_seq (job_arrival j))
============================
False
----------------------------------------------------------------------------- *)
move: A_IN B_IN ⇒ /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 674)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : a <> b
TSKA : job_task a = job_task j
ARRA : a \in arrivals_at arr_seq (job_arrival j)
TSKB : job_task b = job_task j
ARRB : b \in arrivals_at arr_seq (job_arrival j)
============================
False
----------------------------------------------------------------------------- *)
move: (ARRA); move: (ARRB); rewrite /arrivals_at ⇒ A_IN B_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 681)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : a <> b
TSKA : job_task a = job_task j
ARRA : a \in arrivals_at arr_seq (job_arrival j)
TSKB : job_task b = job_task j
ARRB : b \in arrivals_at arr_seq (job_arrival j)
A_IN : b \in arr_seq (job_arrival j)
B_IN : a \in arr_seq (job_arrival j)
============================
False
----------------------------------------------------------------------------- *)
apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 686)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : a <> b
TSKA : job_task a = job_task j
ARRA : a \in arrivals_at arr_seq (job_arrival j)
TSKB : job_task b = job_task j
ARRB : b \in arrivals_at arr_seq (job_arrival j)
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
============================
False
----------------------------------------------------------------------------- *)
have EQ_ARR_A : (job_arrival a = job_arrival j) by apply H_consistent_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 697)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : a <> b
TSKA : job_task a = job_task j
ARRA : a \in arrivals_at arr_seq (job_arrival j)
TSKB : job_task b = job_task j
ARRB : b \in arrivals_at arr_seq (job_arrival j)
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
EQ_ARR_A : job_arrival a = job_arrival j
============================
False
----------------------------------------------------------------------------- *)
have EQ_ARR_B : (job_arrival b = job_arrival j) by apply H_consistent_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 707)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : a <> b
TSKA : job_task a = job_task j
ARRA : a \in arrivals_at arr_seq (job_arrival j)
TSKB : job_task b = job_task j
ARRB : b \in arrivals_at arr_seq (job_arrival j)
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
EQ_ARR_A : job_arrival a = job_arrival j
EQ_ARR_B : job_arrival b = job_arrival j
============================
False
----------------------------------------------------------------------------- *)
apply uneq_job_uneq_arr with (arr_seq0 := arr_seq) (tsk0 := job_task j) in NEQ ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 716)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
j : Job
SIZE_G : 1 < size (task_arrivals_at_job_arrival arr_seq j)
PERIODIC : respects_sporadic_task_model arr_seq (job_task j)
VALID_TMIA : valid_task_min_inter_arrival_time (job_task j)
a, b : Job
NEQ : job_arrival a <> job_arrival b
TSKA : job_task a = job_task j
ARRA : a \in arrivals_at arr_seq (job_arrival j)
TSKB : job_task b = job_task j
ARRB : b \in arrivals_at arr_seq (job_arrival j)
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
EQ_ARR_A : job_arrival a = job_arrival j
EQ_ARR_B : job_arrival b = job_arrival j
============================
False
----------------------------------------------------------------------------- *)
now rewrite EQ_ARR_A EQ_ARR_B in NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We show that no jobs of the task [tsk] other than [j1] arrive at
the same time as [j1], and thus the task arrivals at [job arrival j1]
consists only of job [j1].
Lemma only_j_in_task_arrivals_at_j:
task_arrivals_at_job_arrival arr_seq j1 = [::j1].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 388)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
task_arrivals_at_job_arrival arr_seq j1 = [:: j1]
----------------------------------------------------------------------------- *)
Proof.
set (task_arrivals_at_job_arrival arr_seq j1) as seq in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 394)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
============================
seq = [:: j1]
----------------------------------------------------------------------------- *)
have J_IN_FILTER : (j1 \in seq) by apply arrives_in_task_arrivals_at.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 407)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
============================
seq = [:: j1]
----------------------------------------------------------------------------- *)
have SIZE_CASE : size seq = 0 ∨ size seq = 1 ∨ size seq > 1
by intros; now destruct (size seq) as [ | [ | ]]; try auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 471)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
SIZE_CASE : size seq = 0 \/ size seq = 1 \/ 1 < size seq
============================
seq = [:: j1]
----------------------------------------------------------------------------- *)
move: SIZE_CASE ⇒ [Z|[ONE|GTONE]].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 486)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
Z : size seq = 0
============================
seq = [:: j1]
subgoal 2 (ID 499) is:
seq = [:: j1]
subgoal 3 (ID 500) is:
seq = [:: j1]
----------------------------------------------------------------------------- *)
- apply size0nil in Z.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 501)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
Z : seq = [::]
============================
seq = [:: j1]
subgoal 2 (ID 499) is:
seq = [:: j1]
subgoal 3 (ID 500) is:
seq = [:: j1]
----------------------------------------------------------------------------- *)
now rewrite Z in J_IN_FILTER.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 499)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
ONE : size seq = 1
============================
seq = [:: j1]
subgoal 2 (ID 500) is:
seq = [:: j1]
----------------------------------------------------------------------------- *)
- repeat (destruct seq; try by done).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 620)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
s : Job
J_IN_FILTER : j1 \in [:: s]
ONE : size [:: s] = 1
============================
[:: s] = [:: j1]
subgoal 2 (ID 500) is:
seq = [:: j1]
----------------------------------------------------------------------------- *)
rewrite mem_seq1 in J_IN_FILTER; move : J_IN_FILTER ⇒ /eqP J1_S.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 743)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
s : Job
ONE : size [:: s] = 1
J1_S : j1 = s
============================
[:: s] = [:: j1]
subgoal 2 (ID 500) is:
seq = [:: j1]
----------------------------------------------------------------------------- *)
now rewrite J1_S.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 500)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
GTONE : 1 < size seq
============================
seq = [:: j1]
----------------------------------------------------------------------------- *)
- exfalso.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 746)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
GTONE : 1 < size seq
============================
False
----------------------------------------------------------------------------- *)
apply size_task_arrivals_at_leq_one.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 747)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
GTONE : 1 < size seq
============================
exists j : Job,
1 < size (task_arrivals_at_job_arrival arr_seq j) /\
respects_sporadic_task_model arr_seq (job_task j) /\
valid_task_min_inter_arrival_time (job_task j)
----------------------------------------------------------------------------- *)
∃ j1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 749)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
GTONE : 1 < size seq
============================
1 < size (task_arrivals_at_job_arrival arr_seq j1) /\
respects_sporadic_task_model arr_seq (job_task j1) /\
valid_task_min_inter_arrival_time (job_task j1)
----------------------------------------------------------------------------- *)
now repeat split ⇒ //; try rewrite H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
task_arrivals_at_job_arrival arr_seq j1 = [::j1].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 388)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
task_arrivals_at_job_arrival arr_seq j1 = [:: j1]
----------------------------------------------------------------------------- *)
Proof.
set (task_arrivals_at_job_arrival arr_seq j1) as seq in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 394)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
============================
seq = [:: j1]
----------------------------------------------------------------------------- *)
have J_IN_FILTER : (j1 \in seq) by apply arrives_in_task_arrivals_at.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 407)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
============================
seq = [:: j1]
----------------------------------------------------------------------------- *)
have SIZE_CASE : size seq = 0 ∨ size seq = 1 ∨ size seq > 1
by intros; now destruct (size seq) as [ | [ | ]]; try auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 471)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
SIZE_CASE : size seq = 0 \/ size seq = 1 \/ 1 < size seq
============================
seq = [:: j1]
----------------------------------------------------------------------------- *)
move: SIZE_CASE ⇒ [Z|[ONE|GTONE]].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 486)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
Z : size seq = 0
============================
seq = [:: j1]
subgoal 2 (ID 499) is:
seq = [:: j1]
subgoal 3 (ID 500) is:
seq = [:: j1]
----------------------------------------------------------------------------- *)
- apply size0nil in Z.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 501)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
Z : seq = [::]
============================
seq = [:: j1]
subgoal 2 (ID 499) is:
seq = [:: j1]
subgoal 3 (ID 500) is:
seq = [:: j1]
----------------------------------------------------------------------------- *)
now rewrite Z in J_IN_FILTER.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 499)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
ONE : size seq = 1
============================
seq = [:: j1]
subgoal 2 (ID 500) is:
seq = [:: j1]
----------------------------------------------------------------------------- *)
- repeat (destruct seq; try by done).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 620)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
s : Job
J_IN_FILTER : j1 \in [:: s]
ONE : size [:: s] = 1
============================
[:: s] = [:: j1]
subgoal 2 (ID 500) is:
seq = [:: j1]
----------------------------------------------------------------------------- *)
rewrite mem_seq1 in J_IN_FILTER; move : J_IN_FILTER ⇒ /eqP J1_S.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 743)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
s : Job
ONE : size [:: s] = 1
J1_S : j1 = s
============================
[:: s] = [:: j1]
subgoal 2 (ID 500) is:
seq = [:: j1]
----------------------------------------------------------------------------- *)
now rewrite J1_S.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 500)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
GTONE : 1 < size seq
============================
seq = [:: j1]
----------------------------------------------------------------------------- *)
- exfalso.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 746)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
GTONE : 1 < size seq
============================
False
----------------------------------------------------------------------------- *)
apply size_task_arrivals_at_leq_one.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 747)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
GTONE : 1 < size seq
============================
exists j : Job,
1 < size (task_arrivals_at_job_arrival arr_seq j) /\
respects_sporadic_task_model arr_seq (job_task j) /\
valid_task_min_inter_arrival_time (job_task j)
----------------------------------------------------------------------------- *)
∃ j1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 749)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
seq := task_arrivals_at_job_arrival arr_seq j1 : seq.seq Job
J_IN_FILTER : j1 \in seq
GTONE : 1 < size seq
============================
1 < size (task_arrivals_at_job_arrival arr_seq j1) /\
respects_sporadic_task_model arr_seq (job_task j1) /\
valid_task_min_inter_arrival_time (job_task j1)
----------------------------------------------------------------------------- *)
now repeat split ⇒ //; try rewrite H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We show that no jobs of the task [tsk] other than [j1] arrive at
the same time as [j1], and thus the task arrivals at [job arrival j1]
consists only of job [j1].
Lemma only_j_at_job_arrival_j:
∀ t,
job_arrival j1 = t →
task_arrivals_at arr_seq tsk t = [::j1].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 401)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
forall t : instant,
job_arrival j1 = t -> task_arrivals_at arr_seq tsk t = [:: j1]
----------------------------------------------------------------------------- *)
Proof.
intros t ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 403)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
t : instant
ARR : job_arrival j1 = t
============================
task_arrivals_at arr_seq tsk t = [:: j1]
----------------------------------------------------------------------------- *)
rewrite -ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 405)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
t : instant
ARR : job_arrival j1 = t
============================
task_arrivals_at arr_seq tsk (job_arrival j1) = [:: j1]
----------------------------------------------------------------------------- *)
specialize (only_j_in_task_arrivals_at_j) ⇒ J_AT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 408)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
t : instant
ARR : job_arrival j1 = t
J_AT : task_arrivals_at_job_arrival arr_seq j1 = [:: j1]
============================
task_arrivals_at arr_seq tsk (job_arrival j1) = [:: j1]
----------------------------------------------------------------------------- *)
now rewrite /task_arrivals_at_job_arrival H_j1_task in J_AT.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t,
job_arrival j1 = t →
task_arrivals_at arr_seq tsk t = [::j1].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 401)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
forall t : instant,
job_arrival j1 = t -> task_arrivals_at arr_seq tsk t = [:: j1]
----------------------------------------------------------------------------- *)
Proof.
intros t ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 403)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
t : instant
ARR : job_arrival j1 = t
============================
task_arrivals_at arr_seq tsk t = [:: j1]
----------------------------------------------------------------------------- *)
rewrite -ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 405)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
t : instant
ARR : job_arrival j1 = t
============================
task_arrivals_at arr_seq tsk (job_arrival j1) = [:: j1]
----------------------------------------------------------------------------- *)
specialize (only_j_in_task_arrivals_at_j) ⇒ J_AT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 408)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
t : instant
ARR : job_arrival j1 = t
J_AT : task_arrivals_at_job_arrival arr_seq j1 = [:: j1]
============================
task_arrivals_at arr_seq tsk (job_arrival j1) = [:: j1]
----------------------------------------------------------------------------- *)
now rewrite /task_arrivals_at_job_arrival H_j1_task in J_AT.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We show that a job [j1] is the first job that arrives
in task arrivals at [job_arrival j1] by showing that the
index of job [j1] in [task_arrivals_at_job_arrival arr_seq j1] is 0.
Lemma index_j_in_task_arrivals_at:
index j1 (task_arrivals_at_job_arrival arr_seq j1) = 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 409)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
index j1 (task_arrivals_at_job_arrival arr_seq j1) = 0
----------------------------------------------------------------------------- *)
Proof.
now rewrite only_j_in_task_arrivals_at_j //= eq_refl.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
index j1 (task_arrivals_at_job_arrival arr_seq j1) = 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 409)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
index j1 (task_arrivals_at_job_arrival arr_seq j1) = 0
----------------------------------------------------------------------------- *)
Proof.
now rewrite only_j_in_task_arrivals_at_j //= eq_refl.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We observe that for any job [j] the arrival time of [prev_job j] is
strictly less than the arrival time of [j] in context of periodic tasks.
Lemma prev_job_arr_lt:
job_index arr_seq j1 > 0 →
job_arrival (prev_job arr_seq j1) < job_arrival j1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 422)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
0 < job_index arr_seq j1 ->
job_arrival (prev_job arr_seq j1) < job_arrival j1
----------------------------------------------------------------------------- *)
Proof.
intros IND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 423)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
============================
job_arrival (prev_job arr_seq j1) < job_arrival j1
----------------------------------------------------------------------------- *)
have PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) ≤ job_arrival j1 by apply prev_job_arr_lte ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 441)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
============================
job_arrival (prev_job arr_seq j1) < job_arrival j1
----------------------------------------------------------------------------- *)
rewrite ltn_neqAle; apply /andP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 469)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
============================
job_arrival (prev_job arr_seq j1) != job_arrival j1 /\
job_arrival (prev_job arr_seq j1) <= job_arrival j1
----------------------------------------------------------------------------- *)
split ⇒ //; apply /eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 532)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
============================
job_arrival (prev_job arr_seq j1) <> job_arrival j1
----------------------------------------------------------------------------- *)
apply uneq_job_uneq_arr with (arr_seq0 := arr_seq) (tsk0 := job_task j1) ⇒ //; try by rewrite H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 545)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
============================
arrives_in arr_seq (prev_job arr_seq j1)
subgoal 2 (ID 547) is:
job_task (prev_job arr_seq j1) = job_task j1
subgoal 3 (ID 549) is:
prev_job arr_seq j1 <> j1
----------------------------------------------------------------------------- *)
- now apply prev_job_arr.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 547)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
============================
job_task (prev_job arr_seq j1) = job_task j1
subgoal 2 (ID 549) is:
prev_job arr_seq j1 <> j1
----------------------------------------------------------------------------- *)
- now apply prev_job_task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 549)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
============================
prev_job arr_seq j1 <> j1
----------------------------------------------------------------------------- *)
- intro EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 720)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
EQ : prev_job arr_seq j1 = j1
============================
False
----------------------------------------------------------------------------- *)
have SM_IND: job_index arr_seq j1 - 1 = job_index arr_seq j1 by rewrite -prev_job_index // EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 775)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
EQ : prev_job arr_seq j1 = j1
SM_IND : job_index arr_seq j1 - 1 = job_index arr_seq j1
============================
False
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_index arr_seq j1 > 0 →
job_arrival (prev_job arr_seq j1) < job_arrival j1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 422)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
0 < job_index arr_seq j1 ->
job_arrival (prev_job arr_seq j1) < job_arrival j1
----------------------------------------------------------------------------- *)
Proof.
intros IND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 423)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
============================
job_arrival (prev_job arr_seq j1) < job_arrival j1
----------------------------------------------------------------------------- *)
have PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) ≤ job_arrival j1 by apply prev_job_arr_lte ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 441)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
============================
job_arrival (prev_job arr_seq j1) < job_arrival j1
----------------------------------------------------------------------------- *)
rewrite ltn_neqAle; apply /andP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 469)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
============================
job_arrival (prev_job arr_seq j1) != job_arrival j1 /\
job_arrival (prev_job arr_seq j1) <= job_arrival j1
----------------------------------------------------------------------------- *)
split ⇒ //; apply /eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 532)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
============================
job_arrival (prev_job arr_seq j1) <> job_arrival j1
----------------------------------------------------------------------------- *)
apply uneq_job_uneq_arr with (arr_seq0 := arr_seq) (tsk0 := job_task j1) ⇒ //; try by rewrite H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 545)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
============================
arrives_in arr_seq (prev_job arr_seq j1)
subgoal 2 (ID 547) is:
job_task (prev_job arr_seq j1) = job_task j1
subgoal 3 (ID 549) is:
prev_job arr_seq j1 <> j1
----------------------------------------------------------------------------- *)
- now apply prev_job_arr.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 547)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
============================
job_task (prev_job arr_seq j1) = job_task j1
subgoal 2 (ID 549) is:
prev_job arr_seq j1 <> j1
----------------------------------------------------------------------------- *)
- now apply prev_job_task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 549)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
============================
prev_job arr_seq j1 <> j1
----------------------------------------------------------------------------- *)
- intro EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 720)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
EQ : prev_job arr_seq j1 = j1
============================
False
----------------------------------------------------------------------------- *)
have SM_IND: job_index arr_seq j1 - 1 = job_index arr_seq j1 by rewrite -prev_job_index // EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 775)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
IND : 0 < job_index arr_seq j1
PREV_ARR_LTE : job_arrival (prev_job arr_seq j1) <= job_arrival j1
EQ : prev_job arr_seq j1 = j1
SM_IND : job_index arr_seq j1 - 1 = job_index arr_seq j1
============================
False
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We show that task arrivals at [job_arrival j1] is the
same as task arrivals that arrive between [job_arrival j1]
and [job_arrival j1 + 1].
Lemma task_arrivals_at_as_task_arrivals_between:
task_arrivals_at_job_arrival arr_seq j1 = task_arrivals_between arr_seq tsk (job_arrival j1) (job_arrival j1).+1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 436)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
task_arrivals_at_job_arrival arr_seq j1 =
task_arrivals_between arr_seq tsk (job_arrival j1) (succn (job_arrival j1))
----------------------------------------------------------------------------- *)
Proof.
rewrite /task_arrivals_at_job_arrival /task_arrivals_at /task_arrivals_between /arrivals_between.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 462)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
[seq j <- arrivals_at arr_seq (job_arrival j1) | job_task j == job_task j1] =
[seq j <- \cat_(job_arrival j1<=t<succn (job_arrival j1)|true)
arrivals_at arr_seq t
| job_task j == tsk]
----------------------------------------------------------------------------- *)
now rewrite big_nat1 H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
task_arrivals_at_job_arrival arr_seq j1 = task_arrivals_between arr_seq tsk (job_arrival j1) (job_arrival j1).+1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 436)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
task_arrivals_at_job_arrival arr_seq j1 =
task_arrivals_between arr_seq tsk (job_arrival j1) (succn (job_arrival j1))
----------------------------------------------------------------------------- *)
Proof.
rewrite /task_arrivals_at_job_arrival /task_arrivals_at /task_arrivals_between /arrivals_between.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 462)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
[seq j <- arrivals_at arr_seq (job_arrival j1) | job_task j == job_task j1] =
[seq j <- \cat_(job_arrival j1<=t<succn (job_arrival j1)|true)
arrivals_at arr_seq t
| job_task j == tsk]
----------------------------------------------------------------------------- *)
now rewrite big_nat1 H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We show that the task arrivals up to the previous job [j1] concatenated with
the sequence [::j1] (the sequence containing only the job [j1]) is same as
task arrivals up to [job_arrival j1].
Lemma prev_job_cat:
job_index arr_seq j1 > 0 →
task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++ [::j1] = task_arrivals_up_to_job_arrival arr_seq j1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 458)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
0 < job_index arr_seq j1 ->
task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++ [:: j1] =
task_arrivals_up_to_job_arrival arr_seq j1
----------------------------------------------------------------------------- *)
Proof.
intros JIND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 459)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
JIND : 0 < job_index arr_seq j1
============================
task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++ [:: j1] =
task_arrivals_up_to_job_arrival arr_seq j1
----------------------------------------------------------------------------- *)
rewrite -only_j_in_task_arrivals_at_j task_arrivals_at_as_task_arrivals_between.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 463)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
JIND : 0 < job_index arr_seq j1
============================
task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++
task_arrivals_between arr_seq tsk (job_arrival j1) (succn (job_arrival j1)) =
task_arrivals_up_to_job_arrival arr_seq j1
----------------------------------------------------------------------------- *)
rewrite /task_arrivals_up_to_job_arrival prev_job_task ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 487)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
JIND : 0 < job_index arr_seq j1
============================
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq tsk (job_arrival j1) (succn (job_arrival j1)) =
task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)
----------------------------------------------------------------------------- *)
rewrite [in X in _ = X] (task_arrivals_cat _ _ (job_arrival (prev_job arr_seq j1))); last by
apply ltnW; apply prev_job_arr_lt.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 550)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
JIND : 0 < job_index arr_seq j1
============================
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq tsk (job_arrival j1) (succn (job_arrival j1)) =
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq (job_task j1)
(succn (job_arrival (prev_job arr_seq j1))) (succn (job_arrival j1))
----------------------------------------------------------------------------- *)
rewrite [in X in _ = _ ++ X] (task_arrivals_between_cat _ _ _ (job_arrival j1) _) ⇒ //; last by apply prev_job_arr_lt.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 597)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
JIND : 0 < job_index arr_seq j1
============================
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq tsk (job_arrival j1) (succn (job_arrival j1)) =
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq (job_task j1)
(succn (job_arrival (prev_job arr_seq j1))) (job_arrival j1) ++
task_arrivals_between arr_seq (job_task j1) (job_arrival j1)
(succn (job_arrival j1))
----------------------------------------------------------------------------- *)
rewrite no_jobs_between_consecutive_jobs ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 660)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
JIND : 0 < job_index arr_seq j1
============================
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq tsk (job_arrival j1) (succn (job_arrival j1)) =
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
[::] ++
task_arrivals_between arr_seq (job_task j1) (job_arrival j1)
(succn (job_arrival j1))
----------------------------------------------------------------------------- *)
now rewrite cat0s H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End SporadicArrivals.
job_index arr_seq j1 > 0 →
task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++ [::j1] = task_arrivals_up_to_job_arrival arr_seq j1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 458)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
============================
0 < job_index arr_seq j1 ->
task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++ [:: j1] =
task_arrivals_up_to_job_arrival arr_seq j1
----------------------------------------------------------------------------- *)
Proof.
intros JIND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 459)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
JIND : 0 < job_index arr_seq j1
============================
task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++ [:: j1] =
task_arrivals_up_to_job_arrival arr_seq j1
----------------------------------------------------------------------------- *)
rewrite -only_j_in_task_arrivals_at_j task_arrivals_at_as_task_arrivals_between.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 463)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
JIND : 0 < job_index arr_seq j1
============================
task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++
task_arrivals_between arr_seq tsk (job_arrival j1) (succn (job_arrival j1)) =
task_arrivals_up_to_job_arrival arr_seq j1
----------------------------------------------------------------------------- *)
rewrite /task_arrivals_up_to_job_arrival prev_job_task ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 487)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
JIND : 0 < job_index arr_seq j1
============================
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq tsk (job_arrival j1) (succn (job_arrival j1)) =
task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)
----------------------------------------------------------------------------- *)
rewrite [in X in _ = X] (task_arrivals_cat _ _ (job_arrival (prev_job arr_seq j1))); last by
apply ltnW; apply prev_job_arr_lt.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 550)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
JIND : 0 < job_index arr_seq j1
============================
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq tsk (job_arrival j1) (succn (job_arrival j1)) =
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq (job_task j1)
(succn (job_arrival (prev_job arr_seq j1))) (succn (job_arrival j1))
----------------------------------------------------------------------------- *)
rewrite [in X in _ = _ ++ X] (task_arrivals_between_cat _ _ _ (job_arrival j1) _) ⇒ //; last by apply prev_job_arr_lt.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 597)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
JIND : 0 < job_index arr_seq j1
============================
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq tsk (job_arrival j1) (succn (job_arrival j1)) =
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq (job_task j1)
(succn (job_arrival (prev_job arr_seq j1))) (job_arrival j1) ++
task_arrivals_between arr_seq (job_task j1) (job_arrival j1)
(succn (job_arrival j1))
----------------------------------------------------------------------------- *)
rewrite no_jobs_between_consecutive_jobs ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 660)
Task : TaskType
H : TaskOffset Task
H0 : SporadicModel Task
H1 : TaskMaxInterArrival Task
Job : JobType
H2 : JobTask Job Task
H3 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_sporadic_model : respects_sporadic_task_model arr_seq tsk
H_valid_inter_min_arrival : valid_task_min_inter_arrival_time tsk
H_valid_offset : valid_offset arr_seq tsk
j1, j2 : Job
H_j1_from_arrival_sequence : arrives_in arr_seq j1
H_j2_from_arrival_sequence : arrives_in arr_seq j2
H_j1_task : job_task j1 = tsk
H_j2_task : job_task j2 = tsk
JIND : 0 < job_index arr_seq j1
============================
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
task_arrivals_between arr_seq tsk (job_arrival j1) (succn (job_arrival j1)) =
task_arrivals_up_to arr_seq (job_task j1)
(job_arrival (prev_job arr_seq j1)) ++
[::] ++
task_arrivals_between arr_seq (job_task j1) (job_arrival j1)
(succn (job_arrival j1))
----------------------------------------------------------------------------- *)
now rewrite cat0s H_j1_task.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End SporadicArrivals.