Delete useless assumption in util-lemma

analysis/apa/bertogna_edf_theory.v

@@ -220,12 +220,12 @@ Module ResponseTimeAnalysisEDF.
         Lemma bertogna_edf_specific_bound_holds :
           x tsk_other <= edf_specific_bound tsk_other R_other.
         Proof.
-          apply interference_bound_edf_bounds_interference with (job_deadline0 := job_deadline)
-                                                   (arr_seq0 := arr_seq) (ts0 := ts); try (by done);
-            [ by apply bertogna_edf_tsk_other_in_ts
-            | by apply H_tasks_miss_no_deadlines
-            | by apply H_tasks_miss_no_deadlines | ].
-          by ins; apply H_all_previous_jobs_completed_on_time with (tsk_other := tsk_other). 
+          apply interference_bound_edf_bounds_interference with
+              (job_deadline0 := job_deadline)
+              (arr_seq0 := arr_seq) (ts0 := ts); try (by done);
+            [ by apply bertogna_edf_tsk_other_in_ts | 
+                by apply H_tasks_miss_no_deadlines | ].
+            by ins; apply H_all_previous_jobs_completed_on_time with (tsk_other := tsk_other). 
         Qed.
         
       End LemmasAboutInterferingTasks.
@@ -998,7 +998,7 @@ Module ResponseTimeAnalysisEDF.
         unfold interference_bound_edf, interference_bound_generic in LTmin.
         rewrite minnAC in LTmin; apply min_lt_same in LTmin.
         have BASICBOUND := bertogna_edf_workload_bounds_interference R' j BEFOREok tsk_other R_other HP.
-        have EDFBOUND := (bertogna_edf_specific_bound_holds tsk' R' INbounds j ARRj JOBtsk BEFOREok tsk_other R_other HP).
+        have EDFBOUND := (bertogna_edf_specific_bound_holds tsk' R' j ARRj JOBtsk BEFOREok tsk_other R_other HP).
         unfold minn in LTmin; clear -LTmin HP BASICBOUND EDFBOUND tsk; desf.
         {
           by apply (leq_ltn_trans BASICBOUND) in LTmin; rewrite ltnn in LTmin. 

analysis/apa/interference_bound_edf.v

@@ -609,7 +609,7 @@ Module InterferenceBoundEDF.
               have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
               destruct FST as [FSTarr [FSTtask [LEdl _]]].            
               have LTr := interference_bound_edf_response_time_bound_of_j_fst_after_interval.
-              apply subh3; last by apply LEdk.
+              apply subh3. 
               apply leq_trans with (n := job_interference job_arrival job_cost job_task sched alpha j_i j_fst t1
                                                           (job_arrival j_fst + R_k) + (D_k - R_k));
                 first by rewrite leq_add2r; apply extend_sum; [by apply leqnn|]. 
@@ -955,8 +955,8 @@ Module InterferenceBoundEDF.
               interference_caused_by j_fst t1 t2 <= D_i %% p_k - (D_k - R_k).
             Proof.
               intro LE.
-              apply subh3; last by apply interference_bound_edf_remainder_ge_slack.
-              by rewrite -subndiv_eq_mod; apply subh3; last by apply leq_trunc_div.
+              apply subh3.
+                by rewrite -subndiv_eq_mod; apply subh3. 
             Qed.
               
             (* Next, we prove that interference caused by j_fst is bounded by the length

analysis/global/basic/bertogna_edf_theory.v

@@ -212,7 +212,7 @@ Module ResponseTimeAnalysisEDF.
                                               (arr_seq0 := arr_seq) (ts0 := ts); try (by done);
             [ by apply bertogna_edf_tsk_other_in_ts
             | by apply H_tasks_miss_no_deadlines
-            | by apply H_tasks_miss_no_deadlines | ].
+            | ].
           by ins; apply H_all_previous_jobs_completed_on_time with (tsk_other := tsk_other). 
         Qed.
         
@@ -796,7 +796,7 @@ Module ResponseTimeAnalysisEDF.
         unfold interference_bound_edf, interference_bound_generic in LTmin.
         rewrite minnAC in LTmin; apply min_lt_same in LTmin.
         have BASICBOUND := bertogna_edf_workload_bounds_interference R' j BEFOREok tsk_other R_other HP.
-        have EDFBOUND := (bertogna_edf_specific_bound_holds tsk' R' INbounds j ARRj
+        have EDFBOUND := (bertogna_edf_specific_bound_holds tsk' R' j ARRj
                                                             JOBtsk BEFOREok tsk_other R_other HP).
         unfold minn in LTmin; clear -LTmin HP BASICBOUND EDFBOUND tsk; desf.
         {

analysis/global/basic/interference_bound_edf.v

@@ -604,7 +604,7 @@ Module InterferenceBoundEDF.
               have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
               destruct FST as [FSTarr [FSTtask [LEdl _]]].            
               have LTr := interference_bound_edf_response_time_bound_of_j_fst_after_interval.
-              apply subh3; last by apply LEdk.
+              apply subh3.
               apply leq_trans with (n := job_interference job_arrival job_cost sched j_i j_fst t1
                                                           (job_arrival j_fst + R_k) + (D_k - R_k));
                 first by rewrite leq_add2r; apply extend_sum; [by apply leqnn|]. 
@@ -950,8 +950,8 @@ Module InterferenceBoundEDF.
               interference_caused_by j_fst t1 t2 <= D_i %% p_k - (D_k - R_k).
             Proof.
               intro LE.
-              apply subh3; last by apply interference_bound_edf_remainder_ge_slack.
-              by rewrite -subndiv_eq_mod; apply subh3; last by apply leq_trunc_div.
+              apply subh3.
+                by rewrite -subndiv_eq_mod; apply subh3.
             Qed.
               
             (* Next, we prove that interference caused by j_fst is bounded by the length

analysis/global/jitter/bertogna_edf_theory.v

@@ -228,9 +228,7 @@ Module ResponseTimeAnalysisEDFJitter.
           by apply interference_bound_edf_bounds_interference with (job_deadline0 := job_deadline)
                    (arr_seq0 := arr_seq) (ts0 := ts); try (by done);
           [  by apply bertogna_edf_tsk_other_in_ts
-          |  by apply H_tasks_miss_no_deadlines
-          |  by apply leq_trans with (n := task_jitter tsk + R);
-               [apply leq_addl | by apply H_tasks_miss_no_deadlines]
+          |  by apply H_tasks_miss_no_deadlines         
           |  by ins; apply H_all_previous_jobs_completed_on_time with (tsk_other := tsk_other)].
         Qed.
         
@@ -849,7 +847,7 @@ Module ResponseTimeAnalysisEDFJitter.
         unfold interference_bound_edf, interference_bound_generic in LTmin.
         rewrite minnAC in LTmin; apply min_lt_same in LTmin.
         specialize (BASICBOUND tsk' R' j ARRj JOBtsk BEFOREok tsk_other R_other HP).
-        specialize (EDFBOUND tsk' R' INbounds j ARRj JOBtsk BEFOREok tsk_other R_other HP).
+        specialize (EDFBOUND tsk' R' j ARRj JOBtsk BEFOREok tsk_other R_other HP).
         unfold minn in LTmin; clear -LTmin HP BASICBOUND EDFBOUND tsk; desf.
         {
           by apply (leq_ltn_trans BASICBOUND) in LTmin; rewrite ltnn in LTmin. 

analysis/global/jitter/interference_bound_edf.v

@@ -660,7 +660,7 @@ Module InterferenceBoundEDFJitter.
               have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
               destruct FST as [FSTtask [_ [LEdl _]]].            
               have LTr := interference_bound_edf_response_time_bound_of_j_fst_after_interval.
-              apply subh3; last by apply LEdk.
+              apply subh3.
               apply leq_trans with (n := job_interference job_arrival job_cost job_jitter sched j_i
                                        j_fst t1 (job_arrival j_fst + J_k + R_k) + (D_k - R_k - J_k)).
               {
@@ -1051,8 +1051,8 @@ Module InterferenceBoundEDFJitter.
               interference_caused_by j_fst t1 t2 <= D_i %% p_k - (D_k - R_k - J_k).
             Proof.
               intro LE.
-              apply subh3; last by apply interference_bound_edf_remainder_ge_slack.
-              by rewrite -subndiv_eq_mod; apply subh3; last by apply leq_trunc_div.
+              apply subh3.
+              by rewrite -subndiv_eq_mod; apply subh3.
             Qed.
               
             (* Next, we prove that interference caused by j_fst is bounded by the length

analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v

@@ -755,16 +755,7 @@ Module JitterScheduleService.
               set TSj := fun a b => \sum_(a <= t0 < b)
                                          \sum_(j_hp <- act 0 t2 | hep j_hp) SCHj j_hp t0.
               rewrite -/(TSs t1 (t1 + d).+1) -/(TSs 0 t1).
-              rewrite subh3 //; last first.
-              {
-                apply leq_trans with (n := TSs 0 (t1 + d).+1).
-                {
-                  apply extend_sum; try (by done).
-                  by apply leq_trans with (n := t1 + d); first by apply leq_addr.
-                }
-                rewrite /TSs exchange_big /=.
-                by apply LEWORKs.
-              }
+              rewrite subh3 //.
               rewrite addnC -big_cat_nat //=;
                 last by apply leq_trans with (n := t1 + d); first by apply leq_addr.
               by rewrite exchange_big; apply LEWORKs; rewrite ltn_add2l.
@@ -1116,12 +1107,7 @@ Module JitterScheduleService.
         feed AFTERj; try done.
         set Sj := service_during sched_jitter j arr_j.
         set Shp := service_of_other_hep_jobs_in_sched_jitter arr_j.
-        rewrite subh3 //; last first.
-        {
-          rewrite /Shp /service_of_other_hep_jobs_in_sched_jitter.
-          rewrite -[X in _ <= X](addKn arr_j).
-          by apply service_of_jobs_le_delta, actual_arrivals_uniq.
-        }
+        rewrite subh3 //.
         apply leq_trans with (n := \sum_(arr_j <= t < arr_j + R_j) 1);
           last by simpl_sum_const; rewrite addKn.
         rewrite /Sj /Shp /service_of_other_hep_jobs_in_sched_jitter /service_of_jobs

analysis/uni/susp/sustainability/singlecost/reduction_properties.v

@@ -722,16 +722,10 @@ Module SustainabilitySingleCostProperties.
         rewrite addnC -addnBA; last by rewrite SAME.
         apply leq_trans with (n := R - (Sw j (arr_j + r) (arr_j + R) + 0));
           last by rewrite leq_sub2l // leq_add2l; apply eq_leq; apply/eqP; rewrite subn_eq0 SAME.
-        rewrite addn0 subh3 //; last first.
-        {
-          apply leq_trans with (n := Sw j arr_j (arr_j+R)); last by apply cumulative_service_le_delta.
-          by apply extend_sum; first by apply leq_addr. 
-        }
-        {
-          apply leq_trans with (n := r + \sum_(arr_j+r<=t<arr_j+R) 1);
-            first by rewrite leq_add2l; apply leq_sum; intros t _; apply leq_b1.
+        rewrite addn0 subh3 //.
+        apply leq_trans with (n := r + \sum_(arr_j+r<=t<arr_j+R) 1);
+          first by rewrite leq_add2l; apply leq_sum; intros t _; apply leq_b1.
           by simpl_sum_const; rewrite subnDl subnKC.
-        }
       Qed.      
 
     End ComparingResponseTimes.

model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v

@@ -156,7 +156,7 @@ Module AbstractRTALockInService.
             by apply/andP; split; last (apply negbT in NEQ; apply ltnW; rewrite ltnNge).
         } 
         { move: H_total_workload_is_bounded => BOUND.
-          apply subh3_ext in BOUND.
+          apply subh3 in BOUND.
           apply leq_trans with (delta - cumul_interference j t1 (t1 + delta)); first by done.
           apply leq_trans with (service_during sched j t1 (t1 + delta)).
           { rewrite -{1}[delta](interference_is_complement_to_schedule t1) //. 

model/schedule/uni/limited/platform/priority_inversion_is_bounded.v

@@ -125,7 +125,7 @@ Module PriorityInversionIsBounded.
         exists j_hp.
         have HP: higher_eq_priority j_hp j.
         { apply contraT; move => /negP NOTHP; exfalso.
-          have TEMP: t <= t2.-1; first by rewrite -subn1 subh3 //; [by rewrite addn1 | by apply leq_ltn_trans with t1].
+          have TEMP: t <= t2.-1; first by rewrite -subn1 subh3 // addn1.
           rewrite leq_eqVlt in TEMP; move: TEMP => /orP [/eqP EQUALt2m1 | LTt2m1];
                                                     first rewrite leq_eqVlt in GEt; first move: GEt => /orP [/eqP EQUALt1 | LARGERt1].
           { subst t; clear LEt.
@@ -444,7 +444,7 @@ Module PriorityInversionIsBounded.
           }
           apply SCHEDc; apply/andP; split.
           - rewrite -addn1 in NEQ.
-            apply subh3_ext in NEQ.
+            apply subh3 in NEQ.
               by rewrite subn1 in NEQ.
           - apply leq_trans with t1. by apply leq_pred. by done.
         }

model/schedule/uni/nonpreemptive/schedule.v

@@ -116,8 +116,7 @@ Module NonpreemptiveSchedule.
           apply contraT; rewrite negbK; intros COMP.
           exfalso; move: NOTCOMP => /negP NOTCOMP; apply: NOTCOMP.
           apply completion_monotonic with (t0 := i); try ( by done).
-          apply subh3; first by rewrite addn1.
-            by apply leq_ltn_trans with (n := i).
+            by apply subh3; first rewrite addn1.
         Qed.
         
       End CompletionUnderNonpreemptive.
@@ -333,10 +332,8 @@ Module NonpreemptiveSchedule.
             move: COMP; apply contraR; intros CONTR.
             apply in_nonpreemption_schedule_preemption_implies_completeness
             with (t:=t); [|by done| by done].
-            rewrite subh3 // ?leq_add2l;
-              first by rewrite scheduled_implies_positive_remaining_cost //.
-            rewrite addn_gt0; apply/orP; right;
-            rewrite scheduled_implies_positive_remaining_cost //.
+            rewrite subh3 // ?leq_add2l.
+              by rewrite scheduled_implies_positive_remaining_cost //.
           Qed.
 
           (* ... and it is not scheduled after (t + remaining cost j t - 1). *)       
@@ -364,11 +361,9 @@ Module NonpreemptiveSchedule.
           move => t' /andP [GE LE].
           move: (H_j_is_scheduled_at_t) => SCHED1; move: (H_j_is_scheduled_at_t) => SCHED2.
           rewrite -addn1 in LE; apply subh3 with (m := t') (p := 1) in LE;
-          last by rewrite addn_gt0; apply/orP; right;
-          rewrite scheduled_implies_positive_remaining_cost //.
-          apply continuity_of_nonpreemptive_scheduling with
-          (t1 := t - service sched j t)
-            (t2 := t + job_remaining_cost j t - 1); first by done.
+            apply continuity_of_nonpreemptive_scheduling with
+                (t1 := t - service sched j t)
+                (t2 := t + job_remaining_cost j t - 1); first by done.
           - by apply/andP;split.
           - by apply j_is_scheduled_at_t_minus_service.
           - by apply j_is_scheduled_at_t_plus_remaining_cost_minus_one.

util/nat.v

@@ -23,29 +23,17 @@ Section NatLemmas.
       (m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2).
   Proof. by ins; ssromega. Qed.
   
-  Lemma subh3 :
-    forall m n p,
-      m + p <= n ->
-      n >= p ->
-      m <= n - p.
-  Proof.
-    ins. rewrite <- leq_add2r with (p := p).
-    by rewrite subh1 // -addnBA // subnn addn0.
-  Qed.
-
-  (* subh3: forall m n p : nat, m + p <= n -> p <= n -> m <= n - p *)
-  (*                 unnecessary condition -- ^^^^^^^^^ *)
-  (* TODO: del subh3 *)
-  Lemma subh3_ext:
+  Lemma subh3:
     forall m n p,
       m + p <= n ->
       m <= n - p.
   Proof.
     clear.
     intros.
-    apply subh3; first by done.
-    apply leq_trans with (m+p); last by done.
-      by rewrite leq_addl.
+    rewrite <- leq_add2r with (p := p).
+    rewrite subh1 //.
+    - by rewrite -addnBA // subnn addn0.
+    - by apply leq_trans with (m+p); first rewrite leq_addl.
   Qed.
 
   Lemma subh4: