change [job_task j = tsk] to [job_of_task tsk j]

There are quite a few places where hypotheses about the task of a job are simply stated as equality (even though a proper predicate exists). This patch replaces the equalities with the predicate.

analysis/abstract/abstract_rta.v

@@ -117,7 +117,7 @@ Section Abstract_RTA.
     (** Consider any job j of [tsk] with positive cost. *)
     Variable j: Job. 
     Hypothesis H_j_arrives: arrives_in arr_seq j.
-    Hypothesis H_job_of_tsk: job_task j = tsk.
+    Hypothesis H_job_of_tsk: job_of_task tsk j. 
     Hypothesis H_job_cost_positive: job_cost_positive j.
     
     (** Assume we have a busy interval <<[t1, t2)>> of job j that is bounded by L. *)
@@ -413,7 +413,7 @@ Section Abstract_RTA.
               rewrite addnBA; last by apply PRT1.
               rewrite addnBAC; last by done.
               rewrite leq_sub2r // leq_add2l.
-                by rewrite -H_job_of_tsk; apply H_valid_job_cost.
+              by move: H_job_of_tsk => /eqP <-; apply H_valid_job_cost.
             }
           Qed.
           

analysis/abstract/abstract_seq_rta.v

@@ -94,7 +94,7 @@ Section Sequential_Abstract_RTA.
     Definition interference_and_workload_consistent_with_sequential_tasks :=
       forall (j : Job) (t1 t2 : instant),
           arrives_in arr_seq j ->
-          job_task j = tsk ->
+          job_of_task tsk j ->
           job_cost j > 0 ->
           busy_interval j t1 t2 ->
           task_workload_between 0 t1 = task_service_of_jobs_in (arrivals_between 0 t1) 0 t1.
@@ -134,7 +134,7 @@ Section Sequential_Abstract_RTA.
                (task_interference_bound_function : Task -> duration -> duration -> duration) :=
       forall j R t1 t2,
         arrives_in arr_seq j ->
-        job_task j = tsk ->
+        job_of_task tsk j ->
         t1 + R < t2 ->
         ~~ completed_by sched j (t1 + R) ->
         busy_interval j t1 t2 ->
@@ -216,8 +216,8 @@ Section Sequential_Abstract_RTA.
       Variable j1 j2 : Job.
       Hypothesis H_j1_arrives: arrives_in arr_seq j1.
       Hypothesis H_j2_arrives: arrives_in arr_seq j2.
-      Hypothesis H_j1_from_tsk: job_task j1 = tsk.
-      Hypothesis H_j2_from_tsk: job_task j2 = tsk.
+      Hypothesis H_j1_from_tsk: job_of_task tsk j1.
+      Hypothesis H_j2_from_tsk: job_of_task tsk j2.
       Hypothesis H_j1_cost_positive: job_cost_positive j1.
 
       (** Consider the busy interval <<[t1, t2)>> of job j1. *)
@@ -273,7 +273,7 @@ Section Sequential_Abstract_RTA.
       (** Consider any job [j] of [tsk]. *)
       Variable j : Job.
       Hypothesis H_j_arrives : arrives_in arr_seq j.
-      Hypothesis H_job_of_tsk : job_task j = tsk.
+      Hypothesis H_job_of_tsk : job_of_task tsk j.
       Hypothesis H_job_cost_positive : job_cost_positive j.
 
       (** Consider the busy interval <<[t1, t2)>> of job j. *)
@@ -333,9 +333,8 @@ Section Sequential_Abstract_RTA.
               case INT: (interference j t); last by done.
               simpl; rewrite lt0b.
               apply/hasP; exists j; last by done.
-              rewrite mem_filter; apply/andP; split.
-              - by rewrite H_job_of_tsk.
-              - by apply arrived_between_implies_in_arrivals.
+              rewrite mem_filter; apply/andP; split; first by done.
+              by apply arrived_between_implies_in_arrivals.
             Qed.
 
           End Case1.
@@ -345,7 +344,7 @@ Section Sequential_Abstract_RTA.
             (** Assume a job [j'] from another task is scheduled at time [t]. *)
             Variable j' : Job.
             Hypothesis H_sched :  sched t = Some j'.
-            Hypothesis H_not_job_of_tsk : job_task j' != tsk.
+            Hypothesis H_not_job_of_tsk : ~~ job_of_task tsk j'. 
 
             (** If a job [j]' from another task is scheduled at time [t],
                then [interference j t = 1, scheduled_at j t = 0]. But
@@ -365,19 +364,18 @@ Section Sequential_Abstract_RTA.
               rewrite H_sched H_not_job_of_tsk; simpl.
               have ->: Some j' == Some j = false; last rewrite addn0.
               { apply/negP => /eqP CONTR; inversion CONTR; subst j'.
-                by move: (H_job_of_tsk) (H_not_job_of_tsk) => -> => /eqP NEQ; apply: NEQ. }
+                by move: (H_not_job_of_tsk); rewrite H_job_of_tsk. } 
               have ZERO: \sum_(i <- arrivals_between t1 (t1 + A + ε) | job_task i == tsk) (Some j' == Some i) = 0.
-              { apply big1; move => j2 /eqP TSK2; apply/eqP; rewrite eqb0.
-                apply/negP => /eqP EQ; inversion EQ; subst j'.
-                by move: TSK2 H_not_job_of_tsk => -> /negP.
+              { apply big1 => j2 TSK.
+                apply/eqP; rewrite eqb0; apply/negP => /eqP EQ; inversion EQ; subst j'.                
+                by move: (H_not_job_of_tsk); rewrite / job_of_task TSK.
               }
               rewrite ZERO ?addn0 add0n; simpl; clear ZERO.
               case INT: (interference j t); last by done.
               simpl; rewrite lt0b.
               apply/hasP; exists j; last by done.
-              rewrite  mem_filter; apply/andP; split.
-              - by rewrite H_job_of_tsk.
-              - by eapply arrived_between_implies_in_arrivals.
+              rewrite  mem_filter; apply/andP; split; first by done.
+              by eapply arrived_between_implies_in_arrivals.
             Qed.
 
           End Case2.
@@ -387,7 +385,7 @@ Section Sequential_Abstract_RTA.
             (** Assume a job [j'] (different from j) of task [tsk] is scheduled at time [t]. *)
             Variable j' : Job.
             Hypothesis H_sched :  sched t = Some j'.
-            Hypothesis H_not_job_of_tsk : job_task j' == tsk.
+            Hypothesis H_not_job_of_tsk : job_of_task tsk j'. 
             Hypothesis H_j_neq_j' : j != j'.
 
             (** If a job [j'] (different from [j]) of task [tsk] is scheduled at time [t], then
@@ -405,7 +403,7 @@ Section Sequential_Abstract_RTA.
                       /task_scheduled_at /task_schedule.task_scheduled_at /service_of_jobs_at
                       /service_of_jobs.service_of_jobs_at scheduled_at_def/=.
               have ARRs: arrives_in arr_seq j'; first by apply H_jobs_come_from_arrival_sequence with t; rewrite scheduled_at_def; apply/eqP.
-              rewrite H_sched H_not_job_of_tsk addn0; simpl.
+              move: (H_not_job_of_tsk) => /eqP; rewrite H_sched => ->; rewrite eq_refl addn0; simpl.
               have ->: Some j' == Some j = false by
                   apply/negP => /eqP EQ; inversion EQ; subst j'; move:H_j_neq_j' => /negP NEQ; apply: NEQ.
               replace (interference j t) with true; last first.
@@ -420,7 +418,6 @@ Section Sequential_Abstract_RTA.
               { by move: H_not_job_of_tsk => /eqP TSK; rewrite /job_of_task TSK eq_refl eq_refl. }
               { intros. have ARR:= arrives_after_beginning_of_busy_interval j j' _ _ _ _ _ t1 t2 _ t.
                 feed_n 8 ARR; try (done || by move: H_t_in_interval => /andP [T1 T2]).
-                { by move: H_not_job_of_tsk => /eqP TSK; rewrite TSK. }
                 { move: H_sched => /eqP SCHEDt.
                   apply scheduled_implies_pending;
                     auto using ideal_proc_model_ensures_ideal_progress.
@@ -433,7 +430,7 @@ Section Sequential_Abstract_RTA.
                   apply negbT in ARRNEQ; rewrite -ltnNge in ARRNEQ.
                   move: (H_sequential_tasks j j' t) => CONTR.
                   feed_n 5 CONTR; try done.
-                  { by rewrite /same_task eq_sym H_job_of_tsk. }
+                  { by rewrite /same_task eq_sym; move: (H_job_of_tsk) => /eqP ->. } 
                   { by move: H_sched => /eqP SCHEDt; rewrite scheduled_at_def. }
                   move: H_job_j_is_not_completed => /negP T; apply: T.
                   apply completion_monotonic with t; try done.
@@ -463,7 +460,7 @@ Section Sequential_Abstract_RTA.
                       /Sequential_Abstract_RTA.cumul_task_interference /task_interference_received_before
                       /task_scheduled_at /task_schedule.task_scheduled_at /service_of_jobs_at
                       /service_of_jobs.service_of_jobs_at scheduled_at_def.
-              rewrite H_sched H_job_of_tsk !eq_refl addn0 //=.
+              rewrite H_sched; move: H_job_of_tsk => /eqP ->; rewrite eq_refl eq_refl addn0 //=.
               move: (H_work_conserving j _ _ t H_j_arrives H_job_of_tsk H_job_cost_positive H_busy_interval) => WORK.
               feed WORK.
               { move: H_t_in_interval => /andP [NEQ1 NEQ2].
@@ -472,7 +469,9 @@ Section Sequential_Abstract_RTA.
               feed ZIJT; first by rewrite scheduled_at_def H_sched; simpl.
               move: ZIJT => /negP /eqP; rewrite eqb_negLR; simpl; move => /eqP ZIJT; rewrite ZIJT; simpl; rewrite add0n.
               rewrite big_mkcond //=; apply/sum_seq_gt0P.
-              by exists j; split; [apply j_is_in_arrivals_between | rewrite /job_of_task H_job_of_tsk H_sched !eq_refl].
+              exists j; split.
+              - by apply j_is_in_arrivals_between.
+              - by move: (H_job_of_tsk) => ->; rewrite H_sched !eq_refl.
             Qed.
 
           End Case4.
@@ -518,7 +517,7 @@ Section Sequential_Abstract_RTA.
           rewrite -(leq_add2r (\sum_(t1 <= t < (t1 + x)) service_at sched j t)).
           rewrite [X in _ <= X]addnC addnA subnKC; last first.
           { rewrite exchange_big //= (big_rem j) //=; auto using j_is_in_arrivals_between.
-            by rewrite /job_of_task H_job_of_tsk eq_refl leq_addr. }
+            by rewrite H_job_of_tsk leq_addr. }
           rewrite -big_split -big_split //=.
           rewrite big_nat_cond [X in _ <= X]big_nat_cond leq_sum //; move => t /andP [NEQ _].
           rewrite -scheduled_at_def.
@@ -540,10 +539,9 @@ Section Sequential_Abstract_RTA.
           }
           rewrite leq_add2r.
           rewrite /task_workload /task_service_of_jobs_in
-                  /service_of_jobs.task_service_of_jobs_in/service_of_jobs /workload_of_jobs /job_of_task.
+                  /service_of_jobs.task_service_of_jobs_in/service_of_jobs /workload_of_jobs.
           rewrite (big_rem j) ?[X in _ <= X - _](big_rem j) //=; auto using j_is_in_arrivals_between.
-          rewrite /job_of_task  H_job_of_tsk eq_refl.
-          rewrite addnC -addnBA; last by done.
+          rewrite  H_job_of_tsk addnC -addnBA; last by done.
           rewrite [X in _ <= X - _]addnC -addnBA; last by done.
           rewrite !subnn !addn0.
           by apply service_of_jobs_le_workload; auto using ideal_proc_model_provides_unit_service.
@@ -597,16 +595,15 @@ Section Sequential_Abstract_RTA.
         { by apply workload_of_jobs_cat; apply/andP; split; rewrite leq_addr. } rewrite Step1; clear Step1.
         rewrite -!addnBA; first last.
         { by rewrite /task_workload_between /workload.task_workload_between /task_workload
-             /workload_of_jobs /job_of_task (big_rem j) //=  TSK eq_refl leq_addr. }
+             /workload_of_jobs (big_rem j) //= TSK leq_addr. }
         { apply leq_trans with (task_cost tsk); first by done.
           by rewrite -{1}[task_cost tsk]muln1 leq_mul2l; apply/orP; right. }
         rewrite leq_add; [by done | by eapply task_workload_le_num_of_arrivals_times_cost; eauto | ].
         rewrite /task_workload_between /workload.task_workload_between /task_workload /workload_of_jobs
                 /arrival_sequence.arrivals_between /number_of_task_arrivals /task_arrivals_between
-                /arrival_sequence.arrivals_between /job_of_task.
+                /arrival_sequence.arrivals_between.
         rewrite {1}addn1 big_nat1 addn1 big_nat1.
-        rewrite (big_rem j) //= TSK !eq_refl; simpl.
-        rewrite addnC -addnBA // subnn addn0.
+        rewrite (big_rem j) //= TSK //= addnC -addnBA // subnn addn0.
         rewrite (filter_size_rem j); [ | by done | by rewrite TSK].
         rewrite mulnDr mulnC muln1 -addnBA // subnn addn0 mulnC.
         apply sum_majorant_constant.
@@ -640,7 +637,7 @@ Section Sequential_Abstract_RTA.
       (** Consider any job [j] of [tsk]. *)
       Variable j : Job.
       Hypothesis H_j_arrives : arrives_in arr_seq j.
-      Hypothesis H_job_of_tsk : job_task j = tsk.
+      Hypothesis H_job_of_tsk : job_of_task tsk j.
 
       (** For simplicity, let's define a local name for the search space. *)
       Let is_in_search_space A :=

analysis/abstract/definitions.v

@@ -169,7 +169,7 @@ Section AbstractRTADefinitions.
       Definition work_conserving :=
         forall j t1 t2 t,
           arrives_in arr_seq j ->
-          job_task j = tsk ->
+          job_of_task tsk j ->
           job_cost j > 0 ->
           busy_interval j t1 t2 ->
           t1 <= t < t2 ->
@@ -183,7 +183,7 @@ Section AbstractRTADefinitions.
       Definition busy_intervals_are_bounded_by L :=
         forall j,
           arrives_in arr_seq j ->
-          job_task j = tsk ->
+          job_of_task tsk j ->
           job_cost j > 0 -> 
           exists t1 t2,
             t1 <= job_arrival j < t2 /\
@@ -204,7 +204,7 @@ Section AbstractRTADefinitions.
         forall t1 t2 delta j,
           (** First, we require [j] to be a job of task [tsk]. *)
           arrives_in arr_seq j ->
-          job_task j = tsk ->
+          job_of_task tsk j ->
           (** Next, we require the IBF to bound the interference only within the interval <<[t1, t1 + delta)>>. *)
           busy_interval j t1 t2 ->
           t1 + delta < t2 ->

analysis/abstract/ideal_jlfp_rta.v

@@ -220,7 +220,7 @@ Section JLFPInstantiation.
     Lemma cumulative_task_interference_split: 
       forall j t1 t2 upp_t,
         arrives_in arr_seq j -> 
-        job_task j = tsk ->
+        job_of_task tsk j ->
         j \in arrivals_before arr_seq upp_t ->
         ~~ job_completed_by j t2 ->
         cumulative_task_interference interference tsk upp_t t1 t2 = 
@@ -228,7 +228,7 @@ Section JLFPInstantiation.
         cumulative_interference_from_hep_jobs_from_other_tasks j t1 t2.
     Proof.
       rewrite /cumulative_task_interference /cumul_task_interference.
-      intros j t1 R upp ARRin TSK ARR NCOMPL.
+      intros j t1 R upp ARRin TSK ARR NCOMPL; move: TSK => /eqP TSK.
       rewrite -big_split //= big_nat_cond [X in _ = X]big_nat_cond. 
       apply/eqP; rewrite eqn_leq; apply/andP; split.
       all: rewrite /interference /is_priority_inversion /priority_inversion.is_priority_inversion.
@@ -261,7 +261,7 @@ Section JLFPInstantiation.
           have Fact: forall b, ~~ b + b = true; first by intros b; destruct b.
           rewrite Bool.andb_true_r Fact; simpl; rewrite lt0b; clear Fact.
           apply/hasP; exists j.
-          * rewrite mem_filter; apply/andP; split; first by done.
+          * rewrite mem_filter; apply/andP; split; first by rewrite TSK; apply/eqP.
               by eapply arrivals_between_sub with (t2 := 0) (t3 := upp); eauto 2.
           * destruct (hep_job s j) eqn:HP; apply/orP; [right|left]; last by done.
               by rewrite /is_interference_from_another_hep_job EQ
@@ -432,7 +432,7 @@ Section JLFPInstantiation.
         (** Consider any job j of [tsk]. *)
         Variable j : Job.
         Hypothesis H_j_arrives : arrives_in arr_seq j.
-        Hypothesis H_job_of_tsk : job_task j = tsk.
+        Hypothesis H_job_of_tsk : job_of_task tsk j.
         Hypothesis H_job_cost_positive : job_cost_positive j.
 
         (** To show the equivalence of the notions of busy intervals

analysis/abstract/run_to_completion.v

@@ -62,7 +62,7 @@ Section AbstractRTARunToCompletionThreshold.
   (** Let [j] be any job of task [tsk] with positive cost. *)
   Variable j : Job.
   Hypothesis H_j_arrives : arrives_in arr_seq j.
-  Hypothesis H_job_of_tsk : job_task j = tsk.
+  Hypothesis H_job_of_tsk : job_of_task tsk j.
   Hypothesis H_job_cost_positive : job_cost_positive j.
 
   (** Next, consider any busy interval <<[t1, t2)>> of job [j]. *)

analysis/definitions/priority_inversion.v

@@ -73,7 +73,7 @@ Section CumulativePriorityInversion.
     Definition priority_inversion_is_bounded_by (B : duration) :=
       forall (j : Job),
         arrives_in arr_seq j ->
-        job_task j = tsk ->
+        job_of_task tsk j ->
         job_cost j > 0 -> 
         priority_inversion_of_job_is_bounded_by j B.
 

analysis/definitions/schedulability.v

@@ -38,14 +38,14 @@ Section Task.
   Definition task_response_time_bound :=
     forall j,
       arrives_in arr_seq j ->
-      job_task j = tsk ->
+      job_of_task tsk j ->
       job_response_time_bound sched j R.
 
   (** We say that a task is schedulable if all its jobs meet their deadline *)
   Definition schedulable_task :=
     forall j,
       arrives_in arr_seq j ->
-      job_task j = tsk ->
+      job_of_task tsk j ->
       job_meets_deadline sched j.
   
 End Task.
@@ -94,8 +94,9 @@ Section Schedulability.
     rewrite /job_meets_deadline.
     apply completion_monotonic with (t := job_arrival j + R);
       [ | by apply H_response_time_bounded].
-    rewrite /job_deadline leq_add2l JOBtsk.
-      by erewrite leq_trans; eauto.
+    rewrite /job_deadline leq_add2l.
+    move: JOBtsk => /eqP ->.
+    by erewrite leq_trans; eauto.
   Qed.
 
 End Schedulability.

analysis/facts/model/rbf.v

@@ -136,7 +136,7 @@ Section ProofWorkloadBound.
     (** Next, we consider any job [j] of [tsk]. *)
     Variable j : Job.
     Hypothesis H_j_arrives : arrives_in arr_seq j.
-    Hypothesis H_job_of_tsk : job_task j = tsk.
+    Hypothesis H_job_of_tsk : job_of_task tsk j.
     
     (** We say that two jobs [j1] and [j2] are in relation
       [other_higher_eq_priority], iff [j1] has higher or equal priority than [j2] and
@@ -162,8 +162,9 @@ Section ProofWorkloadBound.
       set l := arrivals_between arr_seq t (t + Δ).
       apply (@leq_trans (\sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk))
                           (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0))).
-      { rewrite /total_ohep_workload /workload_of_jobs /other_higher_eq_priority.
-        rewrite /jlfp_higher_eq_priority /FP_to_JLFP /same_task H_job_of_tsk.
+      { move: (H_job_of_tsk) => /eqP TSK.
+        rewrite /total_ohep_workload /workload_of_jobs /other_higher_eq_priority.
+        rewrite /jlfp_higher_eq_priority /FP_to_JLFP /same_task TSK.
         set P := fun x => hep_task (job_task x) tsk && (job_task x != tsk).
         rewrite (exchange_big_dep P) //=; last by rewrite /P; move => ???/eqP->.
         rewrite /P /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
@@ -190,7 +191,8 @@ Section ProofWorkloadBound.
       set l := arrivals_between arr_seq t (t + Δ).
       apply(@leq_trans (\sum_(tsk' <- ts | hep_task tsk' tsk)
                          (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0))).
-      { rewrite /total_hep_workload /jlfp_higher_eq_priority /FP_to_JLFP H_job_of_tsk.
+      { move: (H_job_of_tsk) => /eqP TSK.
+        rewrite /total_hep_workload /jlfp_higher_eq_priority /FP_to_JLFP TSK.
         have EXCHANGE := exchange_big_dep (fun x => hep_task (job_task x) tsk).
         rewrite EXCHANGE /=; clear EXCHANGE; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
         rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
@@ -268,7 +270,7 @@ Section RequestBoundFunctions.
       job of task [tsk]. *)
   Variable j : Job.
   Hypothesis H_j_arrives : arrives_in arr_seq j.
-  Hypothesis H_job_of_tsk : job_task j = tsk.
+  Hypothesis H_job_of_tsk : job_of_task tsk j.
 
   (** Then we prove that [task_rbf] at [ε] is greater than or equal to task cost. *)
   Lemma task_rbf_1_ge_task_cost:
@@ -288,7 +290,7 @@ Section RequestBoundFunctions.
     apply/hasP; exists j; last by done.
     rewrite /arrivals_between addn1 big_nat_recl; last by done.
     rewrite big_geq ?cats0 //= mem_filter.
-    apply/andP; split; first by apply/eqP.
+    apply/andP; split; first by done.
     move: H_j_arrives => [t ARR]; move: (ARR) => CONS.
     apply H_arrival_times_are_consistent in CONS.
     by rewrite CONS.

analysis/facts/preemption/rtc_threshold/floating.v

@@ -36,7 +36,7 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions.
     - by rewrite /task_rtc_bounded_by_cost.
     - intros j ARR TSK.
       apply leq_trans with (job_cost j); eauto 2 with basic_facts.
-        by rewrite-TSK; apply H_valid_job_cost.
+      by move: TSK => /eqP <-; apply H_valid_job_cost.
   Qed.
   
 End TaskRTCThresholdFloatingNonPreemptiveRegions.

analysis/facts/preemption/rtc_threshold/limited.v

@@ -130,7 +130,7 @@ Section TaskRTCThresholdLimitedPreemptions.
     apply leq_trans with( nth 0 (job_preemption_points j) ((size (job_preemption_points j)).-2)); first by apply undup_nth_le; eauto 2.
     have -> : task_cost tsk = last0 (task_preemption_points tsk) by rewrite COST__task. 
     rewrite last_seq_minus_last_distance_seq; last by apply SORT__task.
-    rewrite -TSK__j.
+    move: TSK__j => /eqP TSK__j; rewrite -TSK__j.
     rewrite T4; last by done.
     apply domination_of_distances_implies_domination_of_seq; try eauto 2.
     - erewrite zero_is_first_element; eauto.

analysis/facts/preemption/rtc_threshold/nonpreemptive.v

@@ -70,7 +70,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
     intros; split.
     - by unfold task_rtc_bounded_by_cost.
     - intros j ARR TSK.
-      rewrite -TSK /fully_nonpreemptive.
+      move: TSK => /eqP <-; rewrite /fully_nonpreemptive.
       edestruct (posnP (job_cost j)) as [ZERO|POS].
       + by rewrite job_rtc_threshold_is_0.
       + by erewrite job_rtc_threshold_is_ε; eauto 2. 

analysis/facts/preemption/rtc_threshold/preemptive.v

@@ -34,7 +34,7 @@ Section TaskRTCThresholdFullyPreemptiveModel.
     - by rewrite /task_rtc_bounded_by_cost.
     - intros j ARR TSK.
       apply leq_trans with (job_cost j); eauto 2 with basic_facts.
-        by rewrite-TSK; apply H_valid_job_cost.
+      by move: TSK => /eqP <-; apply H_valid_job_cost.
   Qed.
     
 End TaskRTCThresholdFullyPreemptiveModel.

model/task/arrivals.v

@@ -21,7 +21,7 @@ Section TaskArrivals.
   (** First, we construct the list of jobs of task [tsk] that arrive
       in a given half-open interval <<[t1, t2)>>. *)
   Definition task_arrivals_between (t1 t2 : instant) :=
-    [seq j <- arrivals_between arr_seq t1 t2 | job_task j == tsk].
+    [seq j <- arrivals_between arr_seq t1 t2 | job_of_task tsk j].
   
   (** Based on that, we define the list of jobs of task [tsk] that
       arrive up to and including time [t], ... *)
@@ -35,7 +35,7 @@ Section TaskArrivals.
 
   (** ... the list of jobs of task [tsk] that arrive exactly at an instant [t], ... *)
   Definition task_arrivals_at (tsk : Task) (t : instant) :=
-    [seq j <- arrivals_at arr_seq t | job_task j == tsk].
+    [seq j <- arrivals_at arr_seq t | job_of_task tsk j].
   
   (** ... and finally count the number of job arrivals. *)
   Definition number_of_task_arrivals (t1 t2 : instant) :=

model/task/preemption/parameters.v

@@ -171,7 +171,7 @@ Section ValidTaskRunToCompletionThreshold.
   Definition job_respects_task_rtc tsk :=
     forall j,
       arrives_in arr_seq j ->
-      job_task j = tsk ->
+      job_of_task tsk j ->
       job_rtct j <= task_rtct tsk.
 
   (** Finally, we require that a valid run-to-completion threshold parameter

results/edf/rta/bounded_nps.v

@@ -150,7 +150,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
     Lemma priority_inversion_is_bounded_by_blocking:
       forall j t,
         arrives_in arr_seq j ->
-        job_task j = tsk ->
+        job_of_task tsk j ->
         t <= job_arrival j ->
         max_length_of_priority_inversion j t <= blocking_bound.
     Proof.
@@ -173,7 +173,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
           { apply/eqP; intros TSKj'.
             rewrite /EDF -ltnNge in NOTHEP.
             rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline in NOTHEP.
-            rewrite TSKj' TSK ltn_add2r in NOTHEP.
+            move: TSK => /eqP -> in NOTHEP; rewrite TSKj' ltn_add2r in NOTHEP.
             move: NOTHEP; rewrite ltnNge; move => /negP T; apply: T.
             apply leq_trans with t; last by done.
             eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2.
@@ -182,7 +182,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
           }
           apply/andP; split; first by done.
           rewrite /EDF -ltnNge in NOTHEP.
-          rewrite -TSK.
+          move: TSK => /eqP <-.
           have ARRLE: job_arrival j' < job_arrival j.
           { apply leq_trans with t; last by done.
             eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2.

results/edf/rta/bounded_pi.v

@@ -268,7 +268,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
       move: (BUSY) => [[ _ [QT [_ /andP [JAj _]]] _]].
       apply QT; try done.
       - eapply in_arrivals_implies_arrived; eauto 2.
-      - unfold edf.EDF, EDF; move: TSKs => /eqP TSKs.
+      - unfold edf.EDF, EDF; move: TSK TSKs => /eqP TSK /eqP TSKs.
         rewrite /job_deadline /job_deadline_from_task_deadline /hep_job TSK TSKs leq_add2r.
           by apply leq_trans with t1; [apply ltnW | ].
     Qed.
@@ -303,7 +303,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
         (** Consider an arbitrary job j of [tsk]. *)
         Variable j : Job.
         Hypothesis H_j_arrives : arrives_in arr_seq j.
-        Hypothesis H_job_of_tsk : job_task j = tsk.
+        Hypothesis H_job_of_tsk : job_of_task tsk j.
         Hypothesis H_job_cost_positive: job_cost_positive j.
 
         (** Consider any busy interval <<[t1, t2)>> of job [j]. *)
@@ -347,7 +347,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
             + by rewrite ltnW.
           - apply H_priority_inversion_is_bounded; try done.
             eapply instantiated_busy_interval_equivalent_busy_interval in H_busy_interval; eauto 2 with basic_facts.
-              by move: H_busy_interval => [PREF _].
+            by move: H_busy_interval => [PREF _].
         Qed.
 
         (** Next, we show that [bound_on_total_hep_workload(A, R)] bounds 
@@ -368,8 +368,8 @@ Section AbstractRTAforEDFwithArrivalCurves.
           move: H_sched_valid => [CARR MBR].
           erewrite instantiated_cumulative_interference_of_hep_tasks_equal_total_interference_of_hep_tasks;
             eauto 2 with basic_facts.
-          - by rewrite -H_job_of_tsk /jobs.
-          - rewrite instantiated_quiet_time_equivalent_quiet_time; eauto 2 with basic_facts.
+          - by move: (H_job_of_tsk) => /eqP ->; rewrite /jobs.
+          - by rewrite instantiated_quiet_time_equivalent_quiet_time; eauto 2 with basic_facts.
         Qed.
 
         (** By lemma [service_of_jobs_le_workload], the total
@@ -484,7 +484,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
             edestruct (leqP (D tsk_o) (A + ε + D tsk)) as [NEQ2|NEQ2]. 
             - move: ARRIN; rewrite leqNgt; move => /negP ARRIN; apply: ARRIN.
               rewrite -(ltn_add2r (D tsk_o)).
-              apply leq_ltn_trans with (job_arrival j + D tsk); first by rewrite -H_job_of_tsk -TSKo.
+              apply leq_ltn_trans with (job_arrival j + D tsk); first by move: (H_job_of_tsk) => /eqP <-; rewrite -TSKo.
               rewrite addnBA // addnA addnA subnKC // subnK.
               + by rewrite ltn_add2r addn1.
               + apply leq_trans with (A + ε + D tsk); first by done.
@@ -493,7 +493,8 @@ Section AbstractRTAforEDFwithArrivalCurves.
               apply leq_ltn_trans with (job_arrival jo + (A + D tsk)). 
               + rewrite addnBAC // addnBA.
                 rewrite [in X in _ <= X]addnC -addnBA.
-                * by rewrite /job_deadline /job_deadline_from_task_deadline H_job_of_tsk leq_addr.
+                * rewrite /job_deadline /job_deadline_from_task_deadline;
+                    by move: (H_job_of_tsk) => /eqP ->; rewrite leq_addr.
                 * by apply leq_trans with (t1 + (A + ε + D tsk - D tsk_o)); first rewrite leq_addr.
                     by apply leq_trans with (job_arrival j); [ | by rewrite leq_addr].
               + rewrite ltn_add2l.

results/edf/rta/fully_nonpreemptive.v

@@ -132,8 +132,10 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
     { intros j ARR TSK.
       have ZEROj: job_cost j = 0.
       { move: (H_valid_job_cost j ARR) => NEQ.
-        rewrite /valid_job_cost TSK ZERO in NEQ.
-          by apply/eqP; rewrite -leqn0.
+        rewrite /valid_job_cost in NEQ.
+        move: TSK => /eqP -> in NEQ.
+        rewrite ZERO in NEQ.
+        by apply/eqP; rewrite -leqn0.
       }
         by rewrite /job_response_time_bound /completed_by ZEROj.
     }

results/edf/rta/limited_preemptive.v

@@ -145,7 +145,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
     case: (posnP (task_cost tsk)) => [ZERO|POSt].
     { intros j ARR TSK.
       move: (H_valid_job_cost _ ARR) => POSt.
-      move: POSt; rewrite /valid_job_cost TSK ZERO leqn0; move => /eqP Z.
+      move: TSK => /eqP TSK; move: POSt; rewrite /valid_job_cost TSK ZERO leqn0; move => /eqP Z.
       by rewrite /job_response_time_bound /completed_by Z.
     }
     eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L).

results/fifo/rta.v

@@ -291,9 +291,8 @@ Section AbstractRTAforFIFOwithArrivalCurves.
       { rewrite /workload_of_jobs /IBF (big_rem tsk) //= (addnC (rbf tsk (job_arrival j - t1 + ε))).
         rewrite -addnBA; last first.
         { apply leq_trans with (task_rbf ε).
-          apply (task_rbf_1_ge_task_cost arr_seq) with (j0 := j) => //=.
-          - by rewrite -TSKj; apply H_is_arrival_curve, H_all_jobs_from_taskset.
-          - by apply task_rbf_monotone; [apply H_valid_arrival_curve | ssrlia]. }
+          apply (task_rbf_1_ge_task_cost arr_seq) with (j0 := j) => //=; first by auto.
+          by apply task_rbf_monotone; [apply H_valid_arrival_curve | ssrlia]. }
         { eapply leq_trans; last first.
           by erewrite leq_add2l; eapply task_rbf_excl_tsk_bounds_task_workload_excl_j; eauto 1.
           rewrite addnBA.
@@ -309,11 +308,11 @@ Section AbstractRTAforFIFOwithArrivalCurves.
               + by apply (task_workload_le_task_rbf _ _ _ IN H_valid_job_cost H_is_arrival_curve t1).
               + by rewrite addnBAC //= subnKC //= addn1; apply leqW. } 
           { rewrite /task_workload_between /task_workload /workload_of_jobs (big_rem j) //=.
-            - by rewrite /job_of_task TSKj //= eq_refl; apply leq_addr. 
+            - by rewrite TSKj; apply leq_addr.
             - apply job_in_arrivals_between => //.
               by apply /andP; split; [| rewrite subnKC; [rewrite addn1 |]].  } } }
-      apply arrivals_uniq; try by done.
-      apply job_in_arrivals_between; try by done.
+      apply: arrivals_uniq => //.
+      apply: job_in_arrivals_between => //.
       by apply /andP; split; [ | rewrite addn1]. 
     Qed.
 
@@ -345,9 +344,7 @@ Section AbstractRTAforFIFOwithArrivalCurves.
           rewrite /task_rbf /rbf; erewrite task_rbf_0_zero; eauto 2.
           rewrite add0n /task_rbf; apply leq_trans with (task_cost tsk).
           - by eapply leq_trans; eauto 2.
-          - eapply task_rbf_1_ge_task_cost; eauto.
-            unfold job_of_task in H_job_of_tsk.
-            by move : H_job_of_tsk => /eqP AAA. }
+          - by eapply task_rbf_1_ge_task_cost; eauto. }
         { apply /andP; split; first by done.
           apply /hasPn.
           move => EQ2. unfold IBF in INSP2.
@@ -415,9 +412,9 @@ Section AbstractRTAforFIFOwithArrivalCurves.
     - by apply instantiated_i_and_w_are_coherent_with_schedule.
     - by apply instantiated_busy_intervals_are_bounded.
     - by apply instantiated_interference_is_bounded.
-    - eapply (exists_solution_for_abstract_response_time_recurrence js) => //=; first by apply /eqP.
-      apply leq_trans with (job_cost js); first by done.
-      rewrite -TSKs.
+    - eapply (exists_solution_for_abstract_response_time_recurrence js) => //=.
+      apply leq_trans with (job_cost js) => //.
+      move: TSKs; rewrite /job_of_task => /eqP <-.
       by eapply H_valid_job_cost.
   Qed.
   

results/fixed_priority/rta/bounded_nps.v

@@ -131,10 +131,10 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
     Lemma priority_inversion_is_bounded_by_blocking:
       forall j t, 
         arrives_in arr_seq j ->
-        job_task j = tsk -> 
+        job_of_task tsk j -> 
         max_length_of_priority_inversion j t <= blocking_bound.
     Proof.
-      intros j t ARR TSK.
+      intros j t ARR TSK; move: TSK => /eqP TSK.
       rewrite /max_length_of_priority_inversion /blocking_bound /FP_to_JLFP
               /priority_inversion.max_length_of_priority_inversion.
       apply leq_trans with
@@ -170,7 +170,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
         rewrite /cumulative_priority_inversion /is_priority_inversion.
         rewrite -[X in _ <= X]addn0 -[t2 - t1]mul1n -iter_addn -big_const_nat leq_sum //. 
         intros t _; case: (sched t); last by done.
-          by intros s; case: (hep_job s j). 
+        by intros s; case: (hep_job s j). 
       } 
       move: NEQ => /negP /negP; rewrite -ltnNge; move => BOUND.
       edestruct (@preemption_time_exists) as [ppt [PPT NEQ]]; eauto 2 with basic_facts.
@@ -179,11 +179,11 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
         last apply leq_trans with (ppt - t1); first last.
       - rewrite leq_subLR.
         apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done.
-          by rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2.
+        by rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2.
       - rewrite /cumulative_priority_inversion /is_priority_inversion.
         rewrite -[X in _ <= X]addn0 -[ppt - t1]mul1n -iter_addn -big_const_nat. 
         rewrite leq_sum //; intros t _; case: (sched t); last by done.
-          by intros s; case: (hep_job s j).
+        by intros s; case: (hep_job s j).
       - rewrite /cumulative_priority_inversion /is_priority_inversion. 
         rewrite (@big_cat_nat _ _ _ ppt) //=; last first.
         { rewrite ltn_subRL in BOUND.
@@ -202,7 +202,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
         apply/eqP; rewrite eqb0 Bool.negb_involutive.
         enough (EQef : s = j_hp); first by subst;auto.
         eapply ideal_proc_model_is_a_uniprocessor_model; eauto 2.
-          by rewrite scheduled_at_def SCHED.
+        by rewrite scheduled_at_def SCHED.
     Qed.
     
   End PriorityInversionIsBounded.