improve theorem statements

rt/analysis/axiomatic_pWCET_full.v

@@ -96,6 +96,14 @@ Section MainLemma.
       with (S := initial_system).
   Qed.
 
+  (** In other words, the transformation is pRT-monotone. *)
+  Corollary probabilistic_rt_monotonicity_of_iid_pWCET' :
+    probabilistic_response_time_monotone_transformation
+      horizon sched1 sched2.
+  Proof.
+    by intros ?; apply probabilistic_rt_monotonicity_of_iid_pWCET.
+  Qed.
+
 End MainLemma.
 
 Print Assumptions probabilistic_rt_monotonicity_of_iid_pWCET.

rt/analysis/axiomatic_pWCET_step.v

@@ -1334,11 +1334,7 @@ Section ProofOfTheorem1.
   Variable ζ : @scheduler𝗔𝗖 Job.
   Hypothesis H_rt_monotonic : rt_monotonic_scheduler horizon ζ.
 
-  (** For simplicity, let [𝓡] denote a function that maps [𝗔] and [𝗖]
-      to a function that computes the response time of any job ... *)
-  Let 𝓡 := scheduler𝗔𝗖_to_rt𝗔𝗖 horizon ζ.
-
-  (** ... and let [sched] denote a schedule generated by [ζ]. *)
+  (** Let [sched] denote a schedule generated by [ζ]. *)
   Let sched S := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).
 
   (** Let [S] be an arbitrary system ... *)
@@ -1351,20 +1347,25 @@ Section ProofOfTheorem1.
       corresponding pWCET via [replace_job_pET]. *)
   Let S' := replace_job_pET j_rep S.
 
-  (** Assuming that the pWCET satisfies our notion of axiomatic pWCET, ... *)
+  (** Consider an arbitrary job [j] ... *)
+  Variable j : Job.
+
+  (** ... and its response times [𝓡j] and [𝓡j'] in schedules [sched S]
+      and [sched S'], respectively. *)
+  Let 𝓡j := response_time (sched S) (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) horizon j.
+  Let 𝓡j' := response_time (sched S') (job_arrival := 𝓐_of S') (job_cost := 𝓒_of S') horizon j.
+
+  (** If pWCET satisfies our notion of axiomatic pWCET, ... *)
   Hypothesis H_axiomatic_pWCET :
     axiomatic_pWCET (μ_of S) (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).
 
-  (** ... then the response-time distribution of any job [j] in
-      schedule [sched S] is [⪯]-bounded by the response-time distribution
-      of job [j] in schedule [sched S']. *)
+  (** ... then the response-time distribution of job [j] in schedule
+      [sched S] is [⪯]-bounded by the response-time distribution of
+      job [j] in schedule [sched S']. That is, [𝓡j ⪯ 𝓡j']. *)
   Lemma prob_rt_monotonic_axiomatic_pWCET_replace_pET :
-    probabilistic_response_time_monotone_transformation
-      horizon
-      (sched S) (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S)
-      (sched S') (job_arrival_s := 𝓐_of S') (job_cost_s := 𝓒_of S').
+    𝓡j ⪯ 𝓡j'.
   Proof.
-    intros  js t.
+    intros t.
     destruct S as [Ω μ arrs costs]. clear S.
     set (S := {| Ω_of := Ω; μ_of := μ; 𝓐_of := arrs; 𝓒_of := costs |}) in *.
     set (ξ__part := @partition_on_ξ _ μ _ arrs).
@@ -1375,7 +1376,7 @@ Section ProofOfTheorem1.
     have HH := transformation_is_pRT_monotone_step2 horizon ζ _ _ _ _ _ _ _ _ ξi ξi' ξEQU.
     specialize (HH H_axiomatic_pWCET).
     destruct ξi as [ξ IN].
-    specialize (HH js t ξ).
+    specialize (HH j t ξ).
     apply: HH => //= => POSξ; clear ξi' ξEQU.
     apply transformation_is_pRT_monotone_step3 => //.
     intros.