Library prosa.analysis.facts.preemption.rtc_threshold.job_preemptable
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.model.task.preemption.parameters.
Run-to-Completion Threshold
In this section, we provide a few basic properties of run-to-completion-threshold-compliant schedules.
Consider any type of jobs.
In addition, we assume existence of a function
mapping jobs to theirs preemption points.
Consider any kind of processor state model, ...
... any job arrival sequence, ...
... and any given schedule.
Assume that the preemption model is valid.
Consider an arbitrary job j from the arrival sequence.
First we prove a few auxiliary lemmas about
[job_preemption_points].
We prove that the sequence of preemption points of a zero-cost
job consists of one element -- 0.
Lemma preemption_points_of_zero_cost_job:
job_cost j = 0 →
job_preemption_points j = [::0].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 33)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost j = 0 -> job_preemption_points j = [:: 0]
----------------------------------------------------------------------------- *)
Proof.
intros ZERO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 34)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ZERO : job_cost j = 0
============================
job_preemption_points j = [:: 0]
----------------------------------------------------------------------------- *)
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ZERO : job_cost j = 0
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
job_preemption_points j = [:: 0]
----------------------------------------------------------------------------- *)
unfold job_preemption_points; rewrite ZERO; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 65)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ZERO : job_cost j = 0
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
(if job_preemptable j 0 then [:: 0] else [::]) = [:: 0]
----------------------------------------------------------------------------- *)
simpl; unfold job_cannot_become_nonpreemptive_before_execution in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 68)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ZERO : job_cost j = 0
A1 : job_preemptable j 0
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
(if job_preemptable j 0 then [:: 0] else [::]) = [:: 0]
----------------------------------------------------------------------------- *)
by rewrite A1.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_cost j = 0 →
job_preemption_points j = [::0].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 33)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost j = 0 -> job_preemption_points j = [:: 0]
----------------------------------------------------------------------------- *)
Proof.
intros ZERO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 34)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ZERO : job_cost j = 0
============================
job_preemption_points j = [:: 0]
----------------------------------------------------------------------------- *)
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 50)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ZERO : job_cost j = 0
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
job_preemption_points j = [:: 0]
----------------------------------------------------------------------------- *)
unfold job_preemption_points; rewrite ZERO; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 65)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ZERO : job_cost j = 0
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
(if job_preemptable j 0 then [:: 0] else [::]) = [:: 0]
----------------------------------------------------------------------------- *)
simpl; unfold job_cannot_become_nonpreemptive_before_execution in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 68)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ZERO : job_cost j = 0
A1 : job_preemptable j 0
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
(if job_preemptable j 0 then [:: 0] else [::]) = [:: 0]
----------------------------------------------------------------------------- *)
by rewrite A1.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
For a positive-cost job, 0 ...
Lemma zero_in_preemption_points:
0 < job_cost j →
0 \in job_preemption_points j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
0 < job_cost j -> 0 \in job_preemption_points j
----------------------------------------------------------------------------- *)
Proof.
intros POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 44)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
0 \in job_preemption_points j
----------------------------------------------------------------------------- *)
unfold job_preemption_points, range.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
0 \in [seq ρ <- index_iota 0 (job_cost j).+1 | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
0 \in [seq ρ <- index_iota 0 (job_cost j).+1 | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
unfold job_cannot_become_nonpreemptive_before_execution in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 70)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
A1 : job_preemptable j 0
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
0 \in [seq ρ <- index_iota 0 (job_cost j).+1 | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
rewrite index_iota_lt_step; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
A1 : job_preemptable j 0
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
0 \in [seq ρ <- 0 :: index_iota 1 (job_cost j).+1 | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
by simpl; rewrite A1 in_cons eq_refl.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
0 < job_cost j →
0 \in job_preemption_points j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
0 < job_cost j -> 0 \in job_preemption_points j
----------------------------------------------------------------------------- *)
Proof.
intros POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 44)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
0 \in job_preemption_points j
----------------------------------------------------------------------------- *)
unfold job_preemption_points, range.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
0 \in [seq ρ <- index_iota 0 (job_cost j).+1 | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 61)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
0 \in [seq ρ <- index_iota 0 (job_cost j).+1 | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
unfold job_cannot_become_nonpreemptive_before_execution in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 70)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
A1 : job_preemptable j 0
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
0 \in [seq ρ <- index_iota 0 (job_cost j).+1 | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
rewrite index_iota_lt_step; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
A1 : job_preemptable j 0
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
0 \in [seq ρ <- 0 :: index_iota 1 (job_cost j).+1 | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
by simpl; rewrite A1 in_cons eq_refl.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
... and [job_cost] are in preemption points.
Lemma job_cost_in_preemption_points:
0 < job_cost j →
job_cost j \in job_preemption_points j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 55)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
0 < job_cost j -> job_cost j \in job_preemption_points j
----------------------------------------------------------------------------- *)
Proof.
intros POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 56)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
job_cost j \in job_preemption_points j
----------------------------------------------------------------------------- *)
unfold job_preemption_points, range, index_iota; rewrite subn0 -addn1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 65)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
job_cost j \in [seq ρ <- iota 0 (job_cost j + 1) | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
rewrite iota_add add0n filter_cat mem_cat.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 87)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
(job_cost j \in [seq ρ <- iota 0 (job_cost j) | job_preemptable j ρ])
|| (job_cost j \in [seq ρ <- iota (job_cost j) 1 | job_preemptable j ρ])
----------------------------------------------------------------------------- *)
apply/orP; right; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 123)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
job_cost j
\in (if job_preemptable j (job_cost j) then [:: job_cost j] else [::])
----------------------------------------------------------------------------- *)
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 139)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
job_cost j
\in (if job_preemptable j (job_cost j) then [:: job_cost j] else [::])
----------------------------------------------------------------------------- *)
unfold job_cannot_be_nonpreemptive_after_completion in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 148)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_preemptable j (job_cost j)
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
job_cost j
\in (if job_preemptable j (job_cost j) then [:: job_cost j] else [::])
----------------------------------------------------------------------------- *)
by rewrite A2 in_cons eq_refl.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
0 < job_cost j →
job_cost j \in job_preemption_points j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 55)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
0 < job_cost j -> job_cost j \in job_preemption_points j
----------------------------------------------------------------------------- *)
Proof.
intros POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 56)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
job_cost j \in job_preemption_points j
----------------------------------------------------------------------------- *)
unfold job_preemption_points, range, index_iota; rewrite subn0 -addn1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 65)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
job_cost j \in [seq ρ <- iota 0 (job_cost j + 1) | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
rewrite iota_add add0n filter_cat mem_cat.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 87)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
(job_cost j \in [seq ρ <- iota 0 (job_cost j) | job_preemptable j ρ])
|| (job_cost j \in [seq ρ <- iota (job_cost j) 1 | job_preemptable j ρ])
----------------------------------------------------------------------------- *)
apply/orP; right; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 123)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
job_cost j
\in (if job_preemptable j (job_cost j) then [:: job_cost j] else [::])
----------------------------------------------------------------------------- *)
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 139)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
job_cost j
\in (if job_preemptable j (job_cost j) then [:: job_cost j] else [::])
----------------------------------------------------------------------------- *)
unfold job_cannot_be_nonpreemptive_after_completion in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 148)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_preemptable j (job_cost j)
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
job_cost j
\in (if job_preemptable j (job_cost j) then [:: job_cost j] else [::])
----------------------------------------------------------------------------- *)
by rewrite A2 in_cons eq_refl.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Therefore, for a positive-cost job size of the sequence of
preemption points is at least two.
Lemma size_of_preemption_points:
0 < job_cost j →
2 ≤ size (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
0 < job_cost j -> 1 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
Proof.
intros POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 63)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
1 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
replace 2 with (size [::0; job_cost j]); last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 73)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
size [:: 0; job_cost j] <= size (job_preemption_points j)
----------------------------------------------------------------------------- *)
apply subseq_leq_size.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 76)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
uniq [:: 0; job_cost j]
subgoal 2 (ID 77) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
- apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 103)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
0 \notin [:: job_cost j]
subgoal 2 (ID 104) is:
(job_cost j \notin [::]) && true
subgoal 3 (ID 77) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
rewrite !in_cons Bool.negb_orb.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 118)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
(0 != job_cost j) && (0 \notin [::])
subgoal 2 (ID 104) is:
(job_cost j \notin [::]) && true
subgoal 3 (ID 77) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
+ apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 144)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
0 != job_cost j
subgoal 2 (ID 145) is:
0 \notin [::]
subgoal 3 (ID 104) is:
(job_cost j \notin [::]) && true
subgoal 4 (ID 77) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
by rewrite neq_ltn POS.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 145)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
0 \notin [::]
subgoal 2 (ID 104) is:
(job_cost j \notin [::]) && true
subgoal 3 (ID 77) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 104)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
(job_cost j \notin [::]) && true
subgoal 2 (ID 77) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
+ apply/andP; split; by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 77)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
- intros ρ; rewrite !in_cons; move ⇒ /orP [/eqP EQ| /orP [/eqP Cost | C]].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 339)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
ρ : nat_eqType
EQ : ρ = 0
============================
ρ \in job_preemption_points j
subgoal 2 (ID 340) is:
ρ \in job_preemption_points j
subgoal 3 (ID 341) is:
ρ \in job_preemption_points j
----------------------------------------------------------------------------- *)
+ by subst; apply zero_in_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 340)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
ρ : nat_eqType
Cost : ρ = job_cost j
============================
ρ \in job_preemption_points j
subgoal 2 (ID 341) is:
ρ \in job_preemption_points j
----------------------------------------------------------------------------- *)
+ by subst; apply job_cost_in_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 341)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
ρ : nat_eqType
C : ρ \in [::]
============================
ρ \in job_preemption_points j
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
0 < job_cost j →
2 ≤ size (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
0 < job_cost j -> 1 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
Proof.
intros POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 63)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
1 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
replace 2 with (size [::0; job_cost j]); last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 73)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
size [:: 0; job_cost j] <= size (job_preemption_points j)
----------------------------------------------------------------------------- *)
apply subseq_leq_size.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 76)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
uniq [:: 0; job_cost j]
subgoal 2 (ID 77) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
- apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 103)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
0 \notin [:: job_cost j]
subgoal 2 (ID 104) is:
(job_cost j \notin [::]) && true
subgoal 3 (ID 77) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
rewrite !in_cons Bool.negb_orb.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 118)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
(0 != job_cost j) && (0 \notin [::])
subgoal 2 (ID 104) is:
(job_cost j \notin [::]) && true
subgoal 3 (ID 77) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
+ apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 144)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
0 != job_cost j
subgoal 2 (ID 145) is:
0 \notin [::]
subgoal 3 (ID 104) is:
(job_cost j \notin [::]) && true
subgoal 4 (ID 77) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
by rewrite neq_ltn POS.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 145)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
0 \notin [::]
subgoal 2 (ID 104) is:
(job_cost j \notin [::]) && true
subgoal 3 (ID 77) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 104)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
(job_cost j \notin [::]) && true
subgoal 2 (ID 77) is:
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
+ apply/andP; split; by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 77)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
============================
forall x : nat_eqType,
x \in [:: 0; job_cost j] -> x \in job_preemption_points j
----------------------------------------------------------------------------- *)
- intros ρ; rewrite !in_cons; move ⇒ /orP [/eqP EQ| /orP [/eqP Cost | C]].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 339)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
ρ : nat_eqType
EQ : ρ = 0
============================
ρ \in job_preemption_points j
subgoal 2 (ID 340) is:
ρ \in job_preemption_points j
subgoal 3 (ID 341) is:
ρ \in job_preemption_points j
----------------------------------------------------------------------------- *)
+ by subst; apply zero_in_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 340)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
ρ : nat_eqType
Cost : ρ = job_cost j
============================
ρ \in job_preemption_points j
subgoal 2 (ID 341) is:
ρ \in job_preemption_points j
----------------------------------------------------------------------------- *)
+ by subst; apply job_cost_in_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 341)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
POS : 0 < job_cost j
ρ : nat_eqType
C : ρ \in [::]
============================
ρ \in job_preemption_points j
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Next we show that the sequence of preemption points is a non-decreasing sequence.
Lemma preemption_points_nondecreasing:
nondecreasing_sequence (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 66)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
nondecreasing_sequence (job_preemption_points j)
----------------------------------------------------------------------------- *)
Proof. by apply increasing_implies_nondecreasing, iota_is_increasing_sequence.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
nondecreasing_sequence (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 66)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
nondecreasing_sequence (job_preemption_points j)
----------------------------------------------------------------------------- *)
Proof. by apply increasing_implies_nondecreasing, iota_is_increasing_sequence.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Next, we prove that the last element of the sequence of
preemption points is [job_cost].
Lemma job_cost_is_last_element_of_preemption_points:
job_cost j = last0 (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 73)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost j = last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
Proof.
unfold job_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 74)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost j = last0 [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
edestruct H_valid_preemption_model as [A1 [A2 [A3 A4]]]; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 92)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
job_cost j = last0 [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
erewrite last0_filter.
(* ----------------------------------[ coqtop ]---------------------------------
4 focused subgoals
(shelved: 1) (ID 96)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
job_cost j = ?x
subgoal 2 (ID 97) is:
range 0 (job_cost j) <> [::]
subgoal 3 (ID 98) is:
last0 (range 0 (job_cost j)) = ?x
subgoal 4 (ID 99) is:
job_preemptable j ?x
----------------------------------------------------------------------------- *)
+ by apply/eqP; apply eq_refl.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 97)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
range 0 (job_cost j) <> [::]
subgoal 2 (ID 98) is:
last0 (range 0 (job_cost j)) = job_cost j
subgoal 3 (ID 99) is:
job_preemptable j (job_cost j)
----------------------------------------------------------------------------- *)
+ unfold range, index_iota; rewrite subn0 -addn1.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 163)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
iota 0 (job_cost j + 1) <> [::]
subgoal 2 (ID 98) is:
last0 (range 0 (job_cost j)) = job_cost j
subgoal 3 (ID 99) is:
job_preemptable j (job_cost j)
----------------------------------------------------------------------------- *)
by rewrite iota_add; destruct (iota 0 (job_cost j)).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 98)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
last0 (range 0 (job_cost j)) = job_cost j
subgoal 2 (ID 99) is:
job_preemptable j (job_cost j)
----------------------------------------------------------------------------- *)
+ unfold range, index_iota; rewrite subn0 -addn1.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 243)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
last0 (iota 0 (job_cost j + 1)) = job_cost j
subgoal 2 (ID 99) is:
job_preemptable j (job_cost j)
----------------------------------------------------------------------------- *)
by rewrite iota_add last0_cat //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 99)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
job_preemptable j (job_cost j)
----------------------------------------------------------------------------- *)
+ by apply A2.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_cost j = last0 (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 73)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost j = last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
Proof.
unfold job_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 74)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost j = last0 [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
edestruct H_valid_preemption_model as [A1 [A2 [A3 A4]]]; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 92)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
job_cost j = last0 [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
erewrite last0_filter.
(* ----------------------------------[ coqtop ]---------------------------------
4 focused subgoals
(shelved: 1) (ID 96)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
job_cost j = ?x
subgoal 2 (ID 97) is:
range 0 (job_cost j) <> [::]
subgoal 3 (ID 98) is:
last0 (range 0 (job_cost j)) = ?x
subgoal 4 (ID 99) is:
job_preemptable j ?x
----------------------------------------------------------------------------- *)
+ by apply/eqP; apply eq_refl.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 97)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
range 0 (job_cost j) <> [::]
subgoal 2 (ID 98) is:
last0 (range 0 (job_cost j)) = job_cost j
subgoal 3 (ID 99) is:
job_preemptable j (job_cost j)
----------------------------------------------------------------------------- *)
+ unfold range, index_iota; rewrite subn0 -addn1.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 163)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
iota 0 (job_cost j + 1) <> [::]
subgoal 2 (ID 98) is:
last0 (range 0 (job_cost j)) = job_cost j
subgoal 3 (ID 99) is:
job_preemptable j (job_cost j)
----------------------------------------------------------------------------- *)
by rewrite iota_add; destruct (iota 0 (job_cost j)).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 98)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
last0 (range 0 (job_cost j)) = job_cost j
subgoal 2 (ID 99) is:
job_preemptable j (job_cost j)
----------------------------------------------------------------------------- *)
+ unfold range, index_iota; rewrite subn0 -addn1.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 243)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
last0 (iota 0 (job_cost j + 1)) = job_cost j
subgoal 2 (ID 99) is:
job_preemptable j (job_cost j)
----------------------------------------------------------------------------- *)
by rewrite iota_add last0_cat //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 99)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
job_preemptable j (job_cost j)
----------------------------------------------------------------------------- *)
+ by apply A2.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Last non-preemptive segment of a positive-cost job has positive length.
Lemma job_last_nonpreemptive_segment_positive:
job_cost_positive j →
0 < job_last_nonpreemptive_segment j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 79)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost_positive j -> 0 < job_last_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
Proof.
intros COST.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < job_last_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
unfold job_last_nonpreemptive_segment.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 81)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < last0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
rewrite last0_nth function_of_distances_is_correct subn_gt0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 92)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
nth 0 (job_preemption_points j) (size (lengths_of_segments j)).-1 <
nth 0 (job_preemption_points j) (size (lengths_of_segments j)).-1.+1
----------------------------------------------------------------------------- *)
rewrite [size _]pred_Sn -addn1-addn1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 104)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
nth 0 (job_preemption_points j) (size (lengths_of_segments j) + 1).-2 + 1 <=
nth 0 (job_preemption_points j) (size (lengths_of_segments j) + 1).-2.+1
----------------------------------------------------------------------------- *)
rewrite -size_of_seq_of_distances ?addn1; last by apply size_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 112)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1
----------------------------------------------------------------------------- *)
rewrite prednK; last first.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 120)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < (size (job_preemption_points j)).-1
subgoal 2 (ID 119) is:
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 120)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < (size (job_preemption_points j)).-1
----------------------------------------------------------------------------- *)
rewrite -(leq_add2r 1) !addn1 prednK.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 135)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
1 < size (job_preemption_points j)
subgoal 2 (ID 136) is:
0 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
- apply size_of_preemption_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 136)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
- rewrite ltnW //; apply size_of_preemption_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 119) is:
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-1
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 119)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-1
----------------------------------------------------------------------------- *)
apply iota_is_increasing_sequence; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 198)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
(size (job_preemption_points j)).-2 < (size (job_preemption_points j)).-1
subgoal 2 (ID 199) is:
(size (job_preemption_points j)).-1 <
size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]
----------------------------------------------------------------------------- *)
- rewrite -(leq_add2r 2) !addn2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 209)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
(size (job_preemption_points j)).-2.+2 <
(size (job_preemption_points j)).-1.+2
subgoal 2 (ID 199) is:
(size (job_preemption_points j)).-1 <
size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]
----------------------------------------------------------------------------- *)
rewrite prednK; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 215)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < (size (job_preemption_points j)).-1
subgoal 2 (ID 199) is:
(size (job_preemption_points j)).-1 <
size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]
----------------------------------------------------------------------------- *)
rewrite -(leq_add2r 1) !addn1.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 225)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
1 < (size (job_preemption_points j)).-1.+1
subgoal 2 (ID 199) is:
(size (job_preemption_points j)).-1 <
size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]
----------------------------------------------------------------------------- *)
rewrite prednK.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 230)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
1 < size (job_preemption_points j)
subgoal 2 (ID 231) is:
0 < size (job_preemption_points j)
subgoal 3 (ID 199) is:
(size (job_preemption_points j)).-1 <
size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]
----------------------------------------------------------------------------- *)
+ by apply size_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 231)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < size (job_preemption_points j)
subgoal 2 (ID 199) is:
(size (job_preemption_points j)).-1 <
size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]
----------------------------------------------------------------------------- *)
+ by rewrite ltnW //; apply size_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 199)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
(size (job_preemption_points j)).-1 <
size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]
----------------------------------------------------------------------------- *)
- rewrite -(leq_add2r 1) !addn1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 270)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
(size (job_preemption_points j)).-1.+1 <
(size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]).+1
----------------------------------------------------------------------------- *)
unfold job_preemption_points, range.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 272)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
(size [seq ρ <- index_iota 0 (job_cost j).+1 | job_preemptable j ρ]).-1.+1 <
(size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]).+1
----------------------------------------------------------------------------- *)
rewrite prednK ?ltnS; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 277)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < size [seq ρ <- index_iota 0 (job_cost j).+1 | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
by rewrite ltnW //; apply size_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_cost_positive j →
0 < job_last_nonpreemptive_segment j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 79)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost_positive j -> 0 < job_last_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
Proof.
intros COST.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < job_last_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
unfold job_last_nonpreemptive_segment.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 81)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < last0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
rewrite last0_nth function_of_distances_is_correct subn_gt0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 92)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
nth 0 (job_preemption_points j) (size (lengths_of_segments j)).-1 <
nth 0 (job_preemption_points j) (size (lengths_of_segments j)).-1.+1
----------------------------------------------------------------------------- *)
rewrite [size _]pred_Sn -addn1-addn1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 104)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
nth 0 (job_preemption_points j) (size (lengths_of_segments j) + 1).-2 + 1 <=
nth 0 (job_preemption_points j) (size (lengths_of_segments j) + 1).-2.+1
----------------------------------------------------------------------------- *)
rewrite -size_of_seq_of_distances ?addn1; last by apply size_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 112)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1
----------------------------------------------------------------------------- *)
rewrite prednK; last first.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 120)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < (size (job_preemption_points j)).-1
subgoal 2 (ID 119) is:
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 120)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < (size (job_preemption_points j)).-1
----------------------------------------------------------------------------- *)
rewrite -(leq_add2r 1) !addn1 prednK.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 135)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
1 < size (job_preemption_points j)
subgoal 2 (ID 136) is:
0 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
- apply size_of_preemption_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 136)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
- rewrite ltnW //; apply size_of_preemption_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 119) is:
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-1
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 119)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-1
----------------------------------------------------------------------------- *)
apply iota_is_increasing_sequence; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 198)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
(size (job_preemption_points j)).-2 < (size (job_preemption_points j)).-1
subgoal 2 (ID 199) is:
(size (job_preemption_points j)).-1 <
size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]
----------------------------------------------------------------------------- *)
- rewrite -(leq_add2r 2) !addn2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 209)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
(size (job_preemption_points j)).-2.+2 <
(size (job_preemption_points j)).-1.+2
subgoal 2 (ID 199) is:
(size (job_preemption_points j)).-1 <
size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]
----------------------------------------------------------------------------- *)
rewrite prednK; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 215)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < (size (job_preemption_points j)).-1
subgoal 2 (ID 199) is:
(size (job_preemption_points j)).-1 <
size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]
----------------------------------------------------------------------------- *)
rewrite -(leq_add2r 1) !addn1.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 225)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
1 < (size (job_preemption_points j)).-1.+1
subgoal 2 (ID 199) is:
(size (job_preemption_points j)).-1 <
size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]
----------------------------------------------------------------------------- *)
rewrite prednK.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 230)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
1 < size (job_preemption_points j)
subgoal 2 (ID 231) is:
0 < size (job_preemption_points j)
subgoal 3 (ID 199) is:
(size (job_preemption_points j)).-1 <
size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]
----------------------------------------------------------------------------- *)
+ by apply size_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 231)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < size (job_preemption_points j)
subgoal 2 (ID 199) is:
(size (job_preemption_points j)).-1 <
size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]
----------------------------------------------------------------------------- *)
+ by rewrite ltnW //; apply size_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 199)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
(size (job_preemption_points j)).-1 <
size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]
----------------------------------------------------------------------------- *)
- rewrite -(leq_add2r 1) !addn1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 270)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
(size (job_preemption_points j)).-1.+1 <
(size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]).+1
----------------------------------------------------------------------------- *)
unfold job_preemption_points, range.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 272)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
(size [seq ρ <- index_iota 0 (job_cost j).+1 | job_preemptable j ρ]).-1.+1 <
(size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]).+1
----------------------------------------------------------------------------- *)
rewrite prednK ?ltnS; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 277)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < size [seq ρ <- index_iota 0 (job_cost j).+1 | job_preemptable j ρ]
----------------------------------------------------------------------------- *)
by rewrite ltnW //; apply size_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Max nonpreemptive segment of a positive-cost job has positive length.
Lemma job_max_nonpreemptive_segment_positive:
job_cost_positive j →
0 < job_max_nonpreemptive_segment j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 85)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost_positive j -> 0 < job_max_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
Proof.
intros COST.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 86)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < job_max_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
eapply leq_trans.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 88)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < ?n
subgoal 2 (ID 89) is:
?n <= job_max_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
- by apply job_last_nonpreemptive_segment_positive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 89)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
job_last_nonpreemptive_segment j <= job_max_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
- by apply last_of_seq_le_max_of_seq.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_cost_positive j →
0 < job_max_nonpreemptive_segment j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 85)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost_positive j -> 0 < job_max_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
Proof.
intros COST.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 86)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < job_max_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
eapply leq_trans.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 88)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < ?n
subgoal 2 (ID 89) is:
?n <= job_max_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
- by apply job_last_nonpreemptive_segment_positive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 89)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
job_last_nonpreemptive_segment j <= job_max_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
- by apply last_of_seq_le_max_of_seq.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Next we show that max nonpreemptive segment is at most the
cost of a job.
Lemma job_max_nonpreemptive_segment_le_job_cost:
job_max_nonpreemptive_segment j ≤ job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 91)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_max_nonpreemptive_segment j <= job_cost j
----------------------------------------------------------------------------- *)
Proof.
eapply leq_trans.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 93)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_max_nonpreemptive_segment j <= ?n
subgoal 2 (ID 94) is:
?n <= job_cost j
----------------------------------------------------------------------------- *)
apply max_distance_in_seq_le_last_element_of_seq; apply preemption_points_nondecreasing.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 94)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 111)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [ZERO|POSt].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 159)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
ZERO : job_cost j = 0
============================
last0 (job_preemption_points j) <= job_cost j
subgoal 2 (ID 160) is:
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 159)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
ZERO : job_cost j = 0
============================
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
unfold job_preemption_points; rewrite ZERO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 163)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
ZERO : job_cost j = 0
============================
last0 [seq ρ <- range 0 0 | job_preemptable j ρ] <= 0
----------------------------------------------------------------------------- *)
simpl; unfold job_cannot_become_nonpreemptive_before_execution in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 176)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_preemptable j 0
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
ZERO : job_cost j = 0
============================
last0 (if job_preemptable j 0 then [:: 0] else [::]) <= 0
----------------------------------------------------------------------------- *)
by rewrite A1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 160) is:
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 160)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
POSt : 0 < job_cost j
============================
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 160)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
POSt : 0 < job_cost j
============================
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
eapply leq_trans; first apply last_of_seq_le_max_of_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 181)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
POSt : 0 < job_cost j
============================
max0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
rewrite job_cost_is_last_element_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 183)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
POSt : 0 < job_cost j
============================
max0 (job_preemption_points j) <= last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
apply last_is_max_in_nondecreasing_seq; first by apply preemption_points_nondecreasing.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 185)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
POSt : 0 < job_cost j
============================
max0 (job_preemption_points j) \in job_preemption_points j
----------------------------------------------------------------------------- *)
apply max0_in_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 186)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
POSt : 0 < job_cost j
============================
job_preemption_points j <> [::]
----------------------------------------------------------------------------- *)
have LL := size_of_preemption_points POSt.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 191)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
POSt : 0 < job_cost j
LL : 1 < size (job_preemption_points j)
============================
job_preemption_points j <> [::]
----------------------------------------------------------------------------- *)
by destruct (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_max_nonpreemptive_segment j ≤ job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 91)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_max_nonpreemptive_segment j <= job_cost j
----------------------------------------------------------------------------- *)
Proof.
eapply leq_trans.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 93)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_max_nonpreemptive_segment j <= ?n
subgoal 2 (ID 94) is:
?n <= job_cost j
----------------------------------------------------------------------------- *)
apply max_distance_in_seq_le_last_element_of_seq; apply preemption_points_nondecreasing.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 94)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 111)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
============================
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [ZERO|POSt].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 159)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
ZERO : job_cost j = 0
============================
last0 (job_preemption_points j) <= job_cost j
subgoal 2 (ID 160) is:
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 159)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
ZERO : job_cost j = 0
============================
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
unfold job_preemption_points; rewrite ZERO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 163)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
ZERO : job_cost j = 0
============================
last0 [seq ρ <- range 0 0 | job_preemptable j ρ] <= 0
----------------------------------------------------------------------------- *)
simpl; unfold job_cannot_become_nonpreemptive_before_execution in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 176)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_preemptable j 0
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
ZERO : job_cost j = 0
============================
last0 (if job_preemptable j 0 then [:: 0] else [::]) <= 0
----------------------------------------------------------------------------- *)
by rewrite A1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 160) is:
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 160)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
POSt : 0 < job_cost j
============================
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 160)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
POSt : 0 < job_cost j
============================
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
eapply leq_trans; first apply last_of_seq_le_max_of_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 181)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
POSt : 0 < job_cost j
============================
max0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
rewrite job_cost_is_last_element_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 183)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
POSt : 0 < job_cost j
============================
max0 (job_preemption_points j) <= last0 (job_preemption_points j)
----------------------------------------------------------------------------- *)
apply last_is_max_in_nondecreasing_seq; first by apply preemption_points_nondecreasing.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 185)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
POSt : 0 < job_cost j
============================
max0 (job_preemption_points j) \in job_preemption_points j
----------------------------------------------------------------------------- *)
apply max0_in_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 186)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
POSt : 0 < job_cost j
============================
job_preemption_points j <> [::]
----------------------------------------------------------------------------- *)
have LL := size_of_preemption_points POSt.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 191)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
A1 : job_cannot_become_nonpreemptive_before_execution j
A2 : job_cannot_be_nonpreemptive_after_completion j
A3 : not_preemptive_implies_scheduled sched j
A4 : execution_starts_with_preemption_point sched j
POSt : 0 < job_cost j
LL : 1 < size (job_preemption_points j)
============================
job_preemption_points j <> [::]
----------------------------------------------------------------------------- *)
by destruct (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We also show that last nonpreemptive segment is at most the
cost of a job.
Lemma job_last_nonpreemptive_segment_le_job_cost:
job_last_nonpreemptive_segment j ≤ job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 97)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_last_nonpreemptive_segment j <= job_cost j
----------------------------------------------------------------------------- *)
Proof.
eapply leq_trans.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 99)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_last_nonpreemptive_segment j <= ?n
subgoal 2 (ID 100) is:
?n <= job_cost j
----------------------------------------------------------------------------- *)
- apply last_of_seq_le_max_of_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 100)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
max0 (lengths_of_segments j) <= job_cost j
----------------------------------------------------------------------------- *)
- apply job_max_nonpreemptive_segment_le_job_cost.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End AuxiliaryLemmas.
job_last_nonpreemptive_segment j ≤ job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 97)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_last_nonpreemptive_segment j <= job_cost j
----------------------------------------------------------------------------- *)
Proof.
eapply leq_trans.
(* ----------------------------------[ coqtop ]---------------------------------
2 focused subgoals
(shelved: 1) (ID 99)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_last_nonpreemptive_segment j <= ?n
subgoal 2 (ID 100) is:
?n <= job_cost j
----------------------------------------------------------------------------- *)
- apply last_of_seq_le_max_of_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 100)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
max0 (lengths_of_segments j) <= job_cost j
----------------------------------------------------------------------------- *)
- apply job_max_nonpreemptive_segment_le_job_cost.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End AuxiliaryLemmas.
We prove that the run-to-completion threshold is positive for
any job with positive cost. I.e., in order to become
non-preemptive a job must receive at least one unit of
service.
Lemma job_run_to_completion_threshold_positive:
job_cost_positive j →
0 < job_rtct j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 29)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost_positive j -> 0 < job_rtct j
----------------------------------------------------------------------------- *)
Proof.
intros COST; unfold job_rtct, ε.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 31)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < job_cost j - (job_last_nonpreemptive_segment j - 1)
----------------------------------------------------------------------------- *)
have N1 := job_last_nonpreemptive_segment_positive COST.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 36)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
N1 : 0 < job_last_nonpreemptive_segment j
============================
0 < job_cost j - (job_last_nonpreemptive_segment j - 1)
----------------------------------------------------------------------------- *)
have N2 := job_last_nonpreemptive_segment_le_job_cost.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 41)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
N1 : 0 < job_last_nonpreemptive_segment j
N2 : job_last_nonpreemptive_segment j <= job_cost j
============================
0 < job_cost j - (job_last_nonpreemptive_segment j - 1)
----------------------------------------------------------------------------- *)
ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_cost_positive j →
0 < job_rtct j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 29)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_cost_positive j -> 0 < job_rtct j
----------------------------------------------------------------------------- *)
Proof.
intros COST; unfold job_rtct, ε.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 31)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
============================
0 < job_cost j - (job_last_nonpreemptive_segment j - 1)
----------------------------------------------------------------------------- *)
have N1 := job_last_nonpreemptive_segment_positive COST.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 36)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
N1 : 0 < job_last_nonpreemptive_segment j
============================
0 < job_cost j - (job_last_nonpreemptive_segment j - 1)
----------------------------------------------------------------------------- *)
have N2 := job_last_nonpreemptive_segment_le_job_cost.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 41)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
COST : job_cost_positive j
N1 : 0 < job_last_nonpreemptive_segment j
N2 : job_last_nonpreemptive_segment j <= job_cost j
============================
0 < job_cost j - (job_last_nonpreemptive_segment j - 1)
----------------------------------------------------------------------------- *)
ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Next we show that the run-to-completion threshold is at most
the cost of a job.
Lemma job_run_to_completion_threshold_le_job_cost:
job_rtct j ≤ job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 35)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_rtct j <= job_cost j
----------------------------------------------------------------------------- *)
Proof. by apply leq_subr.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_rtct j ≤ job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 35)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
job_rtct j <= job_cost j
----------------------------------------------------------------------------- *)
Proof. by apply leq_subr.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We prove that a job cannot be preempted
during execution of the last segment.
Lemma job_cannot_be_preempted_within_last_segment:
∀ (ρ : duration),
job_rtct j ≤ ρ < job_cost j →
~~ job_preemptable j ρ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
forall ρ : duration, job_rtct j <= ρ < job_cost j -> ~~ job_preemptable j ρ
----------------------------------------------------------------------------- *)
Proof.
move ⇒ ρ /andP [GE LT].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 83)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
GE : job_rtct j <= ρ
LT : ρ < job_cost j
============================
~~ job_preemptable j ρ
----------------------------------------------------------------------------- *)
apply/negP; intros C.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 105)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
GE : job_rtct j <= ρ
LT : ρ < job_cost j
C : job_preemptable j ρ
============================
False
----------------------------------------------------------------------------- *)
have POS : 0 < job_cost j; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 110)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
GE : job_rtct j <= ρ
LT : ρ < job_cost j
C : job_preemptable j ρ
POS : 0 < job_cost j
============================
False
----------------------------------------------------------------------------- *)
rewrite /job_rtct subnBA in GE; last by apply job_last_nonpreemptive_segment_positive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 290)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
LT : ρ < job_cost j
C : job_preemptable j ρ
POS : 0 < job_cost j
GE : job_cost j + ε - job_last_nonpreemptive_segment j <= ρ
============================
False
----------------------------------------------------------------------------- *)
rewrite -subh1 in GE; [rewrite addn1 in GE | by apply job_last_nonpreemptive_segment_le_job_cost].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 383)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
LT : ρ < job_cost j
C : job_preemptable j ρ
POS : 0 < job_cost j
GE : job_cost j - job_last_nonpreemptive_segment j < ρ
============================
False
----------------------------------------------------------------------------- *)
rewrite job_cost_is_last_element_of_preemption_points in LT, GE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 409)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : last0 (job_preemption_points j) - job_last_nonpreemptive_segment j < ρ
============================
False
----------------------------------------------------------------------------- *)
rewrite last_seq_minus_last_distance_seq in GE; last by apply preemption_points_nondecreasing.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 437)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
============================
False
----------------------------------------------------------------------------- *)
have EQ := antidensity_of_nondecreasing_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 460)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : forall (xs : seq nat) (x n : nat),
nondecreasing_sequence xs ->
nth 0 xs n < x < nth 0 xs n.+1 -> x \notin xs
============================
False
----------------------------------------------------------------------------- *)
specialize (EQ (job_preemption_points j) ρ (size (job_preemption_points j)).-2 ).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 469)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : nondecreasing_sequence (job_preemption_points j) ->
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
ρ \notin job_preemption_points j
============================
False
----------------------------------------------------------------------------- *)
feed_n 2 EQ; first by apply preemption_points_nondecreasing.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 476)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
ρ \notin job_preemption_points j
============================
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 < ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1
subgoal 2 (ID 481) is:
False
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 476)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
ρ \notin job_preemption_points j
============================
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 < ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1
----------------------------------------------------------------------------- *)
apply/andP; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 508)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
ρ \notin job_preemption_points j
============================
ρ < nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1
----------------------------------------------------------------------------- *)
rewrite prednK; first by rewrite -last0_nth.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 513)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
ρ \notin job_preemption_points j
============================
0 < (size (job_preemption_points j)).-1
----------------------------------------------------------------------------- *)
rewrite -(leq_add2r 1) !addn1 prednK.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 531)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
ρ \notin job_preemption_points j
============================
1 < size (job_preemption_points j)
subgoal 2 (ID 532) is:
0 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
- by apply size_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 532)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
ρ \notin job_preemption_points j
============================
0 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
- by eapply leq_trans; last apply size_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 481) is:
False
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 481)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : ρ \notin job_preemption_points j
============================
False
----------------------------------------------------------------------------- *)
move: EQ ⇒ /negP EQ; apply: EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 570)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
============================
ρ \in job_preemption_points j
----------------------------------------------------------------------------- *)
apply conversion_preserves_equivalence; try done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 582)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
============================
ρ <= job_cost j
----------------------------------------------------------------------------- *)
eapply leq_trans; first by apply ltnW; exact LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 607)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
============================
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
by rewrite job_cost_is_last_element_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ (ρ : duration),
job_rtct j ≤ ρ < job_cost j →
~~ job_preemptable j ρ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
forall ρ : duration, job_rtct j <= ρ < job_cost j -> ~~ job_preemptable j ρ
----------------------------------------------------------------------------- *)
Proof.
move ⇒ ρ /andP [GE LT].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 83)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
GE : job_rtct j <= ρ
LT : ρ < job_cost j
============================
~~ job_preemptable j ρ
----------------------------------------------------------------------------- *)
apply/negP; intros C.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 105)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
GE : job_rtct j <= ρ
LT : ρ < job_cost j
C : job_preemptable j ρ
============================
False
----------------------------------------------------------------------------- *)
have POS : 0 < job_cost j; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 110)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
GE : job_rtct j <= ρ
LT : ρ < job_cost j
C : job_preemptable j ρ
POS : 0 < job_cost j
============================
False
----------------------------------------------------------------------------- *)
rewrite /job_rtct subnBA in GE; last by apply job_last_nonpreemptive_segment_positive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 290)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
LT : ρ < job_cost j
C : job_preemptable j ρ
POS : 0 < job_cost j
GE : job_cost j + ε - job_last_nonpreemptive_segment j <= ρ
============================
False
----------------------------------------------------------------------------- *)
rewrite -subh1 in GE; [rewrite addn1 in GE | by apply job_last_nonpreemptive_segment_le_job_cost].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 383)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
LT : ρ < job_cost j
C : job_preemptable j ρ
POS : 0 < job_cost j
GE : job_cost j - job_last_nonpreemptive_segment j < ρ
============================
False
----------------------------------------------------------------------------- *)
rewrite job_cost_is_last_element_of_preemption_points in LT, GE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 409)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : last0 (job_preemption_points j) - job_last_nonpreemptive_segment j < ρ
============================
False
----------------------------------------------------------------------------- *)
rewrite last_seq_minus_last_distance_seq in GE; last by apply preemption_points_nondecreasing.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 437)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
============================
False
----------------------------------------------------------------------------- *)
have EQ := antidensity_of_nondecreasing_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 460)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : forall (xs : seq nat) (x n : nat),
nondecreasing_sequence xs ->
nth 0 xs n < x < nth 0 xs n.+1 -> x \notin xs
============================
False
----------------------------------------------------------------------------- *)
specialize (EQ (job_preemption_points j) ρ (size (job_preemption_points j)).-2 ).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 469)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : nondecreasing_sequence (job_preemption_points j) ->
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
ρ \notin job_preemption_points j
============================
False
----------------------------------------------------------------------------- *)
feed_n 2 EQ; first by apply preemption_points_nondecreasing.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 476)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
ρ \notin job_preemption_points j
============================
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 < ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1
subgoal 2 (ID 481) is:
False
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 476)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
ρ \notin job_preemption_points j
============================
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 < ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1
----------------------------------------------------------------------------- *)
apply/andP; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 508)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
ρ \notin job_preemption_points j
============================
ρ < nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1
----------------------------------------------------------------------------- *)
rewrite prednK; first by rewrite -last0_nth.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 513)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
ρ \notin job_preemption_points j
============================
0 < (size (job_preemption_points j)).-1
----------------------------------------------------------------------------- *)
rewrite -(leq_add2r 1) !addn1 prednK.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 531)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
ρ \notin job_preemption_points j
============================
1 < size (job_preemption_points j)
subgoal 2 (ID 532) is:
0 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
- by apply size_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 532)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ <
nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
ρ \notin job_preemption_points j
============================
0 < size (job_preemption_points j)
----------------------------------------------------------------------------- *)
- by eapply leq_trans; last apply size_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 481) is:
False
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 481)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
EQ : ρ \notin job_preemption_points j
============================
False
----------------------------------------------------------------------------- *)
move: EQ ⇒ /negP EQ; apply: EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 570)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
============================
ρ \in job_preemption_points j
----------------------------------------------------------------------------- *)
apply conversion_preserves_equivalence; try done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 582)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
============================
ρ <= job_cost j
----------------------------------------------------------------------------- *)
eapply leq_trans; first by apply ltnW; exact LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 607)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
ρ : duration
C : job_preemptable j ρ
POS : 0 < job_cost j
LT : ρ < last0 (job_preemption_points j)
GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
ρ
============================
last0 (job_preemption_points j) <= job_cost j
----------------------------------------------------------------------------- *)
by rewrite job_cost_is_last_element_of_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
In order to get a consistent schedule, the scheduler should respect
the notion of run-to-completion threshold. We assume that, after
a job reaches its run-to-completion threshold, it cannot be preempted
until its completion.
Lemma job_nonpreemptive_after_run_to_completion_threshold:
∀ t t',
t ≤ t' →
job_rtct j ≤ service sched j t →
~~ completed_by sched j t' →
scheduled_at sched j t'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
forall t t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' -> scheduled_at sched j t'
----------------------------------------------------------------------------- *)
Proof.
intros ? ? LE TH COM.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
t, t' : nat
LE : t <= t'
TH : job_rtct j <= service sched j t
COM : ~~ completed_by sched j t'
============================
scheduled_at sched j t'
----------------------------------------------------------------------------- *)
apply H_valid_preemption_model; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
t, t' : nat
LE : t <= t'
TH : job_rtct j <= service sched j t
COM : ~~ completed_by sched j t'
============================
~~ job_preemptable j (service sched j t')
----------------------------------------------------------------------------- *)
apply job_cannot_be_preempted_within_last_segment; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 107)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
t, t' : nat
LE : t <= t'
TH : job_rtct j <= service sched j t
COM : ~~ completed_by sched j t'
============================
job_rtct j <= service sched j t'
subgoal 2 (ID 108) is:
service sched j t' < job_cost j
----------------------------------------------------------------------------- *)
- by apply leq_trans with (service sched j t); last apply service_monotonic.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 108)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
t, t' : nat
LE : t <= t'
TH : job_rtct j <= service sched j t
COM : ~~ completed_by sched j t'
============================
service sched j t' < job_cost j
----------------------------------------------------------------------------- *)
- by rewrite ltnNge.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End RunToCompletionThreshold.
∀ t t',
t ≤ t' →
job_rtct j ≤ service sched j t →
~~ completed_by sched j t' →
scheduled_at sched j t'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
============================
forall t t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' -> scheduled_at sched j t'
----------------------------------------------------------------------------- *)
Proof.
intros ? ? LE TH COM.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
t, t' : nat
LE : t <= t'
TH : job_rtct j <= service sched j t
COM : ~~ completed_by sched j t'
============================
scheduled_at sched j t'
----------------------------------------------------------------------------- *)
apply H_valid_preemption_model; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
t, t' : nat
LE : t <= t'
TH : job_rtct j <= service sched j t
COM : ~~ completed_by sched j t'
============================
~~ job_preemptable j (service sched j t')
----------------------------------------------------------------------------- *)
apply job_cannot_be_preempted_within_last_segment; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 107)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
t, t' : nat
LE : t <= t'
TH : job_rtct j <= service sched j t
COM : ~~ completed_by sched j t'
============================
job_rtct j <= service sched j t'
subgoal 2 (ID 108) is:
service sched j t' < job_cost j
----------------------------------------------------------------------------- *)
- by apply leq_trans with (service sched j t); last apply service_monotonic.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 108)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
H1 : JobPreemptable Job
PState : Type
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_valid_preemption_model : valid_preemption_model arr_seq sched
j : Job
H_j_arrives : arrives_in arr_seq j
t, t' : nat
LE : t <= t'
TH : job_rtct j <= service sched j t
COM : ~~ completed_by sched j t'
============================
service sched j t' < job_cost j
----------------------------------------------------------------------------- *)
- by rewrite ltnNge.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End RunToCompletionThreshold.
We add the above lemmas into a "Hint Database" basic_facts, so Coq
will be able to apply them automatically.
Global Hint Resolve job_run_to_completion_threshold_le_job_cost : basic_facts.