Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.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]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing. Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_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]
(** * Always Higher Priority *) (** In this section, we define what it means for a job to always have a higher priority than another job. *) Section AlwaysHigherPriority. (** Consider any type of jobs ... *) Context {Job : JobType}. (** ... and any JLDP policy. *) Context `{JLDP_policy Job}. (** We say that a job [j1] always has higher priority than job [j2] if, at any time [t], the priority of job [j1] is strictly higher than the priority of job [j2]. *) Definition always_higher_priority (j1 j2 : Job) := forall t, hep_job_at t j1 j2 && ~~ hep_job_at t j2 j1. End AlwaysHigherPriority. (** We note that, under a job-level fixed-priority policy, the property is trivial since job priorities by definition do not change in this case. *) Section UnderJLFP. (** Consider any type of jobs ... *) Context {Job : JobType}. (** ... and any JLFP policy. *) Context `{JLFP_policy Job}. (** The property [always_higher_priority j j'] is equivalent to a statement about [hep_job]. *)
Job: JobType
H: JLFP_policy Job

forall j j' : Job, always_higher_priority j j' <-> hep_job j j' && ~~ hep_job j' j
Job: JobType
H: JLFP_policy Job

forall j j' : Job, always_higher_priority j j' <-> hep_job j j' && ~~ hep_job j' j
by move=> j j'; split => [|HP t]; [apply; exact: 0 | rewrite !hep_job_at_jlfp]. Qed. End UnderJLFP.