automate lemma [unit_supply_is_unit_service]

analysis/abstract/restricted_supply/abstract_seq_rta.v

@@ -173,8 +173,7 @@ Section AbstractRTARestrictedSupplySequential.
       rewrite /intra_IBF addnC leq_add; first by done.
       { rewrite -(leq_add2r (cumul_task_interference arr_seq sched j t1 (t1 + Δ))).
         eapply leq_trans; first last.
-        { rewrite EQ; apply: task.cumulative_job_interference_bound => //.
-          by apply unit_supply_is_unit_service. }
+        { by rewrite EQ; apply: task.cumulative_job_interference_bound => //. }
         { rewrite -big_split //= leq_sum // /cond_interference  => t _.
           by case (interference j t), (has_supply sched t), (nonself arr_seq sched j t) => //. } }
       { rewrite (cumul_cond_interference_pred_eq _ (nonself_intra arr_seq sched)) => //.

analysis/abstract/restricted_supply/bounded_bi/aux.v

@@ -102,8 +102,7 @@ Section BoundedBusyIntervalsAux.
     move_neq_up LE.
     have EQ: workload_of_hep_jobs arr_seq j t1 t = service_of_hep_jobs arr_seq sched j t1 t.
     { apply/eqP; rewrite eqn_leq; apply/andP; split => //.
-      apply service_of_jobs_le_workload => //.
-      by apply unit_supply_is_unit_service.
+      by apply service_of_jobs_le_workload => //.
     }
     clear LE; move: PREF => [LT [QT1 [NQT QT2]]].
     specialize (NQT t ltac:(lia)); apply: NQT => s ARR HEP BF.
@@ -122,13 +121,12 @@ Section BoundedBusyIntervalsAux.
         { by apply: in_arrivals_implies_arrived_before. }
       }
       rewrite addn0; apply/eqP.
-      apply all_jobs_have_completed_impl_workload_eq_service => //; first by apply unit_supply_is_unit_service.
+      apply all_jobs_have_completed_impl_workload_eq_service => //.
       move => h ARRh HEPh; apply: QT1 => //.
       - by apply: in_arrivals_implies_arrived.
       - by apply: in_arrivals_implies_arrived_before.
     }
-    apply: workload_eq_service_impl_all_jobs_have_completed => //.
-    by apply unit_supply_is_unit_service.
+    by apply: workload_eq_service_impl_all_jobs_have_completed => //.
   Qed.
 
   (** Consider a subinterval <<[t1, t1 + Δ)>> of the interval <<[t1,
@@ -156,10 +154,7 @@ Section BoundedBusyIntervalsAux.
       }
     }
     rewrite cumulative_interfering_workload_split // cumulative_interference_split //.
-    rewrite cumulative_iw_hep_eq_workload_of_ohep cumulative_i_ohep_eq_service_of_ohep //;
-            [
-            | exact: unit_supply_is_unit_service
-            | by apply PREF ].
+    rewrite cumulative_iw_hep_eq_workload_of_ohep cumulative_i_ohep_eq_service_of_ohep //; last by apply PREF.
     rewrite -[leqRHS]addnC -[leqRHS]addnA [(_ + workload_of_job _ _ _ _ )]addnC.
     rewrite workload_job_and_ahep_eq_workload_hep //.
     rewrite -addnC -addnA [(_ + service_during _ _ _ _ )]addnC.

analysis/abstract/restricted_supply/bounded_bi/edf.v

@@ -325,7 +325,6 @@ Section BoundedBusyIntervals.
           by apply instantiated_busy_interval_equivalent_busy_interval.
         }
         eapply busy_interval.busy_interval_is_bounded; eauto 2 => //.
-        - by apply unit_supply_is_unit_service.
         - by eapply instantiated_i_and_w_no_speculative_execution; eauto 2 => //.
         - by eapply instantiated_i_and_w_are_coherent_with_schedule; eauto 2 => //.
         - by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.

analysis/abstract/restricted_supply/bounded_bi/fp.v

@@ -185,7 +185,6 @@ Section BoundedBusyIntervals.
           by apply instantiated_busy_interval_equivalent_busy_interval.
         }
         eapply busy_interval.busy_interval_is_bounded; eauto 2 => //.
-        - by apply unit_supply_is_unit_service.
         - by eapply instantiated_i_and_w_no_speculative_execution; eauto 2 => //.
         - by eapply instantiated_i_and_w_are_coherent_with_schedule; eauto 2 => //.
         - by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.

analysis/abstract/restricted_supply/bounded_bi/jlfp.v

@@ -198,7 +198,6 @@ Section BoundedBusyIntervals.
           by apply instantiated_busy_interval_equivalent_busy_interval.
         }
         eapply busy_interval.busy_interval_is_bounded; eauto 2 => //.
-        - by apply unit_supply_is_unit_service.
         - by eapply instantiated_i_and_w_no_speculative_execution; eauto 2 => //.
         - by eapply instantiated_i_and_w_are_coherent_with_schedule; eauto 2 => //.
         - by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.

analysis/abstract/restricted_supply/iw_instantiation.v

@@ -288,11 +288,9 @@ Section JLFPInstantiation.
         { rewrite negb_and negbK; apply/orP.
           by case ARR: (arrived_before j t); [right | left]; [apply QT | ]. }
         { erewrite cumulative_interference_split, cumulative_interfering_workload_split; rewrite eqn_add2l.
-          rewrite cumulative_i_ohep_eq_service_of_ohep //=; last first.
-          { exact: unit_supply_is_unit_service. }
+          rewrite cumulative_i_ohep_eq_service_of_ohep //.
           rewrite //= cumulative_iw_hep_eq_workload_of_ohep eq_sym; apply/eqP.
           apply all_jobs_have_completed_equiv_workload_eq_service => //.
-          { by apply unit_supply_is_unit_service. }
           move => j0 IN HEP; apply QT.
           - by apply in_arrivals_implies_arrived in IN.
           - by move: HEP => /andP [HEP HP].
@@ -310,12 +308,10 @@ Section JLFPInstantiation.
         move => t /andP [T0 T1] 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) => //.
-        { by apply unit_supply_is_unit_service. }
         erewrite service_of_jobs_case_on_pred with (P2 := fun j' => j' != j).
         erewrite workload_of_jobs_case_on_pred with (P' := fun j' => j' != j) => //.
         replace ((fun j0 : Job => hep_job j0 j && (j0 != j))) with (another_hep_job^~j); last by rewrite /another_hep_job.
-        rewrite -/(service_of_other_hep_jobs arr_seq sched j 0 t) -cumulative_i_ohep_eq_service_of_ohep //; last first.
-        { exact: unit_supply_is_unit_service. }
+        rewrite -/(service_of_other_hep_jobs arr_seq sched j 0 t) -cumulative_i_ohep_eq_service_of_ohep //.
         rewrite -/(workload_of_other_hep_jobs arr_seq j 0 t) -cumulative_iw_hep_eq_workload_of_ohep //.
         move: T1; rewrite negb_and => /orP [NA | /negPn COMP].
         { have PRED__eq: {in arrivals_between arr_seq 0 t, (fun j__copy : Job => hep_job j__copy j && ~~ (j__copy != j)) =1 pred0}.
@@ -340,7 +336,6 @@ Section JLFPInstantiation.
           rewrite EQ; clear EQ; apply/eqP; rewrite eqn_add2l.
           apply/eqP; eapply all_jobs_have_completed_equiv_workload_eq_service with
             (P := eq_op j) (t1 := 0) (t2 := t) => //.
-          { by apply unit_supply_is_unit_service. }
           { by move => j__copy _ /eqP EQ; subst j__copy. }
         }
       Qed.
@@ -526,7 +521,6 @@ Section JLFPInstantiation.
       move => j t1 t2 ARR /eqP TSK POS BUSY.
       eapply instantiated_busy_interval_equivalent_busy_interval in BUSY => //.
       eapply all_jobs_have_completed_equiv_workload_eq_service => //.
-      { by apply unit_supply_is_unit_service. }
       move => s INs /eqP TSKs.
       move: (INs) => NEQ.
       eapply in_arrivals_implies_arrived_between in NEQ => //.
@@ -544,11 +538,9 @@ Section JLFPInstantiation.
     Proof.
       move=> j t1.
       rewrite cumulative_interference_split cumulative_interfering_workload_split.
-      rewrite leq_add2l cumulative_i_ohep_eq_service_of_ohep //=; last first.
-      { exact: unit_supply_is_unit_service. }
+      rewrite leq_add2l cumulative_i_ohep_eq_service_of_ohep //=.
       rewrite cumulative_iw_hep_eq_workload_of_ohep.
-      apply service_of_jobs_le_workload => //.
-      by apply unit_supply_is_unit_service.
+      by apply service_of_jobs_le_workload => //.
     Qed.
 
   End I_IW_correctness.

analysis/abstract/restricted_supply/task_intra_interference_bound.v

@@ -110,10 +110,9 @@ Section TaskIntraInterferenceIsBounded.
       by rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + Δ)) //= leq_addr. }
     { erewrite cumulative_i_thep_eq_service_of_othep; eauto 2 => //; last first.
       { by apply instantiated_quiet_time_equivalent_quiet_time => //; apply BUSY. }
-      { exact: unit_supply_is_unit_service. }
       apply: leq_trans.
       { by apply service_of_jobs_le_workload => //; apply unit_supply_is_unit_service. }
-      { apply H_workload_is_bounded => //; apply: abstract_busy_interval_classic_quiet_time => //. }
+      { by apply H_workload_is_bounded => //; apply: abstract_busy_interval_classic_quiet_time => //. }
     }
   Qed.
 

analysis/facts/priority/fifo_ahep_bound.v

@@ -89,10 +89,7 @@ Section RTAforFullyPreemptiveFIFOModelwithArrivalCurves.
     move: (H_busy_window) => [[_ [_ [_ /andP [ARR1 ARR2]]]] _].
     rewrite (cumulative_i_ohep_eq_service_of_ohep _ arr_seq) => //; last  eauto 6 with basic_rt_facts; last first.
     { by move: (H_busy_window) => [[_ [Q _]] _]. }
-    { exact: unit_supply_is_unit_service. }
-    eapply leq_trans.
-    { apply service_of_jobs_le_workload => //.
-      by apply unit_supply_is_unit_service. }
+    eapply leq_trans; first by apply service_of_jobs_le_workload => //.
     rewrite (leqRW (workload_equal_subset _ _ _ _ _ _  _)) => //.
     rewrite (workload_minus_job_cost j)//;
             last by apply job_in_arrivals_between => //; last by rewrite addn1.

model/processor/platform_properties.v

@@ -58,3 +58,10 @@ Section ProcessorModels.
       scheduled_at s j t -> service_at s j t = supply_at s t.
 
 End ProcessorModels.
+
+(** We add the reduction from [unit_supply_proc_model] to
+    [unit_service_proc_model] into the "Hint Database" basic_rt_facts,
+    so Coq will be able to apply it automatically where needed. *)
+Global Hint Resolve
+       unit_supply_is_unit_service
+  : basic_rt_facts.