Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]


(** In this module we collect some basic facts about arrival times in busy
    windows. These are primarily useful for proof automation. *)

Section Facts.

  (** 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 ... *)
  
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JLFP_policy Job
PState: ProcessorState Job
sched: schedule PState
arr_seq: arrival_sequence Job
forall (j : Job) (t t' : instant),
busy_interval_prefix arr_seq sched j t t' ->
t <= job_arrival j

  
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JLFP_policy Job
PState: ProcessorState Job
sched: schedule PState
arr_seq: arrival_sequence Job
forall (j : Job) (t t' : instant),
busy_interval_prefix arr_seq sched j t t' ->
t <= job_arrival j
 by move=> ? ? ? [_ [_ [_ /andP [GEQ _]]]]. Qed.

  (** ... and hence also after the beginning of its busy interval. *)
  
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JLFP_policy Job
PState: ProcessorState Job
sched: schedule PState
arr_seq: arrival_sequence Job
forall (j : Job) (t t' : instant),
busy_interval arr_seq sched j t t' ->
t <= job_arrival j

  
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JLFP_policy Job
PState: ProcessorState Job
sched: schedule PState
arr_seq: arrival_sequence Job
forall (j : Job) (t t' : instant),
busy_interval arr_seq sched j t t' ->
t <= job_arrival j

    
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JLFP_policy Job
PState: ProcessorState Job
sched: schedule PState
arr_seq: arrival_sequence Job
_j_: Job
_t_, _t'_: instant
PREFIX: busy_interval_prefix arr_seq sched _j_ _t_
  _t'_
_t_ <= job_arrival _j_

    by eauto using busy_interval_prefix_job_arrival.
  Qed.

End Facts.

(** 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.