Library prosa.analysis.facts.model.offset


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)

Require Export prosa.model.task.offset.
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_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].
  Lemma first_job_arrival:
    job_index arr_seq j = 0 →
    job_arrival j = task_offset tsk.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 41)
  
  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

----------------------------------------------------------------------------- *)

  Proof.
    intros INDX.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 42)
  
  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

----------------------------------------------------------------------------- *)

    move: H_valid_offset ⇒ [BEFORE [j' [ARR' [TSK ARRIVAL]]]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 84)
  
  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

----------------------------------------------------------------------------- *)

    case: (boolP (j' == j)) ⇒ [/eqP EQ|NEQ]; first by rewrite -EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 128)
  
  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

----------------------------------------------------------------------------- *)

    destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j')) as [Z | [m N]].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 142)
  
  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

subgoal 2 (ID 147) is:
 job_arrival j = task_offset tsk

----------------------------------------------------------------------------- *)

    - move: NEQ ⇒ /eqP NEQ; contradict NEQ.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 193)
  
  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

subgoal 2 (ID 147) is:
 job_arrival j = task_offset tsk

----------------------------------------------------------------------------- *)

      now eapply equal_index_implies_equal_jobs; eauto;
        [rewrite TSK | rewrite Z INDX].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 147)
  
  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

----------------------------------------------------------------------------- *)

    - have IND_LTE : (job_index arr_seq j ≤ job_index arr_seq j') by rewrite INDX N.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 231)
  
  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

----------------------------------------------------------------------------- *)

      apply index_lte_implies_arrival_lte in IND_LTE ⇒ //; last by rewrite TSK.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 237)
  
  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;
        [ssrlia | apply H_valid_offset].

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 50)
  
  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

----------------------------------------------------------------------------- *)

  Proof.
    intros TSK_IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 51)
  
  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

----------------------------------------------------------------------------- *)

    apply in_max0_le.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 52)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End OffsetLemmas.