Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.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.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
(** * Preemptions in Fully Preemptive Model *) (** In this section, we prove that instantiation of predicate [job_preemptable] to the fully preemptive model indeed defines a valid preemption model. *) Section FullyPreemptiveModel. (** We assume that jobs are fully preemptive. *) #[local] Existing Instance fully_preemptive_job_model. (** Consider any type of jobs. *) Context {Job : JobType}. Context `{JobArrival Job}. Context `{JobCost Job}. (** Consider any kind of processor state model, ... *) Context {PState : ProcessorState Job}. (** ... any job arrival sequence, ... *) Variable arr_seq : arrival_sequence Job. (** ... and any given schedule. *) Variable sched : schedule PState. (** Then, we prove that fully_preemptive_model is a valid preemption model. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState

valid_preemption_model arr_seq sched
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState

valid_preemption_model arr_seq sched
by intros j ARR; repeat split; intros t CONTR. Qed. (** We also prove that under the fully preemptive model [job_max_nonpreemptive_segment j] is equal to 0, when [job_cost j = 0] ... *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState

forall j : Job, job_cost j = 0 -> job_max_nonpreemptive_segment j = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState

forall j : Job, job_cost j = 0 -> job_max_nonpreemptive_segment j = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
H1: job_cost j = 0

job_max_nonpreemptive_segment j = 0
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
H1: job_cost j = 0

max0 (distances [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]) = 0
by rewrite H1; compute. Qed. (** ... or ε when [job_cost j > 0]. *)
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState

forall j : Job, 0 < job_cost j -> job_max_nonpreemptive_segment j = ε
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState

forall j : Job, 0 < job_cost j -> job_max_nonpreemptive_segment j = ε
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j

job_max_nonpreemptive_segment j = ε
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j

max0 (distances [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]) = ε
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j

max0 (distances [seq _ <- range 0 (job_cost j) | true]) = ε
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j

max0 (distances (range 0 (job_cost j))) = ε
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j

0 < size (distances (range 0 (job_cost j)))
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j

0 < size (distances (range 0 (job_cost j)))
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j

0 < size (distances (iota 0 (job_cost j).+1))
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j

0 < (job_cost j).+1.-1
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
1 < (job_cost j).+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j

0 < (job_cost j).+1.-1
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
1 < (job_cost j).+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j

1 < (job_cost j).+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j

1 < (job_cost j).+1
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j

forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j

forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε
by apply distances_of_iota_ε. Qed. End FullyPreemptiveModel. Global Hint Resolve valid_fully_preemptive_model : basic_rt_facts.