Library prosa.analysis.facts.busy_interval.quiet_time

Require Export prosa.analysis.definitions.busy_interval.classical.
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.
  Proof. 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 :
    ∀ j t,
      no_carry_in arr_seq sched t →
      quiet_time arr_seq sched j t.
  Proof. 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 :
    ∀ j t1 t2,
      busy_interval_prefix arr_seq sched j t1 t2 →
      (∀ t, t1 < t < t2 → ¬ quiet_time arr_seq sched j t).
  Proof. by move⇒ j t1 t2 [_ [_ [NQT _]]]. Qed.

... and hence also not in a busy interval.
  Fact busy_interval_no_quiet_time :
    ∀ j t1 t2,
      busy_interval arr_seq sched j t1 t2 →
      (∀ t, t1 < t < t2 → ¬ quiet_time arr_seq sched j t).
  Proof. by move⇒ j t1 t2 [BIP _]; exact: busy_interval_prefix_no_quiet_time. Qed.

End Facts.