Require Export prosa.util.nat.
Require Export prosa.analysis.abstract.definitions.
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]

(** * Auxiliary Lemmas About Interference and Interfering Workload. *)

(** In this file we provide a set of auxiliary definitions and lemmas
    about generic properties of Interference and Interfering
    Workload. *)
Section InterferenceAndInterferingWorkloadAuxiliary.

  (** 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}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

  (** Assume we are provided with abstract functions for interference
      and interfering workload. *)
  Context `{Interference Job}.
  Context `{InterferingWorkload Job}.

  (** First, we show that cumulative interference on an interval
      <<[al, ar)>> is bounded by the cumulative interference on an
      interval <<[bl,br)>> if <<[al,ar)>> ⊆ <<[bl,br)>>. *)
  Lemma cumulative_interference_sub :
    forall (j : Job) (al ar bl br : instant),
      bl <= al ->
      ar <= br ->
      cumulative_interference j al ar <= cumulative_interference j bl br.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
forall (j : Job) (al ar bl br : instant),
bl <= al ->
ar <= br ->
cumulative_interference j al ar <=
cumulative_interference j bl br
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
forall (j : Job) (al ar bl br : instant),
bl <= al ->
ar <= br ->
cumulative_interference j al ar <=
cumulative_interference j bl br
    move => j al ar bl br LE1 LE2.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
j: Job
al, ar, bl, br: instant
LE1: bl <= al
LE2: ar <= br
cumulative_interference j al ar <=
cumulative_interference j bl br
    destruct (leqP al ar) as [NEQ|NEQ].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
j: Job
al, ar, bl, br: instant
LE1: bl <= al
LE2: ar <= br
NEQ: al <= ar
cumulative_interference j al ar <=
cumulative_interference j bl br
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
j: Job
al, ar, bl, br: instant
LE1: bl <= al
LE2: ar <= br
NEQ: ar < al
cumulative_interference j al ar <=
cumulative_interference j bl br
    -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
j: Job
al, ar, bl, br: instant
LE1: bl <= al
LE2: ar <= br
NEQ: al <= ar
cumulative_interference j al ar <=
cumulative_interference j bl br
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
j: Job
al, ar, bl, br: instant
LE1: bl <= al
LE2: ar <= br
NEQ: ar < al
cumulative_interference j al ar <=
cumulative_interference j bl br rewrite /cumulative_interference /definitions.cumulative_interference.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
j: Job
al, ar, bl, br: instant
LE1: bl <= al
LE2: ar <= br
NEQ: al <= ar
\sum_(al <= t < ar) interference j t <=
\sum_(bl <= t < br) interference j t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
j: Job
al, ar, bl, br: instant
LE1: bl <= al
LE2: ar <= br
NEQ: ar < al
cumulative_interference j al ar <=
cumulative_interference j bl br
      rewrite [in X in _ <= X](@big_cat_nat _ _ _ al) //=; try lia.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
j: Job
al, ar, bl, br: instant
LE1: bl <= al
LE2: ar <= br
NEQ: al <= ar
\sum_(al <= t < ar) interference j t <=
\sum_(bl <= i < al) interference j i +
\sum_(al <= i < br) interference j i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
j: Job
al, ar, bl, br: instant
LE1: bl <= al
LE2: ar <= br
NEQ: ar < al
cumulative_interference j al ar <=
cumulative_interference j bl br
      by rewrite [in X in _ <= _ + X](@big_cat_nat _ _ _ ar) //=; lia.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
j: Job
al, ar, bl, br: instant
LE1: bl <= al
LE2: ar <= br
NEQ: ar < al
cumulative_interference j al ar <=
cumulative_interference j bl br
    -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
j: Job
al, ar, bl, br: instant
LE1: bl <= al
LE2: ar <= br
NEQ: ar < al
cumulative_interference j al ar <=
cumulative_interference j bl br by rewrite /cumulative_interference /definitions.cumulative_interference big_geq; lia.
  Qed.

  (** We show that the cumulative interference of a job can be split
      into disjoint intervals. *)
  Lemma cumulative_interference_cat :
    forall j t t1 t2,
      t1 <= t <= t2 ->
      cumulative_interference j t1 t2 = cumulative_interference j t1 t + cumulative_interference j t t2.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
forall (j : Job) (t t1 t2 : nat),
t1 <= t <= t2 ->
cumulative_interference j t1 t2 =
cumulative_interference j t1 t +
cumulative_interference j t t2
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
forall (j : Job) (t t1 t2 : nat),
t1 <= t <= t2 ->
cumulative_interference j t1 t2 =
cumulative_interference j t1 t +
cumulative_interference j t t2
    move => j t t1 t2 /andP [LE1 LE2].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
j: Job
t, t1, t2: nat
LE1: t1 <= t
LE2: t <= t2
cumulative_interference j t1 t2 =
cumulative_interference j t1 t +
cumulative_interference j t t2
    rewrite /cumulative_interference /definitions.cumulative_interference.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: Interference Job
H4: InterferingWorkload Job
j: Job
t, t1, t2: nat
LE1: t1 <= t
LE2: t <= t2
\sum_(t1 <= t < t2) interference j t =
\sum_(t1 <= t < t) interference j t +
\sum_(t <= t < t2) interference j t
    by rewrite {1}(@big_cat_nat _ _ _ t) //=.
  Qed.

End InterferenceAndInterferingWorkloadAuxiliary.