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]


(** * 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.