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

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

  (** Next, consider any job arrival sequence consistent with the arrival times
      of the jobs. *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_consistent : consistent_arrival_times arr_seq.

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

  (** 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]. To define the workload of all jobs, since
      [workload_of_jobs] expects a predicate, we use [predT], which
      is the always-true predicate. *)
  Lemma 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
    rewrite /workload_of_jobs (big_rem j) //=  eq_refl //= add0n.
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
\sum_(y <- rem (T:=Job) j jobs | y != j) job_cost y =
\sum_(j <- jobs) job_cost j - job_cost j
    rewrite [in RHS](big_rem j) //= addnC -subnBA //= subnn subn0.
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
\sum_(y <- rem (T:=Job) j jobs | y != j) job_cost y =
\sum_(y <- rem (T:=Job) j jobs) job_cost y
    rewrite [in LHS]big_seq_cond [in RHS]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
\sum_(i <- rem (T:=Job) j jobs | (i
                                    \in rem (T:=Job) j
                                          jobs) &&
                                 (i != j)) job_cost i =
\sum_(i <- rem (T:=Job) j jobs | (i
                                    \in rem (T:=Job) j
                                          jobs) &&
                                 true) job_cost i
    apply eq_bigl => 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
j': Job
(j' \in rem (T:=Job) j jobs) && (j' != j) =
(j' \in rem (T:=Job) j jobs) && true
    rewrite Bool.andb_true_r.
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
j': Job
(j' \in rem (T:=Job) j jobs) && (j' != j) =
(j' \in rem (T:=Job) j jobs)
    destruct (j' \in rem (T:=Job) j jobs) eqn:INjobs; last 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
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
j': Job
INjobs: (j' \in rem (T:=Job) j jobs) = true
true && (j' != j) = true
    apply /negP => /eqP EQUAL.
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
j': Job
INjobs: (j' \in rem (T:=Job) j jobs) = true
EQUAL: j' = j
False
    by rewrite EQUAL mem_rem_uniqF in INjobs.
  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 + ε))
    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 + ε))
      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 + ε))
      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 + ε) | 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 + ε)
              | P x]) job_cost i
      apply leq_sum_sub_uniq; first by apply filter_uniq, arrivals_uniq; rt_eauto.
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 + ε) | 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 + ε) | P x]
      rewrite mem_filter; apply/andP; split; first 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
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 arrivals_between t1 (t + ε)
      apply job_in_arrivals_between; eauto.
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'
arrives_in arr_seq 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_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'
t1 <= job_arrival j' < 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_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'
arrives_in arr_seq 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_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'
t1 <= job_arrival j' < t + ε by eapply in_arrivals_implies_arrived; eauto 2.
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'
t1 <= job_arrival j' < 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_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'
t1 <= job_arrival j' < t + ε apply in_arrivals_implies_arrived_between in A; auto; move: A => /andP [A E].
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: t1 <= job_arrival j'
E: job_arrival j' < t2
t1 <= job_arrival j' < t + ε
        by unfold ε; apply/andP; split; lia.
    Qed.

  End Subset.

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

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

End WorkloadFacts.