Require Export prosa.analysis.definitions.busy_interval.classical.
[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]
Require Export prosa.analysis.definitions.carry_in.

(** In this module we collect some basic facts about quiet times. *)

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 prove that 0 is always a quiet time. *)
  Lemma zero_is_quiet_time (j : Job) :
    quiet_time arr_seq sched j 0.
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
quiet_time arr_seq sched j 0
  Proof.
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
quiet_time arr_seq sched j 0 by move=> jhp ARR HP; rewrite /arrived_before ltn0. Qed.

  (** The fact that there is no carry-in at time instant [t] trivially
      implies that [t] is a quiet time. *)
  Lemma no_carry_in_implies_quiet_time :
    forall j t,
      no_carry_in arr_seq sched t ->
      quiet_time arr_seq sched j t.
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 : instant),
no_carry_in arr_seq sched t ->
quiet_time arr_seq sched j t
  Proof.
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 : instant),
no_carry_in arr_seq sched t ->
quiet_time arr_seq sched j t by move=> j t + j_hp ARR HP BEF; apply. Qed.

  (** For convenience in proofs, we restate that by definition there are no
      quiet times in a busy-interval prefix... *)
  Fact busy_interval_prefix_no_quiet_time :
    forall j t1 t2,
      busy_interval_prefix arr_seq sched j t1 t2 ->
      (forall t, t1 < t < t2 -> ~ quiet_time arr_seq sched j t).
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) (t1 t2 : instant),
busy_interval_prefix arr_seq sched j t1 t2 ->
forall t : nat,
t1 < t < t2 -> ~ quiet_time arr_seq sched j t
  Proof.
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) (t1 t2 : instant),
busy_interval_prefix arr_seq sched j t1 t2 ->
forall t : nat,
t1 < t < t2 -> ~ quiet_time arr_seq sched j t by move=> j t1 t2 [_ [_ [NQT _]]]. Qed.

  (** ... and hence also not in a busy interval. *)
  Fact busy_interval_no_quiet_time :
    forall j t1 t2,
      busy_interval arr_seq sched j t1 t2 ->
      (forall t, t1 < t < t2 -> ~ quiet_time arr_seq sched j t).
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) (t1 t2 : instant),
busy_interval arr_seq sched j t1 t2 ->
forall t : nat,
t1 < t < t2 -> ~ quiet_time arr_seq sched j t
  Proof.
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) (t1 t2 : instant),
busy_interval arr_seq sched j t1 t2 ->
forall t : nat,
t1 < t < t2 -> ~ quiet_time arr_seq sched j t by move=> j t1 t2 [BIP _]; exact: busy_interval_prefix_no_quiet_time. Qed.

End Facts.