From e7d7823f6025e21bf825d00913c91c75b30b21bc Mon Sep 17 00:00:00 2001 From: Sergei Bozhko Date: Mon, 13 May 2019 17:55:48 +0200 Subject: [PATCH] Delete useless assumption in util-lemma --- analysis/apa/bertogna_edf_theory.v | 14 ++++++------ analysis/apa/interference_bound_edf.v | 6 ++--- analysis/global/basic/bertogna_edf_theory.v | 4 ++-- .../global/basic/interference_bound_edf.v | 6 ++--- analysis/global/jitter/bertogna_edf_theory.v | 6 ++--- .../global/jitter/interference_bound_edf.v | 6 ++--- .../dynamic/jitter/jitter_schedule_service.v | 18 ++------------- .../singlecost/reduction_properties.v | 12 +++------- ...sufficient_condition_for_lock_in_service.v | 2 +- .../platform/priority_inversion_is_bounded.v | 4 ++-- model/schedule/uni/nonpreemptive/schedule.v | 17 +++++--------- util/nat.v | 22 +++++-------------- 12 files changed, 39 insertions(+), 78 deletions(-) diff --git a/analysis/apa/bertogna_edf_theory.v b/analysis/apa/bertogna_edf_theory.v index 0f032e40..0d396556 100644 --- a/analysis/apa/bertogna_edf_theory.v +++ b/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. diff --git a/analysis/apa/interference_bound_edf.v b/analysis/apa/interference_bound_edf.v index 8be90929..76c56e8b 100644 --- a/analysis/apa/interference_bound_edf.v +++ b/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 diff --git a/analysis/global/basic/bertogna_edf_theory.v b/analysis/global/basic/bertogna_edf_theory.v index 484620b7..2b47bd42 100644 --- a/analysis/global/basic/bertogna_edf_theory.v +++ b/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. { diff --git a/analysis/global/basic/interference_bound_edf.v b/analysis/global/basic/interference_bound_edf.v index 513cc0b9..2b6cf8a6 100644 --- a/analysis/global/basic/interference_bound_edf.v +++ b/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 diff --git a/analysis/global/jitter/bertogna_edf_theory.v b/analysis/global/jitter/bertogna_edf_theory.v index 639feb34..c94a7ff9 100644 --- a/analysis/global/jitter/bertogna_edf_theory.v +++ b/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. diff --git a/analysis/global/jitter/interference_bound_edf.v b/analysis/global/jitter/interference_bound_edf.v index 88d4f551..266cd3e9 100644 --- a/analysis/global/jitter/interference_bound_edf.v +++ b/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 diff --git a/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v b/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v index c5d88d83..d9f00be4 100644 --- a/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v +++ b/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 diff --git a/analysis/uni/susp/sustainability/singlecost/reduction_properties.v b/analysis/uni/susp/sustainability/singlecost/reduction_properties.v index 1389856c..1bd5425b 100644 --- a/analysis/uni/susp/sustainability/singlecost/reduction_properties.v +++ b/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 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) //. diff --git a/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v b/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v index 2909099f..9a451803 100644 --- a/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v +++ b/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. } diff --git a/model/schedule/uni/nonpreemptive/schedule.v b/model/schedule/uni/nonpreemptive/schedule.v index f22542c0..adada55f 100644 --- a/model/schedule/uni/nonpreemptive/schedule.v +++ b/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. diff --git a/util/nat.v b/util/nat.v index e661c533..7cca339e 100644 --- a/util/nat.v +++ b/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: -- GitLab