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.
[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]
(** In this file, we prove facts about the job-constructor function when used in pair with the concrete arrival sequence. *) Section JobConstructor. (** Assume that an arrival curve based on a concrete prefix is given. *) #[local] Existing Instance ConcreteMaxArrivals. (** Consider a task set [ts] with non-duplicate tasks. *) Variable ts : seq Task. Hypothesis H_ts_uniq : uniq ts. (** First, we show that [generate_jobs_at tsk n t] generates n jobs ... *)
ts: seq Task
H_ts_uniq: uniq ts

forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
ts: seq Task
H_ts_uniq: uniq ts

forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n
ts: seq Task
H_ts_uniq: uniq ts
tsk: Task
n: nat
t: instant
IN: tsk \in ts

size (generate_jobs_at tsk n t) = n
by rewrite size_map size_iota. Qed. (** ... and that each generated job is unique. *)
ts: seq Task
H_ts_uniq: uniq ts

forall (tsk : concrete_task) (n : nat) (t : instant), uniq (generate_jobs_at tsk n t)
ts: seq Task
H_ts_uniq: uniq ts

forall (tsk : concrete_task) (n : nat) (t : instant), uniq (generate_jobs_at tsk n t)
ts: seq Task
H_ts_uniq: uniq ts
tsk: concrete_task
n: nat
t: instant

uniq (generate_jobs_at tsk n t)
ts: seq Task
H_ts_uniq: uniq ts
tsk: concrete_task
n: nat
t: instant

injective (fun id : nat => {| job_id := id; job_arrival := t; job_cost := task_cost tsk; job_deadline := t + task_deadline tsk; job_task := tsk |})
by move=> x1 x2 /eqP /andP [/andP [/andP [/andP [//= /eqP EQ _] _] _] _]. Qed. (** Next, for convenience, we define [arr_seq] as the concrete arrival sequence used with the job constructor. *) Let arr_seq := concrete_arrival_sequence generate_jobs_at ts. (** We start by proving that the arrival time of a job is consistent with its positioning inside the arrival sequence. *)
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job

forall (j : Job) (t : instant), j \in arrivals_at arr_seq t -> job_arrival j = t
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job

forall (j : Job) (t : instant), j \in arrivals_at arr_seq t -> job_arrival j = t
by move=> j t /mem_bigcat_exists [tsk [TSK_IN /mapP [i INi] ->]]. Qed. (** Next, we show that the list of arrivals at any time [t] is unique ... *)
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job

forall t : instant, uniq (arrivals_at arr_seq t)
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job

forall t : instant, uniq (arrivals_at arr_seq t)
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t: instant

uniq (arrivals_at arr_seq t)
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t: instant

forall (x : concrete_job) (y z : concrete_task), x \in generate_jobs_at y (max_arrivals_at y t) t -> x \in generate_jobs_at z (max_arrivals_at z t) t -> y = z
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t: instant
j: concrete_job
task1, task2: concrete_task
i1: Datatypes_nat__canonical__eqtype_Equality
IN1: i1 \in iota 0 (max_arrivals_at task1 t)
EQj1: j = generate_job_at task1 t i1
i2: Datatypes_nat__canonical__eqtype_Equality
IN2: i2 \in iota 0 (max_arrivals_at task2 t)
EQj2: j = generate_job_at task2 t i2

task1 = task2
by move: EQj1 EQj2 => -> [_]. Qed. (** ... and generalize the above result to arbitrary time intervals. *)
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job

forall t1 t2 : instant, uniq (arrivals_between arr_seq t1 t2)
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job

forall t1 t2 : instant, uniq (arrivals_between arr_seq t1 t2)
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t1, t2: instant

uniq (arrivals_between arr_seq t1 t2)
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t1, t2: instant

uniq (\cat_(t1<=t<t2)arrivals_at arr_seq t)
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t1, t2: instant

forall i : nat, uniq (arrivals_at arr_seq i)
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t1, t2: instant
forall (x : Job) (i1 i2 : nat), x \in arrivals_at arr_seq i1 -> x \in arrivals_at arr_seq i2 -> i1 = i2
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t1, t2: instant

forall i : nat, uniq (arrivals_at arr_seq i)
by apply arrivals_at_unique.
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t1, t2: instant

forall (x : Job) (i1 i2 : nat), x \in arrivals_at arr_seq i1 -> x \in arrivals_at arr_seq i2 -> i1 = i2
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t1, t2: instant
j: Job
jt1, jt2: nat
IN1: j \in arrivals_at arr_seq jt1
IN2: j \in arrivals_at arr_seq jt2

jt1 = jt2
by move: (job_arrival_consistent j jt1 IN1) (job_arrival_consistent j jt2 IN2) => <- <-. Qed. (** Finally, we observe that [generate_jobs_at tsk n t] indeed generates jobs of task [tsk] that arrive at [t] *)
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job

forall (tsk : concrete_task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job

forall (tsk : concrete_task) (n : nat) (t : instant) (j : Job), j \in generate_jobs_at tsk n t -> job_task j = tsk /\ job_arrival j = t /\ job_cost j <= task_cost tsk
by move=> tsk n t j /mapP [i INi] ->. Qed. End JobConstructor.