Skip to content
Snippets Groups Projects
Commit 1bd6d79c authored by Sergey Bozhko's avatar Sergey Bozhko :eyes:
Browse files

Rename and move preemption.util file 

File preemption.util is renamed and moved to
util.nondecreasing. The new util file can be used
in both the old Prosa and the new Prosa.
parent df7fe9d2
No related branches found
No related tags found
1 merge request!45Port instantiations
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 985 additions and 763 deletions
classic/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
+ 32
− 32
View file @ 1bd6d79c
......@@ -329,7 +329,7 @@ Module RTAforConcreteModels.
{ have Fact2: 0 < size (task_preemption_points tsk).
{ apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; move: CONTR => /eqP CONTR.
move: (END _ H_tsk_in_ts) => EQ.
move: EQ; rewrite /NondecreasingSequence.last -nth_last nth_default; last by rewrite CONTR.
move: EQ; rewrite /last0 -nth_last nth_default; last by rewrite CONTR.
by intros; rewrite -EQ in POSt.
}
have EQ: 2 = size [::0; task_cost tsk]; first by done.
......@@ -345,14 +345,14 @@ Module RTAforConcreteModels.
{ rewrite EQ; clear EQ.
move: (BEG _ H_tsk_in_ts) => EQ.
rewrite -EQ; clear EQ.
rewrite /NondecreasingSequence.first -nth0.
rewrite /first0 -nth0.
apply/(nthP 0).
exists 0; by done.
}
{ rewrite EQ; clear EQ.
move: (END _ H_tsk_in_ts) => EQ.
rewrite -EQ; clear EQ.
rewrite /NondecreasingSequence.last -nth_last.
rewrite /last0 -nth_last.
apply/(nthP 0).
exists ((size (task_preemption_points tsk)).-1); last by done.
by rewrite -(leq_add2r 1) !addn1 prednK //.
......@@ -367,7 +367,7 @@ Module RTAforConcreteModels.
{ eapply model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions; eauto 2.
intros j ARR.
unfold ModelWithLimitedPreemptions.job_max_nps, task_max_nps, lengths_of_segments.
apply NondecreasingSequence.max_of_dominating_seq.
apply max_of_dominating_seq.
intros. apply HYP2.
by done.
}
......@@ -377,11 +377,11 @@ Module RTAforConcreteModels.
rewrite subn1 -(leq_add2r 1) !addn1 prednK; last first.
apply LSMj; try done.
rewrite /job_last_nps /ModelWithLimitedPreemptions.job_last_nps
ltnS /NondecreasingSequence.last -nth_last NondecreasingSequence.function_of_distances_is_correct.
ltnS /last0 -nth_last function_of_distances_is_correct.
apply leq_trans with (job_max_nps j);
first by apply NondecreasingSequence.distance_between_neighboring_elements_le_max_distance_in_seq.
first by apply distance_between_neighboring_elements_le_max_distance_in_seq.
rewrite -ENDj; last by done.
by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
}
{ by intros j ARR; rewrite leq_subLR leq_addl. }
{ intros ? ? ? ARR LE LS NCOMPL.
......@@ -407,9 +407,9 @@ Module RTAforConcreteModels.
}
clear LS.
rewrite -ENDj in NEQ, SERV; last by done.
rewrite NondecreasingSequence.last_seq_minus_last_distance_seq in NEQ; last by eauto 2.
rewrite /NondecreasingSequence.last -nth_last in SERV.
have EQ := NondecreasingSequence.antidensity_of_nondecreasing_seq.
rewrite last_seq_minus_last_distance_seq in NEQ; last by eauto 2.
rewrite /last0 -nth_last in SERV.
have EQ := antidensity_of_nondecreasing_seq.
specialize (EQ (job_preemption_points j) (service sched j (t + Δ)) (size (job_preemption_points j)).-2).
rewrite CONTR in EQ.
feed_n 2 EQ; first by eauto 2.
......@@ -423,8 +423,8 @@ Module RTAforConcreteModels.
by done.
rewrite -ENDj; last by done.
apply leq_trans with (job_max_nps j).
- by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
- by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
- by apply last_of_seq_le_max_of_seq.
- by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
}
}
{
......@@ -436,31 +436,31 @@ Module RTAforConcreteModels.
unfold task_last_nps.
rewrite !subnBA; first last.
apply LSMj; try done.
rewrite /ModelWithLimitedPreemptions.task_last_nps /NondecreasingSequence.last -nth_last.
rewrite /ModelWithLimitedPreemptions.task_last_nps /last0 -nth_last.
apply HYP3.
by done.
rewrite -(ltn_add2r 1) !addn1 prednK //.
move: (Fact2) => Fact3.
rewrite NondecreasingSequence.size_of_seq_of_distances // addn1 ltnS // in Fact2.
rewrite size_of_seq_of_distances // addn1 ltnS // in Fact2.
rewrite -subh1 -?[in X in _ <= X]subh1; first last.
{ apply leq_trans with (job_max_nps j).
- by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
- by rewrite -ENDj //; apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
- by apply last_of_seq_le_max_of_seq.
- by rewrite -ENDj //; apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
}
{ apply leq_trans with (task_max_nps tsk).
- by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
- by rewrite -END //; apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
- by apply last_of_seq_le_max_of_seq.
- by rewrite -END //; apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
}
rewrite -ENDj; last eauto 2.
rewrite -END; last eauto 2.
rewrite !NondecreasingSequence.last_seq_minus_last_distance_seq.
rewrite !last_seq_minus_last_distance_seq.
have EQ: size (job_preemption_points j) = size (task_preemption_points tsk).
{ rewrite -TSK.
by apply HYP1.
}
rewrite EQ; clear EQ.
rewrite leq_add2r.
apply NondecreasingSequence.domination_of_distances_implies_domination_of_seq; try done; eauto 2.
apply domination_of_distances_implies_domination_of_seq; try done; eauto 2.
rewrite BEG // BEGj //.
eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2.
rewrite -TSK; apply HYP1; try done.
......@@ -470,17 +470,17 @@ Module RTAforConcreteModels.
}
{ rewrite subKn; first by done.
rewrite /task_last_nps -(leq_add2r 1) subn1 !addn1 prednK; last first.
{ rewrite /ModelWithLimitedPreemptions.task_last_nps /NondecreasingSequence.last -nth_last.
{ rewrite /ModelWithLimitedPreemptions.task_last_nps /last0 -nth_last.
apply HYP3; try by done.
rewrite -(ltn_add2r 1) !addn1 prednK //.
move: (Fact2) => Fact3.
by rewrite NondecreasingSequence.size_of_seq_of_distances // addn1 ltnS // in Fact2.
by rewrite size_of_seq_of_distances // addn1 ltnS // in Fact2.
}
{ apply leq_trans with (task_max_nps tsk).
- by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
- by apply last_of_seq_le_max_of_seq.
- rewrite -END; last by done.
apply ltnW; rewrite ltnS; try done.
by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
}
}
Qed.
......@@ -559,10 +559,10 @@ Module RTAforConcreteModels.
rewrite subn1 -(leq_add2r 1) !addn1 prednK; last first.
apply LSMj; try done.
rewrite /job_last_nps /ModelWithLimitedPreemptions.job_last_nps
ltnS /NondecreasingSequence.last -nth_last NondecreasingSequence.function_of_distances_is_correct.
apply leq_trans with (job_max_nps j); first by apply NondecreasingSequence.distance_between_neighboring_elements_le_max_distance_in_seq.
ltnS /last0 -nth_last function_of_distances_is_correct.
apply leq_trans with (job_max_nps j); first by apply distance_between_neighboring_elements_le_max_distance_in_seq.
rewrite -END; last by done.
by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
}
{ by intros j ARR; rewrite leq_subLR leq_addl. }
{ intros ? ? ? ARR LE LS NCOMPL.
......@@ -588,9 +588,9 @@ Module RTAforConcreteModels.
}
clear LS.
rewrite -END in NEQ, SERV; last by done.
rewrite NondecreasingSequence.last_seq_minus_last_distance_seq in NEQ.
rewrite /NondecreasingSequence.last -nth_last in SERV.
have EQ := NondecreasingSequence.antidensity_of_nondecreasing_seq.
rewrite last_seq_minus_last_distance_seq in NEQ.
rewrite /last0 -nth_last in SERV.
have EQ := antidensity_of_nondecreasing_seq.
specialize (EQ (job_preemption_points j) (service sched j (t + Δ)) (size (job_preemption_points j)).-2).
rewrite CONTR in EQ.
feed_n 2 EQ; first by eauto 2.
......@@ -605,8 +605,8 @@ Module RTAforConcreteModels.
eauto 2.
rewrite -END; last by done.
apply leq_trans with (job_max_nps j).
- by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
- by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
- by apply last_of_seq_le_max_of_seq.
- by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
}
}
{
......
classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
+ 32
− 32
View file @ 1bd6d79c
......@@ -304,7 +304,7 @@ Module RTAforConcreteModels.
{ have Fact2: 0 < size (task_preemption_points tsk).
{ apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; move: CONTR => /eqP CONTR.
move: (END _ H_tsk_in_ts) => EQ.
move: EQ; rewrite /NondecreasingSequence.last -nth_last nth_default; last by rewrite CONTR.
move: EQ; rewrite /last0 -nth_last nth_default; last by rewrite CONTR.
by intros; rewrite -EQ in POSt.
}
have EQ: 2 = size [::0; task_cost tsk]; first by done.
......@@ -320,14 +320,14 @@ Module RTAforConcreteModels.
{ rewrite EQ; clear EQ.
move: (BEG _ H_tsk_in_ts) => EQ.
rewrite -EQ; clear EQ.
rewrite /NondecreasingSequence.first -nth0.
rewrite /first0 -nth0.
apply/(nthP 0).
exists 0; by done.
}
{ rewrite EQ; clear EQ.
move: (END _ H_tsk_in_ts) => EQ.
rewrite -EQ; clear EQ.
rewrite /NondecreasingSequence.last -nth_last.
rewrite /last0 -nth_last.
apply/(nthP 0).
exists ((size (task_preemption_points tsk)).-1); last by done.
by rewrite -(leq_add2r 1) !addn1 prednK //.
......@@ -344,7 +344,7 @@ Module RTAforConcreteModels.
eapply model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions; eauto 2.
intros j ARR.
unfold ModelWithLimitedPreemptions.job_max_nps, task_max_nps, lengths_of_segments.
apply NondecreasingSequence.max_of_dominating_seq.
apply max_of_dominating_seq.
intros. apply HYP2.
by done.
}
......@@ -354,11 +354,11 @@ Module RTAforConcreteModels.
rewrite subn1 -(leq_add2r 1) !addn1 prednK; last first.
apply LSMj; try done.
rewrite /job_last_nps /ModelWithLimitedPreemptions.job_last_nps
ltnS /NondecreasingSequence.last -nth_last NondecreasingSequence.function_of_distances_is_correct.
ltnS /last0 -nth_last function_of_distances_is_correct.
apply leq_trans with (job_max_nps j);
first by apply NondecreasingSequence.distance_between_neighboring_elements_le_max_distance_in_seq.
first by apply distance_between_neighboring_elements_le_max_distance_in_seq.
rewrite -ENDj; last by done.
by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
}
{ by intros j ARR; rewrite leq_subLR leq_addl. }
{ intros ? ? ? ARR LE LS NCOMPL.
......@@ -383,9 +383,9 @@ Module RTAforConcreteModels.
}
clear LS.
rewrite -ENDj in NEQ, SERV; last by done.
rewrite NondecreasingSequence.last_seq_minus_last_distance_seq in NEQ; last by eauto 2.
rewrite /NondecreasingSequence.last -nth_last in SERV.
have EQ := NondecreasingSequence.antidensity_of_nondecreasing_seq.
rewrite last_seq_minus_last_distance_seq in NEQ; last by eauto 2.
rewrite /last0 -nth_last in SERV.
have EQ := antidensity_of_nondecreasing_seq.
specialize (EQ (job_preemption_points j) (service sched j (t + Δ)) (size (job_preemption_points j)).-2).
rewrite CONTR in EQ.
feed_n 2 EQ; first by eauto 2.
......@@ -400,8 +400,8 @@ Module RTAforConcreteModels.
rewrite -ENDj; last by done.
apply leq_trans with (job_max_nps j).
- by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
- by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
- by apply last_of_seq_le_max_of_seq.
- by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
}
}
{
......@@ -413,31 +413,31 @@ Module RTAforConcreteModels.
unfold task_last_nps.
rewrite !subnBA; first last.
apply LSMj; try done.
rewrite /ModelWithLimitedPreemptions.task_last_nps /NondecreasingSequence.last -nth_last.
rewrite /ModelWithLimitedPreemptions.task_last_nps /last0 -nth_last.
apply HYP3.
by done.
rewrite -(ltn_add2r 1) !addn1 prednK //.
move: (Fact2) => Fact3.
rewrite NondecreasingSequence.size_of_seq_of_distances // addn1 ltnS // in Fact2.
rewrite size_of_seq_of_distances // addn1 ltnS // in Fact2.
rewrite -subh1 -?[in X in _ <= X]subh1; first last.
{ apply leq_trans with (job_max_nps j).
- by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
- by rewrite -ENDj //; apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
- by apply last_of_seq_le_max_of_seq.
- by rewrite -ENDj //; apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
}
{ apply leq_trans with (task_max_nps tsk).
- by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
- by rewrite -END //; apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
- by apply last_of_seq_le_max_of_seq.
- by rewrite -END //; apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
}
rewrite -ENDj; last eauto 2.
rewrite -END; last eauto 2.
rewrite !NondecreasingSequence.last_seq_minus_last_distance_seq.
rewrite !last_seq_minus_last_distance_seq.
have EQ: size (job_preemption_points j) = size (task_preemption_points tsk).
{ rewrite -TSK.
by apply HYP1.
}
rewrite EQ; clear EQ.
rewrite leq_add2r.
apply NondecreasingSequence.domination_of_distances_implies_domination_of_seq; try done; eauto 2.
apply domination_of_distances_implies_domination_of_seq; try done; eauto 2.
rewrite BEG // BEGj //.
eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2.
rewrite -TSK; apply HYP1; try done.
......@@ -447,17 +447,17 @@ Module RTAforConcreteModels.
}
{ rewrite subKn; first by done.
rewrite /task_last_nps -(leq_add2r 1) subn1 !addn1 prednK; last first.
{ rewrite /ModelWithLimitedPreemptions.task_last_nps /NondecreasingSequence.last -nth_last.
{ rewrite /ModelWithLimitedPreemptions.task_last_nps /last0 -nth_last.
apply HYP3; try by done.
rewrite -(ltn_add2r 1) !addn1 prednK //.
move: (Fact2) => Fact3.
by rewrite NondecreasingSequence.size_of_seq_of_distances // addn1 ltnS // in Fact2.
by rewrite size_of_seq_of_distances // addn1 ltnS // in Fact2.
}
{ apply leq_trans with (task_max_nps tsk).
- by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
- by apply last_of_seq_le_max_of_seq.
- rewrite -END; last by done.
apply ltnW; rewrite ltnS; try done.
by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
}
}
Qed.
......@@ -535,10 +535,10 @@ Module RTAforConcreteModels.
rewrite subn1 -(leq_add2r 1) !addn1 prednK; last first.
apply LSMj; try done.
rewrite /job_last_nps /ModelWithLimitedPreemptions.job_last_nps
ltnS /NondecreasingSequence.last -nth_last NondecreasingSequence.function_of_distances_is_correct.
apply leq_trans with (job_max_nps j); first by apply NondecreasingSequence.distance_between_neighboring_elements_le_max_distance_in_seq.
ltnS /last0 -nth_last function_of_distances_is_correct.
apply leq_trans with (job_max_nps j); first by apply distance_between_neighboring_elements_le_max_distance_in_seq.
rewrite -END; last by done.
by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
}
{ by intros j ARR; rewrite leq_subLR leq_addl. }
{ intros ? ? ? ARR LE LS NCOMPL.
......@@ -563,9 +563,9 @@ Module RTAforConcreteModels.
}
clear LS.
rewrite -END in NEQ, SERV; last by done.
rewrite NondecreasingSequence.last_seq_minus_last_distance_seq in NEQ.
rewrite /NondecreasingSequence.last -nth_last in SERV.
have EQ := NondecreasingSequence.antidensity_of_nondecreasing_seq.
rewrite last_seq_minus_last_distance_seq in NEQ.
rewrite /last0 -nth_last in SERV.
have EQ := antidensity_of_nondecreasing_seq.
specialize (EQ (job_preemption_points j) (service sched j (t + Δ)) (size (job_preemption_points j)).-2).
rewrite CONTR in EQ.
feed_n 2 EQ; first by eauto 2.
......@@ -581,8 +581,8 @@ Module RTAforConcreteModels.
rewrite -END; last by done.
apply leq_trans with (job_max_nps j).
- by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
- by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
- by apply last_of_seq_le_max_of_seq.
- by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
}
}
{
......
classic/model/schedule/uni/limited/platform/limited.v
+ 15
− 15
View file @ 1bd6d79c
......@@ -2,7 +2,7 @@ Require Import rt.classic.util.all.
Require Import rt.classic.model.arrival.basic.job rt.classic.model.arrival.basic.task.
Require Import rt.classic.model.schedule.uni.schedule.
Require Export rt.classic.model.schedule.uni.limited.platform.definitions.
Require Export rt.classic.model.schedule.uni.limited.platform.util.
Require Export rt.util.nondecreasing.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......@@ -13,7 +13,7 @@ From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype
model with floating nonpreemptive regions. *)
Module ModelWithLimitedPreemptions.
Import Job NondecreasingSequence UniprocessorSchedule LimitedPreemptionPlatform.
Import Job UniprocessorSchedule LimitedPreemptionPlatform.
(* In this section, we instantiate can_be_preempted for the model with fixed preemption points and
the model with floating nonpreemptive regions. We also prove that the definitions are correct. *)
......@@ -46,11 +46,11 @@ Module ModelWithLimitedPreemptions.
(* Next, we define a function that maps a job to the
length of the longest nonpreemptive segment of job j. *)
Definition job_max_nps (j: Job) := max (lengths_of_segments j).
Definition job_max_nps (j : Job) := max0 (lengths_of_segments j).
(* Similarly, job_last is a function that maps a job to the
length of the last nonpreemptive segment. *)
Definition job_last_nps (j: Job) := last (lengths_of_segments j).
Definition job_last_nps (j : Job) := last0 (lengths_of_segments j).
(* Next, we describe some structural properties that
a sequence of preemption points should satisfy. *)
......@@ -65,11 +65,11 @@ Module ModelWithLimitedPreemptions.
(* (3) We also require the sequence of preemption points to contain the beginning... *)
Definition beginning_of_execution_in_preemption_points :=
forall j, arrives_in arr_seq j -> first (job_preemption_points j) = 0.
forall j, arrives_in arr_seq j -> first0 (job_preemption_points j) = 0.
(* ... and (4) the end of execution for any job j.*)
Definition end_of_execution_in_preemption_points :=
forall j, arrives_in arr_seq j -> last (job_preemption_points j) = job_cost j.
forall j, arrives_in arr_seq j -> last0 (job_preemption_points j) = job_cost j.
(* (5) We require the sequence of preemption points to be a nondecreasing sequence. *)
Definition preemption_points_is_nondecreasing_sequence :=
......@@ -96,8 +96,8 @@ Module ModelWithLimitedPreemptions.
(* Similarly to job's nonpreemptive segments, we define the length of the max
nonpreemptive segment and lenght of the last nonpreemptive segment. *)
Definition task_last_nps tsk := last (distances (task_preemption_points tsk)).
Definition task_max_nps tsk := max (distances (task_preemption_points tsk)).
Definition task_last_nps tsk := last0 (distances (task_preemption_points tsk)).
Definition task_max_nps tsk := max0 (distances (task_preemption_points tsk)).
(* Consider an arbitrary task set ts. *)
Variable ts: list Task.
......@@ -107,11 +107,11 @@ Module ModelWithLimitedPreemptions.
(* (1) We require the sequence of preemption points to contain the beginning... *)
Definition task_beginning_of_execution_in_preemption_points :=
forall tsk, tsk \in ts -> first (task_preemption_points tsk) = 0.
forall tsk, tsk \in ts -> first0 (task_preemption_points tsk) = 0.
(* ... and (2) the end of execution for any job j.*)
Definition task_end_of_execution_in_preemption_points :=
forall tsk, tsk \in ts -> last (task_preemption_points tsk) = task_cost tsk.
forall tsk, tsk \in ts -> last0 (task_preemption_points tsk) = task_cost tsk.
(* (3) We require the sequence of preemption points
to be a nondecreasing sequence. *)
......@@ -239,7 +239,7 @@ Module ModelWithLimitedPreemptions.
{ by specialize (EMPT j H_j_arrives ZERO); rewrite EMPT. }
apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; move: CONTR => /eqP CONTR.
move: (END _ H_j_arrives) => EQ.
move: EQ; rewrite /last -nth_last nth_default; last by rewrite CONTR.
move: EQ; rewrite /last0 -nth_last nth_default; last by rewrite CONTR.
intros.
by rewrite /job_cost_positive -EQ in POS.
Qed.
......@@ -250,7 +250,7 @@ Module ModelWithLimitedPreemptions.
move: H_limited_preemptions_job_model => [EMPT [LS [BEG [END _]]]].
move: (BEG _ H_j_arrives) => EQ.
rewrite -EQ; clear EQ.
rewrite /first -nth0.
rewrite /first0 -nth0.
apply/(nthP 0).
exists 0.
- by apply list_of_preemption_point_is_not_empty.
......@@ -263,7 +263,7 @@ Module ModelWithLimitedPreemptions.
move: H_limited_preemptions_job_model => [EMPT [LS [BEG [END _]]]].
move: (END _ H_j_arrives) => EQ.
rewrite -EQ; clear EQ.
rewrite /last -nth_last.
rewrite /last0 -nth_last.
apply/(nthP 0).
exists ((size (job_preemption_points j)).-1); last by done.
rewrite -(leq_add2r 1) !addn1 prednK //.
......@@ -348,9 +348,9 @@ Module ModelWithLimitedPreemptions.
}
set (preemptions := job_preemption_points j).
set (serv := progr).
have Fact1: job_cost j <= last preemptions.
have Fact1: job_cost j <= last0 preemptions.
{ by apply last_is_max_in_nondecreasing_seq; eauto 2; apply job_cost_in_nonpreemptive_points. }
have Fact2: first preemptions <= serv < last preemptions.
have Fact2: first0 preemptions <= serv < last0 preemptions.
{ apply/andP; split.
- by rewrite /preemptions BEG.
- rewrite /serv /preemptions END; last by done.
......
classic/model/schedule/uni/limited/platform/util.v deleted 100644 → 0
+ 0
− 684
View file @ df7fe9d2
This diff is collapsed.
util/all.v
+ 1
− 0
View file @ 1bd6d79c
......@@ -12,4 +12,5 @@ Require Export rt.util.step_function.
Require Export rt.util.epsilon.
Require Export rt.util.search_arg.
Require Export rt.util.rel.
Require Export rt.util.nondecreasing.
Require Export rt.util.rewrite_facilities.
util/nondecreasing.v 0 → 100644
+ 905
− 0
View file @ 1bd6d79c
This diff is collapsed.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment