Library prosa.analysis.facts.priority.elf

Require Import prosa.model.priority.elf.
Require Export prosa.analysis.facts.priority.classes.

In this section, we note three basic properties of the ELF policy: the priority relation is reflexive, transitive, and total.
Section PropertiesOfELF.

Consider any type of tasks with relative priority points...
  Context {Task : TaskType} `{PriorityPoint Task}.

...and jobs of these tasks.
  Context {Job : JobType} `{JobArrival Job} `{JobTask Job Task} .

Consider any arbitrary FP policy ...
  Variable FP : FP_policy Task.

... that is reflexive, transitive, and total.
  Hypothesis H_reflexive_priorities : reflexive_task_priorities FP.
  Hypothesis H_transitive_priorities : transitive_task_priorities FP.
  Hypothesis H_total_priorities : total_task_priorities FP.

ELF is reflexive.
  Lemma ELF_is_reflexive : reflexive_job_priorities (ELF FP).

ELF is transitive.
  Lemma ELF_is_transitive : transitive_job_priorities (ELF FP).
ELF is total.
  Lemma ELF_is_total : total_job_priorities (ELF FP).

End PropertiesOfELF.

We add the above facts into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically where needed.
Global Hint Resolve
     ELF_is_reflexive
     ELF_is_transitive
     ELF_is_total
  : basic_rt_facts.