offset.v

Require Export prosa.model.task.offset.[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]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_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.job_index.

(** 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_valid_arrival_sequence : valid_arrival_sequence 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]. *)
  Lemma first_job_arrival:
    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_valid_arrival_sequence: valid_arrival_sequence
  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
  Proof.Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  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
    intros INDX.Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  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
    move: H_valid_offset => [BEFORE [j' [ARR' [TSK ARRIVAL]]]].Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  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
    case: (boolP (j' == j)) => [/eqP EQ|NEQ]; first by rewrite -EQ.Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  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
    destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j')) as [Z | [m N]].Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  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_valid_arrival_sequence: valid_arrival_sequence
  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_valid_arrival_sequence: valid_arrival_sequence
  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 move: NEQ => /eqP NEQ; contradict NEQ.Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  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
      by eapply equal_index_implies_equal_jobs; eauto;
        [rewrite TSK | rewrite Z INDX].
    -Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  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 have IND_LTE : (job_index arr_seq j <= job_index arr_seq j') by rewrite INDX N.Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  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
      apply index_lte_implies_arrival_lte in IND_LTE => //; last by rewrite TSK.Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  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
      by 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]. *)
  Lemma max_offset_g:
    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_valid_arrival_sequence: valid_arrival_sequence
  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
  Proof.Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  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
    intros TSK_IN.Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  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
    apply in_max0_le.Task: TaskType
H: TaskOffset Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  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
    by apply map_f.
  Qed.

End OffsetLemmas.