Platform for Models with Limited Preemptions

In this section, we prove that instantiation of predicate job_preemptable to the model with limited preemptions indeed defines a valid preemption model.
Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

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

In addition, assume the existence of a function that maps a job to the sequence of its preemption points...
  Context `{JobPreemptionPoints Job}.

..., i.e., we assume limited-preemptive jobs.
  #[local] Existing Instance limited_preemptive_job_model.

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.

Next, consider any limited ideal uni-processor schedule of this arrival sequence ...
...where jobs do not execute after their completion.
Next, we assume that preemption points are defined by the job-level model with limited preemptions.
First, we prove a few auxiliary lemmas.
  Section AuxiliaryLemmas.

Consider a job j.
    Variable j : Job.
    Hypothesis H_j_arrives : arrives_in arr_seq j.

Recall that 0 is a preemption point.
Using the fact that job_preemptive_points is a non-decreasing sequence, we prove that the first element of job_preemptive_points is 0.
We prove that the list of preemption points is not empty.
Next, we prove that the cost of a job is a preemption point.
As a corollary, we prove that the sequence of non-preemptive points of a job with positive cost contains at least 2 points.
Next we prove that "anti-density" property (from preemption.util file) holds for job_preemption_point j.
    Lemma antidensity_of_preemption_points:
       (ρ : work),
        ρ job_cost j
        ~~ (ρ \in job_preemptive_points j)
        first0 (job_preemptive_points j) ρ < last0 (job_preemptive_points j).

We also prove that any work that doesn't belong to preemption points of job j is placed strictly between two neighboring preemption points.
    Lemma work_belongs_to_some_nonpreemptive_segment:
       (ρ : work),
        ρ job_cost j
        ~~ (ρ \in job_preemptive_points j)
          n.+1 < size (job_preemptive_points j)
          nth 0 (job_preemptive_points j) n < ρ < nth 0 (job_preemptive_points j) n.+1.

Recall that the module prosa.model.preemption.parameters also defines a notion of preemption points, namely job_preemption_points, which cannot have duplicated preemption points. Therefore, we need additional lemmas to relate job_preemption_points and job_preemptive_points.
First we show that the length of the last non-preemptive segment in job_preemption_points is equal to the length of the last non-empty non-preemptive segment of job_preemptive_points.
    Lemma job_parameters_last_np_to_job_limited:
        last0 (distances (job_preemption_points j)) =
        last0 (filter (fun x ⇒ 0 < x) (distances (job_preemptive_points j))).

Next we show that the length of the max non-preemptive segment of job_preemption_points is equal to the length of the max non-preemptive segment of job_preemptive_points.
We prove that the fixed_preemption_point_model function defines a valid preemption model.
  Lemma valid_fixed_preemption_points_model_lemma:
    valid_preemption_model arr_seq sched.

End ModelWithLimitedPreemptions.
Global Hint Resolve valid_fixed_preemption_points_model_lemma : basic_rt_facts.