Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.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.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
(** In this module, we prove some properties of task offsets. *) Section OffsetLemmas. (** Consider any type of tasks with an offset ... *) Context {Task : TaskType}. Context `{TaskOffset Task}. (** ... and any type of jobs associated with these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. (** Consider any arrival sequence with consistent and non-duplicate arrivals ... *) Variable arr_seq : arrival_sequence Job. Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq. Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq. (** ... and any job [j] (that stems from the arrival sequence) of any task [tsk] with a valid offset. *) Variable tsk : Task. Variable j : Job. Hypothesis H_job_of_task: job_task j = tsk. Hypothesis H_valid_offset: valid_offset arr_seq tsk. Hypothesis H_job_from_arrseq: arrives_in arr_seq j. (** We show that the if [j] is the first job of task [tsk] then [j] arrives at [task_offset tsk]. *)
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j

job_index arr_seq j = 0 -> job_arrival j = task_offset tsk
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j

job_index arr_seq j = 0 -> job_arrival j = task_offset tsk
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
INDX: job_index arr_seq j = 0

job_arrival j = task_offset tsk
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
INDX: job_index arr_seq j = 0
BEFORE: no_jobs_before_offset tsk
j': Job
ARR': arrives_in arr_seq j'
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' = task_offset tsk

job_arrival j = task_offset tsk
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
INDX: job_index arr_seq j = 0
BEFORE: no_jobs_before_offset tsk
j': Job
ARR': arrives_in arr_seq j'
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' = task_offset tsk
NEQ: j' != j

job_arrival j = task_offset tsk
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
INDX: job_index arr_seq j = 0
BEFORE: no_jobs_before_offset tsk
j': Job
ARR': arrives_in arr_seq j'
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' = task_offset tsk
NEQ: j' != j
Z: job_index arr_seq j' = 0

job_arrival j = task_offset tsk
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
INDX: job_index arr_seq j = 0
BEFORE: no_jobs_before_offset tsk
j': Job
ARR': arrives_in arr_seq j'
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' = task_offset tsk
NEQ: j' != j
m: nat
N: job_index arr_seq j' = m.+1
job_arrival j = task_offset tsk
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
INDX: job_index arr_seq j = 0
BEFORE: no_jobs_before_offset tsk
j': Job
ARR': arrives_in arr_seq j'
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' = task_offset tsk
NEQ: j' != j
Z: job_index arr_seq j' = 0

job_arrival j = task_offset tsk
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
INDX: job_index arr_seq j = 0
BEFORE: no_jobs_before_offset tsk
j': Job
ARR': arrives_in arr_seq j'
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' = task_offset tsk
NEQ: j' != j
m: nat
N: job_index arr_seq j' = m.+1
job_arrival j = task_offset tsk
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
INDX: job_index arr_seq j = 0
BEFORE: no_jobs_before_offset tsk
j': Job
ARR': arrives_in arr_seq j'
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' = task_offset tsk
Z: job_index arr_seq j' = 0

j' = j
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
INDX: job_index arr_seq j = 0
BEFORE: no_jobs_before_offset tsk
j': Job
ARR': arrives_in arr_seq j'
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' = task_offset tsk
NEQ: j' != j
m: nat
N: job_index arr_seq j' = m.+1
job_arrival j = task_offset tsk
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
INDX: job_index arr_seq j = 0
BEFORE: no_jobs_before_offset tsk
j': Job
ARR': arrives_in arr_seq j'
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' = task_offset tsk
NEQ: j' != j
m: nat
N: job_index arr_seq j' = m.+1

job_arrival j = task_offset tsk
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
INDX: job_index arr_seq j = 0
BEFORE: no_jobs_before_offset tsk
j': Job
ARR': arrives_in arr_seq j'
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' = task_offset tsk
NEQ: j' != j
m: nat
N: job_index arr_seq j' = m.+1

job_arrival j = task_offset tsk
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
INDX: job_index arr_seq j = 0
BEFORE: no_jobs_before_offset tsk
j': Job
ARR': arrives_in arr_seq j'
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' = task_offset tsk
NEQ: j' != j
m: nat
N: job_index arr_seq j' = m.+1
IND_LTE: job_index arr_seq j <= job_index arr_seq j'

job_arrival j = task_offset tsk
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
INDX: job_index arr_seq j = 0
BEFORE: no_jobs_before_offset tsk
j': Job
ARR': arrives_in arr_seq j'
TSK: job_task j' = tsk
ARRIVAL: job_arrival j' = task_offset tsk
NEQ: j' != j
m: nat
N: job_index arr_seq j' = m.+1
IND_LTE: job_arrival j <= job_arrival j'

job_arrival j = task_offset tsk
now apply/eqP; rewrite eqn_leq; apply/andP; split; [lia | apply H_valid_offset]. Qed. (** Consider any task set [ts]. *) Variable ts : TaskSet Task. (** If task [tsk] is in [ts], then its offset is less than or equal to the maximum offset of all tasks in [ts]. *)
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
ts: TaskSet Task

tsk \in ts -> task_offset tsk <= max_task_offset ts
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
ts: TaskSet Task

tsk \in ts -> task_offset tsk <= max_task_offset ts
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
ts: TaskSet Task
TSK_IN: tsk \in ts

task_offset tsk <= max_task_offset ts
Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_consistent_arrivals: consistent_arrival_times arr_seq
H_uniq_arr_seq: arrival_sequence_uniq arr_seq
tsk: Task
j: Job
H_job_of_task: job_task j = tsk
H_valid_offset: valid_offset arr_seq tsk
H_job_from_arrseq: arrives_in arr_seq j
ts: TaskSet Task
TSK_IN: tsk \in ts

task_offset tsk \in task_offsets ts
now apply map_f. Qed. End OffsetLemmas.