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]
(** * FIFO Priority Policy *) (** We define the basic FIFO priority policy, under which jobs are prioritized in order of their arrival times. The FIFO policy belongs to the class of JLFP policies. *) #[export] Instance FIFO (Job : JobType) `{JobArrival Job} : JLFP_policy Job := { hep_job (j1 j2 : Job) := job_arrival j1 <= job_arrival j2 }. (** In this section, we prove a few basic properties of the FIFO policy. *) Section Properties. (** Consider any type of jobs with arrival times. *) Context {Job : JobType}. Context `{JobArrival Job}. (** FIFO is reflexive. *)
Job: JobType
H: JobArrival Job

reflexive_priorities
Job: JobType
H: JobArrival Job

reflexive_priorities
by move=> t j; apply: leqnn. Qed. (** FIFO is transitive. *)
Job: JobType
H: JobArrival Job

transitive_priorities
Job: JobType
H: JobArrival Job

transitive_priorities
by move=> t y x z; apply: leq_trans. Qed. (** FIFO is total. *)
Job: JobType
H: JobArrival Job

total_priorities
Job: JobType
H: JobArrival Job

total_priorities
by move=> t j1 j2; apply: leq_total. Qed. End Properties. (** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *) Global Hint Resolve FIFO_is_reflexive FIFO_is_transitive FIFO_is_total : basic_rt_facts.