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.
[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.model.task.preemption.fully_nonpreemptive. (** * Platform for Fully Non-Preemptive Model *) (** In this section, we prove that instantiation of functions [job_preemptable] and [task_max_nonpreemptive_segment] to the fully non-preemptive model indeed defines a valid preemption model with bounded non-preemptive regions. *) Section FullyNonPreemptiveModel. (** Consider any type of tasks ... *) Context {Task : TaskType}. Context `{TaskCost Task}. (** ... and any type of jobs associated with these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. Context `{JobCost Job}. (** Assume a fully non-preemptive task model. *) #[local] Existing Instance fully_nonpreemptive_job_model. #[local] Existing Instance fully_nonpreemptive_task_model. #[local] Existing Instance fully_nonpreemptive_rtc_threshold. (** 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. (** Assume that a job cost cannot be larger than a task cost. *) Hypothesis H_valid_job_cost: arrivals_have_valid_job_costs arr_seq. (** Then we prove that the [fully_nonpreemptive_model] function defines a model with bounded non-preemptive regions.*)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq

model_with_bounded_nonpreemptive_segments arr_seq
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq

model_with_bounded_nonpreemptive_segments arr_seq
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n

model_with_bounded_nonpreemptive_segments arr_seq
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j

job_respects_max_nonpreemptive_segment j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j

job_respects_max_nonpreemptive_segment j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j

job_max_nonpreemptive_segment j <= task_max_nonpreemptive_segment (job_task j)
erewrite job_max_nps_is_job_cost; eauto 2.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j

nonpreemptive_regions_have_bounded_length j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j

exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - 1) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
EQ: progr = 0

exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - 1) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - 1) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
EQ: progr = 0

exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - 1) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
EQ: progr = 0

progr <= progr <= progr + (job_max_nonpreemptive_segment j - 1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
EQ: progr = 0
job_preemptable j progr
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
EQ: progr = 0

progr <= progr <= progr + (job_max_nonpreemptive_segment j - 1)
by apply/andP; split; [|rewrite leq_addr].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
EQ: progr = 0

job_preemptable j progr
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
EQ: progr = 0

(progr == 0) || (progr == job_cost j)
by apply/orP; left; rewrite EQ.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr

exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - 1) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr

exists pp : duration, progr <= pp <= progr + (job_max_nonpreemptive_segment j - 1) /\ job_preemptable j pp
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr

progr <= maxn progr (job_cost j) <= progr + (job_max_nonpreemptive_segment j - 1) /\ job_preemptable j (maxn progr (job_cost j))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j

progr <= maxn progr (job_cost j) <= progr + (job_max_nonpreemptive_segment j - 1) /\ job_preemptable j (maxn progr (job_cost j))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j

progr <= maxn progr (job_cost j) <= progr + (job_max_nonpreemptive_segment j - 1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j
job_preemptable j (maxn progr (job_cost j))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j

progr <= maxn progr (job_cost j) <= progr + (job_max_nonpreemptive_segment j - 1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j

maxn progr (job_cost j) <= progr + (job_max_nonpreemptive_segment j - 1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j

maxn progr (job_cost j) <= progr + job_cost j - 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j

progr <= progr + job_cost j - 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j
job_cost j <= progr + job_cost j - 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j

progr <= progr + job_cost j - 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j

progr <= progr + (job_cost j - 1)
by rewrite leq_addr.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j

job_cost j <= progr + job_cost j - 1
by rewrite addnC -addnBA // leq_addr.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j

job_preemptable j (maxn progr (job_cost j))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j

job_preemptable j (maxn progr (job_cost j))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j

maxn progr (job_cost j) == job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j

maxn progr (job_cost j) <= job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j
job_cost j <= maxn progr (job_cost j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j

maxn progr (job_cost j) <= job_cost j
by rewrite geq_max; apply/andP; split.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
F: forall n : nat, n = 0 \/ 0 < n
j: Job
H3: arrives_in arr_seq j
progr: duration
GE: progr <= job_cost j
GT: 0 < progr
POS: 0 < job_cost j

job_cost j <= maxn progr (job_cost j)
by rewrite leq_max; apply/orP; right. } } Qed. (** Which together with lemma [valid_fully_nonpreemptive_model] gives us the fact that [fully_nonpreemptive_model] defined a valid preemption model with bounded non-preemptive regions. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq

valid_model_with_bounded_nonpreemptive_segments arr_seq sched
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq

valid_model_with_bounded_nonpreemptive_segments arr_seq sched
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq

valid_preemption_model arr_seq sched
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
model_with_bounded_nonpreemptive_segments arr_seq
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq

valid_preemption_model arr_seq sched
by apply valid_fully_nonpreemptive_model.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: 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
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq

model_with_bounded_nonpreemptive_segments arr_seq
by apply fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions. Qed. End FullyNonPreemptiveModel. (** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *) Global Hint Resolve valid_fully_nonpreemptive_model fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions fully_nonpreemptive_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_rt_facts.