define a shifted job costs function and prove its validity

analysis/definitions/hyperperiod.v

@@ -5,29 +5,75 @@ From mathcomp Require Import div.
 (** In this file we define the notion of a hyperperiod for periodic tasks. *)
 Section Hyperperiod.
 
-  (** Consider periodic tasks. *)
+  (** Consider any type of periodic tasks ... *)
   Context {Task : TaskType} `{PeriodicModel Task}.
 
-  (** Consider any task set [ts]... *)
+  (** ... and any task set [ts]. *)
   Variable ts : TaskSet Task.
 
-  (** ... and any task [tsk] that belongs to this task set. *)
-  Variable tsk : Task.
-  Hypothesis H_tsk_in_ts : tsk \in ts.
-
   (** The hyperperiod of a task set is defined as the least common multiple
       (LCM) of the periods of all tasks in the task set. **)
   Definition hyperperiod : duration := lcml (map task_period ts).        
 
-  (** Consequently, a task set's hyperperiod is an integral multiple
-   of each task's period in the task set. **)
-  Lemma hyperperiod_int_mult_of_any_task : 
-    exists k, hyperperiod = k * task_period tsk.
-  Proof.
-    apply lcm_seq_is_mult_of_all_ints.
-    apply map_f.
-    by apply H_tsk_in_ts.
-  Qed.
-
 End Hyperperiod.
 
+(** In this section we provide basic definitions concerning the hyperperiod
+    of all tasks in a task set. *)
+Section HyperperiodDefinitions.
+
+  (** Consider any type of periodic tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskOffset Task}.
+  Context `{PeriodicModel Task}.
+
+  (** ... and any type of jobs. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+
+  (** Consider any task set [ts] ... *)
+  Variable ts : TaskSet Task.
+
+  (** ... and any arrival sequence [arr_seq]. *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** Let [O_max] denote the maximum offset of all tasks in [ts] ... *)
+  Let O_max := max_task_offset ts.
+
+  (** ... and let [HP] denote the hyperperiod of all tasks in [ts]. *)
+  Let HP := hyperperiod ts.
+
+  (** We define a hyperperiod index based on an instant [t]
+      which lies in it. *)
+  (** Note that we consider the first hyperperiod to start at time [O_max], 
+      i.e., shifted by the maximum offset (and not at time zero as can also 
+      be found sometimes in the literature) *)
+  Definition hyperperiod_index (t : instant) :=
+    (t - O_max) %/ HP.
+
+  (** Given an instant [t], we define the starting instant of the hyperperiod 
+   that contains [t]. *)
+  Definition starting_instant_of_hyperperiod (t : instant) :=
+    hyperperiod_index t * HP + O_max.
+
+  (** Given a job [j], we define the starting instant of the hyperperiod
+   in which [j] arrives. *)
+  Definition starting_instant_of_corresponding_hyperperiod (j : Job) :=
+    starting_instant_of_hyperperiod (job_arrival j).
+
+  (** We define the sequence of jobs of a task [tsk] that arrive in a hyperperiod
+      given the starting instant [h] of the hyperperiod. *)
+  Definition jobs_in_hyperperiod (h : instant) (tsk : Task) :=
+    task_arrivals_between arr_seq tsk h (h + HP).
+
+  (** We define the index of a job [j] of task [tsk] in a hyperperiod starting at [h]. *)
+  Definition job_index_in_hyperperiod (j : Job) (h : instant) (tsk : Task) :=
+    index j (jobs_in_hyperperiod h tsk).
+
+  (** Given a job [j] of task [tsk] and the hyperperiod starting at [h], we define a 
+      [corresponding_job_in_hyperperiod] which is the job that arrives in given hyperperiod 
+      and has the same [job_index] as [j]. *)
+  Definition corresponding_job_in_hyperperiod (j : Job) (h : instant) (tsk : Task) :=
+    nth j (jobs_in_hyperperiod h tsk) (job_index_in_hyperperiod j (starting_instant_of_corresponding_hyperperiod j) tsk).
+
+End HyperperiodDefinitions.

analysis/definitions/infinite_jobs.v

+Require Export prosa.model.task.arrivals.
+
+(** In this section we define the notion of an infinite release 
+    of jobs by a task. *)
+Section InfiniteJobs.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+
+  (** ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+
+  (** Consider any arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** We say that a task [tsk] releases an infinite number of jobs 
+      if for every integer [n] there exists a job [j] of task [tsk]
+      such that [job_index] of [j] is equal to [n]. *)
+  Definition infinite_jobs :=
+    forall tsk n,
+    exists j,
+      arrives_in arr_seq j /\
+      job_task j = tsk /\
+      job_index arr_seq j = n.
+  
+End InfiniteJobs.

analysis/definitions/job_response_time.v

+Require Export prosa.behavior.all.
+
+(** In this section we define what it means for the response time 
+    of a job to exceed some given duration. *)
+Section JobResponseTimeExceeds.
+
+  (** Consider any kind of jobs ... *)
+  Context {Job : JobType}.
+  Context `{JobCost Job}.
+  Context `{JobArrival Job}.
+
+  (** ... and any kind of processor state. *)
+  Context `{PState : Type}.
+  Context `{ProcessorState Job PState}.
+
+  (** Consider any schedule. *)
+  Variable sched : schedule PState.
+
+  (** We say that a job [j] has a response time exceeding a number [x] 
+      if [j] is pending [x] units of time after its arrival. *)
+  Definition job_response_time_exceeds (j : Job) (x : duration) :=
+    ~~ completed_by sched j ((job_arrival j) + x).
+
+End JobResponseTimeExceeds.

analysis/facts/hyperperiod.v

+Require Export prosa.analysis.definitions.hyperperiod.
+Require Export prosa.analysis.facts.periodic.task_arrivals_size.
+Require Export prosa.util.div_mod.
+
+(** In this file we prove some simple properties of hyperperiods of periodic tasks. *)
+Section Hyperperiod.
+
+  (** Consider any type of periodic tasks, ... *)
+  Context {Task : TaskType} `{PeriodicModel Task}.
+
+  (** ... any task set [ts], ... *)
+  Variable ts : TaskSet Task.
+
+  (** ... and any task [tsk] that belongs to this task set. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts: tsk \in ts.
+
+  (** A task set's hyperperiod is an integral multiple
+      of each task's period in the task set. **)
+  Lemma hyperperiod_int_mult_of_any_task: 
+    exists (k : nat),
+      hyperperiod ts = k * task_period tsk.
+  Proof.
+    apply lcm_seq_is_mult_of_all_ints.
+    apply map_f.
+    now apply H_tsk_in_ts.
+  Qed.
+
+End Hyperperiod.
+
+(** In this section we show a property of hyperperiod in context 
+   of task sets with valid periods. *)
+Section ValidPeriodsImplyPositiveHP.
+
+  (** Consider any type of periodic tasks ... *)
+  Context {Task : TaskType} `{PeriodicModel Task}.
+
+  (** ... and any task set [ts] ... *)
+  Variable ts : TaskSet Task.
+
+  (** ... such that all tasks in [ts] have valid periods. *)
+  Hypothesis H_valid_periods: valid_periods ts.
+
+  (** We show that the hyperperiod of task set [ts] 
+   is positive. *)
+  Lemma valid_periods_imply_pos_hp:
+    hyperperiod ts > 0.
+  Proof.
+    apply all_pos_implies_lcml_pos.
+    move => b /mapP [x IN EQ]; subst b.
+    now apply H_valid_periods.
+  Qed.
+  
+End ValidPeriodsImplyPositiveHP.
+
+(** In this section we prove some lemmas about the hyperperiod
+    in context of the periodic model. *)
+Section PeriodicLemmas.
+
+  (** Consider any type of tasks, ... *)
+  Context {Task : TaskType}.
+  Context `{TaskOffset Task}.
+  Context `{PeriodicModel Task}.
+
+  (** ... any type of jobs, ... *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  
+  (** ... and a consistent arrival sequence with 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.
+  
+  (** Consider a task set [ts] such that all tasks in
+      [ts] have valid periods. *)
+  Variable ts : TaskSet Task.
+  Hypothesis H_valid_periods: valid_periods ts.
+
+  (** Let [tsk] be any periodic task in [ts] with a valid offset and period. *)
+  Variable tsk : Task.
+  Hypothesis H_task_in_ts: tsk \in ts.
+  Hypothesis H_valid_offset: valid_offset arr_seq tsk.
+  Hypothesis H_valid_period: valid_period tsk.
+  Hypothesis H_periodic_task: respects_periodic_task_model arr_seq tsk.
+
+  (** Assume we have an infinite sequence of jobs in the arrival sequence. *)
+  Hypothesis H_infinite_jobs: infinite_jobs arr_seq.
+  
+  (** Let [O_max] denote the maximum task offset in [ts] and let
+   [HP] denote the hyperperiod of all tasks in [ts]. *)
+  Let O_max := max_task_offset ts.
+  Let HP := hyperperiod ts.
+
+  (** We show that the job corresponding to any job [j1] in any other
+      hyperperiod is of the same task as [j1]. *)
+  Lemma corresponding_jobs_have_same_task:
+    forall j1 j2,
+      job_task (corresponding_job_in_hyperperiod ts arr_seq j1
+               (starting_instant_of_corresponding_hyperperiod ts j2) (job_task j1)) = job_task j1.
+  Proof.
+    intros *.
+    set ARRIVALS := (task_arrivals_between arr_seq (job_task j1) (starting_instant_of_hyperperiod ts (job_arrival j2))
+          (starting_instant_of_hyperperiod ts (job_arrival j2) + HP)).
+    set IND := (job_index_in_hyperperiod ts arr_seq j1 (starting_instant_of_hyperperiod ts (job_arrival j1)) (job_task j1)).
+    have SIZE_G : size ARRIVALS <= IND -> job_task (nth j1 ARRIVALS IND) = job_task j1 by intro SG; rewrite nth_default.
+    case: (boolP (size ARRIVALS == IND)) => [/eqP EQ|NEQ]; first by apply SIZE_G; ssrlia.
+    move : NEQ; rewrite neq_ltn; move => /orP [LT | G]; first by apply SIZE_G; ssrlia.
+    set jb := nth j1 ARRIVALS IND.
+    have JOB_IN : jb \in ARRIVALS by apply mem_nth.
+    rewrite /ARRIVALS /task_arrivals_between mem_filter in JOB_IN.
+    now move : JOB_IN => /andP [/eqP TSK JB_IN].
+  Qed.    
+
+  (** We show that if a job [j] lies in the hyperperiod starting
+   at instant [t] then [j] arrives in the interval <<[t, t + HP)>>. *)
+  Lemma all_jobs_arrive_within_hyperperiod:
+    forall j t,
+      j \in jobs_in_hyperperiod ts arr_seq t tsk->
+      t <= job_arrival j < t + HP.
+  Proof.
+    intros * JB_IN_HP.
+    rewrite mem_filter in JB_IN_HP.
+    move : JB_IN_HP => /andP [/eqP TSK JB_IN]; apply mem_bigcat_nat_exists in JB_IN.
+    destruct JB_IN as [i [JB_IN INEQ]]; apply H_consistent_arrivals in JB_IN.
+    now rewrite JB_IN.
+  Qed.
+  
+  (** We show that the number of jobs in a hyperperiod starting at [n1 * HP + O_max] 
+   is the same as the number of jobs in a hyperperiod starting at [n2 * HP + O_max] given 
+   that [n1] is less than or equal to [n2]. *)
+  Lemma eq_size_hyp_lt:
+    forall n1 n2,
+      n1 <= n2 ->
+      size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
+      size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk).
+  Proof.
+    intros * N1_LT.
+    specialize (add_mul_diff n1 n2 HP O_max) => AD; feed_n 1 AD => //.
+    rewrite AD.
+    destruct (hyperperiod_int_mult_of_any_task ts tsk H_task_in_ts) as [k HYP]; rewrite !/HP.
+    rewrite [in X in _ = size (_ (n1 * HP + O_max + _ * X) tsk)]HYP.
+    rewrite mulnA /HP /jobs_in_hyperperiod !size_of_task_arrivals_between.
+    erewrite big_sum_eq_in_eq_sized_intervals => //; intros g G_LT.
+    have OFF_G : task_offset tsk <= O_max by apply max_offset_g.
+    have FG : forall v b n, v + b + n = v + n + b by intros *; ssrlia.
+    erewrite eq_size_of_task_arrivals_seperated_by_period => //; last by ssrlia.
+    now rewrite FG.
+  Qed.
+
+  (** We generalize the above lemma by lifting the condition on 
+   [n1] and [n2]. *)
+  Lemma eq_size_of_arrivals_in_hyperperiod:
+    forall n1 n2,
+      size (jobs_in_hyperperiod ts arr_seq (n1 * HP + O_max) tsk) =
+      size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk).
+  Proof.
+    intros *.
+    case : (boolP (n1 == n2)) => [/eqP EQ | NEQ]; first by rewrite EQ.
+    move : NEQ; rewrite neq_ltn; move => /orP [LT | LT].
+    + now apply eq_size_hyp_lt => //; ssrlia.
+    + move : (eq_size_hyp_lt n2 n1) => EQ_S.
+      now feed_n 1 EQ_S => //; ssrlia.
+  Qed.
+
+  (** Consider any two jobs [j1] and [j2] that stem from the arrival sequence
+   [arr_seq] such that [j1] is of task [tsk]. *)
+  Variable j1 : Job.
+  Variable j2 : Job.
+  Hypothesis H_j1_from_arr_seq: arrives_in arr_seq j1.
+  Hypothesis H_j2_from_arr_seq: arrives_in arr_seq j2.
+  Hypothesis H_j1_task: job_task j1 = tsk.
+
+  (** Assume that both [j1] and [j2] arrive after [O_max]. *)
+  Hypothesis H_j1_arr_after_O_max: O_max <= job_arrival j1.
+  Hypothesis H_j2_arr_after_O_max: O_max <= job_arrival j2.
+
+  (** We show that any job [j] that arrives in task arrivals in the same 
+      hyperperiod as [j2] also arrives in task arrivals up to [job_arrival j2 + HP]. *)
+  Lemma job_in_hp_arrives_in_task_arrivals_up_to:
+    forall j,
+      j \in jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk ->
+      j \in task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP).
+  Proof.
+    intros j J_IN.
+    rewrite /task_arrivals_up_to.
+    set jobs_in_hp := (jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk).
+    move : (J_IN) => J_ARR; apply all_jobs_arrive_within_hyperperiod in J_IN.
+    rewrite /jobs_in_hp /jobs_in_hyperperiod /task_arrivals_up_to /task_arrivals_between mem_filter in J_ARR.
+    move : J_ARR =>  /andP [/eqP TSK' NTH_IN].
+    apply job_in_task_arrivals_between => //; first by apply in_arrivals_implies_arrived in NTH_IN.
+    apply mem_bigcat_nat_exists in NTH_IN.
+    move : NTH_IN => [i [NJ_IN INEQ]]; apply H_consistent_arrivals in NJ_IN; rewrite -NJ_IN in INEQ.
+    apply /andP; split => //.
+    rewrite ltnS.
+    apply leq_trans with (n := (job_arrival j2 - O_max) %/ HP * HP + O_max + HP); first by ssrlia.
+    rewrite leq_add2r.
+    have O_M : (job_arrival j2 - O_max) %/ HP * HP <= job_arrival j2 - O_max by apply leq_trunc_div.
+    have ARR_G : job_arrival j2 >= O_max by auto.
+    now ssrlia.
+  Qed.
+
+  (** We show that job [j1] arrives in its own hyperperiod. *)
+  Lemma job_in_own_hp:
+    j1 \in jobs_in_hyperperiod ts arr_seq ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk.
+  Proof.
+    apply job_in_task_arrivals_between => //.
+    apply /andP; split.
+    + rewrite addnC -leq_subRL => //.
+      now apply leq_trunc_div.
+    + specialize (div_floor_add_g (job_arrival j1 - O_max) HP) => AB.
+      feed_n 1 AB; first by apply valid_periods_imply_pos_hp => //.
+      apply ltn_subLR in AB.
+      now rewrite -/(HP); ssrlia.
+  Qed.
+
+  (** We show that the [corresponding_job_in_hyperperiod] of [j1] in [j2]'s hyperperiod
+   arrives in task arrivals up to [job_arrival j2 + HP]. *)
+  Lemma corr_job_in_task_arrivals_up_to:
+    corresponding_job_in_hyperperiod ts arr_seq j1 (starting_instant_of_corresponding_hyperperiod ts j2) tsk \in
+      task_arrivals_up_to arr_seq tsk (job_arrival j2 + HP).
+  Proof.
+    rewrite /corresponding_job_in_hyperperiod /starting_instant_of_corresponding_hyperperiod.
+    rewrite /job_index_in_hyperperiod /starting_instant_of_hyperperiod /hyperperiod_index.
+    set ind := (index j1 (jobs_in_hyperperiod ts arr_seq ((job_arrival j1 - O_max) %/ HP * HP + O_max) tsk)).
+    set jobs_in_hp := (jobs_in_hyperperiod ts arr_seq ((job_arrival j2 - O_max) %/ HP * HP + O_max) tsk).
+    set nj := nth j1 jobs_in_hp ind.
+    apply job_in_hp_arrives_in_task_arrivals_up_to => //.
+    rewrite mem_nth /jobs_in_hp => //.
+    specialize (eq_size_of_arrivals_in_hyperperiod ((job_arrival j2 - O_max) %/ HP) ((job_arrival j1 - O_max) %/ HP)) => EQ.
+    rewrite EQ /ind index_mem.
+    now apply job_in_own_hp.
+  Qed.    
+
+  (** Finally, we show that the [corresponding_job_in_hyperperiod] of [j1] in [j2]'s hyperperiod 
+   arrives in the arrival sequence [arr_seq]. *)
+  Lemma corresponding_job_arrives:
+      arrives_in arr_seq (corresponding_job_in_hyperperiod ts arr_seq j1 (starting_instant_of_corresponding_hyperperiod ts j2) tsk).
+  Proof.
+    move : (corr_job_in_task_arrivals_up_to) => ARR_G.
+    rewrite /task_arrivals_up_to /task_arrivals_between mem_filter in ARR_G.
+    move : ARR_G =>  /andP [/eqP TSK' NTH_IN].
+    now apply in_arrivals_implies_arrived in NTH_IN.
+  Qed.
+
+End PeriodicLemmas.

analysis/facts/model/offset.v

 Require Export prosa.model.task.offset.
 Require Export prosa.analysis.facts.job_index.
 
-(** In this module, we'll prove a property of task offsets. *)
+(** In this module, we prove some properties of task offsets. *)
 Section OffsetLemmas.
   
   (** Consider any type of tasks with an offset ... *)
@@ -13,12 +13,13 @@ Section OffsetLemmas.
   Context `{JobTask Job Task}.
   Context `{JobArrival Job}.
 
-  (** Consider any arrival sequence with consistent and non-duplicate arrivals, ... *)
+  (** 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] of any task [tsk] with a valid offset. *)
+  (** ... 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.
@@ -44,4 +45,19 @@ Section OffsetLemmas.
         [ssrlia | 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.
+  Proof.
+    intros TSK_IN.
+    apply in_max0_le.
+    now apply map_f.
+  Qed.
+
 End OffsetLemmas.

analysis/facts/model/task_arrivals.v

@@ -13,7 +13,7 @@ Section TaskArrivals.
   
   (** Consider any job arrival sequence with consistent arrivals. *)
   Variable arr_seq : arrival_sequence Job.
-  Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq.
+  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
   
   (** We show that the number of arrivals of task can be split into disjoint intervals. *) 
   Lemma num_arrivals_of_task_cat:
@@ -133,15 +133,26 @@ Section TaskArrivals.
     now apply arrived_between_implies_in_arrivals.
   Qed.
 
+  (** Any job [j] in [task_arrivals_between arr_seq tsk t1 t2] arrives 
+      in the arrival sequence [arr_seq]. *)
+  Lemma arrives_in_task_arrivals_implies_arrived:
+    forall t1 t2 j,
+      j \in (task_arrivals_between arr_seq tsk t1 t2) ->
+      arrives_in arr_seq j.
+  Proof.
+    intros * JB_IN.
+    move : JB_IN; rewrite mem_filter; move => /andP [/eqP TSK JB_IN].
+    now apply in_arrivals_implies_arrived in JB_IN.
+  Qed.
+    
   (** An arrival sequence with non-duplicate arrivals implies that the 
       task arrivals also contain non-duplicate arrivals. *)
   Lemma uniq_task_arrivals:
-    forall j,
-      arrives_in arr_seq j ->
+    forall t,
       arrival_sequence_uniq arr_seq ->
-      uniq (task_arrivals_up_to arr_seq (job_task j) (job_arrival j)).
+      uniq (task_arrivals_up_to arr_seq tsk t).
   Proof.
-    intros j ARR UNQ_ARR.
+    intros * UNQ_SEQ.
     apply filter_uniq.
     now apply arrivals_uniq.
   Qed.
@@ -181,4 +192,57 @@ Section TaskArrivals.
       now rewrite -task_arrivals_cat; try by ssrlia.
   Qed.
 
+  (** For any job [j2] with [job_index] equal to [n], the nth job 
+   in the sequence [task_arrivals_up_to arr_seq tsk t] is [j2], given that
+   [t] is not less than [job_arrival j2]. *)
+  (** Note that [j_def] is used as a default job for the access function and
+   has nothing to do with the lemma. *)
+  Lemma nth_job_of_task_arrivals:
+    forall n j_def j t,
+      arrives_in arr_seq j ->
+      job_task j = tsk ->
+      job_index arr_seq j = n ->
+      t >= job_arrival j ->
+      nth j_def (task_arrivals_up_to arr_seq tsk t) n = j.
+  Proof.
+    intros * ARR TSK IND T_G.
+    rewrite -IND.
+    have EQ_IND : index j (task_arrivals_up_to_job_arrival arr_seq j) = index j (task_arrivals_up_to arr_seq tsk t).
+    { have CAT : exists xs, task_arrivals_up_to_job_arrival arr_seq j ++ xs = task_arrivals_up_to arr_seq tsk t.
+      { rewrite /task_arrivals_up_to_job_arrival TSK.
+        exists (task_arrivals_between arr_seq tsk ((job_arrival j).+1) t.+1).
+        now rewrite -task_arrivals_cat.
+      }
+      move : CAT => [xs ARR_CAT].
+      now rewrite -ARR_CAT index_cat ifT; last by apply arrives_in_task_arrivals_up_to.
+    }
+    rewrite /job_index EQ_IND nth_index => //.
+    rewrite mem_filter; apply /andP.
+    split; first by apply /eqP.
+    now apply job_in_arrivals_between => //.
+  Qed.
+
+  (** We show that task arrivals in the interval <<[t1, t2)>> 
+   is the same as concatenation of task arrivals at each instant in <<[t1, t2)>>. *)
+  Lemma task_arrivals_between_is_cat_of_task_arrivals_at:
+    forall t1 t2,
+      task_arrivals_between arr_seq tsk t1 t2 = \cat_(t1 <= t < t2) task_arrivals_at arr_seq tsk t.
+  Proof.
+    intros *.
+    rewrite /task_arrivals_between /task_arrivals_at /arrivals_between.
+    now apply cat_filter_eq_filter_cat.
+  Qed.
+
+  (** The number of jobs of a task [tsk] in the interval <<[t1, t2)>> is the same 
+   as sum of the number of jobs of the task [tsk] at each instant in <<[t1, t2)>>. *)
+  Lemma size_of_task_arrivals_between:
+    forall t1 t2,
+      size (task_arrivals_between arr_seq tsk t1 t2)
+      = \sum_(t1 <= t < t2) size (task_arrivals_at arr_seq tsk t). 
+  Proof.
+    intros *.
+    rewrite /task_arrivals_between /task_arrivals_at /arrivals_between.
+    now rewrite size_big_nat cat_filter_eq_filter_cat.
+  Qed.
+    
 End TaskArrivals.

analysis/facts/periodic/arrival_times.v

@@ -50,4 +50,46 @@ Section PeriodicArrivalTimes.
     }
   Qed.
 
+  (** We show that for every job [j] of task [tsk] there exists a number 
+   [n] such that [j] arrives at the instant [task_offset tsk + n * task_period tsk]. *)
+  Lemma job_arrival_times:
+    forall j,
+      arrives_in arr_seq j ->
+      job_task j = tsk ->
+      exists n, job_arrival j = task_offset tsk + n * task_period tsk.
+  Proof.
+    intros * ARR TSK.
+    exists (job_index arr_seq j).
+    specialize (periodic_arrival_times (job_index arr_seq j) j) => J_ARR.
+    now feed_n 3 J_ARR => //.
+  Qed.
+
+  (** If a job [j] of task [tsk] arrives at [task_offset tsk + n * task_period tsk] 
+   then the [job_index] of [j] is equal to [n]. *)
+  Lemma job_arr_index:
+    forall n j,
+      arrives_in arr_seq j ->
+      job_task j = tsk ->
+      job_arrival j = task_offset tsk + n * task_period tsk ->
+      job_index arr_seq j = n.
+  Proof.
+    have F : task_period tsk > 0 by auto.
+    induction n.
+    + intros * ARR_J TSK ARR.
+      destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]] => //. 
+      now apply periodic_arrival_times in SUCC => //; ssrlia.
+    + intros * ARR_J TSK ARR.
+      specialize (H_task_respects_periodic_model j); feed_n 3 H_task_respects_periodic_model => //.
+      { rewrite lt0n; apply /eqP; intro EQ.