Library prosa.model.priority.coercion

Automatic FP ➔ JLFP ➔ JLDP Conversion

Since there are natural interpretations of FP and JLFP policies as JLFP and JLDP policies, respectively, we define conversions that express these generalizations. In practice, this means that Coq will be able to automatically satisfy a JLDP assumption if a JLFP or FP policy is in scope.
First, any FP policy can be interpreted as an JLFP policy by comparing jobs according to the priorities of their respective tasks. The priority is lowered to 10 in order to avoid conflict with other instances of JLFP policies which take FP policies as argument.
#[global]
Instance FP_to_JLFP {Job : JobType} {Task : TaskType} {tasks : JobTask Job Task}
    (FP : FP_policy Task) : JLFP_policy Job | 10 :=
  fun j1 j2hep_task (job_task j1) (job_task j2).

Second, any JLFP policy implies a JLDP policy that simply ignores the time parameter. Analogously, priority is lowered to 10 in order to avoid conflict with other instances of JLDP policies which take JLFP policies as argument.
#[global]
Instance JLFP_to_JLDP {Job : JobType}
    (JLFP : JLFP_policy Job) : JLDP_policy Job | 10 :=
  fun _ j1 j2hep_job j1 j2.

We add coercions to enable automatic conversion from JLFP to JLDP...
...and from FP to JLFP.
#[warning="-uniform-inheritance"]
Coercion FP_to_JLFP : FP_policy >-> JLFP_policy.

We now prove lemmas about conversions between the properties of these priority classes.
Consider any type of tasks ...
  Context {Task : TaskType}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.

To simplify later proofs, we make two trivial remarks on the FP->JLFP->JLDP coercion.
First, when considering a JLFP policy, hep_job_at and hep_job are by definition equivalent.
  Remark hep_job_at_jlfp :
     `{JLFP_policy Job} j j' t,
      hep_job_at t j j' = hep_job j j'.

Second, when considering an FP policy, hep_job_at and hep_task are by definition equivalent.
  Remark hep_job_at_fp :
     `{FP_policy Task} j j' t,
      hep_job_at t j j' = hep_task (job_task j) (job_task j').

We observe that lifting an FP_policy to a JLFP_policy trivially maintains reflexivity,...
...transitivity,...
...and totality of priorities.
  Lemma total_priorities_FP_implies_JLFP :
     (fp: FP_policy Task),
      total_task_priorities fp
        total_job_priorities (FP_to_JLFP fp).

Analogously, lifting a JLFP_policy to a JLDP_policy also maintains reflexivity,...
...transitivity,...
...and totality of priorities.
We add the above lemmas into the "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically.
Global Hint Resolve
    reflexive_priorities_FP_implies_JLFP
    reflexive_priorities_JLFP_implies_JLDP
    transitive_priorities_FP_implies_JLFP
    transitive_priorities_JLFP_implies_JLDP
    total_priorities_FP_implies_JLFP
    total_priorities_JLFP_implies_JLDP
  : basic_rt_facts.