Library prosa.analysis.facts.model.workload


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


Require Export prosa.model.aggregate.workload.
Require Export prosa.analysis.facts.behavior.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}.

Consider any job arrival sequence.
  Variable arr_seq : arrival_sequence Job.

For simplicity, let's define a local name.
We prove that workload can be split into two parts.
  Lemma workload_of_jobs_cat:
     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).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 342)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  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.
    movet t1 t2 P /andP [GE LE].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 386)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 392)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  arr_seq : arrival_sequence Job
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

End WorkloadFacts.