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]
(** * Job Arrival Times in the Sporadic Model *)(** In this file, we prove basic facts about the arrival times of jobs in the sporadic task model. *)SectionArrivalTimes.(** Consider sporadic tasks ... *)Context {Task : TaskType} `{SporadicModel Task}.(** ... and any type of jobs associated with these tasks. *)Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.(** Consider any unique arrival sequence with consistent arrivals, ... *)Variablearr_seq : arrival_sequence Job.HypothesisH_consistent_arrivals: consistent_arrival_times arr_seq.HypothesisH_uniq_arrseq: arrival_sequence_uniq arr_seq.(** ... and any sporadic task [tsk] that is to be analyzed. *)Variabletsk : Task.HypothesisH_sporadic_model: respects_sporadic_task_model arr_seq tsk.HypothesisH_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.(** We first show that for any two jobs [j1] and [j2], [j2] arrives after [j1] provided [job_index] of [j2] strictly exceeds the [job_index] of [j1]. *)
bylia.Qed.(** In the following, consider (again) any two jobs from the arrival sequence that stem from task [tsk]. NB: The following variables and hypotheses match the premises of the preceding lemma. However, we cannot move these declarations before the prior lemma because we need [lower_index_implies_earlier_arrival] to be ∀-quantified in the next proof. *)Variablej1 : Job.Variablej2 : Job.HypothesisH_j1_from_arrseq: arrives_in arr_seq j1.HypothesisH_j2_from_arrseq: arrives_in arr_seq j2.HypothesisH_j1_task: job_task j1 = tsk.HypothesisH_j2_task: job_task j2 = tsk.(** We prove that jobs [j1] and [j2] are equal if and only if they arrive at the same time. *)
all: byapply lower_index_implies_earlier_arrival in LT => //; lia.Qed.(** As a corollary, we observe that distinct jobs cannot have equal arrival times. *)