Library prosa.analysis.facts.busy_interval.arrival

In this section, we collect some basic facts about arrival times in busy windows. These are primarily useful for proof automation.
Section BasicFacts.

Consider any kind of jobs...
  Context {Job : JobType} `{JobArrival Job} `{JobCost Job}.
... and a JLFP policy defined on these jobs.
  Context `{JLFP_policy Job}.

Consider any processor state model.
  Context {PState : ProcessorState Job}.

Consider any schedule and arrival sequence.
  Variable sched : schedule PState.
  Variable arr_seq : arrival_sequence Job.

We note the trivial fact that, by definition, a job arrives after the beginning of its busy-interval prefix ...
  Fact busy_interval_prefix_job_arrival :
     j t t',
      busy_interval_prefix arr_seq sched j t t'
      t job_arrival j.

... and hence also after the beginning of its busy interval.
  Fact busy_interval_job_arrival :
     j t t',
      busy_interval arr_seq sched j t t'
      t job_arrival j.

End BasicFacts.

We add the above facts into the "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically where needed.
Global Hint Resolve
  busy_interval_prefix_job_arrival
  busy_interval_job_arrival
  : basic_rt_facts.

In the following section, we prove additional, more involved properties about arrival times within busy intervals.
Section Facts.

Consider any kind of jobs...
  Context {Job : JobType} `{JobArrival Job} `{JobCost Job}.

... and a reflexive JLFP policy defined on these jobs.
  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_JLFP_reflexive : reflexive_job_priorities JLFP.

Consider any processor state model.
  Context {PState : ProcessorState Job}.

Consider any arrival sequence with consistent non-duplicate arrivals
Next, consider any schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
Consider an arbitrary job j with positive cost.
  Variable j : Job.
  Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
  Hypothesis H_job_cost_positive : job_cost_positive j.

The start of a busy interval prefix t1 must coincide with the arrival of some job j_a that has a priority higher than or equal to j.