Add notion of busy interval

classic/util/minmax.v

+Require Export rt.util.minmax.
 Require Import rt.classic.util.tactics rt.classic.util.notation rt.classic.util.sorting rt.classic.util.nat rt.classic.util.list.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
@@ -512,129 +513,6 @@ Section MinMaxSeq.
 
 End MinMaxSeq.
 
-(* Additional lemmas about max. *)
-Section ExtraLemmas.
-
-  Lemma leq_bigmax_cond_seq (T : eqType) (P : pred T) (r : seq T) F i0 :
-    i0 \in r -> P i0 -> F i0 <= \max_(i <- r | P i) F i.
-  Proof.
-    intros IN0 Pi0; by rewrite (big_rem i0) //= Pi0 leq_maxl.
-  Qed.
-
-  Lemma bigmax_sup_seq:
-    forall (T: eqType) (i: T) r (P: pred T) m F,
-      i \in r -> P i -> m <= F i -> m <= \max_(i <- r| P i) F i.
-  Proof.
-    intros.
-    induction r.
-    - by rewrite in_nil  in H.
-      move: H; rewrite in_cons; move => /orP [/eqP EQA | IN].
-      {
-        clear IHr; subst a.
-        rewrite (big_rem i) //=; last by rewrite in_cons; apply/orP; left.
-        apply leq_trans with (F i); first by done.
-          by rewrite H0 leq_maxl.
-      }
-      {
-        apply leq_trans with (\max_(i0 <- r | P i0) F i0); first by apply IHr.
-        rewrite [in X in _ <= X](big_rem a) //=; last by rewrite in_cons; apply/orP; left.
-
-        have Ob: a == a; first by done.
-          by rewrite Ob leq_maxr.
-      }
-  Qed.
-
-  Lemma bigmax_leq_seqP (T : eqType) (P : pred T) (r : seq T) F m :
-    reflect (forall i, i \in r -> P i -> F i <= m)
-            (\max_(i <- r | P i) F i <= m).
-  Proof.
-    apply: (iffP idP) => leFm => [i IINR Pi|];
-      first by apply: leq_trans leFm; apply leq_bigmax_cond_seq.
-    rewrite big_seq_cond; elim/big_ind: _ => // m1 m2.
-      by intros; rewrite geq_max; apply/andP; split. 
-      by move: m2 => /andP [M1IN Pm1]; apply: leFm.
-  Qed.
-
-  Lemma leq_big_max (T : eqType) (P : pred T) (r : seq T) F1 F2 :
-    (forall i, i \in r -> P i -> F1 i <= F2 i) ->
-    \max_(i <- r | P i) F1 i <= \max_(i <- r | P i) F2 i.
-  Proof.
-    intros; apply /bigmax_leq_seqP; intros.
-    specialize (H i); feed_n 2 H; try(done).
-    rewrite (big_rem i) //=; rewrite H1.
-      by apply leq_trans with (F2 i); [ | rewrite leq_maxl].
-  Qed.
-
-  Lemma bigmax_ord_ltn_identity n :
-    n > 0 ->
-    \max_(i < n) i < n.
-  Proof.
-    intros LT.
-    destruct n; first by rewrite ltn0 in LT.
-    clear LT.
-    induction n; first by rewrite big_ord_recr /= big_ord0 maxn0.
-    rewrite big_ord_recr /=.
-    unfold maxn at 1; desf.
-    by apply leq_trans with (n := n.+1).
-  Qed.
-    
-  Lemma bigmax_ltn_ord n (P : pred nat) (i0: 'I_n) :
-    P i0 ->
-    \max_(i < n | P i) i < n.
-  Proof.
-    intros LT.
-    destruct n; first by destruct i0 as [i0 P0]; move: (P0) => P0'; rewrite ltn0 in P0'.
-    rewrite big_mkcond.
-    apply leq_ltn_trans with (n := \max_(i < n.+1) i).
-    {
-      apply/bigmax_leqP; ins.
-      destruct (P i); last by done.
-      by apply leq_bigmax_cond.
-    }
-    by apply bigmax_ord_ltn_identity.
-  Qed.
-
-  Lemma bigmax_pred n (P : pred nat) (i0: 'I_n) :
-    P (i0) ->
-    P (\max_(i < n | P i) i).
-  Proof.
-    intros PRED.
-    induction n.
-    {
-      destruct i0 as [i0 P0].
-      by move: (P0) => P1; rewrite ltn0 in P1. 
-    }
-    rewrite big_mkcond big_ord_recr /=; desf.
-    {
-      destruct n; first by rewrite big_ord0 maxn0.
-      unfold maxn at 1; desf.
-      exfalso.
-      apply negbT in Heq0; move: Heq0 => /negP BUG.
-      apply BUG. 
-      apply leq_ltn_trans with (n := \max_(i < n.+1) i).
-      {
-        apply/bigmax_leqP; ins.
-        destruct (P i); last by done.
-        by apply leq_bigmax_cond.
-      }
-      by apply bigmax_ord_ltn_identity.
-    }
-    {
-      rewrite maxn0.
-      rewrite -big_mkcond /=.
-      have LT: i0 < n.
-      {
-        rewrite ltn_neqAle; apply/andP; split;
-          last by rewrite -ltnS; apply ltn_ord.
-        apply/negP; move => /eqP BUG.
-        by rewrite -BUG PRED in Heq.
-      }
-      by rewrite (IHn (Ordinal LT)).
-    }
-  Qed.
-    
-End ExtraLemmas.
-
 Section Kmin.
 
     Context {T1 T2: eqType}.

classic/util/nat.v

@@ -11,13 +11,6 @@ Section NatLemmas.
     by destruct b1,b2;
     rewrite ?addn0 ?add0n ?addn1 ?orTb ?orbT ?orbF ?orFb.
   Qed.
-
-  Lemma subh2 :
-    forall m1 m2 n1 n2,
-      m1 >= m2 ->
-      n1 >= n2 ->
-      (m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2).
-  Proof. by ins; ssromega. Qed.
   
   Lemma subh4:
     forall m n p,

classic/util/sum.v

@@ -120,51 +120,9 @@ Section ExtraLemmas.
   
 End ExtraLemmas.
 
+
 (* Lemmas about arithmetic with sums. *)
 Section SumArithmetic.
-
-  Lemma sum_seq_diff:
-    forall (T:eqType) (rs: seq T) (F G : T -> nat),
-      (forall i : T, i \in rs -> G i <= F i) ->
-      \sum_(i <- rs) (F i - G i) = \sum_(i <- rs) F i - \sum_(i <- rs) G i.
-  Proof.
-    intros.
-    induction rs; first by rewrite !big_nil subn0. 
-    rewrite !big_cons subh2.
-    - apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHrs.
-        by intros; apply H; rewrite in_cons; apply/orP; right.
-    - by apply H; rewrite in_cons; apply/orP; left.
-    - rewrite big_seq_cond [in X in _ <= X]big_seq_cond.
-      rewrite leq_sum //; move => i /andP [IN _].
-        by apply H; rewrite in_cons; apply/orP; right.
-  Qed.
-  
-  Lemma sum_diff:
-    forall n F G,
-      (forall i (LT: i < n), F i >= G i) ->
-      \sum_(0 <= i < n) (F i - G i) =
-      (\sum_(0 <= i < n) (F i)) - (\sum_(0 <= i < n) (G i)).       
-  Proof.
-    intros n F G ALL.
-    rewrite sum_seq_diff; first by done.
-    move => i; rewrite mem_index_iota; move => /andP [_ LT].
-      by apply ALL.
-  Qed.
-
-  Lemma sum_pred_diff:
-    forall (T: eqType) (rs: seq T) (P: T -> bool) (F: T -> nat),
-      \sum_(r <- rs | P r) F r =
-      \sum_(r <- rs) F r - \sum_(r <- rs | ~~ P r) F r.
-  Proof.
-    clear; intros.
-    induction rs; first by rewrite !big_nil subn0.
-    rewrite !big_cons !IHrs; clear IHrs.
-    case (P a); simpl; last by rewrite subnDl.
-    rewrite addnBA; first by done.
-    rewrite big_mkcond leq_sum //.
-    intros t _.
-      by case (P t).
-  Qed.
   
   Lemma telescoping_sum :
     forall (T: Type) (F: T->nat) r (x0: T),

restructuring/analysis/definitions/busy_interval.v

+From rt.util Require Export all.
+From rt.restructuring.behavior Require Export all.
+From rt.restructuring.analysis.basic_facts Require Export all.
+From rt.restructuring.model Require Export job task.
+From rt.restructuring.model.schedule Require Export work_conserving.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(** * Busy Interval for JLFP-models *)
+(** In this file we define the notion of busy intervals for uniprocessor for JLFP schedulers. *)
+Section BusyIntervalJLFP.
+  
+  (** Consider any type of jobs. *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.    
+
+  (** Consider any arrival sequence with consistent arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+  
+  (** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)
+  Variable sched : schedule (ideal.processor_state Job).
+  
+  (** Assume a given JLFP policy. *)
+  Variable higher_eq_priority : JLFP_policy Job. 
+
+  (** In this section, we define the notion of a busy interval. *)
+  Section BusyInterval.
+    
+    (** Consider any job j. *)
+    Variable j : Job.
+    Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
+    
+    (** We say that t is a quiet time for j iff every higher-priority job from
+         the arrival sequence that arrived before t has completed by that time. *)
+    Definition quiet_time (t : instant) :=
+      forall (j_hp : Job),
+        arrives_in arr_seq j_hp ->
+        higher_eq_priority j_hp j ->
+        arrived_before j_hp t ->
+        completed_by sched j_hp t.
+    
+    (** Based on the definition of quiet time, we say that interval
+         [t1, t_busy) is a (potentially unbounded) busy-interval prefix
+         iff the interval starts with a quiet time where a higher or equal 
+         priority job is released and remains non-quiet. We also require
+         job j to be released in the interval. *)    
+    Definition busy_interval_prefix (t1 t_busy : instant) :=
+      t1 < t_busy /\
+      quiet_time t1 /\
+      (forall t, t1 < t < t_busy -> ~ quiet_time t) /\
+      t1 <= job_arrival j < t_busy.
+
+    (** Next, we say that an interval [t1, t2) is a busy interval iff
+         [t1, t2) is a busy-interval prefix and t2 is a quiet time. *)
+    Definition busy_interval (t1 t2 : instant) :=
+      busy_interval_prefix t1 t2 /\
+      quiet_time t2.
+
+  End BusyInterval.
+
+  (** In this section we define the computational
+       version of the notion of quiet time. *)
+  Section DecidableQuietTime.
+
+    (** We say that t is a quiet time for j iff every higher-priority job from
+         the arrival sequence that arrived before t has completed by that time. *)
+    Definition quiet_time_dec (j : Job) (t : instant) :=
+      all
+        (fun j_hp => higher_eq_priority j_hp j ==> (completed_by sched j_hp t))
+        (arrivals_before arr_seq t).
+
+    (** We also show that the computational and propositional definitions are equivalent. *)
+    Lemma quiet_time_P :
+      forall j t, reflect (quiet_time j t) (quiet_time_dec j t).
+    Proof.
+      intros; apply/introP.
+      - intros QT s ARRs HPs BEFs.
+        move: QT => /allP QT.
+        specialize (QT s); feed QT.
+        eapply arrived_between_implies_in_arrivals; eauto 2.
+          by move: QT => /implyP Q; apply Q in HPs.
+      - move => /negP DEC; intros QT; apply: DEC.
+        apply/allP; intros s ARRs.
+        apply/implyP; intros HPs.
+        apply QT; try done.
+        + by apply in_arrivals_implies_arrived in ARRs.
+        + by eapply in_arrivals_implies_arrived_between in ARRs; eauto 2.
+    Qed.
+
+  End DecidableQuietTime.
+
+End BusyIntervalJLFP.
\ No newline at end of file

restructuring/analysis/definitions/no_carry_in.v

+From rt.util Require Export all.
+From rt.restructuring.behavior Require Export all.
+From rt.restructuring.analysis.basic_facts Require Export all.
+From rt.restructuring Require Export model.job model.task.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(** * No Carry-In *)
+(** In this module we define the notion of no carry-in time for uniprocessor schedulers. *)
+Section NoCarryIn.
+  
+  (** 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}.    
+
+  (** Consider any arrival sequence with consistent arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+  
+  (** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)
+  Variable sched : schedule (ideal.processor_state Job).
+
+  (** The processor has no carry-in at time t iff every job (regardless of priority) 
+      from the arrival sequence released before t has completed by that time. *)
+  Definition no_carry_in (t : instant) :=
+    forall j_o,
+      arrives_in arr_seq j_o ->
+      arrived_before j_o t ->
+      completed_by sched j_o t.
+
+End NoCarryIn.

restructuring/analysis/definitions/priority_inversion.v

+From rt.util Require Export all.
+From rt.restructuring.behavior Require Export all.
+From rt.restructuring.analysis.basic_facts Require Export all.
+From rt.restructuring Require Export model.job model.task.
+From rt.restructuring.model.schedule Require Export work_conserving priority_based.priorities.
+From rt.restructuring.analysis.definitions Require Export busy_interval.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(** * Cumulative Priority Inversion for JLFP-models *)
+(** In this module we define the notion of cumulative priority inversion for uniprocessor for JLFP schedulers. *)
+Section CumulativePriorityInversion.
+  
+  (** 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}.    
+
+  (** Consider any arrival sequence with consistent arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+  
+  (** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)
+  Variable sched : schedule (ideal.processor_state Job).
+
+  (** Assume a given JLFP policy. *)
+  Variable higher_eq_priority : JLFP_policy Job. 
+
+  (** In this section, we define a notion of bounded priority inversion experienced by a job. *)
+  Section JobPriorityInversionBound.
+
+    (** Consider an arbitrary task [tsk]. *)
+    Variable tsk : Task.
+
+    (** Consider any job j of tsk. *)
+    Variable j : Job.
+    Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
+    Hypothesis H_job_task : job_of_task tsk j. 
+
+    (** We say that the job incurs priority inversion if it has higher
+        priority than the scheduled job. Note that this definition
+        implicitly assumes that the scheduler is
+        work-conserving. Therefore, it cannot be applied to models
+        with jitter or self-suspensions. *)
+    Definition is_priority_inversion (t : instant) :=
+      if sched t is Some jlp then
+        ~~ higher_eq_priority jlp j
+      else false.
+    
+    (** Then we compute the cumulative priority inversion incurred by
+         a job within some time interval [t1, t2). *)
+    Definition cumulative_priority_inversion (t1 t2 : instant) :=
+      \sum_(t1 <= t < t2) is_priority_inversion t.
+
+    (** We say that priority inversion of job j is bounded by a constant B iff cumulative 
+         priority inversion within any busy inverval prefix is bounded by B. *)
+    Definition priority_inversion_of_job_is_bounded_by (B : duration) :=
+      forall (t1 t2 : instant),
+        busy_interval_prefix arr_seq sched higher_eq_priority j t1 t2 ->
+        cumulative_priority_inversion t1 t2 <= B.
+
+  End JobPriorityInversionBound.
+
+  (** In this section, we define a notion of the bounded priority inversion for task. *)
+  Section TaskPriorityInversionBound.
+
+    (** Consider an arbitrary task tsk. *)
+    Variable tsk : Task.
+
+    (** We say that task tsk has bounded priority inversion if all 
+         its jobs have bounded cumulative priority inversion. *)
+    Definition priority_inversion_is_bounded_by (B : duration) :=
+      forall (j : Job),
+        arrives_in arr_seq j ->
+        job_task j = tsk ->
+        job_cost j > 0 -> 
+        priority_inversion_of_job_is_bounded_by j B.
+
+  End TaskPriorityInversionBound.
+
+End CumulativePriorityInversion.

restructuring/analysis/facts/no_carry_in_exists.v

+From rt.util Require Export all.
+From rt.restructuring.behavior Require Export all.
+From rt.restructuring.analysis.basic_facts Require Export all.
+From rt.restructuring Require Export model.job model.task.
+From rt.restructuring.model.schedule Require Export work_conserving priority_based.priorities.
+From rt.restructuring.analysis.definitions Require Export no_carry_in busy_interval priority_inversion.
+From rt.restructuring.analysis.facts Require Export busy_interval_exists.
+
+(** Throughout the file we assume for the classic Liu & Layland model
+   of readiness without jitter and no self-suspensions, where prending
+   jobs are always ready. *)
+From rt.restructuring.model Require Import readiness.basic.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(** * Existence of No Carry-In Instant *)
+
+(** In this section, we derive an alternative condition for the existence of 
+       a busy interval. The new condition requires the total workload (instead 
+       of the high-priority workload) generated by the task set to be bounded. *)
+
+(** Next, we derive a sufficient condition for existence of
+    no carry-in instant for uniprocessor for JLFP schedulers *)
+Section ExistsNoCarryIn.
+  
+  (** 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}.    
+
+  (** Consider any arrival sequence with consistent arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+  
+  (** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
+  Variable sched : schedule (ideal.processor_state Job).
+  Hypothesis H_jobs_come_from_arrival_sequence:
+    jobs_come_from_arrival_sequence sched arr_seq.
+  
+  (** ... where jobs do not execute before their arrival or after completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+
+  (** Assume a given JLFP policy. *)
+  Variable higher_eq_priority : JLFP_policy Job. 
+  
+  (** For simplicity, let's define some local names. *)
+  Let job_pending_at := pending sched.
+  Let job_completed_by := completed_by sched.
+  Let arrivals_between := arrivals_between arr_seq.
+  Let no_carry_in := no_carry_in arr_seq sched.
+  Let quiet_time := quiet_time arr_seq sched higher_eq_priority.
+
+  (** 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 t ->
+      quiet_time j t.
+  Proof.
+      by intros j t FQT j_hp ARR HP BEF; apply FQT.
+  Qed.
+
+  (** Assume that the schedule is work-conserving, ... *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+
+  (** ... and there are no duplicate job arrivals. *)
+  Hypothesis H_arrival_sequence_is_a_set:
+    arrival_sequence_uniq arr_seq.
+  
+  (** We show that an idle time implies no carry in at this time instant. *)
+  Lemma idle_instant_implies_no_carry_in_at_t :
+    forall t,
+      is_idle sched t ->
+      no_carry_in t.
+  Proof.
+    intros ? IDLE j ARR HA.
+    apply/negPn/negP; intros NCOMPL.
+    move: IDLE => /eqP IDLE.
+    move: (H_work_conserving j t ARR) => NIDLE. 
+    feed NIDLE.
+    { apply/andP; split; last first.
+      { by rewrite scheduled_at_def IDLE. }
+      { by apply/andP; split; [apply ltnW | done]. }
+    }
+    move: NIDLE => [j' SCHED].
+      by rewrite scheduled_at_def IDLE in SCHED.
+  Qed.
+  
+  (** Moreover, an idle time implies no carry in at the next time instant. *)
+  Lemma idle_instant_implies_no_carry_in_at_t_pl_1 :
+    forall t,
+      is_idle sched t ->
+      no_carry_in t.+1.
+  Proof.
+    intros ? IDLE j ARR HA.
+    apply/negPn/negP; intros NCOMPL.
+    move: IDLE => /eqP IDLE.
+    move: (H_work_conserving j t ARR) => NIDLE. 
+    feed NIDLE.
+    { apply/andP; split; last first.
+      { by rewrite scheduled_at_def IDLE. }
+      { apply/andP; split; first by done.
+        move: NCOMPL => /negP NC1; apply/negP; intros NC2; apply: NC1.
+          by apply completion_monotonic with t. 
+      }  
+    }
+    move: NIDLE => [j' SCHED].
+      by rewrite scheduled_at_def IDLE in SCHED.
+  Qed.
+  
+  (** Let the priority relation be reflexive. *)
+  Hypothesis H_priority_is_reflexive: reflexive_priorities.
+  
+  (** Recall the notion of workload of all jobs released in a given interval [t1, t2)... *)
+  Let total_workload t1 t2 :=
+    workload_of_jobs predT (arrivals_between t1 t2).
+
+  (** ... and total service of jobs within some time interval [t1, t2). *)
+  Let total_service t1 t2 :=
+    service_of_jobs sched predT (arrivals_between 0 t2) t1 t2.
+  
+  (** Assume that for some positive Δ, the sum of requested workload 
+         at time (t + Δ) is bounded by delta (i.e., the supply). 
+         Note that this assumption bounds the total workload of
+         jobs released in a time interval [t, t + Δ) regardless of 
+         their priorities. *)
+  Variable Δ: duration.
+  Hypothesis H_delta_positive: Δ > 0.
+  Hypothesis H_workload_is_bounded: forall t, total_workload t (t + Δ) <= Δ.
+
+  (** Next we prove that since for any time instant t there is a point where 
+         the total workload is upper-bounded by the supply the processor encounters 
+         no carry-in instants at least every Δ time units. *)
+  Section ProcessorIsNotTooBusy.
+
+    (** We start by proving that the processor has no carry-in at 
+           the beginning (i.e., has no carry-in at time instant 0). *)
+    Lemma no_carry_in_at_the_beginning :
+      no_carry_in 0.
+    Proof.
+      intros s ARR AB; exfalso.
+        by rewrite /arrived_before ltn0 in AB.
+    Qed.
+
+    (** In this section, we prove that for any time instant t there
+           exists another time instant t' ∈ (t, t + Δ] such that the 
+           processor has no carry-in at time t'. *)
+    Section ProcessorIsNotTooBusyInduction. 
+
+      (** Consider an arbitrary time instant t... *)
+      Variable t: duration.
+      
+      (** ...such that the processor has no carry-in at time t. *)
+      Hypothesis H_no_carry_in: no_carry_in t.
+
+      (** First, recall that the total service is bounded by the total workload. Therefore
+             the total service of jobs in the interval [t, t + Δ) is bounded by Δ. *)
+      Lemma total_service_is_bounded_by_Δ :
+        total_service t (t + Δ) <= Δ.
+      Proof.
+        unfold total_service. 
+        rewrite -{3}[Δ]addn0 -{2}(subnn t) addnBA // [in X in _ <= X]addnC.
+        apply service_of_jobs_le_length_of_interval'.
+          by eapply arrivals_uniq; eauto 2.
+      Qed.
+
+      (** Next we consider two cases: 
+             (1) The case when the total service is strictly less than Δ, 
+             (2) And when the total service is equal to Δ. *)
+
+      (** In the first case, we use the pigeonhole principle to conclude 
+             that there is an idle time instant; which in turn implies existence
+             of a time instant with no carry-in. *)
+      Lemma low_total_service_implies_existence_of_time_with_no_carry_in :
+        total_service t (t + Δ) < Δ ->
+        exists δ, δ < Δ /\ no_carry_in (t.+1 + δ).
+      Proof.
+        unfold total_service; intros LT.
+        rewrite -{3}[Δ]addn0 -{2}(subnn t) addnBA // [Δ + t]addnC in LT.
+        eapply low_service_implies_existence_of_idle_time in LT; eauto. 
+        move: LT => [t_idle [/andP [LEt GTe] IDLE]].
+        move: LEt; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT].
+        { exists 0; split; first done.
+          rewrite addn0; subst t_idle.
+          intros s ARR BEF.
+          apply idle_instant_implies_no_carry_in_at_t_pl_1 in IDLE; try done.
+            by apply IDLE.
+        }
+        have EX: exists γ, t_idle = t + γ.
+        { by exists (t_idle - t); rewrite subnKC // ltnW. }
+        move: EX => [γ EQ]; subst t_idle; rewrite ltn_add2l in GTe.
+        rewrite -{1}[t]addn0 ltn_add2l in LT.
+        exists (γ.-1); split. 
+        - apply leq_trans with γ. by rewrite prednK. by rewrite ltnW.
+        - rewrite -subn1 -addn1 -addnA subnKC //.
+          intros s ARR BEF.
+            by apply idle_instant_implies_no_carry_in_at_t.
+      Qed.
+      
+      (** In the second case, the total service within the time interval [t, t + Δ) is equal to Δ. 
+             On the other hand, we know that the total workload is lower-bounded by the total service
+             and upper-bounded by Δ. Therefore, the total workload is equal to total service this
+             implies completion of all jobs by time [t + Δ] and hence no carry-in at time [t + Δ]. *)
+      Lemma completion_of_all_jobs_implies_no_carry_in :
+        total_service t (t + Δ) = Δ ->
+        no_carry_in (t + Δ).
+      Proof.
+        unfold total_service; intros EQserv.
+        move: (H_workload_is_bounded t); move => WORK.
+        have EQ: total_workload 0 (t + Δ) = service_of_jobs sched predT (arrivals_between 0 (t + Δ)) 0 (t + Δ).
+        { intros.
+          have COMPL := all_jobs_have_completed_impl_workload_eq_service
+                          arr_seq H_arrival_times_are_consistent sched
+                          H_jobs_must_arrive_to_execute
+                          H_completed_jobs_dont_execute
+                          predT 0 t t.
+          feed COMPL; try done.
+          { intros j A B; apply H_no_carry_in.
+            - eapply in_arrivals_implies_arrived; eauto 2.
+            - eapply in_arrivals_implies_arrived_between in A; eauto 2.
+          }
+          apply/eqP; rewrite eqn_leq; apply/andP; split;
+            last by apply service_of_jobs_le_workload;
+            auto using ideal_proc_model_provides_unit_service.
+          rewrite /total_workload (workload_of_jobs_cat arr_seq t); last first.
+          apply/andP; split; [by done | by rewrite leq_addr].
+          rewrite (service_of_jobs_cat_scheduling_interval _ _ _ _ _ _ _ t); try done; first last.
+          { by apply/andP; split; [by done | by rewrite leq_addr]. }
+          rewrite COMPL -addnA leq_add2l. 
+          rewrite -service_of_jobs_cat_arrival_interval; last first.
+          apply/andP; split; [by done| by rewrite leq_addr].
+          rewrite EQserv.
+            by apply H_workload_is_bounded.
+        }  
+        intros s ARR BEF.
+        eapply workload_eq_service_impl_all_jobs_have_completed; eauto 2; try done.
+          by eapply arrived_between_implies_in_arrivals; eauto 2.
+      Qed.
+
+    End ProcessorIsNotTooBusyInduction.
+
+    (** Finally, we show that any interval of length Δ contains a time instant with no carry-in. *)
+    Lemma processor_is_not_too_busy :
+      forall t, exists δ, δ < Δ /\ no_carry_in (t + δ).
+    Proof.
+      induction t.
+      { by exists 0; split; [ | rewrite addn0; apply no_carry_in_at_the_beginning]. }
+      { move: IHt => [δ [LE FQT]].
+        move: (posnP δ) => [Z|POS]; last first.
+        { exists (δ.-1); split.
+          - by apply leq_trans with δ; [rewrite prednK | apply ltnW]. 
+          - by rewrite -subn1 -addn1 -addnA subnKC //.
+        } subst δ; rewrite addn0 in FQT; clear LE.
+        move: (total_service_is_bounded_by_Δ t); rewrite leq_eqVlt; move => /orP [/eqP EQ | LT].
+        - exists (Δ.-1); split.
+          + by rewrite prednK. 
+          + by rewrite addSn -subn1 -addn1 -addnA subnK; first apply completion_of_all_jobs_implies_no_carry_in.
+        - by apply low_total_service_implies_existence_of_time_with_no_carry_in. 
+      }
+    Qed.
+    
+  End ProcessorIsNotTooBusy.
+  
+  (** 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.    
+
+  (** We show that there must exist a busy interval [t1, t2) that
+         contains the arrival time of j. *)
+  Corollary exists_busy_interval_from_total_workload_bound :
+    exists t1 t2, 
+      t1 <= job_arrival j < t2 /\
+      t2 <= t1 + Δ /\
+      busy_interval arr_seq sched higher_eq_priority j t1 t2.
+  Proof.
+    rename H_from_arrival_sequence into ARR, H_job_cost_positive into POS.
+    edestruct (exists_busy_interval_prefix
+                 arr_seq H_arrival_times_are_consistent sched higher_eq_priority j ARR H_priority_is_reflexive (job_arrival j))
+      as [t1 [PREFIX GE]].
+    apply job_pending_at_arrival; auto. 
+    move: GE => /andP [GE1 _].
+    exists t1; move: (processor_is_not_too_busy t1.+1) => [δ [LE QT]].
+    apply no_carry_in_implies_quiet_time with (j := j) in QT.
+    have EX: exists t2, ((t1 < t2 <= t1.+1 + δ) && quiet_time_dec arr_seq sched higher_eq_priority j t2).
+    { exists (t1.+1 + δ); apply/andP; split.
+      - by apply/andP; split; first rewrite addSn ltnS leq_addr. 
+      - by apply/quiet_time_P. }
+    move: (ex_minnP EX) => [t2 /andP [/andP [GTt2 LEt2] QUIET] MIN]; clear EX.
+    have NEQ: t1 <= job_arrival j < t2.
+    { apply/andP; split; first by done. 
+      rewrite ltnNge; apply/negP; intros CONTR.
+      move: (PREFIX) => [_ [_ [NQT _]]].
+      move: (NQT t2); clear NQT; move  => NQT.
+      feed NQT; first by (apply/andP; split; [|rewrite ltnS]). 
+        by apply: NQT; apply/quiet_time_P.
+    }
+    exists t2; split; last split; first by done. 
+    { apply leq_trans with (t1.+1 + δ); [by done | by rewrite addSn ltn_add2l]. }
+    { move: PREFIX => [_ [QTt1 [NQT _]]]; repeat split; try done.
+      - move => t /andP [GEt LTt] QTt.
+        feed (MIN t).
+        { apply/andP; split.
+          + by apply/andP; split; last (apply leq_trans with t2; [apply ltnW | ]).
+          + by apply/quiet_time_P.
+        }
+          by move: LTt; rewrite ltnNge; move => /negP LTt; apply: LTt.
+      - by apply/quiet_time_P. 
+    }
+  Qed.
+   
+End ExistsNoCarryIn.

util/all.v

@@ -12,5 +12,6 @@ Require Export rt.util.step_function.
 Require Export rt.util.epsilon.
 Require Export rt.util.search_arg.
 Require Export rt.util.rel.
+Require Export rt.util.minmax.
 Require Export rt.util.nondecreasing.
 Require Export rt.util.rewrite_facilities.

util/minmax.v

+Require Import rt.util.tactics rt.util.notation rt.util.nat rt.util.list.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(* Additional lemmas about max. *)
+Section ExtraLemmas.
+
+  Lemma leq_bigmax_cond_seq (T : eqType) (P : pred T) (r : seq T) F i0 :
+    i0 \in r -> P i0 -> F i0 <= \max_(i <- r | P i) F i.
+  Proof.
+    intros IN0 Pi0; by rewrite (big_rem i0) //= Pi0 leq_maxl.
+  Qed.
+
+  Lemma bigmax_sup_seq:
+    forall (T: eqType) (i: T) r (P: pred T) m F,
+      i \in r -> P i -> m <= F i -> m <= \max_(i <- r| P i) F i.
+  Proof.
+    intros.
+    induction r.
+    - by rewrite in_nil  in H.
+      move: H; rewrite in_cons; move => /orP [/eqP EQA | IN].
+      {
+        clear IHr; subst a.
+        rewrite (big_rem i) //=; last by rewrite in_cons; apply/orP; left.
+        apply leq_trans with (F i); first by done.
+          by rewrite H0 leq_maxl.
+      }
+      {
+        apply leq_trans with (\max_(i0 <- r | P i0) F i0); first by apply IHr.
+        rewrite [in X in _ <= X](big_rem a) //=; last by rewrite in_cons; apply/orP; left.
+
+        have Ob: a == a; first by done.
+          by rewrite Ob leq_maxr.
+      }
+  Qed.
+
+  Lemma bigmax_leq_seqP (T : eqType) (P : pred T) (r : seq T) F m :
+    reflect (forall i, i \in r -> P i -> F i <= m)
+            (\max_(i <- r | P i) F i <= m).
+  Proof.
+    apply: (iffP idP) => leFm => [i IINR Pi|];
+      first by apply: leq_trans leFm; apply leq_bigmax_cond_seq.
+    rewrite big_seq_cond; elim/big_ind: _ => // m1 m2.
+      by intros; rewrite geq_max; apply/andP; split. 
+      by move: m2 => /andP [M1IN Pm1]; apply: leFm.
+  Qed.
+
+  Lemma leq_big_max (T : eqType) (P : pred T) (r : seq T) F1 F2 :
+    (forall i, i \in r -> P i -> F1 i <= F2 i) ->
+    \max_(i <- r | P i) F1 i <= \max_(i <- r | P i) F2 i.
+  Proof.
+    intros; apply /bigmax_leq_seqP; intros.
+    specialize (H i); feed_n 2 H; try(done).
+    rewrite (big_rem i) //=; rewrite H1.
+      by apply leq_trans with (F2 i); [ | rewrite leq_maxl].
+  Qed.
+
+  Lemma bigmax_ord_ltn_identity n :
+    n > 0 ->
+    \max_(i < n) i < n.
+  Proof.
+    intros LT.
+    destruct n; first by rewrite ltn0 in LT.
+    clear LT.
+    induction n; first by rewrite big_ord_recr /= big_ord0 maxn0.
+    rewrite big_ord_recr /=.
+      by unfold maxn at 1; rewrite IHn.
+  Qed.
+    
+  Lemma bigmax_ltn_ord n (P : pred nat) (i0: 'I_n) :
+    P i0 ->
+    \max_(i < n | P i) i < n.
+  Proof.
+    intros LT.
+    destruct n; first by destruct i0 as [i0 P0]; move: (P0) => P0'; rewrite ltn0 in P0'.
+    rewrite big_mkcond.
+    apply leq_ltn_trans with (n := \max_(i < n.+1) i).
+    {
+      apply/bigmax_leqP; ins.
+      destruct (P i); last by done.
+      by apply leq_bigmax_cond.
+    }
+    by apply bigmax_ord_ltn_identity.
+  Qed.
+
+  Lemma bigmax_pred n (P : pred nat) (i0: 'I_n) :
+    P (i0) ->
+    P (\max_(i < n | P i) i).
+  Proof.
+    intros PRED.
+    induction n.
+    {
+      destruct i0 as [i0 P0].
+      by move: (P0) => P1; rewrite ltn0 in P1. 
+    }
+    rewrite big_mkcond big_ord_recr /=. destruct (P n) eqn:Pn.
+    {
+      destruct n; first by rewrite big_ord0 maxn0.
+      unfold maxn at 1.
+      destruct (\max_(i < n.+1) (match P (@nat_of_ord (S n) i) return nat with
+                    | true => @nat_of_ord (S n) i
+                    | false => O
+                                 end) < n.+1) eqn:Pi; first by rewrite Pi.
+      exfalso.
+      apply negbT in Pi; move: Pi => /negP BUG.
+      apply BUG. 
+      apply leq_ltn_trans with (n := \max_(i < n.+1) i).
+      {
+        apply/bigmax_leqP; ins.
+        destruct (P i); last by done.
+        by apply leq_bigmax_cond.
+      }
+      by apply bigmax_ord_ltn_identity.
+    }
+    {
+      rewrite maxn0.
+      rewrite -big_mkcond /=.
+      have LT: i0 < n.
+      {
+        rewrite ltn_neqAle; apply/andP; split;
+          last by rewrite -ltnS; apply ltn_ord.
+        apply/negP; move => /eqP BUG.
+        by rewrite -BUG PRED in Pn.
+      }
+      by rewrite (IHn (Ordinal LT)).
+    }
+  Qed.
+    
+End ExtraLemmas.
\ No newline at end of file

util/nat.v

@@ -9,6 +9,13 @@ Section NatLemmas.
       m >= n ->
       m - n + p = m + p - n.
   Proof. by ins; ssromega. Qed.
+
+  Lemma subh2 :
+    forall m1 m2 n1 n2,
+      m1 >= m2 ->
+      n1 >= n2 ->
+      (m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2).
+  Proof. by ins; ssromega. Qed.
   
   Lemma subh3:
     forall m n p,

util/sum.v

-From rt.util Require Import tactics notation nat ssromega.
+From rt.util Require Import tactics notation nat ssromega. 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
 
 (* Lemmas about sum. *)
@@ -196,6 +196,53 @@ Section ExtraLemmas.
         by rewrite ltnS ltnW.
     }
   Qed.
-
   
 End ExtraLemmas.
+
+(* Lemmas about arithmetic with sums. *)
+Section SumArithmetic.
+
+  Lemma sum_seq_diff:
+    forall (T:eqType) (rs: seq T) (F G : T -> nat),
+      (forall i : T, i \in rs -> G i <= F i) ->
+      \sum_(i <- rs) (F i - G i) = \sum_(i <- rs) F i - \sum_(i <- rs) G i.
+  Proof.
+    intros.
+    induction rs; first by rewrite !big_nil subn0. 
+    rewrite !big_cons subh2.
+    - apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHrs.
+        by intros; apply H; rewrite in_cons; apply/orP; right.
+    - by apply H; rewrite in_cons; apply/orP; left.
+    - rewrite big_seq_cond [in X in _ <= X]big_seq_cond.
+      rewrite leq_sum //; move => i /andP [IN _].
+        by apply H; rewrite in_cons; apply/orP; right.
+  Qed.
+  
+  Lemma sum_diff:
+    forall n F G,
+      (forall i (LT: i < n), F i >= G i) ->
+      \sum_(0 <= i < n) (F i - G i) =
+      (\sum_(0 <= i < n) (F i)) - (\sum_(0 <= i < n) (G i)).       
+  Proof.
+    intros n F G ALL.
+    rewrite sum_seq_diff; first by done.
+    move => i; rewrite mem_index_iota; move => /andP [_ LT].
+      by apply ALL.
+  Qed.
+
+  Lemma sum_pred_diff:
+    forall (T: eqType) (rs: seq T) (P: T -> bool) (F: T -> nat),
+      \sum_(r <- rs | P r) F r =
+      \sum_(r <- rs) F r - \sum_(r <- rs | ~~ P r) F r.
+  Proof.
+    clear; intros.
+    induction rs; first by rewrite !big_nil subn0.
+    rewrite !big_cons !IHrs; clear IHrs.
+    case (P a); simpl; last by rewrite subnDl.
+    rewrite addnBA; first by done.
+    rewrite big_mkcond leq_sum //.
+    intros t _.
+      by case (P t).
+  Qed.
+  
+End SumArithmetic.
\ No newline at end of file