adjust lemmas to work-bearing readiness

With some misc. cleanups and reorganization thrown in.

analysis/abstract/abstract_seq_rta.v

@@ -231,13 +231,13 @@ Section Sequential_Abstract_RTA.
         completed_by sched j2 t1.
       Proof.
         move => JA; move: (H_j2_from_tsk) => /eqP TSK2eq.
-        move: (posnP (@job_cost _ H3 j2)) => [ZERO|POS].
-        { by rewrite /completed_by /service.completed_by ZERO. }
-        move: (H_interference_and_workload_consistent_with_sequential_tasks
-                 j1 t1 t2 H_j1_arrives H_j1_from_tsk H_j1_cost_positive H_busy_interval) => SWEQ.
-        eapply all_jobs_have_completed_equiv_workload_eq_service
-          with (j := j2) in SWEQ; eauto 2; try done.
-          by apply arrived_between_implies_in_arrivals.
+        rewrite /completed_by.
+        move: (posnP (@job_cost _ H3 j2)) => [-> | POS]; first by done.
+        move: (H_interference_and_workload_consistent_with_sequential_tasks j1 t1 t2) => SWEQ.
+        feed_n 4 SWEQ; try by done.
+        apply all_jobs_have_completed_equiv_workload_eq_service with (j := j2) in SWEQ => //.
+        - by apply ideal_proc_model_provides_unit_service.
+        - by apply arrived_between_implies_in_arrivals.
       Qed.
 
       (** Next we prove that if a job is pending after the beginning

analysis/abstract/ideal_jlfp_rta.v

@@ -2,13 +2,9 @@ Require Export prosa.analysis.definitions.priority_inversion.
 Require Export prosa.analysis.abstract.abstract_seq_rta.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
-(** In this file we consider an ideal uni-processor ... *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.
 
-(** ... and classic model of readiness without jitter and no
-    self-suspensions, where pending jobs are always ready. *)
-Require Import prosa.model.readiness.basic.
-
 (** * JLFP instantiation of Interference and Interfering Workload for ideal uni-processor. *)
 (** In this module we instantiate functions Interference and Interfering Workload 
     for an arbitrary JLFP-policy that satisfies the sequential tasks hypothesis. 
@@ -372,9 +368,11 @@ Section JLFPInstantiation.
         { ideal_proc_model_sched_case_analysis_eq sched x jo; first by rewrite big1_eq.
           move: (Sched_jo); rewrite scheduled_at_def; move => /eqP EQ; rewrite EQ.
           destruct (another_hep_job jo j) eqn:PRIO.
-          - rewrite -EQ. have SCH := service_of_jobs_le_1 sched _ (arrivals_between t1 t) _ x.
-            eapply leq_trans; last by apply SCH; eauto using arrivals_uniq.
-            erewrite leq_sum; eauto 2.
+          - rewrite -EQ. have SCH := service_of_jobs_le_1 _ _ sched _ (arrivals_between t1 t) _ x.
+            eapply leq_trans; last first. 
+            + apply SCH; eauto using arrivals_uniq, ideal_proc_model_provides_unit_service,
+                            ideal_proc_model_is_a_uniprocessor_model.
+            + by erewrite leq_sum.
           - rewrite leqn0 big1 //; intros joo PRIO2.
             apply/eqP; rewrite eqb0; apply/eqP; intros C.
             inversion C; subst joo; clear C.
@@ -413,9 +411,11 @@ Section JLFPInstantiation.
         { ideal_proc_model_sched_case_analysis_eq sched x jo; first by rewrite big1_eq.
           move: (Sched_jo); rewrite scheduled_at_def; move => /eqP EQ; rewrite EQ.
           destruct (hep_job_from_another_task jo j) eqn:PRIO.
-          - rewrite -EQ. have SCH := service_of_jobs_le_1 sched _ (arrivals_between t1 t) _ x.
-            eapply leq_trans; last by apply SCH; eauto using arrivals_uniq.
-            erewrite leq_sum; eauto 2.
+          - rewrite -EQ. have SCH := service_of_jobs_le_1 _ _ sched _ (arrivals_between t1 t) _ x.
+            eapply leq_trans; last first. 
+            + by apply SCH; eauto using arrivals_uniq, ideal_proc_model_provides_unit_service,
+                            ideal_proc_model_is_a_uniprocessor_model.
+            + by erewrite leq_sum.
           - rewrite leqn0 big1 //; intros joo PRIO2.
             apply/eqP; rewrite eqb0; apply/eqP; intros C.
             inversion C; subst joo; clear C.
@@ -455,8 +455,9 @@ Section JLFPInstantiation.
               last by apply zero_is_quiet_time.
             have L2 := instantiated_cumulative_workload_of_hep_jobs_equal_total_workload_of_hep_jobs.
             rewrite /cumulative_interfering_workload_of_hep_jobs in L2; rewrite L2; clear L2.
-            rewrite eq_sym; apply/eqP. 
-            apply all_jobs_have_completed_equiv_workload_eq_service; try done.
+            rewrite eq_sym; apply/eqP.
+            apply all_jobs_have_completed_equiv_workload_eq_service;
+              eauto using ideal_proc_model_provides_unit_service.
             intros; apply QT.
             - by apply in_arrivals_implies_arrived in H4.
             - by move: H5 => /andP [H6 H7]. 
@@ -479,7 +480,7 @@ Section JLFPInstantiation.
           intros t [T0 T1]; intros jhp ARR HP ARB.
           eapply all_jobs_have_completed_equiv_workload_eq_service with
               (P := fun jhp => hep_job jhp j) (t1 := 0) (t2 := t);
-            eauto 2; last eapply arrived_between_implies_in_arrivals; try done.
+            eauto using arrived_between_implies_in_arrivals, ideal_proc_model_provides_unit_service.
           move: T0; rewrite /cumul_interference /cumul_interfering_workload.
           rewrite CIS !big_split //=; move => /eqP; rewrite eqn_add2l.
           rewrite IC1; last by apply zero_is_quiet_time.

analysis/definitions/task_schedule.v

 Require Export prosa.model.task.concept.
+Require Export prosa.analysis.facts.model.ideal_schedule.
 
 (** Due to historical reasons this file defines the notion of a
     schedule of a task for the ideal uni-processor model. This is not

analysis/facts/busy_interval/busy_interval.v

@@ -3,13 +3,11 @@ Require Export prosa.analysis.definitions.job_properties.
 Require Export prosa.analysis.definitions.priority_inversion.
 Require Export prosa.analysis.facts.behavior.all.
 Require Export prosa.analysis.facts.model.service_of_jobs.
+Require Export prosa.analysis.definitions.work_bearing_readiness.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.
 
-(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import prosa.model.readiness.basic.
-
 (** * Existence of Busy Interval for JLFP-models *)
 (** In this module we derive a sufficient condition for existence of
     busy intervals for uni-processor for JLFP schedulers. *)
@@ -22,8 +20,8 @@ Section ExistsBusyIntervalJLFP.
   (**  ... and any type of jobs associated with these tasks. *)
   Context {Job : JobType}.
   Context `{JobTask Job Task}.
-  Context `{JobArrival Job}.
-  Context `{JobCost Job}.    
+  Context {Arrival: JobArrival Job}.
+  Context {Cost : JobCost Job}.
 
   (** Consider any arrival sequence with consistent arrivals. *)
   Variable arr_seq : arrival_sequence Job.
@@ -39,8 +37,12 @@ Section ExistsBusyIntervalJLFP.
   Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
 
   (** Assume a given JLFP policy. *)
-  Context `{JLFP_policy Job}. 
-  
+  Context `{JLFP_policy Job}.
+
+  (** Further, allow for any work-bearing notion of job readiness. *)
+  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
   (** For simplicity, let's define some local names. *)
   Let job_pending_at := pending sched.
   Let job_completed_by := completed_by sched.
@@ -150,15 +152,15 @@ Section ExistsBusyIntervalJLFP.
     Proof.
       intros t IDLE jhp ARR HP AB.
       apply negbNE; apply/negP; intros NCOMP.
-      rewrite /arrived_before ltnS in AB.
-      move:(H_work_conserving _ t ARR) => WC.
-      feed WC.
-      { apply/andP. split.
-        - apply/negPn/negP; rewrite negb_and; intros COMP.
-          move: COMP => /orP; rewrite Bool.negb_involutive; move => [/negP CON|COM]; auto.
-          move: NCOMP => /negP NCOMP; apply: NCOMP.
-            by apply completion_monotonic with t.
-        - by move: IDLE => /eqP IDLE; rewrite /scheduled_at scheduled_in_def IDLE. 
+      have PEND : job_pending_at jhp t.
+      { apply/andP; split; first by done. 
+        by move: NCOMP; apply contra, completion_monotonic.
+      }
+      apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' _]]].
+      move:(H_work_conserving j' t) => WC.
+      feed_n 2 WC; first by done.
+      { apply/andP; split; first by done.
+        by move: IDLE => /eqP IDLE; rewrite /scheduled_at scheduled_in_def IDLE. 
       }
       move: IDLE WC => /eqP IDLE [jo SCHED].
       by rewrite scheduled_at_def IDLE in SCHED.
@@ -224,8 +226,8 @@ Section ExistsBusyIntervalJLFP.
     Proof.
       intros t NEQ IDLE.
       move: (pending_hp_job_exists _ NEQ) => [jhp [ARR [PEND HP]]].
-      unfold work_conserving in *.
-      feed (H_work_conserving _ t ARR).
+      apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' _]]].
+      feed (H_work_conserving _ t ARR').
       apply/andP; split; first by done.
       move: IDLE => /eqP IDLE; rewrite scheduled_at_def IDLE; by done.
       move: (H_work_conserving) => [jo SCHED].
@@ -288,42 +290,38 @@ Section ExistsBusyIntervalJLFP.
       - by eapply in_arrivals_implies_arrived; eauto 2.
       - by eapply in_arrivals_implies_arrived_before; eauto 2.
     Qed.
-    
+
     (** Next we prove that the total service within a "non-quiet" 
-        time interval <<[t1, t1 + Δ)>> is exactly Δ. *)
+        time interval <<[t1, t1 + Δ)>> is exactly [Δ]. *)
     Lemma no_idle_time_within_non_quiet_time_interval:
       service_of_jobs sched predT (arrivals_between 0 (t1 + Δ)) t1 (t1 + Δ) = Δ.
     Proof.
-      intros; unfold service_of_jobs, service_of_higher_or_equal_priority_jobs.
+      intros; unfold service_of_jobs, service_of_higher_or_equal_priority_jobs. 
       rewrite -{3}[Δ](sum_of_ones t1) exchange_big //=.
       apply/eqP; rewrite eqn_leq; apply/andP; split.
-      { rewrite leq_sum //.
-        move => t' _.
-        have SCH := service_of_jobs_le_1 sched predT (arrivals_between 0 (t1 + Δ)) _ t'. 
-          by eauto using arrivals_uniq.
-      }
-      { rewrite [in X in X <= _]big_nat_cond [in X in _ <= X]big_nat_cond //=; rewrite leq_sum //.
-        move => t' /andP [/andP [LT GT] _].
-        apply/sum_seq_gt0P.
+      { rewrite leq_sum // => t' _.
+        have SCH := @service_of_jobs_le_1 _ _ _ _ _ sched predT (arrivals_between 0 (t1 + Δ)).        
+        eapply leq_trans; last apply SCH; eauto using arrivals_uniq with basic_facts.
+        by rewrite leq_sum // => i _; rewrite -scheduled_at_def service_at_is_scheduled_at. }
+      { rewrite [in X in X <= _]big_nat_cond [in X in _ <= X]big_nat_cond //=
+                leq_sum // => t' /andP [/andP [LT GT] _]; apply/sum_seq_gt0P.
         ideal_proc_model_sched_case_analysis_eq sched t' jo.
         { exfalso; move: LT; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT].
           { subst t'.
             feed (H_no_quiet_time t1.+1); first by apply/andP; split.
-            apply: H_no_quiet_time.
-              by apply idle_time_implies_quiet_time_at_the_next_time_instant.
-          }
+            by apply H_no_quiet_time, idle_time_implies_quiet_time_at_the_next_time_instant. }
           { feed (H_no_quiet_time t'); first by apply/andP; split; last rewrite ltnW.
             apply: H_no_quiet_time; intros j_hp IN HP ARR.
-            apply contraT; intros NOTCOMP.
-            destruct (scheduled_at sched j_hp t') eqn:SCHEDhp;
-              first by rewrite scheduled_at_def EqIdle in SCHEDhp.
-            apply negbT in SCHEDhp.
-            feed (H_work_conserving j_hp t' IN);
-              first by repeat (apply/andP; split); first by apply ltnW.
+            apply contraT; intros NCOMP.
+            have PEND : job_pending_at j_hp t'.
+            { apply/andP; split.
+              - by rewrite /has_arrived ltnW.
+              - by move: NCOMP; apply contra, completion_monotonic. }
+            apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' _]]].
+            feed (H_work_conserving _ t' ARR').
+            { by apply/andP; split; last rewrite scheduled_at_def EqIdle. }
             move: H_work_conserving => [j_other SCHEDother].
-              by rewrite scheduled_at_def EqIdle in SCHEDother.
-          }              
-        }
+            by rewrite scheduled_at_def EqIdle in SCHEDother. } }
         { exists jo; split.
           - apply arrived_between_implies_in_arrivals; try done.
             apply H_jobs_come_from_arrival_sequence with t'; try done.
@@ -472,12 +470,10 @@ Section ExistsBusyIntervalJLFP.
             apply leq_trans with (cumulative_priority_inversion sched j t1 (t1 + delta) + hp_service t1 (t1 + delta)).
             { rewrite /hp_service hep_jobs_receive_no_service_before_quiet_time //.
               rewrite /service_of_higher_or_equal_priority_jobs /service_of_jobs sum_pred_diff. 
-              rewrite addnBA; last first.
-              { by rewrite big_mkcond //= leq_sum //; intros j' _; case (hep_job j' j). } 
+              rewrite addnBA; last by rewrite big_mkcond //= leq_sum //; intros j' _; case (hep_job j' j).
               rewrite addnC -addnBA.
-              { intros. have TT := no_idle_time_within_non_quiet_time_interval.
-                  by unfold service_of_jobs in TT; rewrite TT // leq_addr.
-              } 
+              { have TT := no_idle_time_within_non_quiet_time_interval.
+                by unfold service_of_jobs in TT; rewrite TT // leq_addr. } 
               { rewrite /cumulative_priority_inversion /is_priority_inversion exchange_big //=.
                 apply leq_sum_seq; move => t II _.
                 rewrite mem_index_iota in II; move: II => /andP [GEi LEt].
@@ -485,7 +481,9 @@ Section ExistsBusyIntervalJLFP.
                 { by rewrite leqn0 big1_seq //. }
                 { case PRIO1: (hep_job j1 j); simpl; first last.
                   - rewrite <- SCHED.
-                    have SCH := service_of_jobs_le_1 sched _ _ _ t; eauto using arrivals_uniq. 
+                    have SCH := @service_of_jobs_le_1 _ _ _ _ _ _ (fun i => ~~ hep_job i j) (arrivals_between 0 (t1 + delta)).
+                    eapply leq_trans; last eapply SCH; eauto using arrivals_uniq with basic_facts.
+                    by rewrite leq_sum // => i _; rewrite -scheduled_at_def service_at_is_scheduled_at.
                   - rewrite leqn0 big1_seq; first by done.
                     move => j2 /andP [PRIO2 ARRj2].
                     case EQ: (j1 == j2).
@@ -691,7 +689,7 @@ Section ExistsBusyIntervalJLFP.
         job_completed_by j (job_arrival j + delta).
       Proof.
         have BUSY := exists_busy_interval priority_inversion_bound _ delta.
-        move: (posnP (@job_cost _ H2 j)) => [ZERO|POS].
+        move: (posnP (@job_cost _ Cost j)) => [ZERO|POS].
         { by rewrite /job_completed_by /completed_by ZERO. }
         feed_n 4 BUSY; try by done.
         move: BUSY => [t1 [t2 [/andP [GE1 LT2] [GE2 BUSY]]]].

analysis/facts/busy_interval/carry_in.v

@@ -5,14 +5,12 @@ Require Export prosa.analysis.facts.busy_interval.busy_interval.
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import prosa.model.processor.ideal.
 
-(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import prosa.model.readiness.basic.
-
 (** * 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. *)
+(** 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 *)
@@ -25,8 +23,8 @@ Section ExistsNoCarryIn.
   (**  ... and any type of jobs associated with these tasks. *)
   Context {Job : JobType}.
   Context `{JobTask Job Task}.
-  Context `{JobArrival Job}.
-  Context `{JobCost Job}.    
+  Context {Arrival: JobArrival Job}.
+  Context {Cost : JobCost Job}.
 
   (** Consider any arrival sequence with consistent arrivals. *)
   Variable arr_seq : arrival_sequence Job.
@@ -51,16 +49,10 @@ Section ExistsNoCarryIn.
   Let no_carry_in := no_carry_in arr_seq sched.
   Let quiet_time := quiet_time arr_seq sched.
 
-  (** 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.
-
+  (** Further, allow for any work-bearing notion of job readiness. *)
+  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+  
   (** Assume that the schedule is work-conserving, ... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
 
@@ -68,6 +60,17 @@ Section ExistsNoCarryIn.
   Hypothesis H_arrival_sequence_is_a_set:
     arrival_sequence_uniq arr_seq.
   
+  (** 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.
+  
+  
   (** 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,
@@ -75,13 +78,18 @@ Section ExistsNoCarryIn.
       no_carry_in t.
   Proof.
     intros ? IDLE j ARR HA.
-    apply/negPn/negP; intros NCOMPL.
+    apply/negPn/negP; intros NCOMP.
+    have PEND : job_pending_at j t.
+    { apply/andP; split.
+      - by rewrite /has_arrived ltnW.
+      - by move: NCOMP; apply contra, completion_monotonic.
+    }
+    apply H_job_ready in PEND => //; destruct PEND as [jhp [ARRhp [READYhp _]]].
     move: IDLE => /eqP IDLE.
-    move: (H_work_conserving j t ARR) => NIDLE. 
+    move: (H_work_conserving _ t ARRhp) => NIDLE. 
     feed NIDLE.
-    { apply/andP; split; last first.
-      { by rewrite scheduled_at_def IDLE. }
-      { by apply/andP; split; [apply ltnW | done]. }
+    { apply/andP; split; first by done.
+      by rewrite scheduled_at_def IDLE.
     }
     move: NIDLE => [j' SCHED].
     by rewrite scheduled_at_def IDLE in SCHED.
@@ -94,16 +102,18 @@ Section ExistsNoCarryIn.
       no_carry_in t.+1.
   Proof.
     intros ? IDLE j ARR HA.
-    apply/negPn/negP; intros NCOMPL.
+    apply/negPn/negP; intros NCOMP.
+    have PEND : job_pending_at j t.
+    { apply/andP; split.
+      - by rewrite /has_arrived.
+      - by move: NCOMP; apply contra, completion_monotonic.
+    }
+    apply H_job_ready in PEND => //; destruct PEND as [jhp [ARRhp [READYhp _]]].
     move: IDLE => /eqP IDLE.
-    move: (H_work_conserving j t ARR) => NIDLE. 
+    move: (H_work_conserving _ t ARRhp) => 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. 
-      }  
+    { apply/andP; split; first by done.
+      by rewrite scheduled_at_def IDLE.
     }
     move: NIDLE => [j' SCHED].
     by rewrite scheduled_at_def IDLE in SCHED.
@@ -120,14 +130,13 @@ Section ExistsNoCarryIn.
   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 + Δ) <= Δ.
+  (** Assume that for some positive [Δ], the sum of requested workload
+      at time [t + Δ] is bounded by [Δ] (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,
@@ -162,8 +171,8 @@ Section ExistsNoCarryIn.
       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.
+        apply service_of_jobs_le_length_of_interval'; auto with basic_facts.
+        by eapply arrivals_uniq; eauto 2.
       Qed.
 
       (** Next we consider two cases: 
@@ -215,11 +224,11 @@ Section ExistsNoCarryIn.
         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
+                          _ 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.
+          feed_n 2 COMPL; auto with basic_facts.
           { 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.
@@ -238,8 +247,8 @@ Section ExistsNoCarryIn.
           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.
+        eapply workload_eq_service_impl_all_jobs_have_completed; eauto with basic_facts.
+        by eapply arrived_between_implies_in_arrivals.
       Qed.
 
     End ProcessorIsNotTooBusyInduction.
@@ -281,9 +290,9 @@ Section ExistsNoCarryIn.
   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 j ARR H_priority_is_reflexive (job_arrival j))
-      as [t1 [PREFIX GE]].
-    apply job_pending_at_arrival; auto. 
+                 arr_seq H_arrival_times_are_consistent
+                 sched j ARR H_priority_is_reflexive (job_arrival j))
+      as [t1 [PREFIX GE]]; first by 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.

analysis/facts/busy_interval/priority_inversion.v

@@ -9,11 +9,6 @@ Require Export prosa.analysis.facts.busy_interval.busy_interval.
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.
 
-(** Throughout the file we assume for the classic Liu & Layland model
-    of readiness without jitter and no self-suspensions, where
-    pending jobs are always ready. *)
-Require Import prosa.model.readiness.basic.
-
 (** In preparation of the derivation of the priority inversion bound, we
     establish two basic facts on preemption times. *)
 Section PreemptionTimes.
@@ -93,8 +88,8 @@ Section PriorityInversionIsBounded.
   (**  ... and any type of jobs associated with these tasks. *)
   Context {Job : JobType}.
   Context `{JobTask Job Task}.
-  Context `{JobArrival Job}.
-  Context `{JobCost Job}.
+  Context `{Arrival : JobArrival Job}.
+  Context `{Cost : JobCost Job}.
   
   (** Consider any arrival sequence with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
@@ -129,6 +124,10 @@ Section PriorityInversionIsBounded.
   Hypothesis H_valid_model_with_bounded_nonpreemptive_segments:
     valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
 
+  (** Further, allow for any work-bearing notion of job readiness. *)
+  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+  
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
   
@@ -221,29 +220,34 @@ Section PriorityInversionIsBounded.
           scheduled_at sched jhp t ->
           hep_job jhp j.
       Proof.
-        intros LTt2m1 jhp Sched_jhp.
-        move: (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]]. 
-        apply contraT; move => /negP NOTHP; exfalso. 
-        apply NOTQUIET with (t := t.+1).
+        intros LTt2m1 jlp Sched_jlp; apply contraT; move => /negP NOTHP; exfalso.
+        move: (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
+        apply NOTQUIET with (t := t.+1). 
         { apply/andP; split.
           - by apply leq_ltn_trans with t1.
           - rewrite -subn1 ltn_subRL addnC in LTt2m1.
-              by rewrite -[t.+1]addn1.
+            by rewrite -[t.+1]addn1.
+        }
+        intros j_hp ARR HP BEF.
+        apply contraT => NCOMP'; exfalso. 
+        have PEND : pending sched j_hp t.
+        { apply/andP; split.
+          - by rewrite /has_arrived.
+          - by move: NCOMP'; apply contra, completion_monotonic.
         }
-        intros j_hp' IN HP ARR.
-        apply contraT; move => /negP NOTCOMP'; exfalso.
-        have BACK: backlogged sched j_hp' t.
-        { apply/andP; split; last first.
-          { apply/negP; intro SCHED'.
-            move: (ideal_proc_model_is_a_uniprocessor_model jhp j_hp' sched t Sched_jhp SCHED') => EQ; subst.
-              by apply: NOTHP.
-          } 
-          apply/andP; split. unfold arrived_before, has_arrived in *. by done. 
-          apply/negP; intro COMP; apply NOTCOMP'.
-            by apply completion_monotonic with (t0 := t).
+        apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' HEP']]].
+        have HEP : hep_job j' j by apply (H_priority_is_transitive t j_hp). 
+        clear HEP' NCOMP' BEF HP ARR j_hp.
+        have BACK: backlogged sched j' t.
+        { apply/andP; split; first by done.
+          apply/negP; intro SCHED'.
+          move: (ideal_proc_model_is_a_uniprocessor_model jlp j' sched t Sched_jlp SCHED') => EQ.
+          by subst; apply: NOTHP.
         }
-        apply NOTHP, (H_priority_is_transitive t j_hp'); eauto 2.
+        apply NOTHP, (H_priority_is_transitive t j'); last by eapply HEP.
+        by eapply H_respects_policy; eauto .
       Qed.
+
       
       (** In case when [t = t2 - 1], we cannot use the same proof
           since [t+1 = t2], but [t2] is a quiet time. So we do a
@@ -254,43 +258,46 @@ Section PriorityInversionIsBounded.
           scheduled_at sched jhp t ->
           hep_job jhp j.
       Proof.
-        intros EQUALt2m1 jhp Sched_jhp.
-        move: (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]]. 
-        apply contraT; move => /negP NOTHP; exfalso. 
+        intros EQUALt2m1 jlp Sched_jlp; apply contraT; move => /negP NOTHP; exfalso.
+        move: (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
         rewrite leq_eqVlt in GEt; first move: GEt => /orP [/eqP EQUALt1 | LARGERt1].
-        - subst t; clear LEt.
-          rewrite -EQUALt1 in Sched_jhp; move: EQUALt1 => /eqP EQUALt1.
-          destruct (job_scheduled_at j t1) eqn:SCHEDj.
-          + apply NOTHP; erewrite (ideal_proc_model_is_a_uniprocessor_model j jhp); eauto.
-              by apply (H_priority_is_reflexive 0).
-          + eapply NOTHP, (H_respects_policy _ _ t2.-1); auto;
-              last by rewrite -(eqbool_to_eqprop EQUALt1).
-            apply/andP; split; last first.
-            * by rewrite -(eqbool_to_eqprop EQUALt1); unfold job_scheduled_at in *; rewrite SCHEDj.
-            * have EQ: t1 = job_arrival j.
-              { rewrite -eqSS in EQUALt1.
-                have EQ: t2 = t1.+1.
-                { rewrite prednK in EQUALt1; first by apply/eqP; rewrite eq_sym.
-                  apply negbNE; rewrite -eqn0Ngt; apply/neqP; intros EQ0.
-                  move: INBI; rewrite EQ0; move => /andP [_ CONTR].
-                    by rewrite ltn0 in CONTR.
-                } clear EQUALt1.
-                  by move: INBI; rewrite EQ ltnS -eqn_leq; move => /eqP INBI.
-              }
-                by rewrite -(eqbool_to_eqprop EQUALt1) EQ; eapply job_pending_at_arrival; eauto 2.                  
-        - feed (NOTQUIET t); first by apply/andP; split.
+        { subst t t1; clear LEt SL. 
+          have ARR : job_arrival j = t2.-1.
+          { apply/eqP; rewrite eq_sym eqn_leq. 
+            destruct t2; first by done.
+            rewrite ltnS -pred_Sn in INBI.
+            now rewrite -pred_Sn.
+          }
+          have PEND := job_pending_at_arrival sched _ H_job_cost_positive H_jobs_must_arrive_to_execute.
+          rewrite ARR in PEND.
+          apply H_job_ready in PEND => //; destruct PEND as [jhp [ARRhp [PENDhp HEPhp]]].
+          eapply NOTHP, (H_priority_is_transitive 0); last by apply HEPhp.
+          apply (H_respects_policy _ _ t2.-1); auto.
+          apply/andP; split; first by done.
+          apply/negP; intros SCHED.
+          move: (ideal_proc_model_is_a_uniprocessor_model _ _ sched _ SCHED Sched_jlp) => EQ.
+          by subst; apply: NOTHP.
+        }        
+        { feed (NOTQUIET t); first by apply/andP; split.
           apply NOTQUIET; intros j_hp' IN HP ARR.
-          apply contraT; move => /negP NOTCOMP'; exfalso.
-          have BACK: backlogged sched j_hp' t.
+          apply contraT => NOTCOMP'; exfalso.
+          have PEND : pending sched j_hp' t.
           { apply/andP; split.
-            - apply/andP; split. unfold arrived_before, has_arrived in *. by rewrite ltnW. 
-              apply/negP; intro COMP; apply NOTCOMP'.
-                by apply completion_monotonic with (t0 := t).
-            - apply/negP; intro SCHED'.
-              move: (ideal_proc_model_is_a_uniprocessor_model jhp j_hp' sched t Sched_jhp SCHED') => EQ; subst.
-                by apply: NOTHP.
-          } 
-          apply NOTHP, (H_priority_is_transitive t j_hp'); eauto 2.
+            - by rewrite /has_arrived ltnW.
+            - by move: NOTCOMP'; apply contra, completion_monotonic.
+          }          
+          apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' HEP']]].
+          have HEP : hep_job j' j by apply (H_priority_is_transitive t j_hp'). 
+          clear ARR HP IN HEP' NOTCOMP' j_hp'.
+          have BACK: backlogged sched j' t.
+          { apply/andP; split; first by done.
+            apply/negP; intro SCHED'.
+            move: (ideal_proc_model_is_a_uniprocessor_model jlp j' sched t Sched_jlp SCHED') => EQ.
+              by subst; apply: NOTHP.
+          }
+          apply NOTHP, (H_priority_is_transitive t j'); last by eapply HEP.
+          by eapply H_respects_policy; eauto .
+        }
       Qed.
 
       (** By combining the above facts we conclude that a job that is
@@ -410,8 +417,8 @@ Section PriorityInversionIsBounded.
       move: (H_respects_policy) => PRIO.              
       move => tp t PRPOINT /andP [GEtp LTtp] /andP [LEtp LTt].
       ideal_proc_model_sched_case_analysis_eq sched t jhp.
-      { exfalso; eapply not_quiet_implies_not_idle with (t0 := t); eauto 2.
-          by apply/andP; split; first apply leq_trans with tp. }
+      { apply instant_t_is_not_idle in Idle; first by done.
+        by apply/andP; split; first apply leq_trans with tp. } 
       exists jhp.
       have HP: hep_job jhp j.
       { intros.

analysis/facts/preemption/rtc_threshold/job_preemptable.v

@@ -13,7 +13,7 @@ Section RunToCompletionThreshold.
   Context `{JobCost Job}.
 
   (** In addition, we assume existence of a function
-      mapping jobs to theirs preemption points. *)
+      mapping jobs to their preemption points. *)
   Context `{JobPreemptable Job}.
 
   (** Consider any kind of processor state model, ... *)

analysis/facts/readiness/basic.v

@@ -67,3 +67,7 @@ Section LiuAndLaylandReadiness.
   Qed.
 
 End LiuAndLaylandReadiness.
+
+(** We add the above lemma into a "Hint Database" basic_facts, so Coq
+    will be able to apply it automatically. *)
+Global Hint Resolve basic_readiness_is_work_bearing_readiness : basic_facts.