Library prosa.analysis.facts.preemption.job.preemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.task.preemption.parameters.
Furthermore, we assume the fully preemptive job model.
Preemptions in Fully Preemptive Model
In this section, we prove that instantiation of predicate [job_preemptable] to the fully preemptive model indeed defines a valid preemption model.
Consider any type of jobs.
Consider any kind of processor state model, ...
... any job arrival sequence, ...
... and any given schedule.
Then, we prove that fully_preemptive_model is a valid preemption model.
Lemma valid_fully_preemptive_model:
valid_preemption_model arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 337)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
============================
valid_preemption_model arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
by intros j ARR; repeat split; intros t CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
valid_preemption_model arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 337)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
============================
valid_preemption_model arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
by intros j ARR; repeat split; intros t CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We also prove that under the fully preemptive model
[job_max_nonpreemptive_segment j] is equal to 0, when [job_cost
j = 0] ...
Lemma job_max_nps_is_0:
∀ j,
job_cost j = 0 →
job_max_nonpreemptive_segment j = 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 350)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
============================
forall j : Job, job_cost j = 0 -> job_max_nonpreemptive_segment j = 0
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 352)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
H2 : job_cost j = 0
============================
job_max_nonpreemptive_segment j = 0
----------------------------------------------------------------------------- *)
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 373)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
H2 : job_cost j = 0
============================
max0 (distances [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]) = 0
----------------------------------------------------------------------------- *)
by rewrite H2; compute.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ j,
job_cost j = 0 →
job_max_nonpreemptive_segment j = 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 350)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
============================
forall j : Job, job_cost j = 0 -> job_max_nonpreemptive_segment j = 0
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 352)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
H2 : job_cost j = 0
============================
job_max_nonpreemptive_segment j = 0
----------------------------------------------------------------------------- *)
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 373)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
H2 : job_cost j = 0
============================
max0 (distances [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]) = 0
----------------------------------------------------------------------------- *)
by rewrite H2; compute.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
... or ε when [job_cost j > 0].
Lemma job_max_nps_is_ε:
∀ j,
job_cost j > 0 →
job_max_nonpreemptive_segment j = ε.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 361)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
============================
forall j : Job, 0 < job_cost j -> job_max_nonpreemptive_segment j = ε
----------------------------------------------------------------------------- *)
Proof.
intros ? POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 363)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
job_max_nonpreemptive_segment j = ε
----------------------------------------------------------------------------- *)
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 384)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
max0 (distances [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]) = ε
----------------------------------------------------------------------------- *)
rewrite /job_preemptable /fully_preemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 392)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
max0 (distances [seq _ <- range 0 (job_cost j) | true]) = ε
----------------------------------------------------------------------------- *)
rewrite filter_predT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
max0 (distances (range 0 (job_cost j))) = ε
----------------------------------------------------------------------------- *)
apply max0_of_uniform_set.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 397)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
0 < size (distances (range 0 (job_cost j)))
subgoal 2 (ID 398) is:
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
----------------------------------------------------------------------------- *)
- rewrite /range /index_iota subn0.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 405)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
0 < size (distances (iota 0 (succn (job_cost j))))
subgoal 2 (ID 398) is:
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
----------------------------------------------------------------------------- *)
rewrite [size _]pred_Sn -[in X in _ ≤ X]addn1 -size_of_seq_of_distances size_iota.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 428)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
0 < predn (succn (job_cost j))
subgoal 2 (ID 432) is:
1 < succn (job_cost j)
subgoal 3 (ID 398) is:
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
----------------------------------------------------------------------------- *)
+ by rewrite -pred_Sn.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 432)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
1 < succn (job_cost j)
subgoal 2 (ID 398) is:
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
----------------------------------------------------------------------------- *)
+ by rewrite ltnS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 398)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
----------------------------------------------------------------------------- *)
- by apply distances_of_iota_ε.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FullyPreemptiveModel.
Hint Resolve valid_fully_preemptive_model : basic_facts.
∀ j,
job_cost j > 0 →
job_max_nonpreemptive_segment j = ε.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 361)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
============================
forall j : Job, 0 < job_cost j -> job_max_nonpreemptive_segment j = ε
----------------------------------------------------------------------------- *)
Proof.
intros ? POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 363)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
job_max_nonpreemptive_segment j = ε
----------------------------------------------------------------------------- *)
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 384)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
max0 (distances [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]) = ε
----------------------------------------------------------------------------- *)
rewrite /job_preemptable /fully_preemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 392)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
max0 (distances [seq _ <- range 0 (job_cost j) | true]) = ε
----------------------------------------------------------------------------- *)
rewrite filter_predT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
max0 (distances (range 0 (job_cost j))) = ε
----------------------------------------------------------------------------- *)
apply max0_of_uniform_set.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 397)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
0 < size (distances (range 0 (job_cost j)))
subgoal 2 (ID 398) is:
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
----------------------------------------------------------------------------- *)
- rewrite /range /index_iota subn0.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 405)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
0 < size (distances (iota 0 (succn (job_cost j))))
subgoal 2 (ID 398) is:
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
----------------------------------------------------------------------------- *)
rewrite [size _]pred_Sn -[in X in _ ≤ X]addn1 -size_of_seq_of_distances size_iota.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 428)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
0 < predn (succn (job_cost j))
subgoal 2 (ID 432) is:
1 < succn (job_cost j)
subgoal 3 (ID 398) is:
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
----------------------------------------------------------------------------- *)
+ by rewrite -pred_Sn.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 432)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
1 < succn (job_cost j)
subgoal 2 (ID 398) is:
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
----------------------------------------------------------------------------- *)
+ by rewrite ltnS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 398)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
PState : Type
H1 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
j : Job
POS : 0 < job_cost j
============================
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
----------------------------------------------------------------------------- *)
- by apply distances_of_iota_ε.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FullyPreemptiveModel.
Hint Resolve valid_fully_preemptive_model : basic_facts.