Library prosa.analysis.facts.preemption.job.limited
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.schedule.limited_preemptive.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.analysis.facts.model.ideal_schedule.
Throughout this file, we assume the job model with limited
preemption points.
Platform for Models with Limited Preemptions
In this section, we prove that instantiation of predicate [job_preemptable] to the model with limited preemptions indeed defines a valid preemption model.
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, assume the existence of a function that maps a job
to the sequence of its preemption points.
Consider any arrival sequence.
Next, consider any limited ideal uni-processor 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 after their completion.
Next, we assume that preemption points are defined by the
job-level model with limited preemptions.
First, we prove a few auxiliary lemmas.
Consider a job j.
Recall that 0 is a preemption point.
Remark zero_in_preemption_points: 0 \in job_preemption_points j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1543)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
0 \in job_preemption_points j
----------------------------------------------------------------------------- *)
Proof. by apply H_valid_limited_preemptions_job_model.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1543)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
0 \in job_preemption_points j
----------------------------------------------------------------------------- *)
Proof. by apply H_valid_limited_preemptions_job_model.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Using the fact that [job_preemption_points] is a
non-decreasing sequence, we prove that the first element of
[job_preemption_points] is 0.
Lemma zero_is_first_element: first0 (job_preemption_points j) = 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1548)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
first0 (job_preemption_points j) = 0
----------------------------------------------------------------------------- *)
Proof.
have F := zero_in_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1553)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
F : 0 \in job_preemption_points j
============================
first0 (job_preemption_points j) = 0
----------------------------------------------------------------------------- *)
destruct H_valid_limited_preemptions_job_model as [_ [_ C]]; specialize (C j H_j_arrives).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1567)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
F : 0 \in job_preemption_points j
C : nondecreasing_sequence (job_preemption_points j)
============================
first0 (job_preemption_points j) = 0
----------------------------------------------------------------------------- *)
by apply nondec_seq_zero_first.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1548)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
first0 (job_preemption_points j) = 0
----------------------------------------------------------------------------- *)
Proof.
have F := zero_in_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1553)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
F : 0 \in job_preemption_points j
============================
first0 (job_preemption_points j) = 0
----------------------------------------------------------------------------- *)
destruct H_valid_limited_preemptions_job_model as [_ [_ C]]; specialize (C j H_j_arrives).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1567)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
F : 0 \in job_preemption_points j
C : nondecreasing_sequence (job_preemption_points j)
============================
first0 (job_preemption_points j) = 0
----------------------------------------------------------------------------- *)
by apply nondec_seq_zero_first.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We prove that the list of preemption points is not empty.
Lemma list_of_preemption_point_is_not_empty:
0 < size (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1552)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
0 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
Proof.
move: H_valid_limited_preemptions_job_model ⇒ [BEG [END _]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1575)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
0 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; rewrite size_eq0 in CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1706)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
CONTR : job_preemption_points j == [::]
============================
False
----------------------------------------------------------------------------- *)
specialize (BEG j H_j_arrives).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1708)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : 0 \in job_preemption_points j
END : end_of_execution_in_preemption_points arr_seq
CONTR : job_preemption_points j == [::]
============================
False
----------------------------------------------------------------------------- *)
by rewrite /beginning_of_execution_in_preemption_points (eqbool_to_eqprop CONTR) in BEG.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
0 < size (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1552)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
0 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
Proof.
move: H_valid_limited_preemptions_job_model ⇒ [BEG [END _]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1575)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
0 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; rewrite size_eq0 in CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1706)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
CONTR : job_preemption_points j == [::]
============================
False
----------------------------------------------------------------------------- *)
specialize (BEG j H_j_arrives).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1708)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : 0 \in job_preemption_points j
END : end_of_execution_in_preemption_points arr_seq
CONTR : job_preemption_points j == [::]
============================
False
----------------------------------------------------------------------------- *)
by rewrite /beginning_of_execution_in_preemption_points (eqbool_to_eqprop CONTR) in BEG.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Next, we prove that the cost of a job is a preemption point.
Lemma job_cost_in_nonpreemptive_points: job_cost j \in job_preemption_points j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1561)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost j \in job_preemption_points j
----------------------------------------------------------------------------- *)
Proof.
move: H_valid_limited_preemptions_job_model ⇒ [BEG [END _]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1584)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
job_cost j \in job_preemption_points j
----------------------------------------------------------------------------- *)
move: (END _ H_j_arrives) ⇒ EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1588)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
EQ : last0 (job_preemption_points j) = job_cost j
============================
job_cost j \in job_preemption_points j
----------------------------------------------------------------------------- *)
rewrite -EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1591)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
last0 (job_preemption_points j) \in job_preemption_points j
----------------------------------------------------------------------------- *)
rewrite /last0 -nth_last.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1597)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
nth 0 (job_preemption_points j) (predn (size (job_preemption_points j)))
\in job_preemption_points j
----------------------------------------------------------------------------- *)
apply/(nthP 0).
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 1625)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
exists2 i : nat,
i < size (job_preemption_points j) &
nth 0 (job_preemption_points j) i =
nth 0 (job_preemption_points j) (predn (size (job_preemption_points j)))
----------------------------------------------------------------------------- *)
∃ ((size (job_preemption_points j)).-1); last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1630)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
predn (size (job_preemption_points j)) < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
rewrite -(leq_add2r 1) !addn1 prednK //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1647)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
0 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
by apply list_of_preemption_point_is_not_empty.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1561)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost j \in job_preemption_points j
----------------------------------------------------------------------------- *)
Proof.
move: H_valid_limited_preemptions_job_model ⇒ [BEG [END _]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1584)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
job_cost j \in job_preemption_points j
----------------------------------------------------------------------------- *)
move: (END _ H_j_arrives) ⇒ EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1588)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
EQ : last0 (job_preemption_points j) = job_cost j
============================
job_cost j \in job_preemption_points j
----------------------------------------------------------------------------- *)
rewrite -EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1591)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
last0 (job_preemption_points j) \in job_preemption_points j
----------------------------------------------------------------------------- *)
rewrite /last0 -nth_last.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1597)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
nth 0 (job_preemption_points j) (predn (size (job_preemption_points j)))
\in job_preemption_points j
----------------------------------------------------------------------------- *)
apply/(nthP 0).
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 1625)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
exists2 i : nat,
i < size (job_preemption_points j) &
nth 0 (job_preemption_points j) i =
nth 0 (job_preemption_points j) (predn (size (job_preemption_points j)))
----------------------------------------------------------------------------- *)
∃ ((size (job_preemption_points j)).-1); last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1630)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
predn (size (job_preemption_points j)) < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
rewrite -(leq_add2r 1) !addn1 prednK //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1647)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
0 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
by apply list_of_preemption_point_is_not_empty.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
As a corollary, we prove that the sequence of non-preemptive
points of a job with positive cost contains at least 2
points.
Corollary number_of_preemption_points_at_least_two:
job_cost_positive j →
2 ≤ size (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1567)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost_positive j -> 1 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
Proof.
intros POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1568)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
============================
1 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
move: H_valid_limited_preemptions_job_model ⇒ [BEG [END _]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1591)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
1 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
have EQ: 2 = size [::0; job_cost j]; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1602)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
EQ : 2 = size [:: 0; job_cost j]
============================
1 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
rewrite EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1605)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
size [:: 0; job_cost j] <= size (job_preemption_points j)
----------------------------------------------------------------------------- *)
apply subseq_leq_size.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1607)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
uniq [:: 0; job_cost j]
subgoal 2 (ID 1608) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
rewrite !cons_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1618)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
[&& 0 \notin [:: job_cost j], job_cost j \notin [::] & uniq [::]]
subgoal 2 (ID 1608) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1618)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
[&& 0 \notin [:: job_cost j], job_cost j \notin [::] & uniq [::]]
----------------------------------------------------------------------------- *)
apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1647)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
0 \notin [:: job_cost j]
subgoal 2 (ID 1648) is:
(job_cost j \notin [::]) && uniq [::]
----------------------------------------------------------------------------- *)
rewrite in_cons negb_or; apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1684)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
0 != job_cost j
subgoal 2 (ID 1648) is:
(job_cost j \notin [::]) && uniq [::]
----------------------------------------------------------------------------- *)
rewrite neq_ltn; apply/orP; left; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1648)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
(job_cost j \notin [::]) && uniq [::]
----------------------------------------------------------------------------- *)
apply/andP; split; by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1608)
subgoal 1 (ID 1608) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1608)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
intros t EQ; move: EQ; rewrite !in_cons.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1763)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
t : nat_eqType
============================
[|| t == 0, t == job_cost j | t \in [::]] -> t \in job_preemption_points j
----------------------------------------------------------------------------- *)
move ⇒ /orP [/eqP EQ| /orP [/eqP EQ|EQ]]; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1915)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
t : nat_eqType
EQ : t = 0
============================
t \in job_preemption_points j
subgoal 2 (ID 1916) is:
t \in job_preemption_points j
----------------------------------------------------------------------------- *)
- by rewrite EQ; apply zero_in_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1916)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
t : nat_eqType
EQ : t = job_cost j
============================
t \in job_preemption_points j
----------------------------------------------------------------------------- *)
- by rewrite EQ; apply job_cost_in_nonpreemptive_points.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_cost_positive j →
2 ≤ size (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1567)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost_positive j -> 1 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
Proof.
intros POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1568)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
============================
1 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
move: H_valid_limited_preemptions_job_model ⇒ [BEG [END _]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1591)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
1 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
have EQ: 2 = size [::0; job_cost j]; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1602)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
EQ : 2 = size [:: 0; job_cost j]
============================
1 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
rewrite EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1605)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
size [:: 0; job_cost j] <= size (job_preemption_points j)
----------------------------------------------------------------------------- *)
apply subseq_leq_size.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1607)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
uniq [:: 0; job_cost j]
subgoal 2 (ID 1608) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
rewrite !cons_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1618)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
[&& 0 \notin [:: job_cost j], job_cost j \notin [::] & uniq [::]]
subgoal 2 (ID 1608) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1618)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
[&& 0 \notin [:: job_cost j], job_cost j \notin [::] & uniq [::]]
----------------------------------------------------------------------------- *)
apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1647)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
0 \notin [:: job_cost j]
subgoal 2 (ID 1648) is:
(job_cost j \notin [::]) && uniq [::]
----------------------------------------------------------------------------- *)
rewrite in_cons negb_or; apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1684)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
0 != job_cost j
subgoal 2 (ID 1648) is:
(job_cost j \notin [::]) && uniq [::]
----------------------------------------------------------------------------- *)
rewrite neq_ltn; apply/orP; left; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1648)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
(job_cost j \notin [::]) && uniq [::]
----------------------------------------------------------------------------- *)
apply/andP; split; by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1608)
subgoal 1 (ID 1608) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1608)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
intros t EQ; move: EQ; rewrite !in_cons.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1763)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
t : nat_eqType
============================
[|| t == 0, t == job_cost j | t \in [::]] -> t \in job_preemption_points j
----------------------------------------------------------------------------- *)
move ⇒ /orP [/eqP EQ| /orP [/eqP EQ|EQ]]; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1915)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
t : nat_eqType
EQ : t = 0
============================
t \in job_preemption_points j
subgoal 2 (ID 1916) is:
t \in job_preemption_points j
----------------------------------------------------------------------------- *)
- by rewrite EQ; apply zero_in_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1916)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
POS : job_cost_positive j
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
t : nat_eqType
EQ : t = job_cost j
============================
t \in job_preemption_points j
----------------------------------------------------------------------------- *)
- by rewrite EQ; apply job_cost_in_nonpreemptive_points.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Next we prove that "anti-density" property (from
[preemption.util] file) holds for [job_preemption_point j].
Lemma antidensity_of_preemption_points:
∀ (ρ : work),
ρ ≤ job_cost j →
~~ (ρ \in job_preemption_points j) →
first0 (job_preemption_points j) ≤ ρ < last0 (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1580)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
forall ρ : work,
ρ <= job_cost j ->
ρ \notin job_preemption_points j ->
first0 (job_preemption_points j) <= ρ < last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
Proof.
intros ρ LE NotIN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1583)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
============================
first0 (job_preemption_points j) <= ρ < last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
move: H_valid_limited_preemptions_job_model ⇒ [BEG [END NDEC]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1605)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
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
============================
first0 (job_preemption_points j) <= ρ < last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1631)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
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
============================
first0 (job_preemption_points j) <= ρ
subgoal 2 (ID 1632) is:
ρ < last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
- by rewrite zero_is_first_element.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1632)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
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
============================
ρ < last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
- rewrite END; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1640)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
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
============================
ρ < job_cost j
----------------------------------------------------------------------------- *)
rewrite ltn_neqAle; apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1671)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
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
============================
ρ != job_cost j
----------------------------------------------------------------------------- *)
apply/negP; intros CONTR; move: CONTR ⇒ /eqP CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1730)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
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
CONTR : ρ = job_cost j
============================
False
----------------------------------------------------------------------------- *)
rewrite CONTR in NotIN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1760)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
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
CONTR : ρ = job_cost j
NotIN : job_cost j \notin job_preemption_points j
============================
False
----------------------------------------------------------------------------- *)
move: NotIN ⇒ /negP NIN; apply: NIN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1794)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
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
CONTR : ρ = job_cost j
============================
job_cost j \in job_preemption_points j
----------------------------------------------------------------------------- *)
by apply job_cost_in_nonpreemptive_points.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ (ρ : work),
ρ ≤ job_cost j →
~~ (ρ \in job_preemption_points j) →
first0 (job_preemption_points j) ≤ ρ < last0 (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1580)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
forall ρ : work,
ρ <= job_cost j ->
ρ \notin job_preemption_points j ->
first0 (job_preemption_points j) <= ρ < last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
Proof.
intros ρ LE NotIN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1583)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
============================
first0 (job_preemption_points j) <= ρ < last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
move: H_valid_limited_preemptions_job_model ⇒ [BEG [END NDEC]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1605)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
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
============================
first0 (job_preemption_points j) <= ρ < last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1631)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
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
============================
first0 (job_preemption_points j) <= ρ
subgoal 2 (ID 1632) is:
ρ < last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
- by rewrite zero_is_first_element.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1632)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
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
============================
ρ < last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
- rewrite END; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1640)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
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
============================
ρ < job_cost j
----------------------------------------------------------------------------- *)
rewrite ltn_neqAle; apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1671)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
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
============================
ρ != job_cost j
----------------------------------------------------------------------------- *)
apply/negP; intros CONTR; move: CONTR ⇒ /eqP CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1730)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
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
CONTR : ρ = job_cost j
============================
False
----------------------------------------------------------------------------- *)
rewrite CONTR in NotIN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1760)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
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
CONTR : ρ = job_cost j
NotIN : job_cost j \notin job_preemption_points j
============================
False
----------------------------------------------------------------------------- *)
move: NotIN ⇒ /negP NIN; apply: NIN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1794)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
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
CONTR : ρ = job_cost j
============================
job_cost j \in job_preemption_points j
----------------------------------------------------------------------------- *)
by apply job_cost_in_nonpreemptive_points.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We also prove that any work that doesn't belong to
preemption points of job j is placed strictly between two
neighboring preemption points.
Lemma work_belongs_to_some_nonpreemptive_segment:
∀ (ρ : work),
ρ ≤ job_cost j →
~~ (ρ \in job_preemption_points j)→
∃ n,
n.+1 < size (job_preemption_points j) ∧
nth 0 (job_preemption_points j) n < ρ < nth 0 (job_preemption_points j) n.+1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1600)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
forall ρ : work,
ρ <= job_cost j ->
ρ \notin job_preemption_points j ->
exists n : nat,
succn n < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
----------------------------------------------------------------------------- *)
Proof.
intros ρ LE NotIN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1603)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
============================
exists n : nat,
succn n < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1626)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
ZERO : job_cost j = 0
============================
exists n : nat,
succn n < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
subgoal 2 (ID 1627) is:
exists n : nat,
succn n < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1626)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
ZERO : job_cost j = 0
============================
exists n : nat,
succn n < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
----------------------------------------------------------------------------- *)
exfalso; move: NotIN ⇒ /negP NIN; apply: NIN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1662)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
ZERO : job_cost j = 0
============================
ρ \in job_preemption_points j
----------------------------------------------------------------------------- *)
move: LE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1664)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
ZERO : job_cost j = 0
============================
ρ <= job_cost j -> ρ \in job_preemption_points j
----------------------------------------------------------------------------- *)
rewrite ZERO leqn0; move ⇒ /eqP →.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1706)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
ZERO : job_cost j = 0
============================
0 \in job_preemption_points j
----------------------------------------------------------------------------- *)
by apply zero_in_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1627)
subgoal 1 (ID 1627) is:
exists n : nat,
succn n < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1627)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
POS : 0 < job_cost j
============================
exists n : nat,
succn n < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
----------------------------------------------------------------------------- *)
move: (belonging_to_segment_of_seq_is_total
(job_preemption_points j) ρ (number_of_preemption_points_at_least_two POS)
(antidensity_of_preemption_points _ LE NotIN)) ⇒ [n [SIZE2 /andP [N1 N2]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1771)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) n <= ρ
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
============================
exists n0 : nat,
succn n0 < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n0 < ρ <
nth 0 (job_preemption_points j) (succn n0)
----------------------------------------------------------------------------- *)
∃ n; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1776)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) n <= ρ
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
============================
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
----------------------------------------------------------------------------- *)
apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1802)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) n <= ρ
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
============================
nth 0 (job_preemption_points j) n < ρ
----------------------------------------------------------------------------- *)
move: N1; rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ | G]; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1884)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
EQ : nth 0 (job_preemption_points j) n = ρ
============================
nth 0 (job_preemption_points j) n < ρ
----------------------------------------------------------------------------- *)
exfalso.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1886)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
EQ : nth 0 (job_preemption_points j) n = ρ
============================
False
----------------------------------------------------------------------------- *)
move: NotIN ⇒ /negP CONTR; apply: CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1920)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
EQ : nth 0 (job_preemption_points j) n = ρ
============================
ρ \in job_preemption_points j
----------------------------------------------------------------------------- *)
rewrite -EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1923)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
============================
nth 0 (job_preemption_points j) n \in job_preemption_points j
----------------------------------------------------------------------------- *)
rewrite mem_nth //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1931)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
============================
n < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
by apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ (ρ : work),
ρ ≤ job_cost j →
~~ (ρ \in job_preemption_points j)→
∃ n,
n.+1 < size (job_preemption_points j) ∧
nth 0 (job_preemption_points j) n < ρ < nth 0 (job_preemption_points j) n.+1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1600)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
forall ρ : work,
ρ <= job_cost j ->
ρ \notin job_preemption_points j ->
exists n : nat,
succn n < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
----------------------------------------------------------------------------- *)
Proof.
intros ρ LE NotIN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1603)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
============================
exists n : nat,
succn n < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1626)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
ZERO : job_cost j = 0
============================
exists n : nat,
succn n < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
subgoal 2 (ID 1627) is:
exists n : nat,
succn n < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1626)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
ZERO : job_cost j = 0
============================
exists n : nat,
succn n < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
----------------------------------------------------------------------------- *)
exfalso; move: NotIN ⇒ /negP NIN; apply: NIN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1662)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
ZERO : job_cost j = 0
============================
ρ \in job_preemption_points j
----------------------------------------------------------------------------- *)
move: LE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1664)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
ZERO : job_cost j = 0
============================
ρ <= job_cost j -> ρ \in job_preemption_points j
----------------------------------------------------------------------------- *)
rewrite ZERO leqn0; move ⇒ /eqP →.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1706)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
ZERO : job_cost j = 0
============================
0 \in job_preemption_points j
----------------------------------------------------------------------------- *)
by apply zero_in_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1627)
subgoal 1 (ID 1627) is:
exists n : nat,
succn n < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1627)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
POS : 0 < job_cost j
============================
exists n : nat,
succn n < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
----------------------------------------------------------------------------- *)
move: (belonging_to_segment_of_seq_is_total
(job_preemption_points j) ρ (number_of_preemption_points_at_least_two POS)
(antidensity_of_preemption_points _ LE NotIN)) ⇒ [n [SIZE2 /andP [N1 N2]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1771)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) n <= ρ
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
============================
exists n0 : nat,
succn n0 < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n0 < ρ <
nth 0 (job_preemption_points j) (succn n0)
----------------------------------------------------------------------------- *)
∃ n; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1776)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) n <= ρ
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
============================
nth 0 (job_preemption_points j) n < ρ <
nth 0 (job_preemption_points j) (succn n)
----------------------------------------------------------------------------- *)
apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1802)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) n <= ρ
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
============================
nth 0 (job_preemption_points j) n < ρ
----------------------------------------------------------------------------- *)
move: N1; rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ | G]; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1884)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
EQ : nth 0 (job_preemption_points j) n = ρ
============================
nth 0 (job_preemption_points j) n < ρ
----------------------------------------------------------------------------- *)
exfalso.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1886)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
NotIN : ρ \notin job_preemption_points j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
EQ : nth 0 (job_preemption_points j) n = ρ
============================
False
----------------------------------------------------------------------------- *)
move: NotIN ⇒ /negP CONTR; apply: CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1920)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
EQ : nth 0 (job_preemption_points j) n = ρ
============================
ρ \in job_preemption_points j
----------------------------------------------------------------------------- *)
rewrite -EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1923)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
============================
nth 0 (job_preemption_points j) n \in job_preemption_points j
----------------------------------------------------------------------------- *)
rewrite mem_nth //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1931)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : work
LE : ρ <= job_cost j
POS : 0 < job_cost j
n : nat
SIZE2 : succn n < size (job_preemption_points j)
N2 : ρ < nth 0 (job_preemption_points j) (succn n)
============================
n < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
by apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Recall that file [job.parameters] also defines notion of
preemption points. And note that
[job.parameter.job_preemption_points] cannot have a
duplicating preemption points. Therefore, we need additional
lemmas to relate [job.parameter.job_preemption_points] and
[limited.job_preemption_points]].
First we show that the length of the last non-preemptive
segment of [job.parameter.job_preemption_points] is equal to
the length of the last non-empty non-preemptive segment of
[limited.job_preemption_points].
Lemma job_parameters_last_np_to_job_limited:
last0 (distances (parameter.job_preemption_points j)) =
last0 (filter (fun x ⇒ 0 < x) (distances (job_preemption_points j))).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1611)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
last0 (distances (parameter.job_preemption_points j)) =
last0 [seq x <- distances (job_preemption_points j) | 0 < x]
----------------------------------------------------------------------------- *)
Proof.
destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1621)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
last0 (distances (parameter.job_preemption_points j)) =
last0 [seq x <- distances (job_preemption_points j) | 0 < x]
----------------------------------------------------------------------------- *)
unfold parameter.job_preemption_points, job_preemptable, limited_preemptions_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1623)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
last0
(distances
[seq ρ <- range 0 (job_cost j) | ρ \in job_preemption_points j]) =
last0 [seq x <- distances (job_preemption_points j) | 0 < x]
----------------------------------------------------------------------------- *)
intros; rewrite distances_iota_filtered; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1630)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
forall x : nat, x \in job_preemption_points j -> x <= job_cost j
----------------------------------------------------------------------------- *)
rewrite -A2 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 6695)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
forall x : nat,
x \in job_preemption_points j -> x <= last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
by intros; apply last_is_max_in_nondecreasing_seq; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
last0 (distances (parameter.job_preemption_points j)) =
last0 (filter (fun x ⇒ 0 < x) (distances (job_preemption_points j))).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1611)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
last0 (distances (parameter.job_preemption_points j)) =
last0 [seq x <- distances (job_preemption_points j) | 0 < x]
----------------------------------------------------------------------------- *)
Proof.
destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1621)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
last0 (distances (parameter.job_preemption_points j)) =
last0 [seq x <- distances (job_preemption_points j) | 0 < x]
----------------------------------------------------------------------------- *)
unfold parameter.job_preemption_points, job_preemptable, limited_preemptions_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1623)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
last0
(distances
[seq ρ <- range 0 (job_cost j) | ρ \in job_preemption_points j]) =
last0 [seq x <- distances (job_preemption_points j) | 0 < x]
----------------------------------------------------------------------------- *)
intros; rewrite distances_iota_filtered; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1630)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
forall x : nat, x \in job_preemption_points j -> x <= job_cost j
----------------------------------------------------------------------------- *)
rewrite -A2 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 6695)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
forall x : nat,
x \in job_preemption_points j -> x <= last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
by intros; apply last_is_max_in_nondecreasing_seq; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Next we show that the length of the max non-preemptive
segment of [job.parameter.job_preemption_points] is equal to
the length of the max non-preemptive segment of
[limited.job_preemption_points].
Lemma job_parameters_max_np_to_job_limited:
max0 (distances (parameter.job_preemption_points j)) =
max0 (distances (job_preemption_points j)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1620)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
max0 (distances (parameter.job_preemption_points j)) =
max0 (distances (job_preemption_points j))
----------------------------------------------------------------------------- *)
Proof.
destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1630)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
max0 (distances (parameter.job_preemption_points j)) =
max0 (distances (job_preemption_points j))
----------------------------------------------------------------------------- *)
unfold parameter.job_preemption_points, job_preemptable, limited_preemptions_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1632)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
max0
(distances
[seq ρ <- range 0 (job_cost j) | ρ \in job_preemption_points j]) =
max0 (distances (job_preemption_points j))
----------------------------------------------------------------------------- *)
intros; rewrite distances_iota_filtered; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1638)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
max0 [seq x <- distances (job_preemption_points j) | 0 < x] =
max0 (distances (job_preemption_points j))
subgoal 2 (ID 1639) is:
forall x : nat, x \in job_preemption_points j -> x <= job_cost j
----------------------------------------------------------------------------- *)
rewrite max0_rem0 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1639)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
forall x : nat, x \in job_preemption_points j -> x <= job_cost j
----------------------------------------------------------------------------- *)
rewrite -A2 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1682)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
forall x : nat,
x \in job_preemption_points j -> x <= last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
by intros; apply last_is_max_in_nondecreasing_seq; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End AuxiliaryLemmas.
max0 (distances (parameter.job_preemption_points j)) =
max0 (distances (job_preemption_points j)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1620)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
============================
max0 (distances (parameter.job_preemption_points j)) =
max0 (distances (job_preemption_points j))
----------------------------------------------------------------------------- *)
Proof.
destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1630)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
max0 (distances (parameter.job_preemption_points j)) =
max0 (distances (job_preemption_points j))
----------------------------------------------------------------------------- *)
unfold parameter.job_preemption_points, job_preemptable, limited_preemptions_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1632)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
max0
(distances
[seq ρ <- range 0 (job_cost j) | ρ \in job_preemption_points j]) =
max0 (distances (job_preemption_points j))
----------------------------------------------------------------------------- *)
intros; rewrite distances_iota_filtered; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1638)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
max0 [seq x <- distances (job_preemption_points j) | 0 < x] =
max0 (distances (job_preemption_points j))
subgoal 2 (ID 1639) is:
forall x : nat, x \in job_preemption_points j -> x <= job_cost j
----------------------------------------------------------------------------- *)
rewrite max0_rem0 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1639)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
forall x : nat, x \in job_preemption_points j -> x <= job_cost j
----------------------------------------------------------------------------- *)
rewrite -A2 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1682)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : beginning_of_execution_in_preemption_points arr_seq
A2 : end_of_execution_in_preemption_points arr_seq
A3 : preemption_points_is_nondecreasing_sequence arr_seq
============================
forall x : nat,
x \in job_preemption_points j -> x <= last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
by intros; apply last_is_max_in_nondecreasing_seq; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End AuxiliaryLemmas.
We prove that the [fixed_preemption_point_model] function
defines a valid preemption model.
Lemma valid_fixed_preemption_points_model_lemma:
valid_preemption_model arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1542)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
============================
valid_preemption_model arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
intros j ARR; repeat split.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 1547)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
job_cannot_become_nonpreemptive_before_execution j
subgoal 2 (ID 1551) is:
job_cannot_be_nonpreemptive_after_completion j
subgoal 3 (ID 1555) is:
not_preemptive_implies_scheduled sched j
subgoal 4 (ID 1556) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1547)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
job_cannot_become_nonpreemptive_before_execution j
----------------------------------------------------------------------------- *)
by apply zero_in_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1551)
subgoal 1 (ID 1551) is:
job_cannot_be_nonpreemptive_after_completion j
subgoal 2 (ID 1555) is:
not_preemptive_implies_scheduled sched j
subgoal 3 (ID 1556) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1551)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
job_cannot_be_nonpreemptive_after_completion j
subgoal 2 (ID 1555) is:
not_preemptive_implies_scheduled sched j
subgoal 3 (ID 1556) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1551)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
job_cannot_be_nonpreemptive_after_completion j
----------------------------------------------------------------------------- *)
by apply job_cost_in_nonpreemptive_points.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1555)
subgoal 1 (ID 1555) is:
not_preemptive_implies_scheduled sched j
subgoal 2 (ID 1556) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1555)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
not_preemptive_implies_scheduled sched j
subgoal 2 (ID 1556) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1555)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
not_preemptive_implies_scheduled sched j
----------------------------------------------------------------------------- *)
by move ⇒ t NPP; apply H_schedule_respects_preemption_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1556)
subgoal 1 (ID 1556) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1556)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1556)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
intros t NSCHED SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1574)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
job_preemptable j (service sched j (succn t))
----------------------------------------------------------------------------- *)
have SERV: service sched j t = service sched j t.+1.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1583)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
service sched j t = service sched j (succn t)
subgoal 2 (ID 1585) is:
job_preemptable j (service sched j (succn t))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1583)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
service sched j t = service sched j (succn t)
----------------------------------------------------------------------------- *)
rewrite -[service sched j t]addn0 /service /service_during; apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 1662)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
\sum_(0 <= t0 < t) service_at sched j t0 + 0 ==
\sum_(0 <= t0 < succn t) service_at sched j t0
----------------------------------------------------------------------------- *)
rewrite big_nat_recr //=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1673)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
\sum_(0 <= t0 < t) service_at sched j t0 + 0 ==
\sum_(0 <= i < t) service_at sched j i + service_at sched j t
----------------------------------------------------------------------------- *)
rewrite eqn_add2l eq_sym.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1706)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
service_at sched j t == 0
----------------------------------------------------------------------------- *)
rewrite scheduled_at_def in NSCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1737)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
NSCHED : sched t != Some j
============================
service_at sched j t == 0
----------------------------------------------------------------------------- *)
by rewrite service_at_def eqb0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1585)
subgoal 1 (ID 1585) is:
job_preemptable j (service sched j (succn t))
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1585)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
SERV : service sched j t = service sched j (succn t)
============================
job_preemptable j (service sched j (succn t))
----------------------------------------------------------------------------- *)
rewrite -[job_preemptable _ _]Bool.negb_involutive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1754)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
SERV : service sched j t = service sched j (succn t)
============================
~~ ~~ job_preemptable j (service sched j (succn t))
----------------------------------------------------------------------------- *)
apply/negP; intros CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1776)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
SERV : service sched j t = service sched j (succn t)
CONTR : ~~ job_preemptable j (service sched j (succn t))
============================
False
----------------------------------------------------------------------------- *)
move: NSCHED ⇒ /negP NSCHED; apply: NSCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1810)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
SERV : service sched j t = service sched j (succn t)
CONTR : ~~ job_preemptable j (service sched j (succn t))
============================
scheduled_at sched j t
----------------------------------------------------------------------------- *)
apply H_schedule_respects_preemption_model; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1812)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
SERV : service sched j t = service sched j (succn t)
CONTR : ~~ job_preemptable j (service sched j (succn t))
============================
~~ job_preemptable j (service sched j t)
----------------------------------------------------------------------------- *)
by rewrite SERV.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ModelWithLimitedPreemptions.
Hint Resolve valid_fixed_preemption_points_model_lemma : basic_facts.
valid_preemption_model arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1542)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
============================
valid_preemption_model arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
intros j ARR; repeat split.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 1547)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
job_cannot_become_nonpreemptive_before_execution j
subgoal 2 (ID 1551) is:
job_cannot_be_nonpreemptive_after_completion j
subgoal 3 (ID 1555) is:
not_preemptive_implies_scheduled sched j
subgoal 4 (ID 1556) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1547)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
job_cannot_become_nonpreemptive_before_execution j
----------------------------------------------------------------------------- *)
by apply zero_in_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1551)
subgoal 1 (ID 1551) is:
job_cannot_be_nonpreemptive_after_completion j
subgoal 2 (ID 1555) is:
not_preemptive_implies_scheduled sched j
subgoal 3 (ID 1556) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1551)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
job_cannot_be_nonpreemptive_after_completion j
subgoal 2 (ID 1555) is:
not_preemptive_implies_scheduled sched j
subgoal 3 (ID 1556) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1551)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
job_cannot_be_nonpreemptive_after_completion j
----------------------------------------------------------------------------- *)
by apply job_cost_in_nonpreemptive_points.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1555)
subgoal 1 (ID 1555) is:
not_preemptive_implies_scheduled sched j
subgoal 2 (ID 1556) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1555)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
not_preemptive_implies_scheduled sched j
subgoal 2 (ID 1556) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1555)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
not_preemptive_implies_scheduled sched j
----------------------------------------------------------------------------- *)
by move ⇒ t NPP; apply H_schedule_respects_preemption_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1556)
subgoal 1 (ID 1556) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1556)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1556)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
intros t NSCHED SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1574)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
job_preemptable j (service sched j (succn t))
----------------------------------------------------------------------------- *)
have SERV: service sched j t = service sched j t.+1.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1583)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
service sched j t = service sched j (succn t)
subgoal 2 (ID 1585) is:
job_preemptable j (service sched j (succn t))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1583)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
service sched j t = service sched j (succn t)
----------------------------------------------------------------------------- *)
rewrite -[service sched j t]addn0 /service /service_during; apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 1662)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
\sum_(0 <= t0 < t) service_at sched j t0 + 0 ==
\sum_(0 <= t0 < succn t) service_at sched j t0
----------------------------------------------------------------------------- *)
rewrite big_nat_recr //=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1673)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
\sum_(0 <= t0 < t) service_at sched j t0 + 0 ==
\sum_(0 <= i < t) service_at sched j i + service_at sched j t
----------------------------------------------------------------------------- *)
rewrite eqn_add2l eq_sym.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1706)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
service_at sched j t == 0
----------------------------------------------------------------------------- *)
rewrite scheduled_at_def in NSCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1737)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
NSCHED : sched t != Some j
============================
service_at sched j t == 0
----------------------------------------------------------------------------- *)
by rewrite service_at_def eqb0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1585)
subgoal 1 (ID 1585) is:
job_preemptable j (service sched j (succn t))
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1585)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
SERV : service sched j t = service sched j (succn t)
============================
job_preemptable j (service sched j (succn t))
----------------------------------------------------------------------------- *)
rewrite -[job_preemptable _ _]Bool.negb_involutive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1754)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
SERV : service sched j t = service sched j (succn t)
============================
~~ ~~ job_preemptable j (service sched j (succn t))
----------------------------------------------------------------------------- *)
apply/negP; intros CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1776)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
SERV : service sched j t = service sched j (succn t)
CONTR : ~~ job_preemptable j (service sched j (succn t))
============================
False
----------------------------------------------------------------------------- *)
move: NSCHED ⇒ /negP NSCHED; apply: NSCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1810)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
SERV : service sched j t = service sched j (succn t)
CONTR : ~~ job_preemptable j (service sched j (succn t))
============================
scheduled_at sched j t
----------------------------------------------------------------------------- *)
apply H_schedule_respects_preemption_model; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1812)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
j : Job
ARR : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
SERV : service sched j t = service sched j (succn t)
CONTR : ~~ job_preemptable j (service sched j (succn t))
============================
~~ job_preemptable j (service sched j t)
----------------------------------------------------------------------------- *)
by rewrite SERV.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ModelWithLimitedPreemptions.
Hint Resolve valid_fixed_preemption_points_model_lemma : basic_facts.