Library prosa.analysis.facts.model.workload
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
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.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any job arrival sequence.
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 31)
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.
move ⇒ t t1 t2 P /andP [GE LE].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 74)
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 80)
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.
∀ 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 31)
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.
move ⇒ t t1 t2 P /andP [GE LE].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 74)
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 80)
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.