Library prosa.analysis.facts.periodic.arrival_times


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

Welcome to Coq 8.13.0 (January 2021)

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

Require Export prosa.analysis.facts.periodic.max_inter_arrival.
Require Export prosa.analysis.facts.model.offset.
Require Export prosa.analysis.facts.periodic.sporadic.

In this module, we'll prove the known arrival times of jobs that stem from periodic tasks.
Section PeriodicArrivalTimes.

Consider periodic tasks with an offset ...
  Context {Task : TaskType}.
  Context `{TaskOffset Task}.
  Context `{PeriodicModel Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

Consider any unique arrival sequence with consistent 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 periodic task [tsk] with a valid offset and period.
    Variable tsk : Task.
    Hypothesis H_valid_offset: valid_offset arr_seq tsk.
    Hypothesis H_valid_period: valid_period tsk.
    Hypothesis H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk.

We show that the nth job [j] of task [tsk] arrives at the instant [task_offset tsk + n * task_period tsk].
  Lemma periodic_arrival_times:
    ∀ n (j : Job),
      arrives_in arr_seq j →
      job_task j = tsk →
      job_index arr_seq j = n →
      job_arrival j = task_offset tsk + n × task_period tsk.

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

1 subgoal (ID 51)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  ============================
  forall (n : nat) (j : Job),
  arrives_in arr_seq j ->
  job_task j = tsk ->
  job_index arr_seq j = n ->
  job_arrival j = task_offset tsk + n * task_period tsk

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

  Proof.
    induction n.

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

2 subgoals (ID 56)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  ============================
  forall j : Job,
  arrives_in arr_seq j ->
  job_task j = tsk ->
  job_index arr_seq j = 0 ->
  job_arrival j = task_offset tsk + 0 * task_period tsk

subgoal 2 (ID 59) is:
 forall j : Job,
 arrives_in arr_seq j ->
 job_task j = tsk ->
 job_index arr_seq j = n.+1 ->
 job_arrival j = task_offset tsk + n.+1 * task_period tsk

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

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

1 subgoal (ID 56)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  ============================
  forall j : Job,
  arrives_in arr_seq j ->
  job_task j = tsk ->
  job_index arr_seq j = 0 ->
  job_arrival j = task_offset tsk + 0 * task_period tsk

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

intros j ARR TSK_IN ZINDEX.

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

1 subgoal (ID 63)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  j : Job
  ARR : arrives_in arr_seq j
  TSK_IN : job_task j = tsk
  ZINDEX : job_index arr_seq j = 0
  ============================
  job_arrival j = task_offset tsk + 0 * task_period tsk

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

      rewrite mul0n addn0.

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

1 subgoal (ID 73)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  j : Job
  ARR : arrives_in arr_seq j
  TSK_IN : job_task j = tsk
  ZINDEX : job_index arr_seq j = 0
  ============================
  job_arrival j = task_offset tsk

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

      apply first_job_arrival with (arr_seq0 := arr_seq) (tsk0 := job_task j) ⇒ //.

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

1 subgoal

subgoal 1 (ID 59) is:
 forall j : Job,
 arrives_in arr_seq j ->
 job_task j = tsk ->
 job_index arr_seq j = n.+1 ->
 job_arrival j = task_offset tsk + n.+1 * task_period tsk

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

    }

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

1 subgoal (ID 59)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  n : nat
  IHn : forall j : Job,
        arrives_in arr_seq j ->
        job_task j = tsk ->
        job_index arr_seq j = n ->
        job_arrival j = task_offset tsk + n * task_period tsk
  ============================
  forall j : Job,
  arrives_in arr_seq j ->
  job_task j = tsk ->
  job_index arr_seq j = n.+1 ->
  job_arrival j = task_offset tsk + n.+1 * task_period tsk

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

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

1 subgoal (ID 59)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  n : nat
  IHn : forall j : Job,
        arrives_in arr_seq j ->
        job_task j = tsk ->
        job_index arr_seq j = n ->
        job_arrival j = task_offset tsk + n * task_period tsk
  ============================
  forall j : Job,
  arrives_in arr_seq j ->
  job_task j = tsk ->
  job_index arr_seq j = n.+1 ->
  job_arrival j = task_offset tsk + n.+1 * task_period tsk

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

intros j ARR TSK_IN JB_INDEX.

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

1 subgoal (ID 91)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  n : nat
  IHn : forall j : Job,
        arrives_in arr_seq j ->
        job_task j = tsk ->
        job_index arr_seq j = n ->
        job_arrival j = task_offset tsk + n * task_period tsk
  j : Job
  ARR : arrives_in arr_seq j
  TSK_IN : job_task j = tsk
  JB_INDEX : job_index arr_seq j = n.+1
  ============================
  job_arrival j = task_offset tsk + n.+1 * task_period tsk

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

      move : (H_task_respects_periodic_model j ARR) ⇒ PREV_JOB.

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

1 subgoal (ID 93)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  n : nat
  IHn : forall j : Job,
        arrives_in arr_seq j ->
        job_task j = tsk ->
        job_index arr_seq j = n ->
        job_arrival j = task_offset tsk + n * task_period tsk
  j : Job
  ARR : arrives_in arr_seq j
  TSK_IN : job_task j = tsk
  JB_INDEX : job_index arr_seq j = n.+1
  PREV_JOB : 0 < job_index arr_seq j ->
             job_task j = tsk ->
             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
  ============================
  job_arrival j = task_offset tsk + n.+1 * task_period tsk

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

      feed_n 2 PREV_JOB ⇒ //; first by ssrlia.

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

1 subgoal (ID 105)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  n : nat
  IHn : forall j : Job,
        arrives_in arr_seq j ->
        job_task j = tsk ->
        job_index arr_seq j = n ->
        job_arrival j = task_offset tsk + n * task_period tsk
  j : Job
  ARR : arrives_in arr_seq j
  TSK_IN : job_task j = tsk
  JB_INDEX : job_index arr_seq j = n.+1
  PREV_JOB : 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
  ============================
  job_arrival j = task_offset tsk + n.+1 * task_period tsk

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

      move : PREV_JOB ⇒ [pj [ARR' [IND [TSK ARRIVAL]]]].

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

1 subgoal (ID 1239)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  n : nat
  IHn : forall j : Job,
        arrives_in arr_seq j ->
        job_task j = tsk ->
        job_index arr_seq j = n ->
        job_arrival j = task_offset tsk + n * task_period tsk
  j : Job
  ARR : arrives_in arr_seq j
  TSK_IN : job_task j = tsk
  JB_INDEX : job_index arr_seq j = n.+1
  pj : Job
  ARR' : arrives_in arr_seq pj
  IND : job_index arr_seq pj = job_index arr_seq j - 1
  TSK : job_task pj = tsk
  ARRIVAL : job_arrival j = job_arrival pj + task_period tsk
  ============================
  job_arrival j = task_offset tsk + n.+1 * task_period tsk

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

      specialize (IHn pj); feed_n 3 IHn ⇒ //; first by rewrite IND JB_INDEX; ssrlia.

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

1 subgoal (ID 1259)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  n : nat
  pj : Job
  IHn : job_arrival pj = task_offset tsk + n * task_period tsk
  j : Job
  ARR : arrives_in arr_seq j
  TSK_IN : job_task j = tsk
  JB_INDEX : job_index arr_seq j = n.+1
  ARR' : arrives_in arr_seq pj
  IND : job_index arr_seq pj = job_index arr_seq j - 1
  TSK : job_task pj = tsk
  ARRIVAL : job_arrival j = job_arrival pj + task_period tsk
  ============================
  job_arrival j = task_offset tsk + n.+1 * task_period tsk

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

      rewrite ARRIVAL IHn; ssrlia.

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

No more subgoals.

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

    }

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

No more subgoals.

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

  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:
    ∀ j,
      arrives_in arr_seq j →
      job_task j = tsk →
      ∃ n, job_arrival j = task_offset tsk + n × task_period tsk.

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

1 subgoal (ID 67)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  ============================
  forall j : Job,
  arrives_in arr_seq j ->
  job_task j = tsk ->
  exists n : nat, job_arrival j = task_offset tsk + n * task_period tsk

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

  Proof.
    intros × ARR TSK.

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

1 subgoal (ID 70)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  exists n : nat, job_arrival j = task_offset tsk + n * task_period tsk

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

    ∃ (job_index arr_seq j).

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

1 subgoal (ID 76)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  job_arrival j = task_offset tsk + job_index arr_seq j * task_period tsk

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

    specialize (periodic_arrival_times (job_index arr_seq j) j) ⇒ J_ARR.

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

1 subgoal (ID 83)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  J_ARR : arrives_in arr_seq j ->
          job_task j = tsk ->
          job_index arr_seq j = job_index arr_seq j ->
          job_arrival j =
          task_offset tsk + job_index arr_seq j * task_period tsk
  ============================
  job_arrival j = task_offset tsk + job_index arr_seq j * task_period tsk

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

    now feed_n 3 J_ARR ⇒ //.

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

No more subgoals.

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

  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:
    ∀ 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.

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

1 subgoal (ID 87)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  ============================
  forall (n : nat) (j : Job),
  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.

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

1 subgoal (ID 92)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  F : 0 < task_period tsk
  ============================
  forall (n : nat) (j : Job),
  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

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

    induction n.

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

2 subgoals (ID 97)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  F : 0 < task_period tsk
  ============================
  forall j : Job,
  arrives_in arr_seq j ->
  job_task j = tsk ->
  job_arrival j = task_offset tsk + 0 * task_period tsk ->
  job_index arr_seq j = 0

subgoal 2 (ID 100) is:
 forall j : Job,
 arrives_in arr_seq j ->
 job_task j = tsk ->
 job_arrival j = task_offset tsk + n.+1 * task_period tsk ->
 job_index arr_seq j = n.+1

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

    + intros × ARR_J TSK ARR.

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

2 subgoals (ID 104)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  F : 0 < task_period tsk
  j : Job
  ARR_J : arrives_in arr_seq j
  TSK : job_task j = tsk
  ARR : job_arrival j = task_offset tsk + 0 * task_period tsk
  ============================
  job_index arr_seq j = 0

subgoal 2 (ID 100) is:
 forall j : Job,
 arrives_in arr_seq j ->
 job_task j = tsk ->
 job_arrival j = task_offset tsk + n.+1 * task_period tsk ->
 job_index arr_seq j = n.+1

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

      destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]] ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 120)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  F : 0 < task_period tsk
  j : Job
  ARR_J : arrives_in arr_seq j
  TSK : job_task j = tsk
  ARR : job_arrival j = task_offset tsk + 0 * task_period tsk
  m : nat
  SUCC : job_index arr_seq j = m.+1
  ============================
  job_index arr_seq j = 0

subgoal 2 (ID 100) is:
 forall j : Job,
 arrives_in arr_seq j ->
 job_task j = tsk ->
 job_arrival j = task_offset tsk + n.+1 * task_period tsk ->
 job_index arr_seq j = n.+1

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

      now apply periodic_arrival_times in SUCC ⇒ //; ssrlia.

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

1 subgoal (ID 100)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  F : 0 < task_period tsk
  n : nat
  IHn : forall j : Job,
        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
  ============================
  forall j : Job,
  arrives_in arr_seq j ->
  job_task j = tsk ->
  job_arrival j = task_offset tsk + n.+1 * task_period tsk ->
  job_index arr_seq j = n.+1

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

    + intros × ARR_J TSK ARR.

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

1 subgoal (ID 392)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
  F : 0 < task_period tsk
  n : nat
  IHn : forall j : Job,
        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
  j : Job
  ARR_J : arrives_in arr_seq j
  TSK : job_task j = tsk
  ARR : job_arrival j = task_offset tsk + n.+1 * task_period tsk
  ============================
  job_index arr_seq j = n.+1

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

      specialize (H_task_respects_periodic_model j); feed_n 3 H_task_respects_periodic_model ⇒ //.

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

2 subgoals (ID 401)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  j : Job
  H_task_respects_periodic_model : 0 < job_index arr_seq j ->
                                   job_task j = tsk ->
                                   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
  F : 0 < task_period tsk
  n : nat
  IHn : forall j : Job,
        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
  ARR_J : arrives_in arr_seq j
  TSK : job_task j = tsk
  ARR : job_arrival j = task_offset tsk + n.+1 * task_period tsk
  ============================
  0 < job_index arr_seq j

subgoal 2 (ID 412) is:
 job_index arr_seq j = n.+1

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

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

1 subgoal (ID 401)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  j : Job
  H_task_respects_periodic_model : 0 < job_index arr_seq j ->
                                   job_task j = tsk ->
                                   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
  F : 0 < task_period tsk
  n : nat
  IHn : forall j : Job,
        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
  ARR_J : arrives_in arr_seq j
  TSK : job_task j = tsk
  ARR : job_arrival j = task_offset tsk + n.+1 * task_period tsk
  ============================
  0 < job_index arr_seq j

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

rewrite lt0n; apply /eqP; intro EQ.

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

1 subgoal (ID 497)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  j : Job
  H_task_respects_periodic_model : 0 < job_index arr_seq j ->
                                   job_task j = tsk ->
                                   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
  F : 0 < task_period tsk
  n : nat
  IHn : forall j : Job,
        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
  ARR_J : arrives_in arr_seq j
  TSK : job_task j = tsk
  ARR : job_arrival j = task_offset tsk + n.+1 * task_period tsk
  EQ : job_index arr_seq j = 0
  ============================
  False

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

        apply first_job_arrival with (tsk0 := tsk) in EQ ⇒ //.

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

1 subgoal (ID 504)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  j : Job
  H_task_respects_periodic_model : 0 < job_index arr_seq j ->
                                   job_task j = tsk ->
                                   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
  F : 0 < task_period tsk
  n : nat
  IHn : forall j : Job,
        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
  ARR_J : arrives_in arr_seq j
  TSK : job_task j = tsk
  ARR : job_arrival j = task_offset tsk + n.+1 * task_period tsk
  EQ : job_arrival j = task_offset tsk
  ============================
  False

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

        now rewrite EQ in ARR; ssrlia.

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

1 subgoal

subgoal 1 (ID 412) is:
 job_index arr_seq j = n.+1

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

      }

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

1 subgoal (ID 412)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  j : Job
  H_task_respects_periodic_model : 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
  F : 0 < task_period tsk
  n : nat
  IHn : forall j : Job,
        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
  ARR_J : arrives_in arr_seq j
  TSK : job_task j = tsk
  ARR : job_arrival j = task_offset tsk + n.+1 * task_period tsk
  ============================
  job_index arr_seq j = n.+1

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

      move : H_task_respects_periodic_model ⇒ [j' [ARR' [IND' [TSK' ARRIVAL']]]].

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

1 subgoal (ID 1925)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  j : Job
  H_task_respects_periodic_model : 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
  F : 0 < task_period tsk
  n : nat
  IHn : forall j : Job,
        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
  ARR_J : arrives_in arr_seq j
  TSK : job_task j = tsk
  ARR : job_arrival j = task_offset tsk + n.+1 * task_period tsk
  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
  ARRIVAL' : job_arrival j = job_arrival j' + task_period tsk
  ============================
  job_index arr_seq j = n.+1

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

      specialize (IHn j'); feed_n 3 IHn ⇒ //; first by rewrite ARR in ARRIVAL'; ssrlia.

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

1 subgoal (ID 1945)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  j : Job
  H_task_respects_periodic_model : 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
  F : 0 < task_period tsk
  n : nat
  j' : Job
  IHn : job_index arr_seq j' = n
  ARR_J : arrives_in arr_seq j
  TSK : job_task j = tsk
  ARR : job_arrival j = task_offset tsk + n.+1 * task_period tsk
  ARR' : arrives_in arr_seq j'
  IND' : job_index arr_seq j' = job_index arr_seq j - 1
  TSK' : job_task j' = tsk
  ARRIVAL' : job_arrival j = job_arrival j' + task_period tsk
  ============================
  job_index arr_seq j = n.+1

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

      rewrite IHn in IND'.

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

1 subgoal (ID 2434)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  j : Job
  H_task_respects_periodic_model : 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
  F : 0 < task_period tsk
  n : nat
  j' : Job
  IHn : job_index arr_seq j' = n
  ARR_J : arrives_in arr_seq j
  TSK : job_task j = tsk
  ARR : job_arrival j = task_offset tsk + n.+1 * task_period tsk
  ARR' : arrives_in arr_seq j'
  TSK' : job_task j' = tsk
  ARRIVAL' : job_arrival j = job_arrival j' + task_period tsk
  IND' : n = job_index arr_seq j - 1
  ============================
  job_index arr_seq j = n.+1

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

      destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]]; last by ssrlia.

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

1 subgoal (ID 2445)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  j : Job
  H_task_respects_periodic_model : 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
  F : 0 < task_period tsk
  n : nat
  j' : Job
  IHn : job_index arr_seq j' = n
  ARR_J : arrives_in arr_seq j
  TSK : job_task j = tsk
  ARR : job_arrival j = task_offset tsk + n.+1 * task_period tsk
  ARR' : arrives_in arr_seq j'
  TSK' : job_task j' = tsk
  ARRIVAL' : job_arrival j = job_arrival j' + task_period tsk
  IND' : n = job_index arr_seq j - 1
  Z : job_index arr_seq j = 0
  ============================
  job_index arr_seq j = n.+1

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

      apply first_job_arrival with (tsk0 := tsk) in Z ⇒ //.

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

1 subgoal (ID 2741)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  Job : JobType
  H1 : JobTask Job Task
  H2 : 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
  H_valid_offset : valid_offset arr_seq tsk
  H_valid_period : valid_period tsk
  j : Job
  H_task_respects_periodic_model : 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
  F : 0 < task_period tsk
  n : nat
  j' : Job
  IHn : job_index arr_seq j' = n
  ARR_J : arrives_in arr_seq j
  TSK : job_task j = tsk
  ARR : job_arrival j = task_offset tsk + n.+1 * task_period tsk
  ARR' : arrives_in arr_seq j'
  TSK' : job_task j' = tsk
  ARRIVAL' : job_arrival j = job_arrival j' + task_period tsk
  IND' : n = job_index arr_seq j - 1
  Z : job_arrival j = task_offset tsk
  ============================
  job_index arr_seq j = n.+1

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

      now rewrite Z in ARR; ssrlia.

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

No more subgoals.

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

  Qed.

End PeriodicArrivalTimes.