Library prosa.analysis.facts.periodic.sporadic


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

Welcome to Coq 8.11.2 (June 2020)

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


Require Export prosa.model.task.arrival.periodic.

Treating Periodic Tasks as Sporadic Tasks

Since the periodic-arrivals assumption is stricter than the sporadic-arrivals assumption (i.e., any periodic arrival sequence is also a valid sporadic arrivals sequence), it is sometimes convenient to apply analyses for sporadic tasks to periodic tasks. We therefore provide an automatic "conversion" of periodic tasks to sporadic tasks, i.e., we tell Coq that it may use a periodic task's [task_period] parameter also as the task's minimum inter-arrival time [task_min_inter_arrival_time] parameter.
Any type of periodic tasks ...
  Context {Task : TaskType} `{PeriodicModel Task}.

... and their corresponding jobs from a consistent arrival sequence with non-duplicate arrivals ...
... may be interpreted as a type of sporadic tasks by using each task's period as its minimum inter-arrival time ...
  Global Instance periodic_as_sporadic : SporadicModel Task :=
    {
      task_min_inter_arrival_time := task_period
    }.

... such that the model interpretation is valid, both w.r.t. the minimum inter-arrival time parameter ...
  Remark valid_period_is_valid_inter_arrival_time:
     tsk, valid_period tsk valid_task_min_inter_arrival_time tsk.

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

1 subgoal (ID 44)
  
  Task : TaskType
  H : PeriodicModel 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
  ============================
  forall tsk : Task,
  valid_period tsk -> valid_task_min_inter_arrival_time tsk

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


  Proof. trivial.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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


Qed.

... and the separation of job arrivals.
  Remark periodic_task_respects_sporadic_task_model:
     tsk, valid_period tsk
           respects_periodic_task_model arr_seq tsk
           respects_sporadic_task_model arr_seq tsk.

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

1 subgoal (ID 61)
  
  Task : TaskType
  H : PeriodicModel 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
  ============================
  forall tsk : Task,
  valid_period tsk ->
  respects_periodic_task_model arr_seq tsk ->
  respects_sporadic_task_model arr_seq tsk

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


  Proof.
    intros tsk VALID_PERIOD H_PERIODIC j1 j2 NEQ ARR ARR' TSK TSK' ARR_LT.

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

1 subgoal (ID 73)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  H_PERIODIC : respects_periodic_task_model arr_seq tsk
  j1, j2 : Job
  NEQ : j1 <> j2
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  ARR_LT : job_arrival j1 <= job_arrival j2
  ============================
  job_arrival j1 + task_min_inter_arrival_time tsk <= job_arrival j2

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


    rewrite /task_min_inter_arrival_time /periodic_as_sporadic.

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

1 subgoal (ID 79)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  H_PERIODIC : respects_periodic_task_model arr_seq tsk
  j1, j2 : Job
  NEQ : j1 <> j2
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  ARR_LT : job_arrival j1 <= job_arrival j2
  ============================
  job_arrival j1 + task_period tsk <= job_arrival j2

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


    have IND_LT : job_index arr_seq j1 < job_index arr_seq j2.

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

2 subgoals (ID 88)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  H_PERIODIC : respects_periodic_task_model arr_seq tsk
  j1, j2 : Job
  NEQ : j1 <> j2
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  ARR_LT : job_arrival j1 <= job_arrival j2
  ============================
  job_index arr_seq j1 < job_index arr_seq j2

subgoal 2 (ID 90) is:
 job_arrival j1 + task_period tsk <= job_arrival j2

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


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

1 subgoal (ID 88)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  H_PERIODIC : respects_periodic_task_model arr_seq tsk
  j1, j2 : Job
  NEQ : j1 <> j2
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  ARR_LT : job_arrival j1 <= job_arrival j2
  ============================
  job_index arr_seq j1 < job_index arr_seq j2

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


rewritediff_jobs_iff_diff_indices in NEQ ⇒ //; auto; last by rewrite TSK.

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

1 subgoal (ID 107)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  H_PERIODIC : respects_periodic_task_model arr_seq tsk
  j1, j2 : Job
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  ARR_LT : job_arrival j1 <= job_arrival j2
  NEQ : job_index arr_seq j1 <> job_index arr_seq j2
  ============================
  job_index arr_seq j1 < job_index arr_seq j2

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


      move_neq_up IND_LTE; move_neq_down ARR_LT.

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

1 subgoal (ID 342)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  H_PERIODIC : respects_periodic_task_model arr_seq tsk
  j1, j2 : Job
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  NEQ : job_index arr_seq j1 <> job_index arr_seq j2
  IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
  ============================
  job_arrival j2 < job_arrival j1

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


      specialize (H_PERIODIC j1); feed_n 3 H_PERIODIC ⇒ //; try by ssrlia.

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

1 subgoal (ID 362)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  j1 : Job
  H_PERIODIC : exists j' : Job,
                 arrives_in arr_seq j' /\
                 job_index arr_seq j' = job_index arr_seq j1 - 1 /\
                 job_task j' = tsk /\
                 job_arrival j1 = job_arrival j' + task_period tsk
  j2 : Job
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  NEQ : job_index arr_seq j1 <> job_index arr_seq j2
  IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
  ============================
  job_arrival j2 < job_arrival j1

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


      move : H_PERIODIC ⇒ [pj [ARR_PJ [IND_PJ [TSK_PJ PJ_ARR]]]].

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

1 subgoal (ID 1234)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  j1, j2 : Job
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  NEQ : job_index arr_seq j1 <> job_index arr_seq j2
  IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
  pj : Job
  ARR_PJ : arrives_in arr_seq pj
  IND_PJ : job_index arr_seq pj = job_index arr_seq j1 - 1
  TSK_PJ : job_task pj = tsk
  PJ_ARR : job_arrival j1 = job_arrival pj + task_period tsk
  ============================
  job_arrival j2 < job_arrival j1

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


      have JB_IND_LTE : job_index arr_seq j2 job_index arr_seq pj by ssrlia.

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

1 subgoal (ID 1503)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  j1, j2 : Job
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  NEQ : job_index arr_seq j1 <> job_index arr_seq j2
  IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
  pj : Job
  ARR_PJ : arrives_in arr_seq pj
  IND_PJ : job_index arr_seq pj = job_index arr_seq j1 - 1
  TSK_PJ : job_task pj = tsk
  PJ_ARR : job_arrival j1 = job_arrival pj + task_period tsk
  JB_IND_LTE : job_index arr_seq j2 <= job_index arr_seq pj
  ============================
  job_arrival j2 < job_arrival j1

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


      apply index_lte_implies_arrival_lte in JB_IND_LTE ⇒ //; try by rewrite TSK_PJ.

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

1 subgoal (ID 1508)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  j1, j2 : Job
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  NEQ : job_index arr_seq j1 <> job_index arr_seq j2
  IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
  pj : Job
  ARR_PJ : arrives_in arr_seq pj
  IND_PJ : job_index arr_seq pj = job_index arr_seq j1 - 1
  TSK_PJ : job_task pj = tsk
  PJ_ARR : job_arrival j1 = job_arrival pj + task_period tsk
  JB_IND_LTE : job_arrival j2 <= job_arrival pj
  ============================
  job_arrival j2 < job_arrival j1

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


      rewrite PJ_ARR.

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

1 subgoal (ID 1582)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  j1, j2 : Job
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  NEQ : job_index arr_seq j1 <> job_index arr_seq j2
  IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
  pj : Job
  ARR_PJ : arrives_in arr_seq pj
  IND_PJ : job_index arr_seq pj = job_index arr_seq j1 - 1
  TSK_PJ : job_task pj = tsk
  PJ_ARR : job_arrival j1 = job_arrival pj + task_period tsk
  JB_IND_LTE : job_arrival j2 <= job_arrival pj
  ============================
  job_arrival j2 < job_arrival pj + task_period tsk

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


      have POS_PERIOD : task_period tsk > 0 by auto.

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

1 subgoal (ID 1587)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  j1, j2 : Job
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  NEQ : job_index arr_seq j1 <> job_index arr_seq j2
  IND_LTE : job_index arr_seq j2 <= job_index arr_seq j1
  pj : Job
  ARR_PJ : arrives_in arr_seq pj
  IND_PJ : job_index arr_seq pj = job_index arr_seq j1 - 1
  TSK_PJ : job_task pj = tsk
  PJ_ARR : job_arrival j1 = job_arrival pj + task_period tsk
  JB_IND_LTE : job_arrival j2 <= job_arrival pj
  POS_PERIOD : 0 < task_period tsk
  ============================
  job_arrival j2 < job_arrival pj + task_period tsk

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


      now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 90)

subgoal 1 (ID 90) is:
 job_arrival j1 + task_period tsk <= job_arrival j2

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


}

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

1 subgoal (ID 90)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  H_PERIODIC : respects_periodic_task_model arr_seq tsk
  j1, j2 : Job
  NEQ : j1 <> j2
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  ARR_LT : job_arrival j1 <= job_arrival j2
  IND_LT : job_index arr_seq j1 < job_index arr_seq j2
  ============================
  job_arrival j1 + task_period tsk <= job_arrival j2

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


    specialize (H_PERIODIC j2); feed_n 3 H_PERIODIC ⇒ //; try by ssrlia.

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

1 subgoal (ID 1945)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  j2 : Job
  H_PERIODIC : exists j' : Job,
                 arrives_in arr_seq j' /\
                 job_index arr_seq j' = job_index arr_seq j2 - 1 /\
                 job_task j' = tsk /\
                 job_arrival j2 = job_arrival j' + task_period tsk
  j1 : Job
  NEQ : j1 <> j2
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  ARR_LT : job_arrival j1 <= job_arrival j2
  IND_LT : job_index arr_seq j1 < job_index arr_seq j2
  ============================
  job_arrival j1 + task_period tsk <= job_arrival j2

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


    move: H_PERIODIC ⇒ [pj [ARR_PJ [IND_PJ [TSK_PJ PJ_ARR]]]].

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

1 subgoal (ID 2876)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  j2, j1 : Job
  NEQ : j1 <> j2
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  ARR_LT : job_arrival j1 <= job_arrival j2
  IND_LT : job_index arr_seq j1 < job_index arr_seq j2
  pj : Job
  ARR_PJ : arrives_in arr_seq pj
  IND_PJ : job_index arr_seq pj = job_index arr_seq j2 - 1
  TSK_PJ : job_task pj = tsk
  PJ_ARR : job_arrival j2 = job_arrival pj + task_period tsk
  ============================
  job_arrival j1 + task_period tsk <= job_arrival j2

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


    have JB_IND_LTE : job_index arr_seq j1 job_index arr_seq pj by ssrlia.

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

1 subgoal (ID 3173)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  j2, j1 : Job
  NEQ : j1 <> j2
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  ARR_LT : job_arrival j1 <= job_arrival j2
  IND_LT : job_index arr_seq j1 < job_index arr_seq j2
  pj : Job
  ARR_PJ : arrives_in arr_seq pj
  IND_PJ : job_index arr_seq pj = job_index arr_seq j2 - 1
  TSK_PJ : job_task pj = tsk
  PJ_ARR : job_arrival j2 = job_arrival pj + task_period tsk
  JB_IND_LTE : job_index arr_seq j1 <= job_index arr_seq pj
  ============================
  job_arrival j1 + task_period tsk <= job_arrival j2

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


    apply index_lte_implies_arrival_lte in JB_IND_LTE ⇒ //; try by rewrite TSK_PJ.

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

1 subgoal (ID 3178)
  
  Task : TaskType
  H : PeriodicModel 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
  VALID_PERIOD : valid_period tsk
  j2, j1 : Job
  NEQ : j1 <> j2
  ARR : arrives_in arr_seq j1
  ARR' : arrives_in arr_seq j2
  TSK : job_task j1 = tsk
  TSK' : job_task j2 = tsk
  ARR_LT : job_arrival j1 <= job_arrival j2
  IND_LT : job_index arr_seq j1 < job_index arr_seq j2
  pj : Job
  ARR_PJ : arrives_in arr_seq pj
  IND_PJ : job_index arr_seq pj = job_index arr_seq j2 - 1
  TSK_PJ : job_task pj = tsk
  PJ_ARR : job_arrival j2 = job_arrival pj + task_period tsk
  JB_IND_LTE : job_arrival j1 <= job_arrival pj
  ============================
  job_arrival j1 + task_period tsk <= job_arrival j2

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


    now rewrite PJ_ARR; ssrlia.

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

No more subgoals.

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


  Qed.

For convenience, we state these obvious correspondences also at the level of entire task sets.
First, we show that all tasks in a task set with valid periods also have valid min inter-arrival times.
  Remark valid_periods_are_valid_inter_arrival_times:
     ts, valid_periods ts valid_taskset_inter_arrival_times ts.

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

1 subgoal (ID 69)
  
  Task : TaskType
  H : PeriodicModel 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
  ============================
  forall ts : TaskSet Task,
  valid_periods ts -> valid_taskset_inter_arrival_times ts

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


  Proof. trivial.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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


Qed.

Second, we show that each task in a periodic task set respects the sporadic task model.
  Remark periodic_task_sets_respect_sporadic_task_model:
     ts,
      valid_periods ts
      taskset_respects_periodic_task_model arr_seq ts
      taskset_respects_sporadic_task_model ts arr_seq.

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

1 subgoal (ID 86)
  
  Task : TaskType
  H : PeriodicModel 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
  ============================
  forall ts : TaskSet Task,
  valid_periods ts ->
  taskset_respects_periodic_task_model arr_seq ts ->
  taskset_respects_sporadic_task_model ts arr_seq

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


  Proof.
    intros ts VALID_PERIODS H_PERIODIC tsk TSK_IN.

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

1 subgoal (ID 92)
  
  Task : TaskType
  H : PeriodicModel 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
  ts : TaskSet Task
  VALID_PERIODS : valid_periods ts
  H_PERIODIC : taskset_respects_periodic_task_model arr_seq ts
  tsk : Task
  TSK_IN : tsk \in ts
  ============================
  respects_sporadic_task_model arr_seq tsk

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


    specialize (H_PERIODIC tsk TSK_IN).
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 94)
  
  Task : TaskType
  H : PeriodicModel 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
  ts : TaskSet Task
  VALID_PERIODS : valid_periods ts
  tsk : Task
  H_PERIODIC : respects_periodic_task_model arr_seq tsk
  TSK_IN : tsk \in ts
  ============================
  respects_sporadic_task_model arr_seq tsk

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


    apply periodic_task_respects_sporadic_task_model ⇒ //.

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

1 subgoal (ID 95)
  
  Task : TaskType
  H : PeriodicModel 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
  ts : TaskSet Task
  VALID_PERIODS : valid_periods ts
  tsk : Task
  H_PERIODIC : respects_periodic_task_model arr_seq tsk
  TSK_IN : tsk \in ts
  ============================
  valid_period tsk

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


    now apply VALID_PERIODS.

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

No more subgoals.

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


  Qed.

End PeriodicTasksAsSporadicTasks.

We add the [periodic_task_respects_sporadic_task_model] lemma into a "Hint Database" basic_facts, so Coq will be able to apply it automatically.
Hint Extern 1 ⇒ apply periodic_task_respects_sporadic_task_model : basic_facts.