Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.facts.behavior.all .[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.model.schedule.nonpreemptive.
Require Export prosa.model.preemption.fully_nonpreemptive.
(** * Platform for Fully Non-Preemptive model *)
(** In this section, we prove that instantiation of predicate
[job_preemptable] to the fully non-preemptive model indeed
defines a valid preemption model. *)
Section FullyNonPreemptiveModel .
(** Consider any type of jobs. *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** We assume that jobs are fully non-preemptive. *)
#[local] Existing Instance fully_nonpreemptive_job_model .
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(** Next, consider any non-preemptive unit-service schedule of the arrival sequence ... *)
Context {PState : ProcessorState Job}.
Hypothesis H_unit_service : unit_service_proc_model PState.
Variable sched : schedule PState.
Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Then, we prove that fully_nonpreemptive_model is a valid preemption model. *)
Lemma valid_fully_nonpreemptive_model :
valid_preemption_model arr_seq sched.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched
valid_preemption_model arr_seq sched
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched
valid_preemption_model arr_seq sched
move => j _; split ; [by apply /orP; left | split ; [by apply /orP; right | split ]].Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job
not_preemptive_implies_scheduled sched j
- Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job
not_preemptive_implies_scheduled sched j
move => t; rewrite /job_preemptable /fully_nonpreemptive_job_model Bool.negb_orb -lt0n; move => /andP [POS NCOMPL].Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant POS : 0 < service sched j tNCOMPL : service sched j t != job_cost j
scheduled_at sched j t
move : (incremental_service_during _ H_unit_service _ _ _ _ POS) => [ft [/andP [_ LT] [SCHED SERV]]].Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant POS : 0 < service sched j tNCOMPL : service sched j t != job_cost j ft : nat LT : ft < t SCHED : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
scheduled_at sched j t
apply H_nonpreemptive_sched with ft.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant POS : 0 < service sched j tNCOMPL : service sched j t != job_cost j ft : nat LT : ft < t SCHED : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
ft <= t
+ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant POS : 0 < service sched j tNCOMPL : service sched j t != job_cost j ft : nat LT : ft < t SCHED : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
ft <= t
by apply ltnW.
+ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant POS : 0 < service sched j tNCOMPL : service sched j t != job_cost j ft : nat LT : ft < t SCHED : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
scheduled_at sched j ft
by [].
+ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant POS : 0 < service sched j tNCOMPL : service sched j t != job_cost j ft : nat LT : ft < t SCHED : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
~~ completed_by sched j t
rewrite /completed_by -ltnNge.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant POS : 0 < service sched j tNCOMPL : service sched j t != job_cost j ft : nat LT : ft < t SCHED : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
service sched j t < job_cost j
move : NCOMPL; rewrite neq_ltn; move => /orP [//|GE]; exfalso .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant POS : 0 < service sched j tft : nat LT : ft < t SCHED : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0 GE : job_cost j < service sched j t
False
move : GE; rewrite ltnNge; move => /negP GE; apply : GE.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant POS : 0 < service sched j tft : nat LT : ft < t SCHED : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
service sched j t <= job_cost j
exact : completion.service_at_most_cost.
- Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job
execution_starts_with_preemption_point sched j
intros t NSCHED SCHED.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant NSCHED : ~~ scheduled_at sched j t SCHED : scheduled_at sched j t.+1
job_preemptable j (service sched j t.+1 )
rewrite /job_preemptable /fully_nonpreemptive_job_model.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant NSCHED : ~~ scheduled_at sched j t SCHED : scheduled_at sched j t.+1
(service sched j t.+1 == 0 )
|| (service sched j t.+1 == job_cost j)
apply /orP; left .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant NSCHED : ~~ scheduled_at sched j t SCHED : scheduled_at sched j t.+1
service sched j t.+1 == 0
apply /negP; intros CONTR; move : CONTR => /negP; rewrite -lt0n; intros POS.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant NSCHED : ~~ scheduled_at sched j t SCHED : scheduled_at sched j t.+1 POS : 0 < service sched j t.+1
False
move : (incremental_service_during _ H_unit_service _ _ _ _ POS) => [ft [/andP [_ LT] [SCHEDn SERV]]].Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant NSCHED : ~~ scheduled_at sched j t SCHED : scheduled_at sched j t.+1 POS : 0 < service sched j t.+1 ft : nat LT : ft < t.+1 SCHEDn : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
False
move : NSCHED => /negP NSCHED; apply : NSCHED.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant SCHED : scheduled_at sched j t.+1 POS : 0 < service sched j t.+1 ft : nat LT : ft < t.+1 SCHEDn : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
scheduled_at sched j t
apply H_nonpreemptive_sched with ft.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant SCHED : scheduled_at sched j t.+1 POS : 0 < service sched j t.+1 ft : nat LT : ft < t.+1 SCHEDn : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
ft <= t
+ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant SCHED : scheduled_at sched j t.+1 POS : 0 < service sched j t.+1 ft : nat LT : ft < t.+1 SCHEDn : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
ft <= t
by rewrite -ltnS.
+ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant SCHED : scheduled_at sched j t.+1 POS : 0 < service sched j t.+1 ft : nat LT : ft < t.+1 SCHEDn : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
scheduled_at sched j ft
by [].
+ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant SCHED : scheduled_at sched j t.+1 POS : 0 < service sched j t.+1 ft : nat LT : ft < t.+1 SCHEDn : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
~~ completed_by sched j t
rewrite /completed_by -ltnNge.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant SCHED : scheduled_at sched j t.+1 POS : 0 < service sched j t.+1 ft : nat LT : ft < t.+1 SCHEDn : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
service sched j t < job_cost j
apply leq_ltn_trans with (service sched j t.+1 ).Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant SCHED : scheduled_at sched j t.+1 POS : 0 < service sched j t.+1 ft : nat LT : ft < t.+1 SCHEDn : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
service sched j t <= service sched j t.+1
* Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant SCHED : scheduled_at sched j t.+1 POS : 0 < service sched j t.+1 ft : nat LT : ft < t.+1 SCHEDn : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
service sched j t <= service sched j t.+1
by rewrite /service /service_during big_nat_recr //= leq_addr.
* Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job t : instant SCHED : scheduled_at sched j t.+1 POS : 0 < service sched j t.+1 ft : nat LT : ft < t.+1 SCHEDn : scheduled_at sched j ft SERV : service_during sched j 0 ft = 0
service sched j t.+1 < job_cost j
by apply H_completed_jobs_dont_execute.
Qed .
(** We also prove that under the fully non-preemptive model
[job_max_nonpreemptive_segment j] is equal to [job_cost j] ... *)
Lemma job_max_nps_is_job_cost :
forall j , job_max_nonpreemptive_segment j = job_cost j.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched
forall j : Job,
job_max_nonpreemptive_segment j = job_cost j
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched
forall j : Job,
job_max_nonpreemptive_segment j = job_cost j
move => j.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job
job_max_nonpreemptive_segment j = job_cost j
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points /job_preemptable /fully_nonpreemptive_job_model.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job
max0
(distances
[seq ρ <- range 0 (job_cost j)
| (ρ == 0 ) || (ρ == job_cost j)]) = job_cost j
case : (posnP (job_cost j)) => [ZERO|POS].Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job ZERO : job_cost j = 0
max0
(distances
[seq ρ <- range 0 (job_cost j)
| (ρ == 0 ) || (ρ == job_cost j)]) = job_cost j
{ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job ZERO : job_cost j = 0
max0
(distances
[seq ρ <- range 0 (job_cost j)
| (ρ == 0 ) || (ρ == job_cost j)]) = job_cost j
by rewrite ZERO; compute . } Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job POS : 0 < job_cost j
max0
(distances
[seq ρ <- range 0 (job_cost j)
| (ρ == 0 ) || (ρ == job_cost j)]) = job_cost j
have ->: forall n , n>0 -> [seq ρ <- index_iota 0 n.+1 | (ρ == 0 ) || (ρ == n)] = [:: 0 ; n].Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job POS : 0 < job_cost j
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 n.+1 | (ρ == 0 ) || (ρ == n)] =
[:: 0 ; n]
{ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job POS : 0 < job_cost j
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 n.+1 | (ρ == 0 ) || (ρ == n)] =
[:: 0 ; n]
clear ; simpl ; intros .n : nat H : 0 < n
0 :: [seq ρ <- iota 1 n | (ρ == 0 ) || (ρ == n)] =
[:: 0 ; n]
apply /eqP; rewrite eqseq_cons; apply /andP; split => [//|].n : nat H : 0 < n
[seq ρ <- iota 1 n | (ρ == 0 ) || (ρ == n)] == [:: n]
have ->: forall xs P1 P2 , (forall x , x \in xs -> ~~ P1 x) -> [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x].n : nat H : 0 < n
forall (t : eqType) (xs : seq_predType t)
(P1 P2 : t -> bool),
(forall x : t, x \in xs -> ~~ P1 x) ->
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
{ n : nat H : 0 < n
forall (t : eqType) (xs : seq_predType t)
(P1 P2 : t -> bool),
(forall x : t, x \in xs -> ~~ P1 x) ->
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
clear ; move => t xs P1 P2 H.t : eqType xs : seq_predType t P1, P2 : t -> bool H : forall x : t, x \in xs -> ~~ P1 x
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
apply eq_in_filter.t : eqType xs : seq_predType t P1, P2 : t -> bool H : forall x : t, x \in xs -> ~~ P1 x
{in xs, (fun x : t => P1 x || P2 x) =1 [eta P2]}
move => x IN.t : eqType xs : seq_predType t P1, P2 : t -> bool H : forall x : t, x \in xs -> ~~ P1 xx : t IN : x \in xs
P1 x || P2 x = P2 x
specialize (H _ IN).t : eqType xs : seq_predType t P1, P2 : t -> bool x : t H : ~~ P1 x IN : x \in xs
P1 x || P2 x = P2 x
by destruct (P1 x), (P2 x).
} n : nat H : 0 < n
[seq x <- iota 1 n | x == n] == [:: n]
- n : nat H : 0 < n
[seq x <- iota 1 n | x == n] == [:: n]
rewrite filter_pred1_uniq//; first by apply iota_uniq.n : nat H : 0 < n
n \in iota 1 n
by rewrite mem_iota; apply /andP; split ; [|rewrite add1n].
- n : nat H : 0 < n
forall x : Datatypes_nat__canonical__eqtype_Equality,
x \in iota 1 n -> x != 0
intros x; rewrite mem_iota; move => /andP [POS _].n : nat H : 0 < nx : Datatypes_nat__canonical__eqtype_Equality POS : 0 < x
x != 0
by rewrite -lt0n.
} Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job POS : 0 < job_cost j
max0 (distances [:: 0 ; job_cost j]) = job_cost j
{ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job POS : 0 < job_cost j
max0 (distances [:: 0 ; job_cost j]) = job_cost j
by rewrite /distances/= subn0 /max0/= max0n. } Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job POS : 0 < job_cost j
0 < job_cost j
{ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job POS : 0 < job_cost j
0 < job_cost j
by []. }
Qed .
(** ... and [job_last_nonpreemptive_segment j] is equal to [job_cost j]. *)
Lemma job_last_nps_is_job_cost :
forall j , job_last_nonpreemptive_segment j = job_cost j.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched
forall j : Job,
job_last_nonpreemptive_segment j = job_cost j
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched
forall j : Job,
job_last_nonpreemptive_segment j = job_cost j
move => j.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job
job_last_nonpreemptive_segment j = job_cost j
rewrite /job_last_nonpreemptive_segment /lengths_of_segments
/job_preemption_points /job_preemptable /fully_nonpreemptive_job_model.Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job
last0
(distances
[seq ρ <- range 0 (job_cost j)
| (ρ == 0 ) || (ρ == job_cost j)]) = job_cost j
case : (posnP (job_cost j)) => [ZERO|POS]; first by rewrite ZERO; compute .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job POS : 0 < job_cost j
last0
(distances
[seq ρ <- range 0 (job_cost j)
| (ρ == 0 ) || (ρ == job_cost j)]) = job_cost j
have ->: forall n , n>0 -> [seq ρ <- index_iota 0 n.+1 | (ρ == 0 ) || (ρ == n)] = [:: 0 ; n]; last by done .Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job POS : 0 < job_cost j
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 n.+1 | (ρ == 0 ) || (ρ == n)] =
[:: 0 ; n]
{ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job POS : 0 < job_cost j
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 n.+1 | (ρ == 0 ) || (ρ == n)] =
[:: 0 ; n]
clear ; simpl ; intros .n : nat H : 0 < n
0 :: [seq ρ <- iota 1 n | (ρ == 0 ) || (ρ == n)] =
[:: 0 ; n]
apply /eqP; rewrite eqseq_cons; apply /andP; split => [//|].n : nat H : 0 < n
[seq ρ <- iota 1 n | (ρ == 0 ) || (ρ == n)] == [:: n]
have ->: forall xs P1 P2 , (forall x , x \in xs -> ~~ P1 x) -> [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x].n : nat H : 0 < n
forall (t : eqType) (xs : seq_predType t)
(P1 P2 : t -> bool),
(forall x : t, x \in xs -> ~~ P1 x) ->
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
{ n : nat H : 0 < n
forall (t : eqType) (xs : seq_predType t)
(P1 P2 : t -> bool),
(forall x : t, x \in xs -> ~~ P1 x) ->
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
clear ; move => t xs P1 P2 H.t : eqType xs : seq_predType t P1, P2 : t -> bool H : forall x : t, x \in xs -> ~~ P1 x
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
apply eq_in_filter.t : eqType xs : seq_predType t P1, P2 : t -> bool H : forall x : t, x \in xs -> ~~ P1 x
{in xs, (fun x : t => P1 x || P2 x) =1 [eta P2]}
move => x IN.t : eqType xs : seq_predType t P1, P2 : t -> bool H : forall x : t, x \in xs -> ~~ P1 xx : t IN : x \in xs
P1 x || P2 x = P2 x
specialize (H _ IN).t : eqType xs : seq_predType t P1, P2 : t -> bool x : t H : ~~ P1 x IN : x \in xs
P1 x || P2 x = P2 x
by destruct (P1 x), (P2 x).
} n : nat H : 0 < n
[seq x <- iota 1 n | x == n] == [:: n]
- n : nat H : 0 < n
[seq x <- iota 1 n | x == n] == [:: n]
rewrite filter_pred1_uniq //; first by apply iota_uniq.n : nat H : 0 < n
n \in iota 1 n
by rewrite mem_iota; apply /andP; split ; [|rewrite add1n].
- n : nat H : 0 < n
forall x : Datatypes_nat__canonical__eqtype_Equality,
x \in iota 1 n -> x != 0
intros x; rewrite mem_iota; move => /andP [POS _].n : nat H : 0 < nx : Datatypes_nat__canonical__eqtype_Equality POS : 0 < x
x != 0
by rewrite -lt0n.
} Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job POS : 0 < job_cost j
last0 (distances [:: 0 ; job_cost j]) = job_cost j
{ Job : JobType H : JobArrival Job H0 : JobCost Job arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times arr_seq PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState H_nonpreemptive_sched : nonpreemptive_schedule sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job POS : 0 < job_cost j
last0 (distances [:: 0 ; job_cost j]) = job_cost j
by rewrite /distances/= subn0. }
Qed .
End FullyNonPreemptiveModel .
Global Hint Resolve valid_fully_nonpreemptive_model : basic_rt_facts.
(** In this section, we prove the equivalence between no preemptions and a non-preemptive schedule. *)
Section NoPreemptionsEquivalence .
(** Consider any type of jobs with preemption points. *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any type of schedule. *)
Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
(** We prove that no preemptions in a schedule is equivalent to a non-preemptive schedule. *)
Lemma no_preemptions_equiv_nonpreemptive :
(forall j t , ~~preempted_at sched j t) <-> nonpreemptive_schedule sched.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState
(forall (j : Job) (t : instant),
~~ preempted_at sched j t) <->
nonpreemptive_schedule sched
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState
(forall (j : Job) (t : instant),
~~ preempted_at sched j t) <->
nonpreemptive_schedule sched
split .Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState
(forall (j : Job) (t : instant),
~~ preempted_at sched j t) ->
nonpreemptive_schedule sched
{ Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState
(forall (j : Job) (t : instant),
~~ preempted_at sched j t) ->
nonpreemptive_schedule sched
move => NOT_PREEMPTED j t t'.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NOT_PREEMPTED : forall (j : Job) (t : instant),
~~ preempted_at sched j tj : Job t, t' : instant
t <= t' ->
scheduled_at sched j t ->
~~ completed_by sched j t' -> scheduled_at sched j t'
elim : t'; first by rewrite leqn0 => /eqP ->.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NOT_PREEMPTED : forall (j : Job) (t : instant),
~~ preempted_at sched j tj : Job t : instant
forall n : nat,
(t <= n ->
scheduled_at sched j t ->
~~ completed_by sched j n -> scheduled_at sched j n) ->
t <= n.+1 ->
scheduled_at sched j t ->
~~ completed_by sched j n.+1 ->
scheduled_at sched j n.+1
move => t' IH LE_tt' SCHEDULED INCOMP.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NOT_PREEMPTED : forall (j : Job) (t : instant),
~~ preempted_at sched j tj : Job t : instant t' : nat IH : t <= t' ->
scheduled_at sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' LE_tt' : t <= t'.+1 SCHEDULED : scheduled_at sched j t INCOMP : ~~ completed_by sched j t'.+1
scheduled_at sched j t'.+1
apply contraT => NOT_SCHEDULED'.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NOT_PREEMPTED : forall (j : Job) (t : instant),
~~ preempted_at sched j tj : Job t : instant t' : nat IH : t <= t' ->
scheduled_at sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' LE_tt' : t <= t'.+1 SCHEDULED : scheduled_at sched j t INCOMP : ~~ completed_by sched j t'.+1 NOT_SCHEDULED' : ~~ scheduled_at sched j t'.+1
false
move : LE_tt'.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NOT_PREEMPTED : forall (j : Job) (t : instant),
~~ preempted_at sched j tj : Job t : instant t' : nat IH : t <= t' ->
scheduled_at sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' SCHEDULED : scheduled_at sched j t INCOMP : ~~ completed_by sched j t'.+1 NOT_SCHEDULED' : ~~ scheduled_at sched j t'.+1
t <= t'.+1 -> false
rewrite leq_eqVlt => /orP [/eqP EQ |];
first by move : NOT_SCHEDULED' SCHEDULED; rewrite -EQ => /negP //.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NOT_PREEMPTED : forall (j : Job) (t : instant),
~~ preempted_at sched j tj : Job t : instant t' : nat IH : t <= t' ->
scheduled_at sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' SCHEDULED : scheduled_at sched j t INCOMP : ~~ completed_by sched j t'.+1 NOT_SCHEDULED' : ~~ scheduled_at sched j t'.+1
t < t'.+1 -> false
rewrite ltnS => LEQ.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NOT_PREEMPTED : forall (j : Job) (t : instant),
~~ preempted_at sched j tj : Job t : instant t' : nat IH : t <= t' ->
scheduled_at sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' SCHEDULED : scheduled_at sched j t INCOMP : ~~ completed_by sched j t'.+1 NOT_SCHEDULED' : ~~ scheduled_at sched j t'.+1 LEQ : t <= t'
false
have SCHEDULED': scheduled_at sched j t'
by apply IH, (incompletion_monotonic _ _ _ t'.+1 ) => //.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NOT_PREEMPTED : forall (j : Job) (t : instant),
~~ preempted_at sched j tj : Job t : instant t' : nat IH : t <= t' ->
scheduled_at sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' SCHEDULED : scheduled_at sched j t INCOMP : ~~ completed_by sched j t'.+1 NOT_SCHEDULED' : ~~ scheduled_at sched j t'.+1 LEQ : t <= t' SCHEDULED' : scheduled_at sched j t'
false
move : (NOT_PREEMPTED j t'.+1 ).Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NOT_PREEMPTED : forall (j : Job) (t : instant),
~~ preempted_at sched j tj : Job t : instant t' : nat IH : t <= t' ->
scheduled_at sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' SCHEDULED : scheduled_at sched j t INCOMP : ~~ completed_by sched j t'.+1 NOT_SCHEDULED' : ~~ scheduled_at sched j t'.+1 LEQ : t <= t' SCHEDULED' : scheduled_at sched j t'
~~ preempted_at sched j t'.+1 -> false
rewrite /preempted_at -pred_Sn -andbA negb_and => /orP [/negP //|].Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NOT_PREEMPTED : forall (j : Job) (t : instant),
~~ preempted_at sched j tj : Job t : instant t' : nat IH : t <= t' ->
scheduled_at sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' SCHEDULED : scheduled_at sched j t INCOMP : ~~ completed_by sched j t'.+1 NOT_SCHEDULED' : ~~ scheduled_at sched j t'.+1 LEQ : t <= t' SCHEDULED' : scheduled_at sched j t'
~~
(~~ completed_by sched j t'.+1 &&
~~ scheduled_at sched j t'.+1 ) -> false
rewrite negb_and => /orP [/negPn|/negPn].Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NOT_PREEMPTED : forall (j : Job) (t : instant),
~~ preempted_at sched j tj : Job t : instant t' : nat IH : t <= t' ->
scheduled_at sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' SCHEDULED : scheduled_at sched j t INCOMP : ~~ completed_by sched j t'.+1 NOT_SCHEDULED' : ~~ scheduled_at sched j t'.+1 LEQ : t <= t' SCHEDULED' : scheduled_at sched j t'
completed_by sched j t'.+1 -> false
- Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NOT_PREEMPTED : forall (j : Job) (t : instant),
~~ preempted_at sched j tj : Job t : instant t' : nat IH : t <= t' ->
scheduled_at sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' SCHEDULED : scheduled_at sched j t INCOMP : ~~ completed_by sched j t'.+1 NOT_SCHEDULED' : ~~ scheduled_at sched j t'.+1 LEQ : t <= t' SCHEDULED' : scheduled_at sched j t'
completed_by sched j t'.+1 -> false
by move : INCOMP => /negP.
- Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NOT_PREEMPTED : forall (j : Job) (t : instant),
~~ preempted_at sched j tj : Job t : instant t' : nat IH : t <= t' ->
scheduled_at sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' SCHEDULED : scheduled_at sched j t INCOMP : ~~ completed_by sched j t'.+1 NOT_SCHEDULED' : ~~ scheduled_at sched j t'.+1 LEQ : t <= t' SCHEDULED' : scheduled_at sched j t'
scheduled_at sched j t'.+1 -> false
by move : NOT_SCHEDULED' => /negP. } Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState
nonpreemptive_schedule sched ->
forall (j : Job) (t : instant),
~~ preempted_at sched j t
{ Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState
nonpreemptive_schedule sched ->
forall (j : Job) (t : instant),
~~ preempted_at sched j t
move => NONPRE j t.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NONPRE : nonpreemptive_schedule sched j : Job t : instant
~~ preempted_at sched j t
apply contraT => /negPn /andP [/andP [SCHED_PREV INCOMP] NOT_SCHED].Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NONPRE : nonpreemptive_schedule sched j : Job t : instant SCHED_PREV : scheduled_at sched j t.-1 INCOMP : ~~ completed_by sched j t NOT_SCHED : ~~ scheduled_at sched j t
false
have SCHED: scheduled_at sched j t
by apply : (NONPRE j t.-1 t) => //; apply leq_pred.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NONPRE : nonpreemptive_schedule sched j : Job t : instant SCHED_PREV : scheduled_at sched j t.-1 INCOMP : ~~ completed_by sched j t NOT_SCHED : ~~ scheduled_at sched j t SCHED : scheduled_at sched j t
false
contradict NOT_SCHED.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NONPRE : nonpreemptive_schedule sched j : Job t : instant SCHED_PREV : scheduled_at sched j t.-1 INCOMP : ~~ completed_by sched j t SCHED : scheduled_at sched j t
~ ~~ scheduled_at sched j t
apply /negP.Job : JobType H : JobArrival Job H0 : JobCost Job PState : ProcessorState Job sched : schedule PState NONPRE : nonpreemptive_schedule sched j : Job t : instant SCHED_PREV : scheduled_at sched j t.-1 INCOMP : ~~ completed_by sched j t SCHED : scheduled_at sched j t
~~ ~~ scheduled_at sched j t
by rewrite Bool.negb_involutive.
}
Qed .
End NoPreemptionsEquivalence .