Library prosa.analysis.facts.shifted_job_costs

In this file we define a new function for job costs in an observation interval and prove its validity.
Consider any type of periodic tasks ...
  Context {Task : TaskType}.
  Context `{TaskOffset Task}.
  Context `{PeriodicModel Task}.
  Context `{TaskCost Task}.

... and any type of jobs.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.
  Context `{JobDeadline Job}.

Consider a consistent arrival sequence with non-duplicate arrivals.
Furthermore, assume that arrivals have valid job costs.
Consider a periodic task set ts such that all tasks in ts have valid periods and offsets.
Consider a job j that stems from the arrival sequence.
  Variable j : Job.
  Hypothesis H_j_from_arrival_sequence: arrives_in arr_seq j.

Let O_max denote the maximum task 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 now define a new function for job costs in the observation interval.
Given that job j arrives after O_max, the cost of a job j' that arrives in the interval [O_max + HP, O_max + 2HP) is defined to be the same as the job cost of its corresponding job in j's hyperperiod.
Assume that we have an infinite sequence of jobs.
Assume all jobs in the arrival sequence arr_seq belong to some task in ts.
We assign the job costs as defined by the job_costs_shifted function.
  Instance job_costs_in_oi : JobCost Job :=

We show that the job_costs_shifted function is valid.
  Lemma job_costs_shifted_valid: arrivals_have_valid_job_costs arr_seq.
    rewrite /arrivals_have_valid_job_costs /valid_job_cost.
    intros j' ARR.
    unfold job_cost; rewrite /job_costs_in_oi /job_costs_shifted.
    destruct (leqP O_max (job_arrival j)) as [A | B];
      last by apply H_arrivals_have_valid_job_costs ⇒ //.
    destruct (leqP (O_max + HP) (job_arrival j')) as [NEQ | NEQ];
      last by apply H_arrivals_have_valid_job_costs ⇒ //.
    destruct (leqP (O_max + 2 × HP) (job_arrival j')) as [LT | LT];
      first by apply H_arrivals_have_valid_job_costs ⇒ //.
    specialize (corresponding_jobs_have_same_task arr_seq ts j' j) ⇒ TSK.
    rewrite -[in X in _ task_cost X]TSK.
    have IN : job_task j' \in ts by apply H_jobs_from_taskset.
    by apply H_arrivals_have_valid_job_costs, corresponding_job_arrives ⇒ //; lia.

End ValidJobCostsShifted.