Library prosa.analysis.facts.preemption.task.limited
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.preemption.job.limited.
Furthermore, we assume the task model with fixed preemption points.
Require Import prosa.model.task.preemption.limited_preemptive.
Require Import prosa.model.preemption.limited_preemptive.
Require Import prosa.model.preemption.limited_preemptive.
Platform for Models with Limited Preemptions
In this section, we prove that instantiation of functions [job_preemptable and task_preemption_points] to the limited preemptions model indeed defines a valid preemption model with bounded non-preemptive regions.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
In addition, we assume the existence of functions mapping a
job and task to the sequence of its preemption points.
Consider any arrival sequence.
Next, consider any ideal uni-processor preemption-aware schedule
of this arrival sequence ...
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_schedule_respects_preemption_model:
schedule_respects_preemption_model arr_seq sched.
Hypothesis H_schedule_respects_preemption_model:
schedule_respects_preemption_model arr_seq sched.
... where jobs do not execute before their arrival or after completion.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Consider an arbitrary task set ts.
Next, we assume that preemption points are defined by the model
with fixed preemption points.
Then we prove that functions [job_preemptable and
task_preemption_points] define a model with bounded non-preemptive
regions.
Lemma fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq .
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 46)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
Proof.
intros j ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 49)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
move: H_valid_fixed_preemption_points_model ⇒ [LIM FIX].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
move: (LIM) ⇒ [BEG [END NDEC]]; move: (FIX) ⇒ [A1 [A2 [A3 [A4 A5]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 125)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 148)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO : job_cost j = 0
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
subgoal 2 (ID 149) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 151)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO : job_cost j = 0
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 152) is:
nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 149) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
rewrite /job_respects_max_nonpreemptive_segment /job_max_nonpreemptive_segment
/lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 199)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO : job_cost j = 0
============================
max0 (distances (if job_preemptable j 0 then [:: 0] else [::])) <=
task_max_nonpreemptive_segment (job_task j)
subgoal 2 (ID 152) is:
nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 149) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 152)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO : job_cost j = 0
============================
nonpreemptive_regions_have_bounded_length j
subgoal 2 (ID 149) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
+ move ⇒ progr; rewrite ZERO leqn0; move ⇒ /andP [_ /eqP LE].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 484)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO : job_cost j = 0
progr : duration
LE : progr = 0
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 2 (ID 149) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
∃ 0; rewrite LE; split; first by apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 491)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO : job_cost j = 0
progr : duration
LE : progr = 0
============================
job_preemptable j 0
subgoal 2 (ID 149) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
by eapply zero_in_preemption_points; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 149)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- split; last (move ⇒ progr /andP [_ LE]; destruct (progr \in job_preemption_points j) eqn:NotIN).
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 526)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 584) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 3 (ID 585) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
+ rewrite /job_respects_max_nonpreemptive_segment
/job_max_nonpreemptive_segment /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 617)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
============================
max0 (distances (job_preemption_points j)) <=
task_max_nonpreemptive_segment (job_task j)
subgoal 2 (ID 584) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 3 (ID 585) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
by apply max_of_dominating_seq; intros; apply A5.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 584)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : (progr \in job_preemption_points j) = true
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 2 (ID 585) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
+ ∃ progr; split; first apply/andP; first split; rewrite ?leq_addr; by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 585)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : (progr \in job_preemption_points j) = false
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
+ move: NotIN ⇒ /eqP; rewrite eqbF_neg; move ⇒ NotIN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2591)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
edestruct (work_belongs_to_some_nonpreemptive_segment arr_seq) as [x [SIZE2 N]]; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2616)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N : nth 0 (job_preemption_points j) x < progr <
nth 0 (job_preemption_points j) x.+1
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
move: N ⇒ /andP [N1 N2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2675)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
set ptl := nth 0 (job_preemption_points j) x.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2680)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
set ptr := nth 0 (job_preemption_points j) x.+1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2685)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
∃ ptr; split; first last.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2690)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
job_preemptable j ptr
subgoal 2 (ID 2689) is:
progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
× by unfold job_preemptable, limited_preemptions_model; apply mem_nth.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2689)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
× apply/andP; split; first by apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2719)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
apply leq_trans with (ptl + (job_max_nonpreemptive_segment j - ε) + 1); first last.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2726)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptl + (job_max_nonpreemptive_segment j - ε) + 1 <=
progr + (job_max_nonpreemptive_segment j - ε)
subgoal 2 (ID 2725) is:
ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1
----------------------------------------------------------------------------- *)
-- rewrite addn1 ltn_add2r; apply N1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2725)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1
----------------------------------------------------------------------------- *)
-- unfold job_max_nonpreemptive_segment.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2735)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr <= ptl + (max0 (lengths_of_segments j) - ε) + 1
----------------------------------------------------------------------------- *)
rewrite -addnA -leq_subLR -(leq_add2r 1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2751)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr - ptl + 1 <= max0 (lengths_of_segments j) - ε + 1 + 1
----------------------------------------------------------------------------- *)
rewrite [in X in _ ≤ X]addnC -leq_subLR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2767)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr - ptl + 1 - 1 <= max0 (lengths_of_segments j) - ε + 1
----------------------------------------------------------------------------- *)
rewrite !subn1 !addn1 prednK.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2785)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
(ptr - ptl).+1.-1 <= max0 (lengths_of_segments j)
subgoal 2 (ID 2786) is:
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2785)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
(ptr - ptl).+1.-1 <= max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
rewrite -[_.+1.-1]pred_Sn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2790)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr - ptl <= max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
rewrite /lengths_of_segments.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2797)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr - ptl <= max0 (distances (parameter.job_preemption_points j))
----------------------------------------------------------------------------- *)
erewrite job_parameters_max_np_to_job_limited; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2802)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr - ptl <= max0 (distances (job_preemption_points j))
----------------------------------------------------------------------------- *)
by apply distance_between_neighboring_elements_le_max_distance_in_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 2786) is:
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2786)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2786)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
rewrite /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 4875)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
0 < max0 (distances (job_preemption_points j))
----------------------------------------------------------------------------- *)
apply max_distance_in_nontrivial_seq_is_positive; first by eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 9210)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
exists x0 y : nat_eqType,
x0 \in job_preemption_points j /\
y \in job_preemption_points j /\ x0 <> y
----------------------------------------------------------------------------- *)
∃ 0, (job_cost j); repeat split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 9219)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
0 \in job_preemption_points j
subgoal 2 (ID 9223) is:
job_cost j \in job_preemption_points j
subgoal 3 (ID 9224) is:
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by eapply zero_in_preemption_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 9223)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
job_cost j \in job_preemption_points j
subgoal 2 (ID 9224) is:
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by eapply job_cost_in_nonpreemptive_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 9224)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by apply/eqP; rewrite eq_sym -lt0n; apply POS.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
model_with_bounded_nonpreemptive_segments arr_seq .
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 46)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
Proof.
intros j ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 49)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
move: H_valid_fixed_preemption_points_model ⇒ [LIM FIX].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
move: (LIM) ⇒ [BEG [END NDEC]]; move: (FIX) ⇒ [A1 [A2 [A3 [A4 A5]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 125)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 148)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO : job_cost j = 0
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
subgoal 2 (ID 149) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 151)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO : job_cost j = 0
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 152) is:
nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 149) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
rewrite /job_respects_max_nonpreemptive_segment /job_max_nonpreemptive_segment
/lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 199)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO : job_cost j = 0
============================
max0 (distances (if job_preemptable j 0 then [:: 0] else [::])) <=
task_max_nonpreemptive_segment (job_task j)
subgoal 2 (ID 152) is:
nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 149) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 152)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO : job_cost j = 0
============================
nonpreemptive_regions_have_bounded_length j
subgoal 2 (ID 149) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
+ move ⇒ progr; rewrite ZERO leqn0; move ⇒ /andP [_ /eqP LE].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 484)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO : job_cost j = 0
progr : duration
LE : progr = 0
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 2 (ID 149) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
∃ 0; rewrite LE; split; first by apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 491)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
ZERO : job_cost j = 0
progr : duration
LE : progr = 0
============================
job_preemptable j 0
subgoal 2 (ID 149) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
by eapply zero_in_preemption_points; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 149)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- split; last (move ⇒ progr /andP [_ LE]; destruct (progr \in job_preemption_points j) eqn:NotIN).
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 526)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 584) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 3 (ID 585) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
+ rewrite /job_respects_max_nonpreemptive_segment
/job_max_nonpreemptive_segment /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 617)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
============================
max0 (distances (job_preemption_points j)) <=
task_max_nonpreemptive_segment (job_task j)
subgoal 2 (ID 584) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 3 (ID 585) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
by apply max_of_dominating_seq; intros; apply A5.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 584)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : (progr \in job_preemption_points j) = true
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 2 (ID 585) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
+ ∃ progr; split; first apply/andP; first split; rewrite ?leq_addr; by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 585)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : (progr \in job_preemption_points j) = false
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
+ move: NotIN ⇒ /eqP; rewrite eqbF_neg; move ⇒ NotIN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2591)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
edestruct (work_belongs_to_some_nonpreemptive_segment arr_seq) as [x [SIZE2 N]]; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2616)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N : nth 0 (job_preemption_points j) x < progr <
nth 0 (job_preemption_points j) x.+1
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
move: N ⇒ /andP [N1 N2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2675)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
set ptl := nth 0 (job_preemption_points j) x.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2680)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
set ptr := nth 0 (job_preemption_points j) x.+1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2685)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
∃ ptr; split; first last.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2690)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
job_preemptable j ptr
subgoal 2 (ID 2689) is:
progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
× by unfold job_preemptable, limited_preemptions_model; apply mem_nth.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2689)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
× apply/andP; split; first by apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2719)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
apply leq_trans with (ptl + (job_max_nonpreemptive_segment j - ε) + 1); first last.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2726)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptl + (job_max_nonpreemptive_segment j - ε) + 1 <=
progr + (job_max_nonpreemptive_segment j - ε)
subgoal 2 (ID 2725) is:
ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1
----------------------------------------------------------------------------- *)
-- rewrite addn1 ltn_add2r; apply N1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2725)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1
----------------------------------------------------------------------------- *)
-- unfold job_max_nonpreemptive_segment.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2735)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr <= ptl + (max0 (lengths_of_segments j) - ε) + 1
----------------------------------------------------------------------------- *)
rewrite -addnA -leq_subLR -(leq_add2r 1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2751)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr - ptl + 1 <= max0 (lengths_of_segments j) - ε + 1 + 1
----------------------------------------------------------------------------- *)
rewrite [in X in _ ≤ X]addnC -leq_subLR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2767)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr - ptl + 1 - 1 <= max0 (lengths_of_segments j) - ε + 1
----------------------------------------------------------------------------- *)
rewrite !subn1 !addn1 prednK.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2785)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
(ptr - ptl).+1.-1 <= max0 (lengths_of_segments j)
subgoal 2 (ID 2786) is:
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2785)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
(ptr - ptl).+1.-1 <= max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
rewrite -[_.+1.-1]pred_Sn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2790)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr - ptl <= max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
rewrite /lengths_of_segments.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2797)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr - ptl <= max0 (distances (parameter.job_preemption_points j))
----------------------------------------------------------------------------- *)
erewrite job_parameters_max_np_to_job_limited; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2802)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
ptr - ptl <= max0 (distances (job_preemption_points j))
----------------------------------------------------------------------------- *)
by apply distance_between_neighboring_elements_le_max_distance_in_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 2786) is:
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2786)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2786)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
rewrite /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 4875)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
0 < max0 (distances (job_preemption_points j))
----------------------------------------------------------------------------- *)
apply max_distance_in_nontrivial_seq_is_positive; first by eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 9210)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
exists x0 y : nat_eqType,
x0 \in job_preemption_points j /\
y \in job_preemption_points j /\ x0 <> y
----------------------------------------------------------------------------- *)
∃ 0, (job_cost j); repeat split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 9219)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
0 \in job_preemption_points j
subgoal 2 (ID 9223) is:
job_cost j \in job_preemption_points j
subgoal 3 (ID 9224) is:
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by eapply zero_in_preemption_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 9223)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
job_cost j \in job_preemption_points j
subgoal 2 (ID 9224) is:
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by eapply job_cost_in_nonpreemptive_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 9224)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
FIX : valid_fixed_preemption_points_task_model arr_seq ts
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
A1 : task_beginning_of_execution_in_preemption_points ts
A2 : task_end_of_execution_in_preemption_points ts
A3 : nondecreasing_task_preemption_points ts
A4 : consistent_job_segment_count arr_seq
A5 : job_respects_segment_lengths arr_seq /\ task_segments_are_nonempty ts
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : x.+1 < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) x.+1
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) x.+1 : nat
============================
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by apply/eqP; rewrite eq_sym -lt0n; apply POS.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Which together with lemma [valid_fixed_preemption_points_model]
gives us the fact that functions [job_preemptable and
task_preemption_points] defines a valid preemption model with
bounded non-preemptive regions.
Corollary fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions:
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 57)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
============================
valid_model_with_bounded_nonpreemptive_segments arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 59)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
============================
valid_preemption_model arr_seq sched
subgoal 2 (ID 60) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- by apply valid_fixed_preemption_points_model_lemma; destruct H_valid_fixed_preemption_points_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 60)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- by apply fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End LimitedPreemptionsModel.
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 57)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
============================
valid_model_with_bounded_nonpreemptive_segments arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 59)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
============================
valid_preemption_model arr_seq sched
subgoal 2 (ID 60) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- by apply valid_fixed_preemption_points_model_lemma; destruct H_valid_fixed_preemption_points_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 60)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
H4 : TaskPreemptionPoints Task
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- by apply fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End LimitedPreemptionsModel.
We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically.
Global Hint Resolve
valid_fixed_preemption_points_model_lemma
fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.
valid_fixed_preemption_points_model_lemma
fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.