Library rt.restructuring.analysis.basic_facts.workload
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Export workload schedule.priority_based.priorities.
From rt.restructuring.analysis Require Import basic_facts.arrivals.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
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 182)
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 : Job -> bool),
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 226)
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 : Job -> bool
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 232)
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 : Job -> bool
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 182)
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 : Job -> bool),
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 226)
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 : Job -> bool
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 232)
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 : Job -> bool
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.