Require Export prosa.model.priority.classes.
[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]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_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]
Require Export prosa.analysis.definitions.priority.classes.

(** In this section, we prove some basic properties about priority relations. *)
Section BasicLemmas.

  (** Consider any type of tasks ... *)
  Context {Task : TaskType}.

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

  (** Consider a JLFP policy that indicates a higher-or-equal priority
      relation. *)
  Context `{JLFP_policy Job}.

  (** First, we prove that [another_hep_job] relation is anti-reflexive. *)
  Lemma another_hep_job_antireflexive :
    forall j, ~ another_hep_job j j.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
forall j : Job, ~ another_hep_job j j
  Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
forall j : Job, ~ another_hep_job j j
    by move => j /andP [_ /negP NEQ]; apply: NEQ.
  Qed.

  (** Second, we relate [another_hep_job] to [same_task]. *)
  Lemma another_hep_job_diff_task :
    forall j j',
      ~~ same_task j j' ->
      another_hep_job j j' = hep_job j j'.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
forall j j' : Job,
~~ same_task j j' ->
another_hep_job j j' = hep_job j j'
  Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
forall j j' : Job,
~~ same_task j j' ->
another_hep_job j j' = hep_job j j'
    move => j j' DIFF; rewrite /another_hep_job.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
j, j': Job
DIFF: ~~ same_task j j'
hep_job j j' && (j != j') = hep_job j j'
    case: (hep_job j j'); [rewrite andTb|rewrite andFb //].
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
j, j': Job
DIFF: ~~ same_task j j'
(j != j') = true
    apply: (contra _ DIFF) => /eqP -> {DIFF}.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
j, j': Job
same_task j' j'
    by apply/eqP.
  Qed.

  (** We show that [another_task_hep_job] is "task-wise"
      anti-reflexive; that is, given two jobs [j] and [j'] from the
      same task, [another_task_hep_job j' j] is false. *)
  Lemma another_task_hep_job_taskwise_antireflexive :
    forall tsk j j',
      job_of_task tsk j ->
      job_of_task tsk j' ->
      ~ another_task_hep_job j' j.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
forall (tsk : Task) (j j' : Job),
job_of_task tsk j ->
job_of_task tsk j' -> ~ another_task_hep_job j' j
  Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
forall (tsk : Task) (j j' : Job),
job_of_task tsk j ->
job_of_task tsk j' -> ~ another_task_hep_job j' j
    move=> tsko j j' /eqP TSK1 /eqP TSK2 /andP [_ AA].
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
tsko: Task
j, j': Job
TSK1: job_task j = tsko
TSK2: job_task j' = tsko
AA: job_task j' != job_task j
False
    by move: AA; rewrite TSK1 TSK2 => /negP A; apply: A.
  Qed.

  (** Alternative definition of [another_task_hep_job] using
      [another_hep_job] instead of [hep_job]. *)
  Lemma another_task_hep_job_another_hep_job :
    forall j1 j2,
      another_task_hep_job j1 j2
      = another_hep_job j1 j2 && (job_task j1 != job_task j2).
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
forall j1 j2 : Job,
another_task_hep_job j1 j2 =
another_hep_job j1 j2 && (job_task j1 != job_task j2)
  Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
forall j1 j2 : Job,
another_task_hep_job j1 j2 =
another_hep_job j1 j2 && (job_task j1 != job_task j2)
    move=> j1 j2.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
j1, j2: Job
another_task_hep_job j1 j2 =
another_hep_job j1 j2 && (job_task j1 != job_task j2)
    by rewrite -andbA [X in _ && X]andb_idl//; apply: contraNN => /eqP->.
  Qed.

  (** [another_hep_job] can either come from another or the same task... *)
  Lemma another_hep_job_split_task :
    forall j1 j2,
      another_hep_job j1 j2
      = another_task_hep_job j1 j2 || another_hep_job_of_same_task j1 j2.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
forall j1 j2 : Job,
another_hep_job j1 j2 =
another_task_hep_job j1 j2
|| another_hep_job_of_same_task j1 j2
  Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
forall j1 j2 : Job,
another_hep_job j1 j2 =
another_task_hep_job j1 j2
|| another_hep_job_of_same_task j1 j2
    move=> j1 j2.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
j1, j2: Job
another_hep_job j1 j2 =
another_task_hep_job j1 j2
|| another_hep_job_of_same_task j1 j2
    by rewrite another_task_hep_job_another_hep_job -andb_orr orNb andbT.
  Qed.

  (** ...but not both. *)
  Lemma another_hep_job_exclusive :
    forall j1 j2,
      ~~ (another_task_hep_job j1 j2 && another_hep_job_of_same_task j1 j2).
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
forall j1 j2 : Job,
~~
(another_task_hep_job j1 j2 &&
 another_hep_job_of_same_task j1 j2)
  Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JLFP_policy Job
forall j1 j2 : Job,
~~
(another_task_hep_job j1 j2 &&
 another_hep_job_of_same_task j1 j2)
    by move=> j1 j2; rewrite !negb_and negbK; case: eqP; rewrite /= !orbT.
  Qed.

End BasicLemmas.

(** In the following section, we establish properties of [hp_task] and [ep_task ]auxiliary
    priority relations defined for FP policies. They are useful in proving properties of the
    ELF scheduling policy. *)
Section FPRelationsProperties.

  (** Consider any type of tasks and an FP policy that indicates a higher-or-equal
      priority relation on the tasks.*)
  Context {Task : TaskType} {FP_policy : FP_policy Task}.

  (** First, we prove some trivial lemmas about the [hep_task] and [ep_task]
      relations. *)
  Section BasicProperties.

    (** [hp_task] is irreflexive. *)
    Lemma hp_task_irrefl : irreflexive hp_task.
Task: TaskType
FP_policy: definitions.FP_policy Task
irreflexive (T:=Task) hp_task
    Proof.
Task: TaskType
FP_policy: definitions.FP_policy Task
irreflexive (T:=Task) hp_task by move=> tsk; rewrite /hp_task; case: hep_task. Qed.

    (** If a task [tsk1] has higher priority than task [tsk2], then task [tsk1] has
        higher-or-equal priority than task [tsk2]. *)
    Lemma hp_hep_task :
      forall tsk1 tsk2,
        hp_task tsk1 tsk2 ->
        hep_task tsk1 tsk2.
Task: TaskType
FP_policy: definitions.FP_policy Task
forall tsk1 tsk2 : Task,
hp_task tsk1 tsk2 -> hep_task tsk1 tsk2
    Proof.
Task: TaskType
FP_policy: definitions.FP_policy Task
forall tsk1 tsk2 : Task,
hp_task tsk1 tsk2 -> hep_task tsk1 tsk2 by move=> ? ? /andP[]. Qed.

    (** If a task [tsk1] has equal priority as task [tsk2], then task [tsk1] has
        higher-or-equal priority than task [tsk2]. *)
    Lemma ep_hep_task :
      forall tsk1 tsk2,
        ep_task tsk1 tsk2 ->
        hep_task tsk1 tsk2.
Task: TaskType
FP_policy: definitions.FP_policy Task
forall tsk1 tsk2 : Task,
ep_task tsk1 tsk2 -> hep_task tsk1 tsk2
    Proof.
Task: TaskType
FP_policy: definitions.FP_policy Task
forall tsk1 tsk2 : Task,
ep_task tsk1 tsk2 -> hep_task tsk1 tsk2 by move=> ? ? /andP[]. Qed.

    (** If a task has higher priority than another task, then the two do not
        have equal priority. *)
    Lemma ep_not_hp_task :
      forall tsk1 tsk2,
        ep_task tsk1 tsk2 ->
        ~~ hp_task tsk1 tsk2.
Task: TaskType
FP_policy: definitions.FP_policy Task
forall tsk1 tsk2 : Task,
ep_task tsk1 tsk2 -> ~~ hp_task tsk1 tsk2
    Proof.
Task: TaskType
FP_policy: definitions.FP_policy Task
forall tsk1 tsk2 : Task,
ep_task tsk1 tsk2 -> ~~ hp_task tsk1 tsk2
      move=> ? ? /andP[_ ?].
Task: TaskType
FP_policy: definitions.FP_policy Task
_tsk1_, _tsk2_: Task
_b_: hep_task _tsk2_ _tsk1_
~~ hp_task _tsk1_ _tsk2_
      by rewrite negb_and; apply/orP; right; apply/negPn.
    Qed.

    (** Task [tsk1] having equal priority as task [tsk2] is equivalent to task [tsk2]
        having equal priority as task [tsk1]. *)
    Lemma ep_task_sym :
      forall tsk1 tsk2,
        ep_task tsk1 tsk2 = ep_task tsk2 tsk1.
Task: TaskType
FP_policy: definitions.FP_policy Task
forall tsk1 tsk2 : Task,
ep_task tsk1 tsk2 = ep_task tsk2 tsk1
    Proof.
Task: TaskType
FP_policy: definitions.FP_policy Task
forall tsk1 tsk2 : Task,
ep_task tsk1 tsk2 = ep_task tsk2 tsk1 by move=> x y; rewrite /ep_task andbC. Qed.

    (** If a task [tsk1] has higher-or-equal priority than a task
        [tsk2], then [tsk1] either has strictly higher priority than
        [tsk2] or the two have equal priority. *)
    Lemma hep_hp_ep_task :
      forall tsk1 tsk2,
        hep_task tsk1 tsk2 = hp_task tsk1 tsk2 || ep_task tsk1 tsk2.
Task: TaskType
FP_policy: definitions.FP_policy Task
forall tsk1 tsk2 : Task,
hep_task tsk1 tsk2 =
hp_task tsk1 tsk2 || ep_task tsk1 tsk2
    Proof.
Task: TaskType
FP_policy: definitions.FP_policy Task
forall tsk1 tsk2 : Task,
hep_task tsk1 tsk2 =
hp_task tsk1 tsk2 || ep_task tsk1 tsk2 by move=> ? ?; rewrite /hp_task /ep_task -andb_orr orNb andbT. Qed.

  End BasicProperties.

  (** In the following section, we establish a useful property about the equal
      priority relation, which follows when the FP policy is reflexive.  *)
  Section ReflexiveProperties.

    (** Assuming that the FP policy is reflexive ... *)
    Hypothesis H_reflexive : reflexive hep_task.

    (** ... it follows that the equal priority relation is reflexive. *)
    Lemma eq_reflexive : reflexive ep_task.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_reflexive: reflexive (T:=Task) hep_task
reflexive (T:=Task) ep_task
    Proof.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_reflexive: reflexive (T:=Task) hep_task
reflexive (T:=Task) ep_task by move=> ?; apply /andP; split. Qed.

  End ReflexiveProperties.

  (** Now we establish useful properties about the higher priority relation,
      which follow when the FP policy is transitive.  *)
  Section TransitiveProperties.

    (** Assuming that the FP policy is transitive ... *)
    Hypothesis H_transitive : transitive hep_task.

    (** ... it follows that the higher priority relation is also transitive.  *)
    Lemma hp_trans : transitive hp_task.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
transitive (T:=Task) hp_task
    Proof.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
transitive (T:=Task) hp_task
      move=> y x z /andP[hepxy Nhepyx] /andP[hepyz Nhepyz]; apply/andP; split.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
y, x, z: Task
hepxy: hep_task x y
Nhepyx: ~~ hep_task y x
hepyz: hep_task y z
Nhepyz: ~~ hep_task z y
hep_task x z
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
y, x, z: Task
hepxy: hep_task x y
Nhepyx: ~~ hep_task y x
hepyz: hep_task y z
Nhepyz: ~~ hep_task z y
~~ hep_task z x
      {
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
y, x, z: Task
hepxy: hep_task x y
Nhepyx: ~~ hep_task y x
hepyz: hep_task y z
Nhepyz: ~~ hep_task z y
hep_task x z exact: H_transitive hepyz. }
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
y, x, z: Task
hepxy: hep_task x y
Nhepyx: ~~ hep_task y x
hepyz: hep_task y z
Nhepyz: ~~ hep_task z y
~~ hep_task z x
      {
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
y, x, z: Task
hepxy: hep_task x y
Nhepyx: ~~ hep_task y x
hepyz: hep_task y z
Nhepyz: ~~ hep_task z y
~~ hep_task z x by apply: contraNN Nhepyx; exact: H_transitive. }
    Qed.

    (** If task [tsk1] has higher priority than task [tsk2], and task [tsk2] has
        higher-or-equal priority than task [tsk3], then task [tsk1] has higher priority
        than task [tsk3]. *)
    Lemma hp_hep_trans :
      forall tsk1 tsk2 tsk3,
        hp_task tsk1 tsk2 ->
        hep_task tsk2 tsk3 ->
        hp_task tsk1 tsk3.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
forall tsk1 tsk2 tsk3 : Task,
hp_task tsk1 tsk2 ->
hep_task tsk2 tsk3 -> hp_task tsk1 tsk3
    Proof.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
forall tsk1 tsk2 tsk3 : Task,
hp_task tsk1 tsk2 ->
hep_task tsk2 tsk3 -> hp_task tsk1 tsk3
      move=> x y z /andP[hepxy Nhepyx] hepyz; apply/andP; split.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
x, y, z: Task
hepxy: hep_task x y
Nhepyx: ~~ hep_task y x
hepyz: hep_task y z
hep_task x z
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
x, y, z: Task
hepxy: hep_task x y
Nhepyx: ~~ hep_task y x
hepyz: hep_task y z
~~ hep_task z x
      {
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
x, y, z: Task
hepxy: hep_task x y
Nhepyx: ~~ hep_task y x
hepyz: hep_task y z
hep_task x z exact: H_transitive hepyz. }
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
x, y, z: Task
hepxy: hep_task x y
Nhepyx: ~~ hep_task y x
hepyz: hep_task y z
~~ hep_task z x
      {
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
x, y, z: Task
hepxy: hep_task x y
Nhepyx: ~~ hep_task y x
hepyz: hep_task y z
~~ hep_task z x by apply: contraNN Nhepyx; exact: H_transitive. }
    Qed.

    (** If task [tsk1] has higher-or-equal priority than task [tsk2], and task [tsk2]
        has strictly higher priority than task [tsk3], then task [tsk1]
        has higher priority than task [tsk3]. *)
    Lemma hep_hp_trans :
      forall tsk1 tsk2 tsk3,
        hep_task tsk1 tsk2 ->
        hp_task tsk2 tsk3 ->
        hp_task tsk1 tsk3.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
forall tsk1 tsk2 tsk3 : Task,
hep_task tsk1 tsk2 ->
hp_task tsk2 tsk3 -> hp_task tsk1 tsk3
    Proof.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
forall tsk1 tsk2 tsk3 : Task,
hep_task tsk1 tsk2 ->
hp_task tsk2 tsk3 -> hp_task tsk1 tsk3
      move=> x y z hepxy /andP[hepyz Nhepzy]; apply/andP; split.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
x, y, z: Task
hepxy: hep_task x y
hepyz: hep_task y z
Nhepzy: ~~ hep_task z y
hep_task x z
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
x, y, z: Task
hepxy: hep_task x y
hepyz: hep_task y z
Nhepzy: ~~ hep_task z y
~~ hep_task z x
      {
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
x, y, z: Task
hepxy: hep_task x y
hepyz: hep_task y z
Nhepzy: ~~ hep_task z y
hep_task x z exact: H_transitive hepyz. }
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
x, y, z: Task
hepxy: hep_task x y
hepyz: hep_task y z
Nhepzy: ~~ hep_task z y
~~ hep_task z x
      {
Task: TaskType
FP_policy: definitions.FP_policy Task
H_transitive: transitive (T:=Task) hep_task
x, y, z: Task
hepxy: hep_task x y
hepyz: hep_task y z
Nhepzy: ~~ hep_task z y
~~ hep_task z x apply: contraNN Nhepzy => hepzy; exact: H_transitive hepxy. }
    Qed.

  End TransitiveProperties.

  (** Finally, we establish a useful property about the higher priority relation,
      which follows when the FP policy is total.  *)
  Section TotalProperties.

    (** We assume that the FP policy is total. *)
    Hypothesis H_total : total hep_task.

    (** If a task [tsk1] does not have higher-or-equal priority than task [tsk2], then
        task [tsk2] has higher priority than task [tsk1].  *)
    Lemma not_hep_hp_task :
      forall tsk1 tsk2, ~~ hep_task tsk1 tsk2 = hp_task tsk2 tsk1.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_total: total (T:=Task) hep_task
forall tsk1 tsk2 : Task,
~~ hep_task tsk1 tsk2 = hp_task tsk2 tsk1
    Proof.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_total: total (T:=Task) hep_task
forall tsk1 tsk2 : Task,
~~ hep_task tsk1 tsk2 = hp_task tsk2 tsk1
      move=> x y; apply /idP/idP => [| /andP[//]].
Task: TaskType
FP_policy: definitions.FP_policy Task
H_total: total (T:=Task) hep_task
x, y: Task
~~ hep_task x y -> hp_task y x
      move=> Nhepxy; apply /andP; split=> [|//].
Task: TaskType
FP_policy: definitions.FP_policy Task
H_total: total (T:=Task) hep_task
x, y: Task
Nhepxy: ~~ hep_task x y
hep_task y x
      have /orP[h | //] := H_total x y.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_total: total (T:=Task) hep_task
x, y: Task
Nhepxy: ~~ hep_task x y
h: hep_task x y
hep_task y x
      by exfalso; move/negP: Nhepxy.
    Qed.

    (** The converse also holds. *)
    Lemma not_hp_hep_task :
      forall tsk1 tsk2, ~~ hp_task tsk1 tsk2 = hep_task tsk2 tsk1.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_total: total (T:=Task) hep_task
forall tsk1 tsk2 : Task,
~~ hp_task tsk1 tsk2 = hep_task tsk2 tsk1
    Proof.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_total: total (T:=Task) hep_task
forall tsk1 tsk2 : Task,
~~ hp_task tsk1 tsk2 = hep_task tsk2 tsk1 by move=> x y; rewrite -not_hep_hp_task negbK. Qed.

    (** If a task [tsk1] does not have higher priority than a task
        [tsk2], then [tsk1] either has lesser priority than
        [tsk2] or the two have equal priority. *)
    Lemma nhp_ep_nhep_task :
      forall tsk1 tsk2,
        ~~hp_task tsk1 tsk2 = ~~hep_task tsk1 tsk2 || ep_task tsk1 tsk2.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_total: total (T:=Task) hep_task
forall tsk1 tsk2 : Task,
~~ hp_task tsk1 tsk2 =
~~ hep_task tsk1 tsk2 || ep_task tsk1 tsk2
    Proof.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_total: total (T:=Task) hep_task
forall tsk1 tsk2 : Task,
~~ hp_task tsk1 tsk2 =
~~ hep_task tsk1 tsk2 || ep_task tsk1 tsk2
      move=> tsk1 tsk2; rewrite not_hp_hep_task not_hep_hp_task.
Task: TaskType
FP_policy: definitions.FP_policy Task
H_total: total (T:=Task) hep_task
tsk1, tsk2: Task
hep_task tsk2 tsk1 =
hp_task tsk2 tsk1 || ep_task tsk1 tsk2
      by rewrite hep_hp_ep_task ep_task_sym.
    Qed.

  End TotalProperties.

End FPRelationsProperties.

(** In the following section, we show that FP policies respect the sequential
    tasks hypothesis. It means that later-arrived jobs of a task don't have
    higher priority than earlier-arrived jobs of the same task (assuming that
    task priorities are reflexive).*)
Section FPRemarks.

  (** Consider any type of tasks ... *)
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

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

  (** .. and assume that jobs have a cost and an arrival time. *)
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

  (** Consider any FP policy. *)
  Context {FP : FP_policy Task}.

  Remark respects_sequential_tasks :
    reflexive_task_priorities FP ->
    policy_respects_sequential_tasks (FP_to_JLFP FP).
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
FP: FP_policy Task
reflexive_task_priorities FP ->
policy_respects_sequential_tasks FP
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
FP: FP_policy Task
reflexive_task_priorities FP ->
policy_respects_sequential_tasks FP
    move => REFL j1 j2 /eqP EQ LT.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
FP: FP_policy Task
REFL: reflexive_task_priorities FP
j1, j2: Job
EQ: job_task j1 = job_task j2
LT: job_arrival j1 <= job_arrival j2
hep_job j1 j2
    by rewrite /hep_job /FP_to_JLFP EQ.
  Qed.

End FPRemarks.

Section JLFPFP.
   (** Consider any type of tasks ... *)
  Context {Task : TaskType}.

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

  (** Consider any pair of JLFP and FP policies that are compatible. *)
  Context (JLFP : JLFP_policy Job) (FP : FP_policy Task).
  Hypothesis H_compatible : JLFP_FP_compatible JLFP FP.

  (** We restate [JLFP_FP_compatible] to make it easier to discover
      with [Search]. Here is the first part... *)
  Lemma hep_job_implies_hep_task :
    forall j1 j2,
      hep_job j1 j2 ->
      hep_task (job_task j1) (job_task j2).
Task: TaskType
Job: JobType
H: JobTask Job Task
JLFP: JLFP_policy Job
FP: FP_policy Task
H_compatible: JLFP_FP_compatible JLFP FP
forall j1 j2 : Job,
hep_job j1 j2 -> hep_task (job_task j1) (job_task j2)
  Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
JLFP: JLFP_policy Job
FP: FP_policy Task
H_compatible: JLFP_FP_compatible JLFP FP
forall j1 j2 : Job,
hep_job j1 j2 -> hep_task (job_task j1) (job_task j2) exact: H_compatible.1. Qed.

  (** ...and second part. *)
  Lemma hp_task_implies_hep_job :
    forall j1 j2,
      hp_task (job_task j1) (job_task j2) ->
      hep_job j1 j2.
Task: TaskType
Job: JobType
H: JobTask Job Task
JLFP: JLFP_policy Job
FP: FP_policy Task
H_compatible: JLFP_FP_compatible JLFP FP
forall j1 j2 : Job,
hp_task (job_task j1) (job_task j2) -> hep_job j1 j2
  Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
JLFP: JLFP_policy Job
FP: FP_policy Task
H_compatible: JLFP_FP_compatible JLFP FP
forall j1 j2 : Job,
hp_task (job_task j1) (job_task j2) -> hep_job j1 j2 exact: H_compatible.2. Qed.

End JLFPFP.

(** We add a lemma into the "Hint Database" basic_rt_facts, so Coq will be able
    to apply it automatically. *)
Global Hint Resolve respects_sequential_tasks : basic_rt_facts.