Require Export prosa.model.aggregate.workload.
[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.facts.behavior.arrivals.
Require Export prosa.analysis.definitions.request_bound_function.
Require Export prosa.analysis.facts.model.task_arrivals.


(** * Lemmas about Workload of Sets of Jobs *)
(** In this file, we establish basic facts about the workload of sets of jobs. *)
Section WorkloadFacts.

  (** 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}.

  (** To begin with, we establish an auxiliary rewriting lemma that allows us to
      introduce a [filter] on the considered set of jobs, provided the filter
      predicate [P2] is implied by the job-selection predicate [P1]. *)
  Lemma workload_of_jobs_filter :
    forall (P1 P2 : pred Job) (jobs : seq Job),
      (forall j, j \in jobs -> P1 j -> P2 j) ->
      workload_of_jobs P1 jobs = workload_of_jobs P1 [seq j <- jobs | P2 j ].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
forall (P1 P2 : pred Job) (jobs : seq Job),
(forall j : Job, j \in jobs -> P1 j -> P2 j) ->
workload_of_jobs P1 jobs =
workload_of_jobs P1 [seq j <- jobs | P2 j]
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
forall (P1 P2 : pred Job) (jobs : seq Job),
(forall j : Job, j \in jobs -> P1 j -> P2 j) ->
workload_of_jobs P1 jobs =
workload_of_jobs P1 [seq j <- jobs | P2 j]
    move=> P1 P2 jobs IMPL.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPL: forall j : Job, j \in jobs -> P1 j -> P2 j
workload_of_jobs P1 jobs =
workload_of_jobs P1 [seq j <- jobs | P2 j]
    rewrite /workload_of_jobs big_filter_cond big_seq_cond [RHS]big_seq_cond.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPL: forall j : Job, j \in jobs -> P1 j -> P2 j
\sum_(i <- jobs | (i \in jobs) && P1 i) job_cost i =
\sum_(i <- jobs | [&& i \in jobs, P2 i & P1 i])
   job_cost i
    apply: eq_bigl => j.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPL: forall j : Job, j \in jobs -> P1 j -> P2 j
j: Job
(j \in jobs) && P1 j = [&& j \in jobs, P2 j & P1 j]
    case: (boolP (j \in jobs)) => // IN.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPL: forall j : Job, j \in jobs -> P1 j -> P2 j
j: Job
IN: j \in jobs
true && P1 j = [&& true, P2 j & P1 j]
    rewrite !andTb.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPL: forall j : Job, j \in jobs -> P1 j -> P2 j
j: Job
IN: j \in jobs
P1 j = P2 j && P1 j
    case: (boolP (P1 j)) => //= P1j; first by rewrite (IMPL j IN P1j).
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPL: forall j : Job, j \in jobs -> P1 j -> P2 j
j: Job
IN: j \in jobs
P1j: ~~ P1 j
false = P2 j && false
    by rewrite andbF.
  Qed.

  (** We establish that if the predicate [P1] implies the predicate [P2],
      then the cumulative workload of jobs that respect [P1] is bounded
      by the cumulative workload of jobs that respect [P2]. *)
  Lemma workload_of_jobs_weaken :
    forall (P1 P2 : pred Job) (jobs : seq Job),
      (forall j, P1 j -> P2 j) ->
      workload_of_jobs P1 jobs <= workload_of_jobs P2 jobs.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
forall (P1 P2 : pred Job) (jobs : seq Job),
(forall j : Job, P1 j -> P2 j) ->
workload_of_jobs P1 jobs <= workload_of_jobs P2 jobs
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
forall (P1 P2 : pred Job) (jobs : seq Job),
(forall j : Job, P1 j -> P2 j) ->
workload_of_jobs P1 jobs <= workload_of_jobs P2 jobs
    move => P1 P2 jobs IMPLIES; rewrite /workload_of_jobs.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPLIES: forall j : Job, P1 j -> P2 j
\sum_(j <- jobs | P1 j) job_cost j <=
\sum_(j <- jobs | P2 j) job_cost j
    apply: leq_sum_seq_pred => j' _.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P1, P2: pred Job
jobs: seq Job
IMPLIES: forall j : Job, P1 j -> P2 j
j': Job
P1 j' -> P2 j'
    by apply: IMPLIES.
  Qed.

  (** The cumulative workload of jobs from an empty sequence is always zero. *)
  Lemma workload_of_jobs0 :
    forall (P : pred Job), workload_of_jobs P [::] = 0.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
forall P : pred Job, workload_of_jobs P [::] = 0
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
forall P : pred Job, workload_of_jobs P [::] = 0 by move => ?; rewrite /workload_of_jobs big_nil. Qed.

  (** The workload of a set of jobs can be equivalently rewritten as sum over
      their tasks. *)
  Lemma workload_of_jobs_partitioned_by_tasks :
    forall {P : pred Job} (Q : pred Task) {js : seq Job} (ts : seq Task),
      {in js, forall j, (job_task j) \in ts} ->
      {in js, forall j, P j -> Q (job_task j)} ->
      uniq js ->
      uniq ts ->
      let P_and_job_of tsk_o j := P j && (job_task j == tsk_o) in
      workload_of_jobs P js
      = \sum_(tsk_o <- ts | Q tsk_o ) workload_of_jobs (P_and_job_of tsk_o) js.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
forall (P : pred Job) (Q : pred Task) (js : seq Job)
  (ts : seq Task),
{in js, forall j : Job, job_task j \in ts} ->
{in js, forall j : Job, P j -> Q (job_task j)} ->
uniq js ->
uniq ts ->
let P_and_job_of :=
  fun (tsk_o : Task) (j : Job) =>
  P j && (job_task j == tsk_o) in
workload_of_jobs P js =
\sum_(tsk_o <- ts | Q tsk_o)
   workload_of_jobs (P_and_job_of tsk_o) js
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
forall (P : pred Job) (Q : pred Task) (js : seq Job)
  (ts : seq Task),
{in js, forall j : Job, job_task j \in ts} ->
{in js, forall j : Job, P j -> Q (job_task j)} ->
uniq js ->
uniq ts ->
let P_and_job_of :=
  fun (tsk_o : Task) (j : Job) =>
  P j && (job_task j == tsk_o) in
workload_of_jobs P js =
\sum_(tsk_o <- ts | Q tsk_o)
   workload_of_jobs (P_and_job_of tsk_o) js
    move=> P Q js ts IN_ts PQ UJ UT //=.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P: pred Job
Q: pred Task
js: seq Job
ts: seq Task
IN_ts: {in js, forall j : Job, job_task j \in ts}
PQ: {in js, forall j : Job, P j -> Q (job_task j)}
UJ: uniq js
UT: uniq ts
workload_of_jobs P js =
\sum_(tsk_o <- ts | Q tsk_o)
   workload_of_jobs
     (fun j : Job => P j && (job_task j == tsk_o)) js
    rewrite -big_filter {1}/workload_of_jobs //.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P: pred Job
Q: pred Task
js: seq Job
ts: seq Task
IN_ts: {in js, forall j : Job, job_task j \in ts}
PQ: {in js, forall j : Job, P j -> Q (job_task j)}
UJ: uniq js
UT: uniq ts
\sum_(j <- js | P j) job_cost j =
\sum_(i <- [seq x <- ts | Q x])
   workload_of_jobs
     (fun j : Job => P j && (job_task j == i)) js
    apply: sum_over_partitions_eq => // [j IN Px|]; last exact: filter_uniq.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P: pred Job
Q: pred Task
js: seq Job
ts: seq Task
IN_ts: {in js, forall j : Job, job_task j \in ts}
PQ: {in js, forall j : Job, P j -> Q (job_task j)}
UJ: uniq js
UT: uniq ts
j: Job
IN: j \in js
Px: P j
job_task j \in [seq x <- ts | Q x]
    rewrite mem_filter; apply/andP; split; last by apply: IN_ts.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
P: pred Job
Q: pred Task
js: seq Job
ts: seq Task
IN_ts: {in js, forall j : Job, job_task j \in ts}
PQ: {in js, forall j : Job, P j -> Q (job_task j)}
UJ: uniq js
UT: uniq ts
j: Job
IN: j \in js
Px: P j
Q (job_task j)
    by apply: PQ.
  Qed.

  (** In this section we state a lemma about splitting the workload among tasks
      of different priority relative to a job [j]. *)
  Section WorkloadPartitioningByPriority.

    (** Consider any JLFP policy. *)
    Context `{JLFP_policy Job}.

    (** Consider the workload of all the jobs that have priority
        higher-than-or-equal-to the priority of [j]. This workload can be split
        by task into the workload of higher-or-equal priority jobs from the task of [j]
        and higher-or-equal priority jobs from all tasks except for the task of [j]. *)
    Lemma workload_of_other_jobs_split :
      forall jobs j,
        workload_of_jobs (another_hep_job^~j) jobs =
          workload_of_jobs (another_task_hep_job^~j) jobs
          + workload_of_jobs (another_hep_job_of_same_task^~j) jobs.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
forall (jobs : seq Job) (j : Job),
workload_of_jobs (another_hep_job^~ j) jobs =
workload_of_jobs (another_task_hep_job^~ j) jobs +
workload_of_jobs (another_hep_job_of_same_task^~ j)
  jobs
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
forall (jobs : seq Job) (j : Job),
workload_of_jobs (another_hep_job^~ j) jobs =
workload_of_jobs (another_task_hep_job^~ j) jobs +
workload_of_jobs (another_hep_job_of_same_task^~ j)
  jobs
      move => jobs j.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j: Job
workload_of_jobs (another_hep_job^~ j) jobs =
workload_of_jobs (another_task_hep_job^~ j) jobs +
workload_of_jobs (another_hep_job_of_same_task^~ j)
  jobs
      rewrite /workload_of_jobs.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j: Job
\sum_(j0 <- jobs | another_hep_job j0 j) job_cost j0 =
\sum_(j0 <- jobs | another_task_hep_job j0 j)
   job_cost j0 +
\sum_(j0 <- jobs | another_hep_job_of_same_task j0 j)
   job_cost j0
      apply sum_split_exhaustive_mutually_exclusive_preds  => jo.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job
another_hep_job jo j =
another_task_hep_job jo j
|| another_hep_job_of_same_task jo j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job
~~
(another_task_hep_job jo j &&
 another_hep_job_of_same_task jo j)
      -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job
another_hep_job jo j =
another_task_hep_job jo j
|| another_hep_job_of_same_task jo j rewrite /another_hep_job /another_task_hep_job /another_hep_job_of_same_task
          /same_task /another_hep_job.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job
hep_job jo j && (jo != j) =
hep_job jo j && (job_task jo != job_task j)
|| hep_job jo j && (jo != j) &&
   (job_task jo == job_task j)
        case (hep_job jo j) eqn: EQ1;
          case (jo != j) eqn: EQ2;
          case (job_task jo != job_task j) eqn: EQ3; try lia.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job
EQ1: hep_job jo j = true
EQ2: (jo != j) = false
EQ3: (job_task jo != job_task j) = true
true && false =
true && true
|| true && false && (job_task jo == job_task j)
        move : EQ2 => /eqP EQ2.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job
EQ1: hep_job jo j = true
EQ3: (job_task jo != job_task j) = true
EQ2: jo = j
true && false =
true && true
|| true && false && (job_task jo == job_task j)
        rewrite EQ2 in EQ3.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job
EQ1: hep_job jo j = true
EQ2: jo = j
EQ3: (job_task j != job_task j) = true
true && false =
true && true
|| true && false && (job_task jo == job_task j)
        contradict EQ3.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job
EQ1: hep_job jo j = true
EQ2: jo = j
(job_task j != job_task j) <> true
        by apply /negP /negPn /eqP.
      -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job
~~
(another_task_hep_job jo j &&
 another_hep_job_of_same_task jo j) rewrite /another_hep_job /another_task_hep_job /another_hep_job_of_same_task
          /same_task /another_hep_job.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
H3: JLFP_policy Job
jobs: seq Job
j, jo: Job
~~
[&& hep_job jo j && (job_task jo != job_task j),
    hep_job jo j && (jo != j)
  & job_task jo == job_task j]
        by case (hep_job jo j) eqn: EQ1; case (jo != j) eqn: EQ2;
          case (job_task jo != job_task j) eqn: EQ3; try lia.
    Qed.

  End WorkloadPartitioningByPriority.

  (** Consider any arrival sequence with consistent arrivals. *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_consistent : consistent_arrival_times arr_seq.

  (** In this section, we prove a few useful properties regarding the
      predicate of [workload_of_jobs]. *)
  Section PredicateProperties.

    (** Consider a sequence of jobs [jobs]. *)
    Variable jobs : seq Job.

    (** First, we show that workload of [jobs] for an unsatisfiable
        predicate is equal to [0]. *)
    Lemma workload_of_jobs_pred0 :
      workload_of_jobs pred0 jobs = 0.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
workload_of_jobs pred0 jobs = 0
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
workload_of_jobs pred0 jobs = 0 by rewrite /workload_of_jobs; apply big_pred0. Qed.

    (** Next, consider two arbitrary predicates [P] and [P']. *)
    Variable P P' : pred Job.

    (** We show that [workload_of_jobs] conditioned on [P] can be split into two summands:
        (1) [workload_of_jobs] conditioned on [P /\ P'] and
        (2) [workload_of_jobs] conditioned on [P /\ ~~ P']. *)
    Lemma workload_of_jobs_case_on_pred :
      workload_of_jobs P jobs =
        workload_of_jobs (fun j => P j && P' j) jobs + workload_of_jobs (fun j => P j && ~~ P' j) jobs.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job
workload_of_jobs P jobs =
workload_of_jobs (fun j : Job => P j && P' j) jobs +
workload_of_jobs (fun j : Job => P j && ~~ P' j) jobs
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job
workload_of_jobs P jobs =
workload_of_jobs (fun j : Job => P j && P' j) jobs +
workload_of_jobs (fun j : Job => P j && ~~ P' j) jobs
      rewrite /workload_of_jobs !big_mkcond [in X in _ = X]big_mkcond
              [in X in _ = _ + X]big_mkcond //= -big_split //=.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job
\sum_(i <- jobs) (if P i then job_cost i else 0) =
\sum_(i <- jobs)
   ((if P i && P' i then job_cost i else 0) +
    (if P i && ~~ P' i then job_cost i else 0))
      apply: eq_big_seq => j' IN.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job
j': Job
IN: j' \in jobs
(if P j' then job_cost j' else 0) =
(if P j' && P' j' then job_cost j' else 0) +
(if P j' && ~~ P' j' then job_cost j' else 0)
      by destruct (P _), (P' _); simpl; lia.
    Qed.

    (** We show that if [P] is indistinguishable from [P'] on set
        [jobs], then [workload_of_jobs] conditioned on [P] is equal to
        [workload_of_jobs] conditioned on [P']. *)
    Lemma workload_of_jobs_equiv_pred :
      {in jobs, P =1 P'} ->
      workload_of_jobs P jobs = workload_of_jobs P' jobs.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job
{in jobs, P =1 P'} ->
workload_of_jobs P jobs = workload_of_jobs P' jobs
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job
{in jobs, P =1 P'} ->
workload_of_jobs P jobs = workload_of_jobs P' jobs
      intros * EQUIV.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job
EQUIV: {in jobs, P =1 P'}
workload_of_jobs P jobs = workload_of_jobs P' jobs
      rewrite /workload_of_jobs !big_mkcond [in X in _ = X]big_mkcond //=.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
jobs: seq Job
P, P': pred Job
EQUIV: {in jobs, P =1 P'}
\sum_(i <- jobs) (if P i then job_cost i else 0) =
\sum_(i <- jobs) (if P' i then job_cost i else 0)
      by apply: eq_big_seq => j' IN; rewrite EQUIV.
    Qed.

  End PredicateProperties.

  (** In this section, we bound the workload of jobs of a particular task by the task's [RBF]. *)
  Section WorkloadRBF.

    (** Consider an arbitrary task. *)
    Variable tsk : Task.

    (** Consider a valid arrival curve that is respected by the task [tsk]. *)
    Context `{MaxArrivals Task}.
    Hypothesis H_task_repsects_max_arrivals : respects_max_arrivals arr_seq tsk (max_arrivals tsk).

    (** Suppose all arrivals have WCET-compliant job costs. *)
    Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.

    (** Consider an instant [t1] and a duration [Δ]. *)
    Variable t1 : instant.
    Variable Δ : duration.

    (** We prove that the workload of jobs of a task [tsk] in any interval is
        bound by the request bound function of the task in that interval. *)
    Lemma workload_le_rbf :
      workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 (t1 + Δ))
      <= task_request_bound_function tsk Δ.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
workload_of_jobs (job_of_task tsk)
  (arrivals_between arr_seq t1 (t1 + Δ)) <=
task_request_bound_function tsk Δ
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
workload_of_jobs (job_of_task tsk)
  (arrivals_between arr_seq t1 (t1 + Δ)) <=
task_request_bound_function tsk Δ
      apply: (@leq_trans (task_cost tsk * number_of_task_arrivals arr_seq tsk t1 (t1 + Δ))).
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
workload_of_jobs (job_of_task tsk)
  (arrivals_between arr_seq t1 (t1 + Δ)) <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <=
task_request_bound_function tsk Δ
      {
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
workload_of_jobs (job_of_task tsk)
  (arrivals_between arr_seq t1 (t1 + Δ)) <=
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) rewrite /workload_of_jobs /number_of_task_arrivals/task_arrivals_between/job_of_task.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
\sum_(j <- arrivals_between arr_seq t1 (t1 + Δ) | 
job_task j == tsk) job_cost j <=
task_cost tsk *
size
  [seq j <- arrivals_between arr_seq t1 (t1 + Δ)
     | job_task j == tsk]
        apply: sum_majorant_constant => j IN TSK.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
j: Job
IN: j \in arrivals_between arr_seq t1 (t1 + Δ)
TSK: job_task j == tsk
job_cost j <= task_cost tsk
        have: valid_job_cost j; last by rewrite /valid_job_cost; move: TSK => /eqP ->.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
j: Job
IN: j \in arrivals_between arr_seq t1 (t1 + Δ)
TSK: job_task j == tsk
valid_job_cost j
        exact/H_valid_job_cost/in_arrivals_implies_arrived. }
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <=
task_request_bound_function tsk Δ
      {
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
task_cost tsk *
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <=
task_request_bound_function tsk Δ rewrite leq_mul2l; apply/orP; right.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <=
max_arrivals tsk Δ
        rewrite -{2}[Δ](addKn t1).
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <=
max_arrivals tsk (t1 + Δ - t1)
        by apply H_task_repsects_max_arrivals; lia. }
    Qed.

    (** For convenience, we combine the preceding bound with
        [workload_of_jobs_weaken], as the two are often used together. *)
    Corollary workload_le_rbf' :
      forall P,
        workload_of_jobs (fun j => (P j) && (job_task j == tsk))
          (arrivals_between arr_seq t1 (t1 + Δ))
        <= task_request_bound_function tsk Δ.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
forall P : Job -> bool,
workload_of_jobs
  (fun j : Job => P j && (job_task j == tsk))
  (arrivals_between arr_seq t1 (t1 + Δ)) <=
task_request_bound_function tsk Δ
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
forall P : Job -> bool,
workload_of_jobs
  (fun j : Job => P j && (job_task j == tsk))
  (arrivals_between arr_seq t1 (t1 + Δ)) <=
task_request_bound_function tsk Δ
      move=> P.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
P: Job -> bool
workload_of_jobs
  (fun j : Job => P j && (job_task j == tsk))
  (arrivals_between arr_seq t1 (t1 + Δ)) <=
task_request_bound_function tsk Δ
      have LEQ: forall ar, workload_of_jobs (fun j : Job => P j && (job_task j == tsk)) ar
                      <= workload_of_jobs (job_of_task tsk) ar
        by move=> ar; apply: workload_of_jobs_weaken => j /andP [_ +].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
tsk: Task
H3: MaxArrivals Task
H_task_repsects_max_arrivals: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
H_valid_job_cost: arrivals_have_valid_job_costs
  arr_seq
t1: instant
Δ: duration
P: Job -> bool
LEQ: forall ar : seq Job,
workload_of_jobs
  (fun j : Job => P j && (job_task j == tsk)) ar <=
workload_of_jobs (job_of_task tsk) ar
workload_of_jobs
  (fun j : Job => P j && (job_task j == tsk))
  (arrivals_between arr_seq t1 (t1 + Δ)) <=
task_request_bound_function tsk Δ
      by apply/(leq_trans (LEQ _))/workload_le_rbf.
    Qed.

  End WorkloadRBF.

  (** In this section, we prove one equality about the workload of a job. *)
  Section WorkloadOfJob.

    (** Assume there are no duplicates in the arrival sequence. *)
    Hypothesis H_arrival_sequence_is_a_set : arrival_sequence_uniq arr_seq.

    (** We prove that the workload of a job in an interval <<[t1,
        t2)>> is equal to the cost of the job if the job's arrival is
        in the interval and [0] otherwise. *)
    Lemma workload_of_job_eq_job_arrival :
      forall (j : Job) (t1 t2 : instant),
        arrives_in arr_seq j ->
        workload_of_job arr_seq j t1 t2
        = if t1 <= job_arrival j < t2 then job_cost j else 0.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq
  arr_seq
forall (j : Job) (t1 t2 : instant),
arrives_in arr_seq j ->
workload_of_job arr_seq j t1 t2 =
(if t1 <= job_arrival j < t2 then job_cost j else 0)
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq
  arr_seq
forall (j : Job) (t1 t2 : instant),
arrives_in arr_seq j ->
workload_of_job arr_seq j t1 t2 =
(if t1 <= job_arrival j < t2 then job_cost j else 0)
      move=> j t1 t2 ARR; case NEQ: (_ <= _ < _).
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq
  arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true
workload_of_job arr_seq j t1 t2 = job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq
  arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = false
workload_of_job arr_seq j t1 t2 = 0
      {
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq
  arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true
workload_of_job arr_seq j t1 t2 = job_cost j rewrite /workload_of_job /workload_of_jobs.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq
  arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true
\sum_(j0 <- arrivals_between arr_seq t1 t2 | j0 == j)
   job_cost j0 = job_cost j
        erewrite big_pred1_seq; first reflexivity.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq
  arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true
j \in arrivals_between arr_seq t1 t2
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq
  arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true
uniq (arrivals_between arr_seq t1 t2)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq
  arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true
eq_op^~ j =1 pred1 j
        -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq
  arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true
j \in arrivals_between arr_seq t1 t2 by apply arrived_between_implies_in_arrivals => //=.
        -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq
  arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true
uniq (arrivals_between arr_seq t1 t2) by done.
        -
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq
  arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = true
eq_op^~ j =1 pred1 j by move => j'; rewrite /pred1 //=.
      }
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq
  arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = false
workload_of_job arr_seq j t1 t2 = 0
      {
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq
  arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = false
workload_of_job arr_seq j t1 t2 = 0 apply big1_seq => j' /andP [/eqP EQ IN]; subst j'; exfalso.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
H_arrival_sequence_is_a_set: arrival_sequence_uniq
  arr_seq
j: Job
t1, t2: instant
ARR: arrives_in arr_seq j
NEQ: (t1 <= job_arrival j < t2) = false
IN: j \in arrivals_between arr_seq t1 t2
False
        by apply job_arrival_between in IN => //.
      }
    Qed.

  End WorkloadOfJob.

  (** In the following section, we relate three types of workload:
      workload of a job [j], workload of higher-or-equal priority jobs
      distinct from [j], and workload of higher-or-equal priority
      jobs. *)
  Section HEPWorkload.

    (** Consider a JLFP policy that indicates a higher-or-equal
        priority relation and assume that the relation is
        reflexive. *)
    Context {JLFP : JLFP_policy Job}.
    Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.

    (** We prove that the sum of the workload of a job [j] and the
        workload of higher-or-equal priority jobs distinct from [j] is
        equal to the workload of higher-or-equal priority jobs. *)
    Lemma workload_job_and_ahep_eq_workload_hep :
      forall (j : Job) (t1 t2 : instant),
        workload_of_job arr_seq j t1 t2 + workload_of_other_hep_jobs arr_seq j t1 t2
        = workload_of_hep_jobs arr_seq j t1 t2.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
forall (j : Job) (t1 t2 : instant),
workload_of_job arr_seq j t1 t2 +
workload_of_other_hep_jobs arr_seq j t1 t2 =
workload_of_hep_jobs arr_seq j t1 t2
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
forall (j : Job) (t1 t2 : instant),
workload_of_job arr_seq j t1 t2 +
workload_of_other_hep_jobs arr_seq j t1 t2 =
workload_of_hep_jobs arr_seq j t1 t2
      move=> j t1 t2.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t1, t2: instant
workload_of_job arr_seq j t1 t2 +
workload_of_other_hep_jobs arr_seq j t1 t2 =
workload_of_hep_jobs arr_seq j t1 t2
      rewrite /workload_of_job /workload_of_other_hep_jobs /workload_of_hep_jobs.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t1, t2: instant
workload_of_jobs (eq_op^~ j)
  (arrivals_between arr_seq t1 t2) +
workload_of_jobs (another_hep_job^~ j)
  (arrivals_between arr_seq t1 t2) =
workload_of_jobs (hep_job^~ j)
  (arrivals_between arr_seq t1 t2)
      rewrite [RHS](workload_of_jobs_case_on_pred _ _  (fun jhp => jhp != j)).
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t1, t2: instant
workload_of_jobs (eq_op^~ j)
  (arrivals_between arr_seq t1 t2) +
workload_of_jobs (another_hep_job^~ j)
  (arrivals_between arr_seq t1 t2) =
workload_of_jobs
  (fun j0 : Job => hep_job j0 j && (j0 != j))
  (arrivals_between arr_seq t1 t2) +
workload_of_jobs
  (fun j0 : Job => hep_job j0 j && ~~ (j0 != j))
  (arrivals_between arr_seq t1 t2)
      have EQ: forall a b c d, a = b -> c = d -> a + c = b + d by lia.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t1, t2: instant
EQ: forall a b c d : nat,
a = b -> c = d -> a + c = b + d
workload_of_jobs (eq_op^~ j)
  (arrivals_between arr_seq t1 t2) +
workload_of_jobs (another_hep_job^~ j)
  (arrivals_between arr_seq t1 t2) =
workload_of_jobs
  (fun j0 : Job => hep_job j0 j && (j0 != j))
  (arrivals_between arr_seq t1 t2) +
workload_of_jobs
  (fun j0 : Job => hep_job j0 j && ~~ (j0 != j))
  (arrivals_between arr_seq t1 t2)
      rewrite addnC; apply EQ; first by reflexivity.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t1, t2: instant
EQ: forall a b c d : nat,
a = b -> c = d -> a + c = b + d
workload_of_jobs (eq_op^~ j)
  (arrivals_between arr_seq t1 t2) =
workload_of_jobs
  (fun j0 : Job => hep_job j0 j && ~~ (j0 != j))
  (arrivals_between arr_seq t1 t2)
      clear EQ; apply workload_of_jobs_equiv_pred => jo IN.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t1, t2: instant
jo: Job
IN: jo \in arrivals_between arr_seq t1 t2
(jo == j) = hep_job jo j && ~~ (jo != j)
      have [EQ|NEQ] := eqVneq j jo.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t1, t2: instant
jo: Job
IN: jo \in arrivals_between arr_seq t1 t2
EQ: j = jo
true = hep_job jo j && ~~ ~~ true
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t1, t2: instant
jo: Job
IN: jo \in arrivals_between arr_seq t1 t2
NEQ: j != jo
false = hep_job jo j && ~~ ~~ false
      {
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t1, t2: instant
jo: Job
IN: jo \in arrivals_between arr_seq t1 t2
EQ: j = jo
true = hep_job jo j && ~~ ~~ true by subst; rewrite andbT; symmetry; apply H_priority_is_reflexive. }
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
j: Job
t1, t2: instant
jo: Job
IN: jo \in arrivals_between arr_seq t1 t2
NEQ: j != jo
false = hep_job jo j && ~~ ~~ false
      by rewrite andbF.
    Qed.

  End HEPWorkload.

  (** If at some point in time [t] the predicate [P] by which we select jobs
      from the set of arrivals in an interval <<[t1, t2)>> becomes certainly
      false, then we may disregard all jobs arriving at time [t] or later. *)
  Lemma workload_of_jobs_nil_tail :
    forall {P t1 t2 t},
      t <= t2 ->
      (forall j, j \in (arrivals_between arr_seq t1 t2) -> job_arrival j >= t -> ~~ P j) ->
      workload_of_jobs P (arrivals_between arr_seq t1 t2)
      = workload_of_jobs P (arrivals_between arr_seq t1 t).
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
forall (P : Job -> bool) (t1 : instant) (t2 t : nat),
t <= t2 ->
(forall j : Job,
 j \in arrivals_between arr_seq t1 t2 ->
 t <= job_arrival j -> ~~ P j) ->
workload_of_jobs P (arrivals_between arr_seq t1 t2) =
workload_of_jobs P (arrivals_between arr_seq t1 t)
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
forall (P : Job -> bool) (t1 : instant) (t2 t : nat),
t <= t2 ->
(forall j : Job,
 j \in arrivals_between arr_seq t1 t2 ->
 t <= job_arrival j -> ~~ P j) ->
workload_of_jobs P (arrivals_between arr_seq t1 t2) =
workload_of_jobs P (arrivals_between arr_seq t1 t)
    move=> P t1 t2 t LE IMPL.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
P: Job -> bool
t1: instant
t2, t: nat
LE: t <= t2
IMPL: forall j : Job,
j \in arrivals_between arr_seq t1 t2 ->
t <= job_arrival j -> ~~ P j
workload_of_jobs P (arrivals_between arr_seq t1 t2) =
workload_of_jobs P (arrivals_between arr_seq t1 t)
    have -> : arrivals_between arr_seq t1 t = [seq j <- (arrivals_between arr_seq t1 t2) | job_arrival j < t]
      by apply: arrivals_between_filter.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
P: Job -> bool
t1: instant
t2, t: nat
LE: t <= t2
IMPL: forall j : Job,
j \in arrivals_between arr_seq t1 t2 ->
t <= job_arrival j -> ~~ P j
workload_of_jobs P (arrivals_between arr_seq t1 t2) =
workload_of_jobs P
  [seq j <- arrivals_between arr_seq t1 t2
     | job_arrival j < t]
    rewrite (workload_of_jobs_filter _ (fun j => job_arrival j < t)) // => j IN Pj.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
P: Job -> bool
t1: instant
t2, t: nat
LE: t <= t2
IMPL: forall j : Job,
j \in arrivals_between arr_seq t1 t2 ->
t <= job_arrival j -> ~~ P j
j: Job
IN: j \in arrivals_between arr_seq t1 t2
Pj: P j
job_arrival j < t
    case: (leqP t (job_arrival j)) => // TAIL.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
P: Job -> bool
t1: instant
t2, t: nat
LE: t <= t2
IMPL: forall j : Job,
j \in arrivals_between arr_seq t1 t2 ->
t <= job_arrival j -> ~~ P j
j: Job
IN: j \in arrivals_between arr_seq t1 t2
Pj: P j
TAIL: t <= job_arrival j
false
    by move: (IMPL j IN TAIL) => /negP.
  Qed.

  (** For simplicity, let's define a local name. *)
  Let arrivals_between := arrivals_between arr_seq.

  (** We observe that the cumulative workload of all jobs arriving in a time
      interval <<[t1, t2)>> and respecting a predicate [P] can be split into two parts. *)
   Lemma workload_of_jobs_cat:
    forall t t1 t2 P,
      t1 <= t <= t2 ->
      workload_of_jobs P (arrivals_between t1 t2) =
      workload_of_jobs P (arrivals_between t1 t) + workload_of_jobs P (arrivals_between t t2).
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
forall (t t1 t2 : nat) (P : pred Job),
t1 <= t <= t2 ->
workload_of_jobs P (arrivals_between t1 t2) =
workload_of_jobs P (arrivals_between t1 t) +
workload_of_jobs P (arrivals_between t t2)
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
forall (t t1 t2 : nat) (P : pred Job),
t1 <= t <= t2 ->
workload_of_jobs P (arrivals_between t1 t2) =
workload_of_jobs P (arrivals_between t1 t) +
workload_of_jobs P (arrivals_between t t2)
    move => t t1 t2 P /andP [GE LE].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
t, t1, t2: nat
P: pred Job
GE: t1 <= t
LE: t <= t2
workload_of_jobs P (arrivals_between t1 t2) =
workload_of_jobs P (arrivals_between t1 t) +
workload_of_jobs P (arrivals_between t t2)
    rewrite /workload_of_jobs /arrivals_between.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
t, t1, t2: nat
P: pred Job
GE: t1 <= t
LE: t <= t2
\sum_(j <- arrival_sequence.arrivals_between arr_seq
             t1 t2 | P j) job_cost j =
\sum_(j <- arrival_sequence.arrivals_between arr_seq
             t1 t | P j) job_cost j +
\sum_(j <- arrival_sequence.arrivals_between arr_seq t
             t2 | P j) job_cost j
    by rewrite (arrivals_between_cat _ _ t) // big_cat.
  Qed.

  (** As a corollary, we prove that the workload in any range <<[t1,t3)>>
      always bounds the workload in any sub-range <<[t1,t2)>>. *)
    Corollary workload_of_jobs_reduce_range :
      forall t1 t2 t3 P,
        t1 <= t2 ->
        t2 <= t3 ->
        workload_of_jobs P (arrivals_between t1 t2)
        <= workload_of_jobs P (arrivals_between t1 t3).
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
forall (t1 t2 t3 : nat) (P : pred Job),
t1 <= t2 ->
t2 <= t3 ->
workload_of_jobs P (arrivals_between t1 t2) <=
workload_of_jobs P (arrivals_between t1 t3)
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
forall (t1 t2 t3 : nat) (P : pred Job),
t1 <= t2 ->
t2 <= t3 ->
workload_of_jobs P (arrivals_between t1 t2) <=
workload_of_jobs P (arrivals_between t1 t3)
      move => t1 t2 t3 P ??.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
t1, t2, t3: nat
P: pred Job
_Hyp_: t1 <= t2
_Hyp1_: t2 <= t3
workload_of_jobs P (arrivals_between t1 t2) <=
workload_of_jobs P (arrivals_between t1 t3)
      rewrite (workload_of_jobs_cat t2 t1 t3 P _  ) //=; [| apply /andP; split; done].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
t1, t2, t3: nat
P: pred Job
_Hyp_: t1 <= t2
_Hyp1_: t2 <= t3
workload_of_jobs P (arrivals_between t1 t2) <=
workload_of_jobs P (arrivals_between t1 t2) +
workload_of_jobs P (arrivals_between t2 t3)
      by apply leq_addr.
    Qed.

  (** Consider a job [j] ... *)
  Variable j : Job.

  (** ... and a duplicate-free sequence of jobs [jobs]. *)
  Variable jobs : seq Job.
  Hypothesis H_jobs_uniq : uniq jobs.

  (** Further, assume that [j] is contained in [jobs]. *)
  Hypothesis H_j_in_jobs : j \in jobs.

  (** To help with rewriting, we prove that the workload of [jobs]
      minus the job cost of [j] is equal to the workload of all jobs
      except [j]. *)
  Lemma workload_minus_job_cost' :
    forall P,
      workload_of_jobs (fun jhp : Job => P jhp && (jhp != j)) jobs
      = workload_of_jobs P jobs - (if P j then job_cost j else 0).
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
forall P : Job -> bool,
workload_of_jobs
  (fun jhp : Job => P jhp && (jhp != j)) jobs =
workload_of_jobs P jobs -
(if P j then job_cost j else 0)
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
forall P : Job -> bool,
workload_of_jobs
  (fun jhp : Job => P jhp && (jhp != j)) jobs =
workload_of_jobs P jobs -
(if P j then job_cost j else 0)
    move => P.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
workload_of_jobs
  (fun jhp : Job => P jhp && (jhp != j)) jobs =
workload_of_jobs P jobs -
(if P j then job_cost j else 0)
    rewrite /workload_of_jobs.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
\sum_(j0 <- jobs | P j0 && (j0 != j)) job_cost j0 =
\sum_(j <- jobs | P j) job_cost j -
(if P j then job_cost j else 0)
    rewrite [in X in _ = X - _](bigID_idem _ _ (fun jo => (jo != j))) //=.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
\sum_(j0 <- jobs | P j0 && (j0 != j)) job_cost j0 =
\sum_(i <- jobs | P i && (i != j)) job_cost i +
\sum_(i <- jobs | P i && ~~ (i != j)) job_cost i -
(if P j then job_cost j else 0)
    have -> :  \sum_(j0 <- jobs | P j0 && ~~ (j0 != j)) job_cost j0 =(if P j then job_cost j else 0);
      last by lia.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
\sum_(j0 <- jobs | P j0 && ~~ (j0 != j)) job_cost j0 =
(if P j then job_cost j else 0)
    rewrite (big_rem j) //=.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
(if P j && ~~ (j != j) then job_cost j else 0) +
\sum_(y <- rem (T:=Job) j jobs | P y && ~~ (y != j))
   job_cost y = (if P j then job_cost j else 0)
    rewrite negbK eq_refl andbT.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
(if P j then job_cost j else 0) +
\sum_(y <- rem (T:=Job) j jobs | P y && ~~ (y != j))
   job_cost y = (if P j then job_cost j else 0)
    have -> :  \sum_(y <- rem (T:=Job) j jobs | P y && ~~ (y != j)) job_cost y= 0;
      last by rewrite addn0.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
\sum_(y <- rem (T:=Job) j jobs | P y && ~~ (y != j))
   job_cost y = 0
    rewrite big_seq_cond.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
\sum_(i <- rem (T:=Job) j jobs | [&& i
                                       \in rem
                                             (T:=Job)
                                             j jobs,
                                     P i
                                   & ~~ (i != j)])
   job_cost i = 0
    apply big_pred0 => jo.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
jo: Job
[&& jo \in rem (T:=Job) j jobs, P jo & ~~ (jo != j)] =
false
    rewrite negbK andbA andbC andbA.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
jo: Job
(jo == j) && (jo \in rem (T:=Job) j jobs) && P jo =
false
    case (P jo); [rewrite andbT | lia].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
jo: Job
(jo == j) && (jo \in rem (T:=Job) j jobs) = false
    case (jo == j) eqn: JJ; [rewrite andTb| lia].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
jo: Job
JJ: (jo == j) = true
(jo \in rem (T:=Job) j jobs) = false
    move : JJ => /eqP ->.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
P: Job -> bool
jo: Job
(j \in rem (T:=Job) j jobs) = false
    by apply mem_rem_uniqF => //=.
  Qed.

  (** Next, we specialize the above lemma to the trivial predicate [predT]. *)
  Corollary workload_minus_job_cost :
    workload_of_jobs (fun jhp : Job => jhp != j) jobs =
    workload_of_jobs predT jobs - job_cost j.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
workload_of_jobs (fun jhp : Job => jhp != j) jobs =
workload_of_jobs predT jobs - job_cost j
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
workload_of_jobs (fun jhp : Job => jhp != j) jobs =
workload_of_jobs predT jobs - job_cost j
    by rewrite (workload_minus_job_cost' predT) //=.
  Qed.

  (** In this section, we prove the relation between two different ways of constraining
      [workload_of_jobs] to only those jobs that arrive prior to a given time. *)
  Section Subset.

    (** Assume that arrival times are consistent and that arrivals are unique. *)
    Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

    (** Consider a time interval <<[t1, t2)>> and a time instant [t]. *)
    Variable t1 t2 t : instant.
    Hypothesis H_t1_le_t2 : t1 <= t2.

    (** Let [P] be an arbitrary predicate on jobs. *)
    Variable P : pred Job.

    (** Consider the window <<[t1,t2)>>. We prove that the total workload of the jobs
        arriving in this window before some [t] is the same as the workload of the jobs
        arriving in <<[t1,t)>>. Note that we only require [t1] to be less-or-equal
        than [t2]. Consequently, the interval <<[t1,t)>> may be empty. *)
    Lemma workload_equal_subset :
      workload_of_jobs (fun j => (job_arrival j <= t) && P j) (arrivals_between t1 t2)
      <= workload_of_jobs (fun j => P j) (arrivals_between t1 (t + ε)).
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
t1, t2, t: instant
H_t1_le_t2: t1 <= t2
P: pred Job
workload_of_jobs
  (fun j : Job => (job_arrival j <= t) && P j)
  (arrivals_between t1 t2) <=
workload_of_jobs [eta P] (arrivals_between t1 (t + 1))
    Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_jobs_uniq: uniq jobs
H_j_in_jobs: j \in jobs
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
t1, t2, t: instant
H_t1_le_t2: t1 <= t2
P: pred Job
workload_of_jobs
  (fun j : Job => (job_arrival j <= t) && P j)
  (arrivals_between t1 t2) <=
workload_of_jobs [eta P] (arrivals_between t1 (t + 1))
      clear H_jobs_uniq H_j_in_jobs H_t1_le_t2.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
t1, t2, t: instant
P: pred Job
workload_of_jobs
  (fun j : Job => (job_arrival j <= t) && P j)
  (arrivals_between t1 t2) <=
workload_of_jobs [eta P] (arrivals_between t1 (t + 1))
      rewrite /workload_of_jobs big_seq_cond.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
t1, t2, t: instant
P: pred Job
\sum_(i <- arrivals_between t1 t2 | [&& i
                                          \in arrivals_between
                                                t1 t2,
                                        job_arrival i <=
                                        t
                                      & P i])
   job_cost i <=
\sum_(j <- arrivals_between t1 (t + 1) | P j)
   job_cost j
      rewrite -[in X in X <= _]big_filter -[in X in _ <= X]big_filter.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
t1, t2, t: instant
P: pred Job
\sum_(i <- [seq i <- arrivals_between t1 t2
              | i \in arrivals_between t1 t2
              & (job_arrival i <= t) && P i])
   job_cost i <=
\sum_(i <- [seq x <- arrivals_between t1 (t + 1)
              | P x]) job_cost i
      apply leq_sum_sub_uniq; first by apply filter_uniq, arrivals_uniq.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
t1, t2, t: instant
P: pred Job
{subset [seq i <- arrivals_between t1 t2
           | i \in arrivals_between t1 t2
           & (job_arrival i <= t) && P i]
     <= [seq x <- arrivals_between t1 (t + 1) | P x]}
      move => j'; rewrite mem_filter => [/andP [/andP [A  /andP [C D]] _]].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
t1, t2, t: instant
P: pred Job
j': Job
A: j' \in arrivals_between t1 t2
C: job_arrival j' <= t
D: P j'
j' \in [seq x <- arrivals_between t1 (t + 1) | P x]
      rewrite job_arrival_in_bounds in A => //=.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
t1, t2, t: instant
P: pred Job
j': Job
C: job_arrival j' <= t
D: P j'
A: arrives_in arr_seq j' /\ t1 <= job_arrival j' < t2
j' \in [seq x <- arrivals_between t1 (t + 1) | P x]
      move : A => [A /andP[A1 A2]].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
t1, t2, t: instant
P: pred Job
j': Job
C: job_arrival j' <= t
D: P j'
A: arrives_in arr_seq j'
A1: t1 <= job_arrival j'
A2: job_arrival j' < t2
j' \in [seq x <- arrivals_between t1 (t + 1) | P x]
      rewrite mem_filter; apply/andP; split=> [//|].
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
t1, t2, t: instant
P: pred Job
j': Job
C: job_arrival j' <= t
D: P j'
A: arrives_in arr_seq j'
A1: t1 <= job_arrival j'
A2: job_arrival j' < t2
j' \in arrivals_between t1 (t + 1)
      apply job_in_arrivals_between => //=.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
H_consistent: consistent_arrival_times arr_seq
arrivals_between:= arrival_sequence.arrivals_between
  arr_seq: instant -> instant -> seq Job
j: Job
jobs: seq Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
t1, t2, t: instant
P: pred Job
j': Job
C: job_arrival j' <= t
D: P j'
A: arrives_in arr_seq j'
A1: t1 <= job_arrival j'
A2: job_arrival j' < t2
job_arrival j' < t + 1
      by lia.
    Qed.

  End Subset.

End WorkloadFacts.