Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Import prosa.model.priority.elf.[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 ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_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.priority.classes.
Require Export prosa.analysis.definitions.priority.classes.
Require Export prosa.analysis.facts.model.workload.
(** In this file, we prove lemmas that are useful when both an FP policy and
a JLFP policy are present in context. *)
(** In this section, we prove a lemma about workload partitioning which is useful
for reasoning about the interference bound function for the ELF scheduling policy. *)
Section WorkloadTaskSum .
(** Consider any type of tasks with relative priority points...*)
Context {Task : TaskType} `{PriorityPoint Task}.
(** ...and jobs of these tasks. *)
Context {Job : JobType} `{JobArrival Job} `{JobTask Job Task} `{JobCost Job} .
(** Let us consider an FP policy and a compatible JLFP policy present in context. *)
Context {FP : FP_policy Task}.
Context {JLFP : JLFP_policy Job}.
Hypothesis JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP.
(** Consider any valid arrival sequence [arr_seq]. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence (arr_seq).
(** We consider an arbitrary task set [ts]... *)
Variable ts : seq Task.
Hypothesis H_task_set : uniq ts.
(** ... and assume that all jobs stem from tasks in this task set. *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** Let [tsk] be any task in [ts] that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** We define a predicate to identify others tasks which have equal priority as [tsk]. *)
Definition other_ep_task := fun tsk_o => (ep_task tsk tsk_o) && (tsk_o != tsk).
(** We consider a job [j] belonging to this task ... *)
Variable j : Job.
Hypothesis H_job_of_task : job_of_task tsk j.
(** ... and focus on the jobs arriving in an arbitrary interval <<[t1, t2)>>. *)
Variable t1 t2 : duration.
Let jobs_arrived := arrivals_between arr_seq t1 t2.
(** We first consider jobs that belong to other tasks that have equal priority
as [tsk] and have higher-or-equal priority [JLFP] than [j]. *)
Definition hep_job_of_ep_other_task :=
fun j' : Job =>
hep_job j' j
&& ep_task (job_task j') (job_task j)
&& (job_task j' != job_task j).
(** We then establish that the cumulative workload of these jobs can be partitioned
task-wise. *)
Lemma hep_workload_from_other_ep_partitioned_by_tasks :
workload_of_jobs hep_job_of_ep_other_task jobs_arrived
= \sum_(tsk_o <- ts | other_ep_task tsk_o)
workload_of_jobs
(fun j0 => hep_job_of_ep_other_task j0 && (job_task j0 == tsk_o))
jobs_arrived.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job
workload_of_jobs hep_job_of_ep_other_task jobs_arrived =
\sum_(tsk_o <- ts | other_ep_task tsk_o)
workload_of_jobs
(fun j0 : Job =>
hep_job_of_ep_other_task j0 &&
(job_task j0 == tsk_o)) jobs_arrived
Proof .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job
workload_of_jobs hep_job_of_ep_other_task jobs_arrived =
\sum_(tsk_o <- ts | other_ep_task tsk_o)
workload_of_jobs
(fun j0 : Job =>
hep_job_of_ep_other_task j0 &&
(job_task j0 == tsk_o)) jobs_arrived
apply : workload_of_jobs_partitioned_by_tasks => //.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job
{in jobs_arrived, forall j : Job, job_task j \in ts}
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job
{in jobs_arrived, forall j : Job, job_task j \in ts}
by move => j' IN'; apply /H_all_jobs_from_taskset/in_arrivals_implies_arrived/IN'.
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job
{in jobs_arrived,
forall j : Job,
hep_job_of_ep_other_task j ->
other_ep_task (job_task j)}
move : H_job_of_task => /eqP TSK j' IN'.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job TSK : job_task j = tsk j' : Job IN' : j' \in jobs_arrived
hep_job_of_ep_other_task j' ->
other_ep_task (job_task j')
rewrite /other_ep_task /hep_job_of_ep_other_task TSK
=> /andP [/andP [_ EP] NEQ].Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job TSK : job_task j = tsk j' : Job IN' : j' \in jobs_arrived EP : ep_task (job_task j') tsk NEQ : job_task j' != tsk
ep_task tsk (job_task j') && (job_task j' != tsk)
apply /andP; split => //.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job TSK : job_task j = tsk j' : Job IN' : j' \in jobs_arrived EP : ep_task (job_task j') tsk NEQ : job_task j' != tsk
ep_task tsk (job_task j')
by rewrite ep_task_sym.
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job
uniq jobs_arrived
by apply : arrivals_uniq.
Qed .
(** Now we focus on jobs belonging to tasks which have higher priority than [tsk]. *)
Definition from_hp_task (j' : Job) :=
hp_task (job_task j') (job_task j).
(** We also identify higher-or-equal-priority jobs [JLFP] that belong to
(1) tasks having higher priority than [tsk] ... *)
Definition hep_from_hp_task (j' : Job) :=
hep_job j' j && hp_task (job_task j') (job_task j).
(** ... (2) tasks having equal priority as [tsk]. *)
Definition hep_from_ep_task (j' : Job) :=
hep_job j' j && ep_task (job_task j') (job_task j).
(** First, we establish that the cumulative workload of higher-or-equal-priority
jobs belonging to tasks having higher priority than [tsk] is equal to the
cumulative workload of jobs belonging to higher-priority tasks. *)
Lemma hep_hp_workload_hp :
workload_of_jobs hep_from_hp_task jobs_arrived = workload_of_jobs from_hp_task jobs_arrived.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job
workload_of_jobs hep_from_hp_task jobs_arrived =
workload_of_jobs from_hp_task jobs_arrived
Proof .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job
workload_of_jobs hep_from_hp_task jobs_arrived =
workload_of_jobs from_hp_task jobs_arrived
apply /eq_bigl =>j0; apply /idP/idP.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job j0 : Job
hep_from_hp_task j0 -> from_hp_task j0
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job j0 : Job
hep_from_hp_task j0 -> from_hp_task j0
by move => /andP[].
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job j0 : Job
from_hp_task j0 -> hep_from_hp_task j0
move => Hp; apply /andP; split =>//.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job j0 : Job Hp : from_hp_task j0
hep_job j0 j
by apply : (hp_task_implies_hep_job JLFP FP).
Qed .
(** We then establish that the cumulative workload of higher-or-equal priority jobs
is equal to the sum of cumulative workload of higher-or-equal priority jobs
belonging to higher-priority tasks and the cumulative workload of
higher-or-equal-priority jobs belonging to equal-priority tasks. *)
Lemma hep_workload_partitioning_taskwise :
workload_of_higher_or_equal_priority_jobs j jobs_arrived
= workload_of_jobs hep_from_hp_task jobs_arrived
+ workload_of_jobs hep_from_ep_task jobs_arrived.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job
workload_of_higher_or_equal_priority_jobs j
jobs_arrived =
workload_of_jobs hep_from_hp_task jobs_arrived +
workload_of_jobs hep_from_ep_task jobs_arrived
Proof .Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job
workload_of_higher_or_equal_priority_jobs j
jobs_arrived =
workload_of_jobs hep_from_hp_task jobs_arrived +
workload_of_jobs hep_from_ep_task jobs_arrived
rewrite /workload_of_higher_or_equal_priority_jobs /workload_of_jobs.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job
\sum_(j0 <- jobs_arrived | hep_job j0 j) job_cost j0 =
\sum_(j <- jobs_arrived | hep_from_hp_task j)
job_cost j +
\sum_(j <- jobs_arrived | hep_from_ep_task j)
job_cost j
rewrite (bigID from_hp_task) /=; congr (_ + _); apply : eq_bigl => j0.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job j0 : Job
hep_job j0 j && ~~ from_hp_task j0 =
hep_from_ep_task j0
apply : andb_id2l => HEPj.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job j0 : Job HEPj : hep_job j0 j
~~ from_hp_task j0 =
ep_task (job_task j0) (job_task j)
have HEPt : hep_task (job_task j0) (job_task j) by apply (hep_job_implies_hep_task JLFP).Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job j0 : Job HEPj : hep_job j0 j HEPt : hep_task (job_task j0) (job_task j)
~~ from_hp_task j0 =
ep_task (job_task j0) (job_task j)
apply /idP/idP; rewrite negb_and.Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job j0 : Job HEPj : hep_job j0 j HEPt : hep_task (job_task j0) (job_task j)
~~ hep_task (job_task j0) (job_task j)
|| ~~ ~~ hep_task (job_task j) (job_task j0) ->
ep_task (job_task j0) (job_task j)
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job j0 : Job HEPj : hep_job j0 j HEPt : hep_task (job_task j0) (job_task j)
~~ hep_task (job_task j0) (job_task j)
|| ~~ ~~ hep_task (job_task j) (job_task j0) ->
ep_task (job_task j0) (job_task j)
move =>/orP[nHEPt| /negPn ?].Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job j0 : Job HEPj : hep_job j0 j HEPt : hep_task (job_task j0) (job_task j) nHEPt : ~~ hep_task (job_task j0) (job_task j)
ep_task (job_task j0) (job_task j)
+ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job j0 : Job HEPj : hep_job j0 j HEPt : hep_task (job_task j0) (job_task j) nHEPt : ~~ hep_task (job_task j0) (job_task j)
ep_task (job_task j0) (job_task j)
exfalso ; by move : nHEPt; rewrite HEPt.
+ Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job j0 : Job HEPj : hep_job j0 j HEPt : hep_task (job_task j0) (job_task j) __view_subject_2_ : hep_task (job_task j)
(job_task j0)
ep_task (job_task j0) (job_task j)
by apply /andP.
- Task : TaskType H : PriorityPoint Task Job : JobType H0 : JobArrival Job H1 : JobTask Job Task H2 : JobCost Job FP : FP_policy Task JLFP : JLFP_policy Job JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq ts : seq Task H_task_set : uniq ts H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts j : Job H_job_of_task : job_of_task tsk j t1, t2 : duration jobs_arrived := arrivals_between arr_seq t1 t2 : seq Job j0 : Job HEPj : hep_job j0 j HEPt : hep_task (job_task j0) (job_task j)
ep_task (job_task j0) (job_task j) ->
~~ hep_task (job_task j0) (job_task j)
|| ~~ ~~ hep_task (job_task j) (job_task j0)
by move => /andP[? ?]; apply /orP; right ; apply /negPn.
Qed .
End WorkloadTaskSum .