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]


(** * EDF Priority Policy *)

(** We introduce the classic EDF priority policy, under which jobs are
    scheduled in order of their urgency, i.e., jobs are ordered according to
    their absolute deadlines. The EDF policy belongs to the class of JLFP
    policies. *)
#[export] Instance EDF (Job : JobType) `{JobDeadline Job} : JLFP_policy Job :=
{
  hep_job (j1 j2 : Job) := job_deadline j1 <= job_deadline j2
}.

(** In this section, we prove a few properties about EDF policy. *)
Section PropertiesOfEDF.

  (**  Consider any type of jobs with deadlines. *)
  Context {Job : JobType}.
  Context `{JobDeadline Job}.

  (** Consider any arrival sequence. *)
  Variable arr_seq : arrival_sequence Job.

  (** EDF is reflexive. *)
  
Job: JobType
H: JobDeadline Job
arr_seq: arrival_sequence Job
reflexive_job_priorities (EDF Job)

  
Job: JobType
H: JobDeadline Job
arr_seq: arrival_sequence Job
reflexive_job_priorities (EDF Job)
 by move=> j; apply:leqnn. Qed.

  (** EDF is transitive. *)
  
Job: JobType
H: JobDeadline Job
arr_seq: arrival_sequence Job
transitive_job_priorities (EDF Job)

  
Job: JobType
H: JobDeadline Job
arr_seq: arrival_sequence Job
transitive_job_priorities (EDF Job)
 by move=> y x z; apply: leq_trans. Qed.

  (** EDF is total. *)
  
Job: JobType
H: JobDeadline Job
arr_seq: arrival_sequence Job
total_job_priorities (EDF Job)

  
Job: JobType
H: JobDeadline Job
arr_seq: arrival_sequence Job
total_job_priorities (EDF Job)
 by move=> j1 j2; apply: leq_total. Qed.

End PropertiesOfEDF.

(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
    will be able to apply them automatically. *)
Global Hint Resolve
     EDF_is_reflexive
     EDF_is_transitive
     EDF_is_total
  : basic_rt_facts.