Require Export prosa.analysis.facts.periodic.arrival_separation.
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]

(** ** Periodic Task Model respects the Task Max Inter-Arrival model. *)

(** In this section, we show that the periodic task model 
    respects the task max inter-arrival model (i.e. consecutive jobs 
    of a task are separated at most by a certain duration specified by
    the [task_max_inter_arrival_time] parameter). *)
Section PeriodicTasksRespectMaxInterArrivalModel.
  
  (** Consider any type of periodic tasks, ... *)
  Context {Task : TaskType} `{PeriodicModel Task}.
  
  (** ... any type of jobs associated with the tasks, ... *)
  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
  
  (** ... and any arrival sequence. *)
  Variable arr_seq : arrival_sequence Job.

  (** By using each task's period as its maximum inter-arrival time, ... *)
  Global Instance max_inter_eq_period : TaskMaxInterArrival Task :=
    {
      task_max_inter_arrival_time := task_period
    }.
  
  (** ... we observe that for any task [tsk], 
      [task_max_inter_arrival_time tsk] is positive, ... *)
  Remark valid_period_is_valid_max_inter_arrival_time:
    forall tsk, valid_period tsk -> positive_task_max_inter_arrival_time tsk.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
forall tsk : Task,
valid_period tsk ->
positive_task_max_inter_arrival_time tsk
  Proof.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
forall tsk : Task,
valid_period tsk ->
positive_task_max_inter_arrival_time tsk trivial. Qed.

  (** ... and show that the periodic model respects the task max inter-arrival model. *)
  Remark periodic_model_respects_max_inter_arrival_model:
    forall tsk,
      valid_period tsk -> 
      respects_periodic_task_model arr_seq tsk ->
      valid_task_max_inter_arrival_time arr_seq tsk.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
forall tsk : Task,
valid_period tsk ->
respects_periodic_task_model arr_seq tsk ->
valid_task_max_inter_arrival_time arr_seq tsk
    Proof.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
forall tsk : Task,
valid_period tsk ->
respects_periodic_task_model arr_seq tsk ->
valid_task_max_inter_arrival_time arr_seq tsk
      intros tsk VALID_PERIOD PERIODIC.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
PERIODIC: respects_periodic_task_model arr_seq tsk
valid_task_max_inter_arrival_time arr_seq tsk
      split; first by apply VALID_PERIOD => //.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
PERIODIC: respects_periodic_task_model arr_seq tsk
arr_sep_task_max_inter_arrival arr_seq tsk
      intros j ARR TSK IND.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
PERIODIC: respects_periodic_task_model arr_seq tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
exists j' : Job,
  j <> j' /\
  arrives_in arr_seq j' /\
  job_task j' = tsk /\
  job_arrival j' <= job_arrival j <=
  job_arrival j' + task_max_inter_arrival_time tsk
      specialize (PERIODIC j); feed_n 3 PERIODIC => //.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
PERIODIC: exists j' : Job,
  arrives_in arr_seq j' /\
  job_index arr_seq j' =
  job_index arr_seq j - 1 /\
  job_task j' = tsk /\
  job_arrival j =
  job_arrival j' + task_period tsk
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
exists j' : Job,
  j <> j' /\
  arrives_in arr_seq j' /\
  job_task j' = tsk /\
  job_arrival j' <= job_arrival j <=
  job_arrival j' + task_max_inter_arrival_time tsk 
      move : PERIODIC => [j' [ARR' [IND' [TSK' ARRJ']]]].
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
exists j' : Job,
  j <> j' /\
  arrives_in arr_seq j' /\
  job_task j' = tsk /\
  job_arrival j' <= job_arrival j <=
  job_arrival j' + task_max_inter_arrival_time tsk
      exists j'; repeat split => //.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
j <> j'
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
job_arrival j' <= job_arrival j <=
job_arrival j' + task_max_inter_arrival_time tsk
      {
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
j <> j' case: (boolP (j == j')) => [/eqP EQ|NEQ].
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
EQ: j = j'
j <> j'
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
NEQ: j != j'
j <> j'
        -
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
EQ: j = j'
j <> j'
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
NEQ: j != j'
j <> j' have EQ_IND : (job_index arr_seq j' = job_index arr_seq j) by apply f_equal => //.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
EQ: j = j'
EQ_IND: job_index arr_seq j' = job_index arr_seq j
j <> j'
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
NEQ: j != j'
j <> j'
          now exfalso; lia.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
NEQ: j != j'
j <> j'
        -
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
NEQ: j != j'
j <> j' now apply /eqP. }
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
job_arrival j' <= job_arrival j <=
job_arrival j' + task_max_inter_arrival_time tsk
      {
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
job_arrival j' <= job_arrival j <=
job_arrival j' + task_max_inter_arrival_time tsk have NZ_PERIOD : (task_period tsk > 0) by apply VALID_PERIOD.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
NZ_PERIOD: 0 < task_period tsk
job_arrival j' <= job_arrival j <=
job_arrival j' + task_max_inter_arrival_time tsk
        rewrite /max_inter_eq_period /task_max_inter_arrival_time ARRJ'.
Task: TaskType
H: PeriodicModel Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
tsk: Task
VALID_PERIOD: valid_period tsk
j: Job
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
IND: 0 < job_index arr_seq j
j': Job
ARR': arrives_in arr_seq j'
IND': job_index arr_seq j' = job_index arr_seq j - 1
TSK': job_task j' = tsk
ARRJ': job_arrival j =
job_arrival j' + task_period tsk
NZ_PERIOD: 0 < task_period tsk
job_arrival j' <= job_arrival j' + task_period tsk <=
job_arrival j' + task_period tsk 
        now lia. }
    Qed.
    
End PeriodicTasksRespectMaxInterArrivalModel.