diff --git a/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
index 7e35d99c9a9a903633a5beed3b37aa758757eb3c..7395efd14b48ce19a3b16450086012f7906a551b 100644
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -278,7 +278,7 @@ Section Abstract_RTA.
{ eapply job_run_to_completion_threshold_le_job_cost; eauto. }
{ rewrite {2}H_A_F_fixpoint.
rewrite /definitions.cumul_interference.
- rewrite -[in X in _ <= X]subh1; last by rewrite leq_subr.
+ rewrite -[in X in _ <= X]addnBAC; last by rewrite leq_subr.
rewrite {2}/optimism.
rewrite subKn; last by apply H_valid_run_to_completion_threshold.
rewrite leq_add2l.
@@ -404,13 +404,13 @@ Section Abstract_RTA.
apply leq_trans with (F_sp - optimism + job_last ); first by rewrite leq_add2r leq_sub2r.
apply leq_trans with (F_sp + (task_cost tsk - task_rtct tsk)); last by done.
rewrite /optimism subnBA; last by apply PRT2.
- rewrite -subh1 //.
+ rewrite -addnBAC //.
rewrite /job_last.
rewrite addnBA; last by eapply job_run_to_completion_threshold_le_job_cost; eauto.
- rewrite -subh1; last by rewrite leq_addl.
+ rewrite -addnBAC; last by rewrite leq_addl.
rewrite -addnBA // subnn addn0.
rewrite addnBA; last by apply PRT1.
- rewrite subh1; last by done.
+ rewrite addnBAC; last by done.
rewrite leq_sub2r // leq_add2l.
by rewrite -H_job_of_tsk; apply H_valid_job_cost.
}
diff --git a/analysis/abstract/run_to_completion.v b/analysis/abstract/run_to_completion.v
index 2ffbc554959e111aaee62a0b8abba04d1751393c..110cf51fdc23e65d110c3069ecc7f0434d1bdc5e 100644
--- a/analysis/abstract/run_to_completion.v
+++ b/analysis/abstract/run_to_completion.v
@@ -144,7 +144,7 @@ Section AbstractRTARunToCompletionThreshold.
by apply/andP; split; last (apply negbT in NEQ; apply ltnW; rewrite ltnNge).
}
{ move: H_total_workload_is_bounded => BOUND.
- apply subh3 in BOUND.
+ apply leq_subRL_impl 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/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index 89adb263233906cd2e2c08354c54e724e28402c8..ae227fe670a4c2f5ad25779c4380af8182ea44f2 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -202,7 +202,7 @@ Section PriorityInversionIsBounded.
Proof.
have TEMP: t <= t2.-1.
{ move: (H_t_in_busy_interval) => /andP [GEt LEt].
- by rewrite -subn1 subh3 // addn1.
+ by rewrite -subn1 leq_subRL_impl // addn1.
}
rewrite leq_eqVlt in TEMP; move: TEMP => /orP [/eqP EQUALt2m1 | LTt2m1].
- right; auto.
@@ -552,7 +552,7 @@ Section PriorityInversionIsBounded.
by have ->: jlp = jhp by eapply ideal_proc_model_is_a_uniprocessor_model; eauto.
}
apply SCHEDc; apply/andP; split.
- - by rewrite -addn1 in LT2; apply subh3 in LT2; rewrite subn1 in LT2.
+ - by rewrite -addn1 in LT2; apply leq_subRL_impl in LT2; rewrite subn1 in LT2.
- by apply leq_trans with t1; first apply leq_pred.
Qed.
@@ -789,7 +789,7 @@ Section PriorityInversionIsBounded.
all: unfold service.service; try done.
intros; apply MIN; apply/andP; split; by done.
- apply preemption_time_le_max_len_of_priority_inversion.
- unfold service.service; try done.
+ by unfold service.service.
Qed.
End Case3.
@@ -798,7 +798,7 @@ Section PriorityInversionIsBounded.
(** By doing the case analysis, we show that indeed there is a
preemption time in time interval [[t1, t1 +
- max_length_of_priority_inversion j t1]. *)
+ max_length_of_priority_inversion j t1]]. *)
Lemma preemption_time_exists:
exists pr_t,
preemption_time sched pr_t /\
@@ -812,7 +812,7 @@ Section PriorityInversionIsBounded.
- destruct (hep_job s j) eqn:PRIO.
+ by eapply preemption_time_exists_case2; eauto.
+ eapply preemption_time_exists_case3 with s; eauto.
- by rewrite -eqbF_neg; apply /eqP.
+ by rewrite -eqbF_neg; apply /eqP.
Qed.
End PreemptionTimeExists.
diff --git a/analysis/facts/preemption/rtc_threshold/job_preemptable.v b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 62e23bfaf29a5f6469c1d9f149927d5b0746727d..8efd14e7358d87ee0f46366db485e677ba4cf4dd 100644
--- a/analysis/facts/preemption/rtc_threshold/job_preemptable.v
+++ b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -221,7 +221,7 @@ Section RunToCompletionThreshold.
apply/negP; intros C.
have POS : 0 < job_cost j; first by ssrlia.
rewrite /job_rtct subnBA in GE; last by apply job_last_nonpreemptive_segment_positive.
- rewrite -subh1 in GE; [rewrite addn1 in GE | by apply job_last_nonpreemptive_segment_le_job_cost].
+ rewrite -addnBAC in GE; [rewrite addn1 in GE | by apply job_last_nonpreemptive_segment_le_job_cost].
rewrite job_cost_is_last_element_of_preemption_points in LT, GE.
rewrite last_seq_minus_last_distance_seq in GE; last by apply preemption_points_nondecreasing.
have EQ := antidensity_of_nondecreasing_seq.
diff --git a/analysis/facts/tdma.v b/analysis/facts/tdma.v
index db99d8a91606bf0c2180d8b6938fab41c2965adb..a94adcd6a9df2d9d417f8ca43ddbfb23ed52dfa7 100644
--- a/analysis/facts/tdma.v
+++ b/analysis/facts/tdma.v
@@ -116,30 +116,33 @@ Section TDMAFacts.
(** Then, we proved that no two tasks share the same time slot at any time. *)
Lemma task_in_time_slot_uniq:
- forall tsk1 tsk2 t, tsk1 \in ts -> task_time_slot tsk1 > 0 ->
- tsk2 \in ts -> task_time_slot tsk2 > 0 ->
- task_in_time_slot ts tsk1 t ->
- task_in_time_slot ts tsk2 t ->
- tsk1 = tsk2.
+ forall tsk1 tsk2 t,
+ tsk1 \in ts -> task_time_slot tsk1 > 0 ->
+ tsk2 \in ts -> task_time_slot tsk2 > 0 ->
+ task_in_time_slot ts tsk1 t ->
+ task_in_time_slot ts tsk2 t ->
+ tsk1 = tsk2.
Proof.
- intros* IN1 SLOT1 IN2 SLOT2.
+ intros * IN1 SLOT1 IN2 SLOT2.
rewrite /task_in_time_slot.
- set cycle:=TDMA_cycle ts.
- set O1:= task_slot_offset ts tsk1.
- set O2:= task_slot_offset ts tsk2.
- have CO1: O1 < cycle by apply Offset_lt_cycle.
- have CO2: O2 < cycle by apply Offset_lt_cycle.
- have C: cycle > 0 by apply (TDMA_cycle_positive tsk1).
- have GO1:O1 %% cycle = O1 by apply modn_small,Offset_lt_cycle. rewrite GO1.
- have GO2:O2 %% cycle = O2 by apply modn_small,Offset_lt_cycle. rewrite GO2.
- have SO1:O1 + task_time_slot tsk1 <= cycle by apply (Offset_add_slot_leq_cycle tsk1).
- have SO2:O2 + task_time_slot tsk2 <= cycle by apply (Offset_add_slot_leq_cycle tsk2).
- repeat rewrite mod_elim;auto.
- case (O1 <= t%%cycle)eqn:O1T;case (O2 <= t %%cycle)eqn:O2T;intros G1 G2;try ssrlia.
- apply ltn_subLR in G1;apply ltn_subLR in G2. case (tsk1==tsk2) eqn:NEQ;move/eqP in NEQ;auto.
- destruct (slot_order_total tsk1 tsk2) as [order |order];auto;apply relation_offset in order;
- fold O1 O2 in order;try ssrlia;auto. by move/eqP in NEQ. apply /eqP;auto.
+ set cycle := TDMA_cycle ts.
+ set O1 := task_slot_offset ts tsk1.
+ set O2 := task_slot_offset ts tsk2.
+ have CO1 : O1 < cycle by apply Offset_lt_cycle.
+ have CO2 : O2 < cycle by apply Offset_lt_cycle.
+ have C : cycle > 0 by apply (TDMA_cycle_positive tsk1).
+ have -> : O1 %% cycle = O1 by apply modn_small, Offset_lt_cycle.
+ have -> : O2 %% cycle = O2 by apply modn_small, Offset_lt_cycle.
+ have SO1 : O1 + task_time_slot tsk1 <= cycle by apply (Offset_add_slot_leq_cycle tsk1).
+ have SO2 : O2 + task_time_slot tsk2 <= cycle by apply (Offset_add_slot_leq_cycle tsk2).
+ repeat rewrite mod_elim; auto.
+ case (O1 <= t %% cycle) eqn:O1T; case (O2 <= t %% cycle) eqn:O2T; intros G1 G2; try ssrlia.
+ rewrite ltn_subLR // in G1; rewrite ltn_subLR // in G2.
+ case (tsk1 == tsk2) eqn:NEQ; move/eqP in NEQ; auto.
+ destruct (slot_order_total tsk1 tsk2) as [order | order]; auto.
+ all: by apply relation_offset in order; fold O1 O2 in order; try ssrlia; auto; apply/eqP; auto.
Qed.
End TimeSlotOrderFacts.
+
End TDMAFacts.
diff --git a/classic/analysis/apa/bertogna_edf_comp.v b/classic/analysis/apa/bertogna_edf_comp.v
index 858a202df9a162c577c12fe108f1275808c79eb6..50234b06a462f005140d72e1c28b7160a72b3bfe 100755
--- a/classic/analysis/apa/bertogna_edf_comp.v
+++ b/classic/analysis/apa/bertogna_edf_comp.v
@@ -657,7 +657,7 @@ Module ResponseTimeIterationEDF.
rewrite (eq_bigr (fun i => snd i)); last first.
{
intro i; rewrite andbT; intro IN;
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
have GE_COST := edf_claimed_bounds_ge_cost ts step.
by destruct i; apply GE_COST.
}
@@ -665,7 +665,7 @@ Module ResponseTimeIterationEDF.
{
intro i; rewrite andbT; intro IN.
unfold update_bound; destruct i; simpl.
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
apply (edf_claimed_bounds_ge_cost ts step.+1).
by rewrite iterS; apply/mapP; exists (s, t).
}
@@ -776,7 +776,7 @@ Module ResponseTimeIterationEDF.
rewrite (eq_bigr (fun x => snd x)); last first.
{
intro i; rewrite andbT; intro IN.
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
have GE_COST := edf_claimed_bounds_ge_cost ts (max_steps ts).
fold (f (max_steps ts)) in GE_COST.
by destruct i; apply GE_COST.
@@ -784,7 +784,7 @@ Module ResponseTimeIterationEDF.
rewrite (eq_bigr (fun x => task_deadline x)); last first.
{
intro i; rewrite andbT; intro IN.
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
by specialize (VALID i IN); des.
}
rewrite -2!big_seq_cond.
diff --git a/classic/analysis/apa/bertogna_edf_theory.v b/classic/analysis/apa/bertogna_edf_theory.v
index 9a7a57381759e8784f91a8c88f0b4235c6280118..5eea9fd4429e868325920825b0690254783a3f11 100644
--- a/classic/analysis/apa/bertogna_edf_theory.v
+++ b/classic/analysis/apa/bertogna_edf_theory.v
@@ -243,7 +243,7 @@ Module ResponseTimeAnalysisEDF.
unfold completed, valid_sporadic_job in *.
unfold X, total_interference; rewrite addn1.
rewrite -(ltn_add2r (task_cost tsk)).
- rewrite subh1; last by rewrite [R](REC tsk) // leq_addr.
+ rewrite addnBAC; last by rewrite [R](REC tsk) // leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite -ltnNge in NOTCOMP.
@@ -881,7 +881,7 @@ Module ResponseTimeAnalysisEDF.
first by apply H_at_least_one_cpu; rewrite -JOBtsk FROMTS.
rewrite -(ltn_add2l (task_cost tsk)) -REC; last first. by done.
rewrite -addn1 -leq_subLR.
- rewrite -[R + 1 - _]subh1; last by apply GE_COST.
+ rewrite -[R + 1 - _]addnBAC; last by apply GE_COST.
rewrite leq_divRL;
last by apply H_at_least_one_cpu; rewrite -JOBtsk FROMTS.
apply EXCEEDS, SUB.
@@ -1007,4 +1007,4 @@ Module ResponseTimeAnalysisEDF.
End ResponseTimeBound.
-End ResponseTimeAnalysisEDF.
\ No newline at end of file
+End ResponseTimeAnalysisEDF.
diff --git a/classic/analysis/apa/bertogna_fp_comp.v b/classic/analysis/apa/bertogna_fp_comp.v
index 08b572022a99f543f9fb501fe512f225a10e547c..3708a6267de79bff64729f78567ce327bafe77d5 100644
--- a/classic/analysis/apa/bertogna_fp_comp.v
+++ b/classic/analysis/apa/bertogna_fp_comp.v
@@ -415,7 +415,7 @@ Module ResponseTimeIterationFP.
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
induction k.
{
- intros _; rewrite add0n -addn1 subh1;
+ intros _; rewrite add0n -addn1 addnBAC;
first by rewrite -addnBA // subnn addn0 /= leqnn.
by apply PARAMS.
}
@@ -425,7 +425,7 @@ Module ResponseTimeIterationFP.
apply leq_ltn_trans with (n := f k);last by apply INC, ltnW.
rewrite -addn1 -addnA [1 + _]addnC addnA -addnBA // subnn addn0.
rewrite -(ltn_add2r 1) in IHk.
- rewrite subh1 in IHk;
+ rewrite addnBAC in IHk;
last by apply leq_trans with (n := task_cost tsk);
[by apply PARAMS | by apply leq_addl].
by rewrite -addnBA // subnn addn0 addn1 ltnS in IHk.
@@ -466,7 +466,7 @@ Module ResponseTimeIterationFP.
exploit TOOMUCH; [by apply DIFF | by apply leq_addr |].
exploit (TASK_PARAMS tsk);
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
- rewrite subh1; last by apply PARAMS2.
+ rewrite addnBAC; last by apply PARAMS2.
rewrite -addnBA // subnn addn0 subn1 prednK //.
intros LT; apply (leq_ltn_trans LT).
by rewrite /max_steps [_ - _ + 1]addn1; apply INC, leq_addr.
diff --git a/classic/analysis/apa/bertogna_fp_theory.v b/classic/analysis/apa/bertogna_fp_theory.v
index 6f628887cd894d84e6bba6d7042178ea7cbfe0dd..8e2ff02af996188f7d0536b66806bfc1d7287cfb 100644
--- a/classic/analysis/apa/bertogna_fp_theory.v
+++ b/classic/analysis/apa/bertogna_fp_theory.v
@@ -255,7 +255,7 @@ Module ResponseTimeAnalysisFP.
unfold completed, valid_sporadic_job in *.
unfold X, total_interference; rewrite addn1.
rewrite -(ltn_add2r (task_cost tsk)).
- rewrite subh1; last by rewrite [R]REC // leq_addr.
+ rewrite addnBAC; last by rewrite [R]REC // leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite -ltnNge in NOTCOMP.
@@ -947,7 +947,7 @@ Module ResponseTimeAnalysisFP.
apply ltn_div_trunc with (d := #|alpha' tsk|); first by apply NONEMPTY.
rewrite -(ltn_add2l (task_cost tsk)) -REC.
rewrite -addn1 -leq_subLR.
- rewrite -[R + 1 - _]subh1; last by rewrite REC; apply leq_addr.
+ rewrite -[R + 1 - _]addnBAC; last by rewrite REC; apply leq_addr.
rewrite leq_divRL; last by apply NONEMPTY.
apply EXCEEDS, SUB.
apply leq_trans with (n := X * #|alpha tsk|); last by rewrite ALLBUSY.
@@ -1046,4 +1046,4 @@ Module ResponseTimeAnalysisFP.
End ResponseTimeBound.
-End ResponseTimeAnalysisFP.
\ No newline at end of file
+End ResponseTimeAnalysisFP.
diff --git a/classic/analysis/apa/interference_bound_edf.v b/classic/analysis/apa/interference_bound_edf.v
index 0abd7cae53b8a2e8ae40b7831e0f9f7f00fd2085..66a0480d6e19686a84db5cb4181efb16f0243c84 100644
--- a/classic/analysis/apa/interference_bound_edf.v
+++ b/classic/analysis/apa/interference_bound_edf.v
@@ -497,7 +497,7 @@ Module InterferenceBoundEDF.
(job_arrival0 := job_arrival); try (by done); apply leqnn.
}
{
- rewrite -(leq_add2r (D_k - R_k)) subh1 // -addnBA // subnn addn0.
+ rewrite -(leq_add2r (D_k - R_k)) addnBAC // -addnBA // subnn addn0.
assert (SUBST: D_k - R_k = \sum_(a_fst + R_k <= i < a_fst + D_k) 1).
{
rewrite big_const_nat iter_addn mul1n addn0.
@@ -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.
+ apply leq_subRL_impl.
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|].
@@ -832,7 +832,7 @@ Module InterferenceBoundEDF.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
by rewrite CURtsk.
}
- by rewrite subh3 // addnC /p_k -CURtsk.
+ by rewrite leq_subRL_impl // addnC /p_k -CURtsk.
Qed.
(* Using the lemma above, we prove that the ratio n_k is at least the number of
@@ -928,7 +928,7 @@ Module InterferenceBoundEDF.
rewrite addnBA; last by apply leq_trunc_div.
apply leq_trans with (n := R_k + D_i - (a_lst - a_fst)); last by apply leq_sub2l.
rewrite subnBA; last by apply interference_bound_edf_j_fst_before_j_lst.
- rewrite -(leq_add2r a_lst) subh1; last first.
+ rewrite -(leq_add2r a_lst) addnBAC; last first.
{
apply leq_trans with (n := t2);
[by apply ltnW, interference_bound_edf_last_job_arrives_before_end_of_interval|].
@@ -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.
- by rewrite -subndiv_eq_mod; apply subh3.
+ apply leq_subRL_impl.
+ by rewrite -subndiv_eq_mod; apply leq_subRL_impl.
Qed.
(* Next, we prove that interference caused by j_fst is bounded by the length
@@ -1202,4 +1202,4 @@ Module InterferenceBoundEDF.
End MonotonicitySpecificBound.
-End InterferenceBoundEDF.
\ No newline at end of file
+End InterferenceBoundEDF.
diff --git a/classic/analysis/apa/workload_bound.v b/classic/analysis/apa/workload_bound.v
index 35be6eb26aacba50a1539c5f50a286e678ebd440..dc2aca7e32e90773a70ce36ae30113ba8d9e9e63 100644
--- a/classic/analysis/apa/workload_bound.v
+++ b/classic/analysis/apa/workload_bound.v
@@ -480,7 +480,7 @@ Module WorkloadBound.
have lemma1 := workload_bound_last_job_arrives_before_end_of_interval.
have lemma2 := workload_bound_response_time_of_first_job_inside_interval.
rewrite addnBA; last by apply ltnW.
- rewrite subh1 // -addnBA; last by apply leq_addr.
+ rewrite addnBAC // -addnBA; last by apply leq_addr.
rewrite addnC [job_arrival _ + _]addnC.
unfold t2; rewrite [t1 + _]addnC -[delta + t1 - _]subnBA // subnn subn0.
rewrite addnA -subnBA; first by ins.
@@ -553,7 +553,7 @@ Module WorkloadBound.
by rewrite sort_uniq -/scheduled_jobs filter_uniq // undup_uniq.
by rewrite CURtsk.
}
- by rewrite subh3 // addnC -CURtsk.
+ by rewrite leq_subRL_impl // addnC -CURtsk.
Qed.
(* Prove that n_k is at least the number of the middle jobs *)
@@ -577,7 +577,7 @@ Module WorkloadBound.
by apply workload_bound_many_periods_in_between.
}
rewrite <- leq_add2r with (p := job_arrival j_fst) in DISTmax.
- rewrite addnC subh1 in DISTmax; last first.
+ rewrite addnC addnBAC in DISTmax; last first.
{
unfold j_fst, j_lst; rewrite -[_.+1]add0n.
apply prev_le_next; last by rewrite H_at_least_two_jobs add0n leqnn.
@@ -741,4 +741,4 @@ Module WorkloadBound.
End ProofWorkloadBound.
-End WorkloadBound.
\ No newline at end of file
+End WorkloadBound.
diff --git a/classic/analysis/global/basic/bertogna_edf_comp.v b/classic/analysis/global/basic/bertogna_edf_comp.v
index 3da4d8d31c183d1ed08c30ad7e1ec8351d0b5e40..d8e82c98da4c14650ef544d4e8146f9e207d4568 100755
--- a/classic/analysis/global/basic/bertogna_edf_comp.v
+++ b/classic/analysis/global/basic/bertogna_edf_comp.v
@@ -650,7 +650,7 @@ Module ResponseTimeIterationEDF.
rewrite (eq_bigr (fun i => snd i)); last first.
{
intro i; rewrite andbT; intro IN;
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
have GE_COST := edf_claimed_bounds_ge_cost ts step.
by destruct i; apply GE_COST.
}
@@ -658,7 +658,7 @@ Module ResponseTimeIterationEDF.
{
intro i; rewrite andbT; intro IN.
unfold update_bound; destruct i; simpl.
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
apply (edf_claimed_bounds_ge_cost ts step.+1).
by rewrite iterS; apply/mapP; exists (s, t).
}
@@ -770,7 +770,7 @@ Module ResponseTimeIterationEDF.
rewrite (eq_bigr (fun x => snd x)); last first.
{
intro i; rewrite andbT; intro IN.
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
have GE_COST := edf_claimed_bounds_ge_cost ts (max_steps ts).
fold (f (max_steps ts)) in GE_COST.
by destruct i; apply GE_COST.
@@ -778,7 +778,7 @@ Module ResponseTimeIterationEDF.
rewrite (eq_bigr (fun x => task_deadline x)); last first.
{
intro i; rewrite andbT; intro IN.
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
by specialize (VALID i IN); des.
}
rewrite -2!big_seq_cond.
diff --git a/classic/analysis/global/basic/bertogna_edf_theory.v b/classic/analysis/global/basic/bertogna_edf_theory.v
index 06d39c254817a3d0d7ab2aa1a6e0a9071e6d7ae6..79b5faec63a6ba26f9063766026afa812957cf7c 100644
--- a/classic/analysis/global/basic/bertogna_edf_theory.v
+++ b/classic/analysis/global/basic/bertogna_edf_theory.v
@@ -231,7 +231,7 @@ Module ResponseTimeAnalysisEDF.
unfold completed, valid_sporadic_job in *.
unfold X, total_interference; rewrite addn1.
rewrite -(ltn_add2r (task_cost tsk)).
- rewrite subh1; last by rewrite [R](REC tsk) // leq_addr.
+ rewrite addnBAC; last by rewrite [R](REC tsk) // leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite -ltnNge in NOTCOMP.
@@ -680,7 +680,7 @@ Module ResponseTimeAnalysisEDF.
apply ltn_div_trunc with (d := num_cpus); first by apply H_at_least_one_cpu.
rewrite -(ltn_add2l (task_cost tsk)) -REC; last by done.
rewrite -addn1 -leq_subLR.
- rewrite -[R + 1 - _]subh1; last by apply GE_COST.
+ rewrite -[R + 1 - _]addnBAC; last by apply GE_COST.
rewrite leq_divRL; last by apply H_at_least_one_cpu.
apply EXCEEDS.
apply leq_trans with (n := X * num_cpus);
@@ -806,4 +806,4 @@ Module ResponseTimeAnalysisEDF.
End ResponseTimeBound.
-End ResponseTimeAnalysisEDF.
\ No newline at end of file
+End ResponseTimeAnalysisEDF.
diff --git a/classic/analysis/global/basic/bertogna_fp_comp.v b/classic/analysis/global/basic/bertogna_fp_comp.v
index 58c6e1c1aa44335f361c66308d996b68a4d13f28..e87a8263112d8aa52d0163ea5adc67829d5f27c5 100644
--- a/classic/analysis/global/basic/bertogna_fp_comp.v
+++ b/classic/analysis/global/basic/bertogna_fp_comp.v
@@ -408,7 +408,7 @@ Module ResponseTimeIterationFP.
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
induction k.
{
- intros _; rewrite add0n -addn1 subh1;
+ intros _; rewrite add0n -addn1 addnBAC;
first by rewrite -addnBA // subnn addn0 /= leqnn.
by apply PARAMS.
}
@@ -418,7 +418,7 @@ Module ResponseTimeIterationFP.
apply leq_ltn_trans with (n := f k); last by apply INC, ltnW.
rewrite -addn1 -addnA [1 + _]addnC addnA -addnBA // subnn addn0.
rewrite -(ltn_add2r 1) in IHk.
- rewrite subh1 in IHk;
+ rewrite addnBAC in IHk;
last by apply leq_trans with (n := task_cost tsk);
[by apply PARAMS | by apply leq_addl].
by rewrite -addnBA // subnn addn0 addn1 ltnS in IHk.
@@ -459,7 +459,7 @@ Module ResponseTimeIterationFP.
exploit TOOMUCH; [by apply DIFF | by apply leq_addr |].
exploit (TASK_PARAMS tsk);
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
- rewrite subh1; last by apply PARAMS2.
+ rewrite addnBAC; last by apply PARAMS2.
rewrite -addnBA // subnn addn0 subn1 prednK //.
intros LT; apply (leq_ltn_trans LT).
by rewrite /max_steps [_ - _ + 1]addn1; apply INC, leq_addr.
diff --git a/classic/analysis/global/basic/bertogna_fp_theory.v b/classic/analysis/global/basic/bertogna_fp_theory.v
index 5ed912a7fdf415154ccaba9597ae9c22a36b8c7a..2c0706715294950b68605a824f518bcb5d61ece9 100644
--- a/classic/analysis/global/basic/bertogna_fp_theory.v
+++ b/classic/analysis/global/basic/bertogna_fp_theory.v
@@ -239,7 +239,7 @@ Module ResponseTimeAnalysisFP.
unfold completed, valid_sporadic_job in *.
unfold X, total_interference; rewrite addn1.
rewrite -(ltn_add2r (task_cost tsk)).
- rewrite subh1; last by rewrite [R](REC) // leq_addr.
+ rewrite addnBAC; last by rewrite [R](REC) // leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite -ltnNge in NOTCOMP.
@@ -681,7 +681,7 @@ Module ResponseTimeAnalysisFP.
first by apply H_at_least_one_cpu.
rewrite -(ltn_add2l (task_cost tsk)) -REC.
rewrite -addn1 -leq_subLR.
- rewrite -[R + 1 - _]subh1; last by rewrite REC; apply leq_addr.
+ rewrite -[R + 1 - _]addnBAC; last by rewrite REC; apply leq_addr.
rewrite leq_divRL; last by apply H_at_least_one_cpu.
apply EXCEEDS.
apply leq_trans with (n := X * num_cpus); last by rewrite ALLBUSY.
@@ -784,4 +784,4 @@ Module ResponseTimeAnalysisFP.
End ResponseTimeBound.
-End ResponseTimeAnalysisFP.
\ No newline at end of file
+End ResponseTimeAnalysisFP.
diff --git a/classic/analysis/global/basic/interference_bound_edf.v b/classic/analysis/global/basic/interference_bound_edf.v
index 8956d8a19030decbdf42e74c16a1913912d05c60..d5a5f211c79fdcc73b28453a11662f4e67b11118 100644
--- a/classic/analysis/global/basic/interference_bound_edf.v
+++ b/classic/analysis/global/basic/interference_bound_edf.v
@@ -484,7 +484,7 @@ Module InterferenceBoundEDF.
(job_arrival0 := job_arrival); try (by done); apply leqnn.
}
{
- rewrite -(leq_add2r (D_k - R_k)) subh1 // -addnBA // subnn addn0.
+ rewrite -(leq_add2r (D_k - R_k)) addnBAC // -addnBA // subnn addn0.
assert (SUBST: D_k - R_k = \sum_(a_fst + R_k <= i < a_fst + D_k) 1).
{
rewrite big_const_nat iter_addn mul1n addn0.
@@ -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.
+ apply leq_subRL_impl.
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|].
@@ -827,7 +827,7 @@ Module InterferenceBoundEDF.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
by rewrite CURtsk.
}
- by rewrite subh3 // addnC /p_k -CURtsk.
+ by rewrite leq_subRL_impl // addnC /p_k -CURtsk.
Qed.
(* Using the lemma above, we prove that the ratio n_k is at least the number of
@@ -923,7 +923,7 @@ Module InterferenceBoundEDF.
rewrite addnBA; last by apply leq_trunc_div.
apply leq_trans with (n := R_k + D_i - (a_lst - a_fst)); last by apply leq_sub2l.
rewrite subnBA; last by apply interference_bound_edf_j_fst_before_j_lst.
- rewrite -(leq_add2r a_lst) subh1; last first.
+ rewrite -(leq_add2r a_lst) addnBAC; last first.
{
apply leq_trans with (n := t2);
[by apply ltnW, interference_bound_edf_last_job_arrives_before_end_of_interval|].
@@ -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.
- by rewrite -subndiv_eq_mod; apply subh3.
+ apply leq_subRL_impl.
+ by rewrite -subndiv_eq_mod; apply leq_subRL_impl.
Qed.
(* Next, we prove that interference caused by j_fst is bounded by the length
@@ -1197,4 +1197,4 @@ Module InterferenceBoundEDF.
End MonotonicitySpecificBound.
-End InterferenceBoundEDF.
\ No newline at end of file
+End InterferenceBoundEDF.
diff --git a/classic/analysis/global/basic/workload_bound.v b/classic/analysis/global/basic/workload_bound.v
index 833da314873b5e5fb1a36d828ca34d7cc958aa07..178b7e5c884d3366dbc3f5a9b8a968f1a6363ab3 100644
--- a/classic/analysis/global/basic/workload_bound.v
+++ b/classic/analysis/global/basic/workload_bound.v
@@ -483,7 +483,7 @@ Module WorkloadBound.
have lemma1 := workload_bound_last_job_arrives_before_end_of_interval.
have lemma2 := workload_bound_response_time_of_first_job_inside_interval.
rewrite addnBA; last by apply ltnW.
- rewrite subh1 // -addnBA; last by apply leq_addr.
+ rewrite addnBAC // -addnBA; last by apply leq_addr.
rewrite addnC [job_arrival _ + _]addnC.
unfold t2; rewrite [t1 + _]addnC -[delta + t1 - _]subnBA // subnn subn0.
rewrite addnA -subnBA; first by ins.
@@ -556,7 +556,7 @@ Module WorkloadBound.
by rewrite sort_uniq -/scheduled_jobs filter_uniq // undup_uniq.
by rewrite CURtsk.
}
- by rewrite subh3 // addnC -CURtsk.
+ by rewrite leq_subRL_impl // addnC -CURtsk.
Qed.
(* Prove that n_k is at least the number of the middle jobs *)
@@ -580,7 +580,7 @@ Module WorkloadBound.
by apply workload_bound_many_periods_in_between.
}
rewrite <- leq_add2r with (p := job_arrival j_fst) in DISTmax.
- rewrite addnC subh1 in DISTmax; last first.
+ rewrite addnC addnBAC in DISTmax; last first.
{
unfold j_fst, j_lst; rewrite -[_.+1]add0n.
apply prev_le_next; last by rewrite H_at_least_two_jobs add0n leqnn.
@@ -740,4 +740,4 @@ Module WorkloadBound.
End ProofWorkloadBound.
-End WorkloadBound.
\ No newline at end of file
+End WorkloadBound.
diff --git a/classic/analysis/global/jitter/bertogna_edf_comp.v b/classic/analysis/global/jitter/bertogna_edf_comp.v
index 20605b30a2f8db16eb6e85cf70a155459f3918fb..ac4e387c97daf422f044a9b4c131c753eb1c89c1 100755
--- a/classic/analysis/global/jitter/bertogna_edf_comp.v
+++ b/classic/analysis/global/jitter/bertogna_edf_comp.v
@@ -704,7 +704,7 @@ Module ResponseTimeIterationEDF.
rewrite (eq_bigr (fun i => snd i)); last first.
{
intro i; rewrite andbT; intro IN;
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
have GE_COST := edf_claimed_bounds_ge_cost ts step.
by destruct i; apply GE_COST.
}
@@ -712,7 +712,7 @@ Module ResponseTimeIterationEDF.
{
intro i; rewrite andbT; intro IN.
unfold update_bound; destruct i; simpl.
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
apply (edf_claimed_bounds_ge_cost ts step.+1).
by rewrite iterS; apply/mapP; exists (s, t).
}
@@ -824,7 +824,7 @@ Module ResponseTimeIterationEDF.
rewrite (eq_bigr (fun x => snd x)); last first.
{
intro i; rewrite andbT; intro IN.
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
have GE_COST := edf_claimed_bounds_ge_cost ts (max_steps ts).
fold (f (max_steps ts)) in GE_COST.
by destruct i; apply GE_COST.
@@ -832,7 +832,7 @@ Module ResponseTimeIterationEDF.
rewrite (eq_bigr (fun x => task_deadline x)); last first.
{
intro i; rewrite andbT; intro IN.
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
by specialize (VALID i IN); des.
}
rewrite -2!big_seq_cond.
diff --git a/classic/analysis/global/jitter/bertogna_edf_theory.v b/classic/analysis/global/jitter/bertogna_edf_theory.v
index 02511f7478cd7eb159a852846abcb64711b14ce7..99e44750db46a2b25576bfdcd27c3ad10843faa8 100644
--- a/classic/analysis/global/jitter/bertogna_edf_theory.v
+++ b/classic/analysis/global/jitter/bertogna_edf_theory.v
@@ -247,7 +247,7 @@ Module ResponseTimeAnalysisEDFJitter.
unfold completed, valid_sporadic_job_with_jitter, valid_sporadic_job in *.
unfold X, total_interference; rewrite addn1.
rewrite -(ltn_add2r (task_cost tsk)).
- rewrite subh1; last by rewrite [R](REC tsk) // leq_addr.
+ rewrite addnBAC; last by rewrite [R](REC tsk) // leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite -ltnNge in NOTCOMP.
@@ -720,7 +720,7 @@ Module ResponseTimeAnalysisEDFJitter.
apply ltn_div_trunc with (d := num_cpus); first by apply H_at_least_one_cpu.
rewrite -(ltn_add2l (task_cost tsk)) -REC; last by done.
rewrite -addn1 -leq_subLR.
- rewrite -[R + 1 - _]subh1; last by apply GE_COST.
+ rewrite -[R + 1 - _]addnBAC; last by apply GE_COST.
rewrite leq_divRL; last by apply H_at_least_one_cpu.
apply EXCEEDS.
apply leq_trans with (n := X * num_cpus); last by rewrite ALLBUSY.
@@ -855,4 +855,4 @@ Module ResponseTimeAnalysisEDFJitter.
End ResponseTimeBound.
-End ResponseTimeAnalysisEDFJitter.
\ No newline at end of file
+End ResponseTimeAnalysisEDFJitter.
diff --git a/classic/analysis/global/jitter/bertogna_fp_comp.v b/classic/analysis/global/jitter/bertogna_fp_comp.v
index 5f1f67c5270cd2e3cb3a467ae09ebccdab4633f1..ced62fb7ed300515b7292f38d1d9dda9672221b8 100644
--- a/classic/analysis/global/jitter/bertogna_fp_comp.v
+++ b/classic/analysis/global/jitter/bertogna_fp_comp.v
@@ -408,7 +408,7 @@ Module ResponseTimeIterationFP.
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
induction k.
{
- intros _; rewrite add0n -addn1 subh1;
+ intros _; rewrite add0n -addn1 addnBAC;
first by rewrite -addnBA // subnn addn0 /= leqnn.
by apply PARAMS.
}
@@ -419,7 +419,7 @@ Module ResponseTimeIterationFP.
last by apply INC, ltnW.
rewrite -addn1 -addnA [1 + _]addnC addnA -addnBA // subnn addn0.
rewrite -(ltn_add2r 1) in IHk.
- rewrite subh1 in IHk;
+ rewrite addnBAC in IHk;
last by apply leq_trans with (n := task_cost tsk);
[by apply PARAMS | by apply leq_addl].
by rewrite -addnBA // subnn addn0 addn1 ltnS in IHk.
@@ -460,7 +460,7 @@ Module ResponseTimeIterationFP.
exploit TOOMUCH; [by apply DIFF | by apply leq_addr |].
exploit (TASK_PARAMS tsk);
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
- rewrite subh1; last by apply PARAMS2.
+ rewrite addnBAC; last by apply PARAMS2.
rewrite -addnBA // subnn addn0 subn1 prednK //.
intros LT; apply (leq_ltn_trans LT).
by rewrite /max_steps [_ - _ + 1]addn1; apply INC, leq_addr.
diff --git a/classic/analysis/global/jitter/bertogna_fp_theory.v b/classic/analysis/global/jitter/bertogna_fp_theory.v
index 17c1aa647e7a21b7412ac6e93ec5ae41cca23826..70af2a72be2ffebc61fe806a513752afb8cc9858 100644
--- a/classic/analysis/global/jitter/bertogna_fp_theory.v
+++ b/classic/analysis/global/jitter/bertogna_fp_theory.v
@@ -252,7 +252,7 @@ Module ResponseTimeAnalysisFP.
unfold completed, valid_sporadic_job_with_jitter, valid_sporadic_job in *.
unfold X, total_interference; rewrite addn1.
rewrite -(ltn_add2r (task_cost tsk)).
- rewrite subh1; last by rewrite [R](REC) // leq_addr.
+ rewrite addnBAC; last by rewrite [R](REC) // leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite -ltnNge in NOTCOMP.
@@ -723,7 +723,7 @@ Module ResponseTimeAnalysisFP.
unfold div_floor in REC.
rewrite -(ltn_add2l (task_cost tsk)) -REC.
rewrite -addn1 -leq_subLR.
- rewrite -[R + 1 - _]subh1; last by rewrite REC; apply leq_addr.
+ rewrite -[R + 1 - _]addnBAC; last by rewrite REC; apply leq_addr.
rewrite leq_divRL; last by apply H_at_least_one_cpu.
apply EXCEEDS.
apply leq_trans with (n := X * num_cpus); last by rewrite ALLBUSY.
@@ -827,4 +827,4 @@ Module ResponseTimeAnalysisFP.
End ResponseTimeBound.
-End ResponseTimeAnalysisFP.
\ No newline at end of file
+End ResponseTimeAnalysisFP.
diff --git a/classic/analysis/global/jitter/interference_bound_edf.v b/classic/analysis/global/jitter/interference_bound_edf.v
index a279e9f62e0631881a488c0df859ee3165b71616..e1ecadb16ec94943c2333625fba00ffd633310b2 100644
--- a/classic/analysis/global/jitter/interference_bound_edf.v
+++ b/classic/analysis/global/jitter/interference_bound_edf.v
@@ -508,7 +508,7 @@ Module InterferenceBoundEDFJitter.
apply leq_trans with (n := job_interference job_arrival job_cost job_jitter sched j_i j_fst a_i t2);
first by apply extend_sum; [by apply leq_addr | by apply leqnn].
- rewrite -(leq_add2r (D_k - R_k - J_k)) subh1 // -addnBA // subnn addn0.
+ rewrite -(leq_add2r (D_k - R_k - J_k)) addnBAC // -addnBA // subnn addn0.
assert (SUBST: D_k - R_k - J_k = \sum_(a_fst + J_k + R_k <= i < a_fst + D_k) 1).
{
@@ -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.
+ apply leq_subRL_impl.
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)).
{
@@ -920,7 +920,7 @@ Module InterferenceBoundEDFJitter.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
by rewrite CURtsk.
}
- by rewrite subh3 // addnC /p_k -INnth.
+ by rewrite leq_subRL_impl // addnC /p_k -INnth.
Qed.
(* Using the lemma above, we prove that the ratio n_k is at least the number of
@@ -1021,7 +1021,7 @@ Module InterferenceBoundEDFJitter.
rewrite addnBA; last by apply leq_trunc_div.
apply leq_trans with (n := J_k + R_k + D_i - (a_lst - a_fst)); last by apply leq_sub2l.
rewrite subnBA; last by apply interference_bound_edf_j_fst_before_j_lst.
- rewrite -(leq_add2r a_lst) subh1; last first.
+ rewrite -(leq_add2r a_lst) addnBAC; last first.
{
apply leq_trans with (n := t2);
[by apply ltnW, interference_bound_edf_last_job_arrives_before_end_of_interval|].
@@ -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.
- by rewrite -subndiv_eq_mod; apply subh3.
+ apply leq_subRL_impl.
+ by rewrite -subndiv_eq_mod; apply leq_subRL_impl.
Qed.
(* Next, we prove that interference caused by j_fst is bounded by the length
@@ -1302,4 +1302,4 @@ Module InterferenceBoundEDFJitter.
End MonotonicitySpecificBound.
-End InterferenceBoundEDFJitter.
\ No newline at end of file
+End InterferenceBoundEDFJitter.
diff --git a/classic/analysis/global/jitter/workload_bound.v b/classic/analysis/global/jitter/workload_bound.v
index 2e7309f0b820ec6a48412b1db4e042d1d39e900b..68a0619f6775f12697ec0864b3df78f99011aba0 100644
--- a/classic/analysis/global/jitter/workload_bound.v
+++ b/classic/analysis/global/jitter/workload_bound.v
@@ -488,7 +488,7 @@ Module WorkloadBoundJitter.
have lemma1 := workload_bound_last_job_arrives_before_end_of_interval.
have lemma2 := workload_bound_response_time_of_first_job_inside_interval.
rewrite addnBA; last by apply ltnW.
- rewrite subh1; last by done.
+ rewrite addnBAC; last by done.
rewrite -addnBA; last by apply leq_addr.
rewrite addnC; unfold t2.
@@ -571,7 +571,7 @@ Module WorkloadBoundJitter.
by rewrite sort_uniq -/scheduled_jobs filter_uniq // undup_uniq.
by rewrite CURtsk NEXTtsk.
}
- by rewrite subh3 // addnC -CURtsk.
+ by rewrite leq_subRL_impl // addnC -CURtsk.
Qed.
(* Prove that n_k is at least the number of the middle jobs *)
@@ -595,7 +595,7 @@ Module WorkloadBoundJitter.
by apply workload_bound_many_periods_in_between.
}
rewrite <- leq_add2r with (p := job_arrival j_fst) in DISTmax.
- rewrite addnC subh1 in DISTmax; last first.
+ rewrite addnC addnBAC in DISTmax; last first.
{
unfold j_fst, j_lst; rewrite -[_.+1]add0n.
apply prev_le_next; last by rewrite H_at_least_two_jobs add0n leqnn.
@@ -769,4 +769,4 @@ Module WorkloadBoundJitter.
End ProofWorkloadBound.
-End WorkloadBoundJitter.
\ No newline at end of file
+End WorkloadBoundJitter.
diff --git a/classic/analysis/global/parallel/bertogna_edf_comp.v b/classic/analysis/global/parallel/bertogna_edf_comp.v
index efda9be790a99c0651a3ca806c2271bccf8a676d..3006502d987d9e919dab8ffcce85f1165f4f4d69 100755
--- a/classic/analysis/global/parallel/bertogna_edf_comp.v
+++ b/classic/analysis/global/parallel/bertogna_edf_comp.v
@@ -646,7 +646,7 @@ Module ResponseTimeIterationEDF.
rewrite (eq_bigr (fun i => snd i)); last first.
{
intro i; rewrite andbT; intro IN;
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
have GE_COST := edf_claimed_bounds_ge_cost ts step.
by destruct i; apply GE_COST.
}
@@ -654,7 +654,7 @@ Module ResponseTimeIterationEDF.
{
intro i; rewrite andbT; intro IN.
unfold update_bound; destruct i; simpl.
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
apply (edf_claimed_bounds_ge_cost ts step.+1).
by rewrite iterS; apply/mapP; exists (s, t).
}
@@ -765,7 +765,7 @@ Module ResponseTimeIterationEDF.
rewrite (eq_bigr (fun x => snd x)); last first.
{
intro i; rewrite andbT; intro IN.
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
have GE_COST := edf_claimed_bounds_ge_cost ts (max_steps ts).
fold (f (max_steps ts)) in GE_COST.
by destruct i; apply GE_COST.
@@ -773,7 +773,7 @@ Module ResponseTimeIterationEDF.
rewrite (eq_bigr (fun x => task_deadline x)); last first.
{
intro i; rewrite andbT; intro IN.
- rewrite subh1; first by rewrite -addnBA // subnn addn0.
+ rewrite addnBAC; first by rewrite -addnBA // subnn addn0.
by specialize (VALID i IN); des.
}
rewrite -2!big_seq_cond.
diff --git a/classic/analysis/global/parallel/bertogna_edf_theory.v b/classic/analysis/global/parallel/bertogna_edf_theory.v
index 5e3b7051ef426e1f8ebfa2aa6f3e80a7a3e75807..3604a3cca1bcb19312b0576f5481be35925db26e 100644
--- a/classic/analysis/global/parallel/bertogna_edf_theory.v
+++ b/classic/analysis/global/parallel/bertogna_edf_theory.v
@@ -231,7 +231,7 @@ Module ResponseTimeAnalysisEDF.
unfold completed, valid_sporadic_job in *.
unfold X, total_interference; rewrite addn1.
rewrite -(ltn_add2r (task_cost tsk)).
- rewrite subh1; last by rewrite [R](REC tsk) // leq_addr.
+ rewrite addnBAC; last by rewrite [R](REC tsk) // leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite -ltnNge in NOTCOMP.
@@ -379,7 +379,7 @@ Module ResponseTimeAnalysisEDF.
apply ltn_div_trunc with (d := num_cpus); first by apply H_at_least_one_cpu.
rewrite -(ltn_add2l (task_cost tsk)) -REC; last by done.
rewrite -addn1 -leq_subLR.
- rewrite -[R + 1 - _]subh1; last by apply GE_COST.
+ rewrite -[R + 1 - _]addnBAC; last by apply GE_COST.
rewrite leq_divRL; last by apply H_at_least_one_cpu.
rewrite ALLBUSY.
by rewrite leq_mul2r; apply/orP; right; apply TOOMUCH.
@@ -492,4 +492,4 @@ Module ResponseTimeAnalysisEDF.
End ResponseTimeBound.
-End ResponseTimeAnalysisEDF.
\ No newline at end of file
+End ResponseTimeAnalysisEDF.
diff --git a/classic/analysis/global/parallel/bertogna_fp_comp.v b/classic/analysis/global/parallel/bertogna_fp_comp.v
index 7310318945e4a0678bb8dfe3e2c0c8892dd0bf93..aca334eb937788bb97a2c2871b3e58780811fed9 100644
--- a/classic/analysis/global/parallel/bertogna_fp_comp.v
+++ b/classic/analysis/global/parallel/bertogna_fp_comp.v
@@ -398,7 +398,7 @@ Module ResponseTimeIterationFP.
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
induction k.
{
- intros _; rewrite add0n -addn1 subh1;
+ intros _; rewrite add0n -addn1 addnBAC;
first by rewrite -addnBA // subnn addn0 /= leqnn.
by apply PARAMS.
}
@@ -408,7 +408,7 @@ Module ResponseTimeIterationFP.
apply leq_ltn_trans with (n := f k); last by apply INC, ltnW.
rewrite -addn1 -addnA [1 + _]addnC addnA -addnBA // subnn addn0.
rewrite -(ltn_add2r 1) in IHk.
- rewrite subh1 in IHk;
+ rewrite addnBAC in IHk;
last by apply leq_trans with (n := task_cost tsk);
[by apply PARAMS | by apply leq_addl].
by rewrite -addnBA // subnn addn0 addn1 ltnS in IHk.
@@ -449,7 +449,7 @@ Module ResponseTimeIterationFP.
exploit TOOMUCH; [by apply DIFF | by apply leq_addr |].
exploit (TASK_PARAMS tsk);
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
- rewrite subh1; last by apply PARAMS2.
+ rewrite addnBAC; last by apply PARAMS2.
rewrite -addnBA // subnn addn0 subn1 prednK //.
intros LT; apply (leq_ltn_trans LT).
by rewrite /max_steps [_ - _ + 1]addn1; apply INC, leq_addr.
diff --git a/classic/analysis/global/parallel/bertogna_fp_theory.v b/classic/analysis/global/parallel/bertogna_fp_theory.v
index 97444465bfc0834f058f614610dde0fc9e69dc16..0dc7ebf46f51c213d288a1abdef3b4215971d6b4 100644
--- a/classic/analysis/global/parallel/bertogna_fp_theory.v
+++ b/classic/analysis/global/parallel/bertogna_fp_theory.v
@@ -225,7 +225,7 @@ Module ResponseTimeAnalysisFP.
unfold completed, valid_sporadic_job in *.
unfold X, total_interference; rewrite addn1.
rewrite -(ltn_add2r (task_cost tsk)).
- rewrite subh1; last by rewrite REC leq_addr.
+ rewrite addnBAC; last by rewrite REC leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite -ltnNge in NOTCOMP.
@@ -374,7 +374,7 @@ Module ResponseTimeAnalysisFP.
first by apply H_at_least_one_cpu.
rewrite -(ltn_add2l (task_cost tsk)) -REC.
rewrite -addn1 -leq_subLR.
- rewrite -[R + 1 - _]subh1; last by rewrite REC; apply leq_addr.
+ rewrite -[R + 1 - _]addnBAC; last by rewrite REC; apply leq_addr.
rewrite leq_divRL; last by apply H_at_least_one_cpu.
rewrite ALLBUSY.
by rewrite leq_mul2r; apply/orP; right; apply TOOMUCH.
diff --git a/classic/analysis/global/parallel/interference_bound_edf.v b/classic/analysis/global/parallel/interference_bound_edf.v
index a20bc4299298f6234296d3c0ecfc44e53b38b15b..a4cdcb5f72da4335839c4fc6b345b35edac836bf 100644
--- a/classic/analysis/global/parallel/interference_bound_edf.v
+++ b/classic/analysis/global/parallel/interference_bound_edf.v
@@ -638,7 +638,7 @@ Module InterferenceBoundEDF.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
by rewrite CURtsk.
}
- by rewrite subh3 // addnC /p_k -CURtsk.
+ by rewrite leq_subRL_impl // addnC /p_k -CURtsk.
Qed.
Lemma interference_bound_edf_slack_le_delta:
@@ -688,13 +688,13 @@ Module InterferenceBoundEDF.
- by rewrite -addn1; apply ltnW, ltn_ceil.
}
rewrite leq_subLR in SLACK.
- rewrite -(leq_add2r a_fst) subh1 in BUG;
+ rewrite -(leq_add2r a_fst) addnBAC in BUG;
last by apply interference_bound_edf_j_fst_before_j_lst.
rewrite -[a_lst + _ - _]subnBA // subnn subn0 in BUG.
rewrite addnC addnS in BUG.
rewrite addnBA // in BUG; last by rewrite addnC.
rewrite -(ltn_add2r D_k) in BUG.
- rewrite subh1 in BUG; last first.
+ rewrite addnBAC in BUG; last first.
{
rewrite [D_i + R_k]addnC.
by apply leq_trans with (n := R_k + D_i);
@@ -830,4 +830,4 @@ Module InterferenceBoundEDF.
End MonotonicitySpecificBound.
-End InterferenceBoundEDF.
\ No newline at end of file
+End InterferenceBoundEDF.
diff --git a/classic/analysis/global/parallel/workload_bound.v b/classic/analysis/global/parallel/workload_bound.v
index 9dd7fa8e2a0d2bde64dac0e63d5c6806264ddfca..fb000bd0f0bd06b167adcbf814a83e7286812319 100644
--- a/classic/analysis/global/parallel/workload_bound.v
+++ b/classic/analysis/global/parallel/workload_bound.v
@@ -416,7 +416,7 @@ Module WorkloadBound.
by rewrite sort_uniq -/scheduled_jobs filter_uniq // undup_uniq.
by rewrite CURtsk.
}
- by rewrite subh3 // addnC -CURtsk.
+ by rewrite leq_subRL_impl // addnC -CURtsk.
Qed.
(* Next, we prove that n_k covers every scheduled job, ... *)
@@ -441,7 +441,7 @@ Module WorkloadBound.
by apply ltnW, ltn_ceil, PARAMS0.
}
rewrite <- leq_add2r with (p := job_arrival j_fst) in DISTmax.
- rewrite addnC subh1 in DISTmax; last first.
+ rewrite addnC addnBAC in DISTmax; last first.
{
unfold j_fst, j_lst; rewrite -[_.+1]add0n.
apply prev_le_next; last by rewrite H_at_least_two_jobs add0n leqnn.
@@ -526,4 +526,4 @@ Module WorkloadBound.
End ProofWorkloadBound.
-End WorkloadBound.
\ No newline at end of file
+End WorkloadBound.
diff --git a/classic/analysis/uni/basic/tdma_wcrt_analysis.v b/classic/analysis/uni/basic/tdma_wcrt_analysis.v
index 4c53d9cf3ed9d00d16c6dcd89f53b823a2b57390..0ee56ff9d97b13c3a181fca53dc71de7a7dcd091 100644
--- a/classic/analysis/uni/basic/tdma_wcrt_analysis.v
+++ b/classic/analysis/uni/basic/tdma_wcrt_analysis.v
@@ -812,7 +812,7 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
+ have F:in_time_slot_at (job_arrival j) = false by auto. rewrite F.
rewrite /to_next_slot EXISTS /duration_to_finish_from_start_of_slot_with.
rewrite mulnBl mul1n addnA {1}gtn_eqF // -COST_WCET.
- apply /eqP. rewrite eqn_add2r addnC subh1.
+ apply /eqP. rewrite eqn_add2r addnC addnBAC.
* by rewrite addnK.
* by apply leq_pmull, ceil_neq0.
Qed.
diff --git a/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v b/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v
index c6a1e0372f1418a54584d5711416a27d23cbf4cf..83a02d312f57e474be4884500f605c3c23984942 100644
--- a/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v
+++ b/classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v
@@ -751,7 +751,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 //.
+ rewrite leq_subRL_impl //.
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.
@@ -1102,7 +1102,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 //.
+ rewrite leq_subRL_impl //.
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/classic/analysis/uni/susp/sustainability/singlecost/reduction_properties.v b/classic/analysis/uni/susp/sustainability/singlecost/reduction_properties.v
index 5972733d96dd62aefbf0ec13f03a348d1a357653..d49674b477e3e7c727a757f0a60e68ffe533e39b 100644
--- a/classic/analysis/uni/susp/sustainability/singlecost/reduction_properties.v
+++ b/classic/analysis/uni/susp/sustainability/singlecost/reduction_properties.v
@@ -721,7 +721,7 @@ 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 //.
+ rewrite addn0 leq_subRL_impl //.
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.
diff --git a/classic/model/policy_tdma.v b/classic/model/policy_tdma.v
index 5cd2450f99fe958160997a1ae32b7330d02b3bf7..5d6bd08fb6c7cb768332a1378d4ac6c2e91e2737 100644
--- a/classic/model/policy_tdma.v
+++ b/classic/model/policy_tdma.v
@@ -198,7 +198,7 @@ Module PolicyTDMA.
have SO2:O2 + task_time_slot tsk2 <= cycle by apply (Offset_add_slot_leq_cycle tsk2).
repeat rewrite mod_elim;auto.
case (O1 <= t%%cycle)eqn:O1T;case (O2 <= t %%cycle)eqn:O2T;intros G1 G2;try ssrlia.
- apply util.nat.ltn_subLR in G1;apply util.nat.ltn_subLR in G2. case (tsk1==tsk2) eqn:NEQ;move/eqP in NEQ;auto.
+ rewrite ltn_subLR // in G1; rewrite ltn_subLR // in G2. case (tsk1==tsk2) eqn:NEQ;move/eqP in NEQ;auto.
destruct (slot_order_total tsk1 tsk2) as [order |order];auto;apply relation_offset in order;
fold O1 O2 in order;try ssrlia;auto. by move/eqP in NEQ. apply /eqP;auto.
Qed.
diff --git a/classic/model/schedule/uni/basic/platform.v b/classic/model/schedule/uni/basic/platform.v
index e616cbde28c065389e73797e85b8f7d594a5f67c..959fd1047abd51b567d2e21b1de92f0cf7527eee 100644
--- a/classic/model/schedule/uni/basic/platform.v
+++ b/classic/model/schedule/uni/basic/platform.v
@@ -178,7 +178,7 @@ Module Platform.
first by apply leq_sum; ins; apply leq_b1.
simpl_sum_const; rewrite -(ltn_add2r 1).
rewrite [job_cost j + 1]addn1 ltnS.
- by rewrite subh1 // leq_subLR addn1.
+ by rewrite addnBAC // leq_subLR addn1.
Qed.
End JobNeverBacklogged.
diff --git a/classic/model/schedule/uni/limited/abstract_RTA/abstract_rta.v b/classic/model/schedule/uni/limited/abstract_RTA/abstract_rta.v
index ede0c4c24519f5da18fbb0f9e6b16bdde7e52b7f..6da35e3635ce2862adc7703184df914e74955e96 100644
--- a/classic/model/schedule/uni/limited/abstract_RTA/abstract_rta.v
+++ b/classic/model/schedule/uni/limited/abstract_RTA/abstract_rta.v
@@ -309,13 +309,13 @@ Module AbstractRTA.
apply leq_trans with (F_sp - optimism + job_last ); first by rewrite leq_add2r leq_sub2r.
apply leq_trans with (F_sp + (task_cost tsk - task_lock_in_service tsk)); last by done.
rewrite /optimism subnBA; last by apply PRT2.
- rewrite -subh1 //.
+ rewrite -addnBAC //.
rewrite /job_last.
rewrite addnBA; last by auto.
- rewrite -subh1; last by rewrite leq_addl.
+ rewrite -addnBAC; last by rewrite leq_addl.
rewrite -addnBA // subnn addn0.
rewrite addnBA; last by auto.
- rewrite subh1; last by done.
+ rewrite addnBAC; last by done.
rewrite leq_sub2r // leq_add2l.
by rewrite -H_job_of_tsk; apply H_job_cost_le_task_cost.
}
@@ -333,7 +333,7 @@ Module AbstractRTA.
feed_n 7 ESERV; eauto 2.
{ rewrite {2}FIX2.
rewrite /AbstractRTADefinitions.cumul_interference.
- rewrite -[in X in _ <= X]subh1; last by rewrite leq_subr.
+ rewrite -[in X in _ <= X]addnBAC; last by rewrite leq_subr.
rewrite {2}/optimism.
rewrite subKn; last by auto.
rewrite leq_add2l.
diff --git a/classic/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v b/classic/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
index 8ef8bba69bc3cb619bbccae009ec9a2b59d6d403..90d1e133d40b902004b5acbf27ff6d59a8a338a1 100644
--- a/classic/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
+++ b/classic/model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
@@ -154,7 +154,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 in BOUND.
+ apply leq_subRL_impl 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/classic/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v b/classic/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
index 3811b6c30c9e9a1cf47b09ba09866ccd037054b0..bbe2677bacc9e06c839ff3e1d4ec7e688d25c4ef 100644
--- a/classic/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
@@ -393,7 +393,7 @@ Module RTAforConcreteModels.
have EQ: exists Δ, t' = t + Δ.
{ exists (t' - t); rewrite subnKC; by done. }
move: EQ => [Δ EQ]; subst t'; clear LE.
- rewrite -subh1 in LS.
+ rewrite -addnBAC in LS.
rewrite addn1 in LS.
apply H_schedule_with_limited_preemptions; first by done.
rewrite /can_be_preempted_for_model_with_limited_preemptions; apply/negP.
@@ -442,7 +442,7 @@ Module RTAforConcreteModels.
rewrite -(ltn_add2r 1) !addn1 prednK //.
move: (Fact2) => Fact3.
rewrite size_of_seq_of_distances // addn1 ltnS // in Fact2.
- rewrite -subh1 -?[in X in _ <= X]subh1; first last.
+ rewrite -addnBAC -?[in X in _ <= X]addnBAC; first last.
{ apply leq_trans with (job_max_nps j).
- by apply last_of_seq_le_max_of_seq.
- by rewrite -ENDj //; apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
@@ -574,7 +574,7 @@ Module RTAforConcreteModels.
have EQ: exists Δ, t' = t + Δ.
{ exists (t' - t); rewrite subnKC; by done. }
move: EQ => [Δ EQ]; subst t'; clear LE.
- rewrite -subh1 in LS.
+ rewrite -addnBAC in LS.
rewrite addn1 in LS.
apply H_schedule_with_limited_preemptions; first by done.
rewrite /can_be_preempted_for_model_with_limited_preemptions; apply/negP.
diff --git a/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v b/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
index 94345334f21a2c09108a43017fe170c326a4a012..b595a2b20f7d343aedd458f33e91557764fc8944 100644
--- a/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
@@ -219,13 +219,11 @@ Module RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
have F: forall a b c d, a + b < c + d -> a > c -> b < d.
{ clear.
intros.
- rewrite -addn1 -addnA -leq_subLR -subh1 in H; last by apply ltnW.
+ rewrite -addn1 -addnA -leq_subLR -addnBAC in H; last by apply ltnW.
rewrite addn1 addnS in H.
rewrite -subn_gt0 in H0.
apply ltn_trans with (a - c + b); last by done.
- apply util.nat.ltn_subLR.
- have EQ: b - b = 0. apply/eqP. rewrite subn_eq0. by done.
- by rewrite EQ.
+ ssrlia.
}
eapply F; eauto 2.
}
@@ -341,4 +339,4 @@ Module RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
End Analysis.
-End RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
\ No newline at end of file
+End RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
diff --git a/classic/model/schedule/uni/limited/edf/response_time_bound.v b/classic/model/schedule/uni/limited/edf/response_time_bound.v
index 36bcbd570bfc29ff8b8f6b4abb09153420771c07..1fe0594a048466a218a5f3a9d3ecc91e4d603860 100644
--- a/classic/model/schedule/uni/limited/edf/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/edf/response_time_bound.v
@@ -455,7 +455,7 @@ Module AbstractRTAforEDFwithArrivalCurves.
{ apply negbT in NEQ2; rewrite -ltnNge in NEQ2.
move: HEP; rewrite leqNgt; move => /negP HEP; apply: HEP.
apply leq_ltn_trans with (job_arrival jo + (job_arrival j - t1 + task_deadline tsk)).
- { rewrite subh1; last by done.
+ { rewrite addnBAC; last by done.
rewrite addnBA; last apply leq_trans with (job_arrival j); [ | by done | by rewrite leq_addr].
rewrite [in X in _ <= X]addnC.
rewrite -addnBA; first by rewrite leq_addr.
diff --git a/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v b/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
index d702ae98d3b4307417cf64d1f43f727f650db7e2..d49d5ecb76703f7bd0dc5bb38514e3553ae3cd2e 100644
--- a/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
+++ b/classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
@@ -369,7 +369,7 @@ Module RTAforConcreteModels.
have EQ: exists Δ, t' = t + Δ.
{ exists (t' - t); rewrite subnKC; by done. }
move: EQ => [Δ EQ]; subst t'; clear LE.
- rewrite -subh1 in LS.
+ rewrite -addnBAC in LS.
rewrite addn1 in LS.
apply H_schedule_with_limited_preemptions; first by done.
rewrite /can_be_preempted_for_model_with_limited_preemptions; apply/negP.
@@ -419,7 +419,7 @@ Module RTAforConcreteModels.
rewrite -(ltn_add2r 1) !addn1 prednK //.
move: (Fact2) => Fact3.
rewrite size_of_seq_of_distances // addn1 ltnS // in Fact2.
- rewrite -subh1 -?[in X in _ <= X]subh1; first last.
+ rewrite -addnBAC -?[in X in _ <= X]addnBAC; first last.
{ apply leq_trans with (job_max_nps j).
- by apply last_of_seq_le_max_of_seq.
- by rewrite -ENDj //; apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
@@ -549,7 +549,7 @@ Module RTAforConcreteModels.
have EQ: exists Δ, t' = t + Δ.
{ exists (t' - t); rewrite subnKC; by done. }
move: EQ => [Δ EQ]; subst t'; clear LE.
- rewrite -subh1 in LS.
+ rewrite -addnBAC in LS.
rewrite addn1 in LS.
apply H_schedule_with_limited_preemptions; first by done.
rewrite /can_be_preempted_for_model_with_limited_preemptions; apply/negP.
diff --git a/classic/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v b/classic/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
index 02ada3aa8056b903bf7fee32271d2626779a4097..1ac018cda26363e98e8291de0c14252eb739a476 100644
--- a/classic/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
+++ b/classic/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 // addn1.
+ have TEMP: t <= t2.-1; first by rewrite -subn1 leq_subRL_impl // 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 in NEQ.
+ apply leq_subRL_impl in NEQ.
by rewrite subn1 in NEQ.
- apply leq_trans with t1. by apply leq_pred. by done.
}
diff --git a/classic/model/schedule/uni/nonpreemptive/schedule.v b/classic/model/schedule/uni/nonpreemptive/schedule.v
index f6fc8e52f0aaa8bc4ba75a826c5478cb053eb107..f157484058d2402c4e48d1555cdc43697284269c 100644
--- a/classic/model/schedule/uni/nonpreemptive/schedule.v
+++ b/classic/model/schedule/uni/nonpreemptive/schedule.v
@@ -114,7 +114,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).
- by apply subh3; first rewrite addn1.
+ by apply leq_subRL_impl; first rewrite addn1.
Qed.
End CompletionUnderNonpreemptive.
@@ -181,11 +181,11 @@ Module NonpreemptiveSchedule.
rewrite leq_sum //; intros; by destruct (scheduled_at sched j i).
simpl_sum_const. by done.
unfold job_remaining_cost, remaining_cost.
- rewrite -addn1 -addn1 subh1; first by
+ rewrite -addn1 -addn1 addnBAC; first by
by rewrite leq_subLR addnBA;
- first by rewrite -addnA [1+job_cost j]addnC addnA -subh1.
+ first by rewrite -addnA [1+job_cost j]addnC addnA -addnBAC.
{
- rewrite subh1; last by done.
+ rewrite addnBAC; last by done.
rewrite leq_subLR addnA.
rewrite addnBA; last by done.
rewrite [_+t]addnC [_+job_cost j]addnC addnA.
@@ -196,7 +196,7 @@ Module NonpreemptiveSchedule.
{
unfold remaining_cost.
rewrite addnBA; last by done.
- rewrite -addn1 subh1; last by done.
+ rewrite -addn1 addnBAC; last by done.
rewrite leq_subLR -addnBA; last by done.
rewrite addnA [_+t]addnC -addnA leq_add2l addnBA; last by done.
by rewrite addnC -addnBA; first by rewrite subnn addn0.
@@ -247,7 +247,7 @@ Module NonpreemptiveSchedule.
have LLF: t' < t - service sched j t.
{
by apply ltn_trans with (t - service sched j t - 1);
- last by rewrite -addn1 subh1 // -addnBA // subnn addn0.
+ last by rewrite -addn1 addnBAC // -addnBA // subnn addn0.
} clear LT.
rewrite !addnBA;
try(rewrite H_completed_jobs_dont_execute //).
@@ -257,7 +257,7 @@ Module NonpreemptiveSchedule.
rewrite -addnBA ?leq_add2l; last by done.
by apply leq_trans with (t' + 1 - 1);
rewrite addn1 subn1 -pred_Sn;
- [rewrite leq_subr | rewrite subh3 // addn1].
+ [rewrite leq_subr | rewrite leq_subRL_impl // addn1].
}
have L3 := job_doesnt_complete_before_remaining_cost job_cost sched
j H_completed_jobs_dont_execute t;
@@ -266,8 +266,8 @@ Module NonpreemptiveSchedule.
by move: L3 => /negP L3; apply L3.
}
rewrite /job_remaining_cost /remaining_cost T1 subn0 addnBA; last by done.
- rewrite -subh1.
- by rewrite -[(t-service sched j t) + _ - _]subh1.
+ rewrite -addnBAC.
+ by rewrite -[(t-service sched j t) + _ - _]addnBAC.
by rewrite cumulative_service_le_delta.
}
move: L1 => /neqP L1; apply: L1.
@@ -309,7 +309,7 @@ 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.
+ rewrite leq_subRL_impl // ?leq_add2l.
by rewrite scheduled_implies_positive_remaining_cost //.
Qed.
@@ -337,7 +337,7 @@ Module NonpreemptiveSchedule.
Proof.
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;
+ rewrite -addn1 in LE; apply leq_subRL_impl with (m := t') (n := 1) in LE;
apply continuity_of_nonpreemptive_scheduling with
(t1 := t - service sched j t)
(t2 := t + job_remaining_cost j t - 1); first by done.
@@ -352,4 +352,4 @@ Module NonpreemptiveSchedule.
End Definitions.
-End NonpreemptiveSchedule.
\ No newline at end of file
+End NonpreemptiveSchedule.
diff --git a/classic/util/div_mod.v b/classic/util/div_mod.v
index 4782e4b9d67b5b9c89a1ffc35fe196af051d2cba..1b7cfd089f699a8eea578e4c35501aed5a4db560 100644
--- a/classic/util/div_mod.v
+++ b/classic/util/div_mod.v
@@ -39,7 +39,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop d
{
exploit (@ltn_pmod n d); [by apply GT0 | intro LTd; fold y in LTd].
rewrite -(ltn_add2r 1) [y+1]addn1 ltnS in BUG.
- rewrite subh1 in BUG; last by apply GT0.
+ rewrite addnBAC in BUG; last by apply GT0.
rewrite -addnBA // subnn addn0 in BUG.
by apply (leq_ltn_trans BUG) in LTd; rewrite ltnn in LTd.
}
@@ -47,7 +47,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop d
{
(* Case 1: y = d - 1*)
move: GE => /eqP GE; rewrite -(eqn_add2r 1) in GE.
- rewrite subh1 in GE; last by apply GT0.
+ rewrite addnBAC in GE; last by apply GT0.
rewrite -addnBA // subnn addn0 in GE.
move: GE => /eqP GE.
apply f_equal with (f := fun x => x %/ d) in GE.
@@ -80,10 +80,10 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop d
{
unfold x, y in *.
rewrite -2!subndiv_eq_mod.
- rewrite subh1 ?addn1; last by apply leq_trunc_div.
+ rewrite addnBAC ?addn1; last by apply leq_trunc_div.
rewrite EQDIV; apply/eqP.
rewrite -(eqn_add2r (n%/d*d)).
- by rewrite subh1; last by apply leq_trunc_div.
+ by rewrite addnBAC; last by apply leq_trunc_div.
}
}
Qed.
diff --git a/classic/util/sum.v b/classic/util/sum.v
index f5539c82a957d4fcf5265e6907843627ffde9ecd..3a14881e32a53bbf63880a28d34b734e342011cb 100644
--- a/classic/util/sum.v
+++ b/classic/util/sum.v
@@ -122,7 +122,7 @@ Section SumArithmetic.
specialize (RECL nat 0 addn (size r).-1 0 (fun i => F (nth x0 r i))).
rewrite sum_diff; last by ins.
rewrite addmovr; last by rewrite -[_.-1]add0n; apply prev_le_next; try rewrite add0n leqnn.
- rewrite subh1; last by apply leq_sum_nat; move => i /andP [_ LT] _; apply ALL.
+ rewrite addnBAC; last by apply leq_sum_nat; move => i /andP [_ LT] _; apply ALL.
rewrite addnC -RECL //.
rewrite addmovl; last by rewrite big_nat_recr // -{1}[\sum_(_ <= _ < _) _]addn0; apply leq_add.
by rewrite addnC -big_nat_recr.
@@ -155,4 +155,4 @@ Section SumArithmetic.
}
Qed.
-End SumArithmetic.
\ No newline at end of file
+End SumArithmetic.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 1ebccdbdcac7f14651d267f8bbf032b61d80df1e..64f7782f0b53be5c3a5920e10be2e6250d6ad581 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -489,7 +489,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
by rewrite !leq_add2r leq_subr.
- move: HEP; rewrite /EDF /edf.EDF leqNgt; move => /negP HEP; apply: HEP.
apply leq_ltn_trans with (job_arrival jo + (A + D tsk)).
- + rewrite subh1 // addnBA.
+ + 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.
* by apply leq_trans with (t1 + (A + ε + D tsk - D tsk_o)); first rewrite leq_addr.
diff --git a/scripts/wordlist.pws b/scripts/wordlist.pws
index 48cb9fea3df396dbcc79c1b37ec613a90ccf6639..15a39ea9711bfb0a49552decfd1b7f44e20ed143 100644
--- a/scripts/wordlist.pws
+++ b/scripts/wordlist.pws
@@ -1,6 +1,7 @@
personal_ws-1.1 en 0
Prosa
Coq
+ssreflect's
ssreflect
typeclass
iff
diff --git a/util/div_mod.v b/util/div_mod.v
index 100a2b28fd77e371b50908b33ff5d08012066447..2dddf8a272d12799401f9977d80c13724716a631 100644
--- a/util/div_mod.v
+++ b/util/div_mod.v
@@ -6,14 +6,15 @@ Definition div_ceil (x y: nat) := if y %| x then x %/ y else (x %/ y).+1.
Lemma mod_elim:
forall a b c,
- c>0 ->
- b<c ->
- (a + c - b)%%c = ( if a%%c >= b then (a%%c - b) else (a%%c + c - b)).
+ c > 0 ->
+ b < c ->
+ (a + c - b) %% c = if a %% c >= b then (a %% c - b) else (a %% c + c - b).
Proof.
- intros* CP BC.
- have G: a%%c < c by apply ltn_pmod.
- case (b <= a %% c)eqn:CASE;rewrite -addnBA;auto;rewrite -modnDml.
- - rewrite add_subC;auto. rewrite -modnDmr modnn addn0 modn_small;auto;ssrlia.
+ intros * CP BC.
+ have G : a %% c < c by apply ltn_pmod.
+ case (b <= a %% c) eqn:CASE; rewrite -addnBA; auto; rewrite -modnDml.
+ - rewrite addnABC; auto.
+ rewrite -modnDmr modnn addn0 modn_small;auto;ssrlia.
- rewrite modn_small;try ssrlia.
Qed.
diff --git a/util/epsilon.v b/util/epsilon.v
index 91d91c9d3aa6f910fcf06ddcde5d6b1389cc5597..8fb3a1f580c6cf5970ca1be43c40f3a220ac79b1 100644
--- a/util/epsilon.v
+++ b/util/epsilon.v
@@ -1,6 +1,2 @@
-Section Epsilon.
-
- (* [ε] is defined as the smallest positive number. *)
- Definition ε := 1.
-
-End Epsilon.
\ No newline at end of file
+(** [ε] is defined as the smallest positive number. *)
+Definition ε := 1.
diff --git a/util/list.v b/util/list.v
index 25ff61aed6476fdbc989a126665b07e15f6541f6..b637252192d9df088d08263ecdd32d46ad516a1f 100644
--- a/util/list.v
+++ b/util/list.v
@@ -251,10 +251,10 @@ Section Max0.
End Max0.
-(* Additional lemmas about rem for lists. *)
+(** Additional lemmas about rem for lists. *)
Section RemList.
- (* We prove that if [x] lies in [xs] excluding [y], then [x] also lies in [xs]. *)
+ (** We prove that if [x] lies in [xs] excluding [y], then [x] also lies in [xs]. *)
Lemma rem_in:
forall (T: eqType) (x y: T) (xs: seq T),
x \in rem y xs -> x \in xs.
@@ -272,7 +272,7 @@ Section RemList.
}
Qed.
- (* We prove that if we remove an element [x] for which [P x] from
+ (** We prove that if we remove an element [x] for which [P x] from
a filter, then the size of the filter decreases by [1]. *)
Lemma filter_size_rem:
forall (T: eqType) (x:T) (xs: seq T) (P: T -> bool),
@@ -297,17 +297,17 @@ Section RemList.
End RemList.
-(* Additional lemmas about sequences. *)
+(** Additional lemmas about sequences. *)
Section AdditionalLemmas.
- (* First, we show that if [n > 0], then [nth (x::xs) n = nth xs (n-1)]. *)
+ (** First, we show that if [n > 0], then [nth (x::xs) n = nth xs (n-1)]. *)
Lemma nth0_cons:
forall x xs n,
n > 0 ->
nth 0 (x :: xs) n = nth 0 xs n.-1.
Proof. by intros; destruct n. Qed.
- (* We prove that a sequence [xs] of size [n.+1] can be destructed
+ (** We prove that a sequence [xs] of size [n.+1] can be destructed
into a sequence [xs_l] of size [n] and an element [x] such that
[x = xs ++ [::x]]. *)
Lemma seq_elim_last:
@@ -331,7 +331,7 @@ Section AdditionalLemmas.
by apply eq_S.
Qed.
- (* Next, we prove that [x ∈ xs] implies that [xs] can be split
+ (** Next, we prove that [x ∈ xs] implies that [xs] can be split
into two parts such that [xs = xsl ++ [::x] ++ [xsr]]. *)
Lemma in_cat:
forall {X : eqType} (x : X) (xs : list X),
@@ -346,7 +346,7 @@ Section AdditionalLemmas.
by subst; exists (a::xsl), xsr.
Qed.
- (* We prove that for any two sequences [xs] and [ys] the fact that [xs] is a sub-sequence
+ (** We prove that for any two sequences [xs] and [ys] the fact that [xs] is a sub-sequence
of [ys] implies that the size of [xs] is at most the size of [ys]. *)
Lemma subseq_leq_size:
forall {X : eqType} (xs ys: seq X),
@@ -390,7 +390,7 @@ Section AdditionalLemmas.
}
Qed.
- (* We prove that if no element of a sequence [xs] satisfies
+ (** We prove that if no element of a sequence [xs] satisfies
a predicate [P], then [filter P xs] is equal to an empty
sequence. *)
Lemma filter_in_pred0:
diff --git a/util/nat.v b/util/nat.v
index 524f50ba1194c31e35f603d858b6d261962471be..9bf128120d0ec82d0c81921df2b179d60c2911a0 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -1,81 +1,45 @@
Require Export prosa.util.tactics prosa.util.ssrlia.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
-(* Additional lemmas about natural numbers. *)
+(** Additional lemmas about natural numbers. *)
Section NatLemmas.
- Lemma subh1:
- forall m n p,
- m >= n ->
- m - n + p = m + p - n.
- Proof. by ins; ssrlia. Qed.
-
- Lemma subh2:
+ (** First, we show that, given [m1 >= m2] and [n1 >= n2], an
+ expression [(m1 + n1) - (m2 + n2)] can be transformed into
+ expression [(m1 - m2) + (n1 - n2)]. *)
+ Lemma subnD:
forall m1 m2 n1 n2,
m1 >= m2 ->
n1 >= n2 ->
- (m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2).
+ (m1 + n1) - (m2 + n2) = (m1 - m2) + (n1 - n2).
Proof. by ins; ssrlia. Qed.
- Lemma subh3:
+ (** Next, we show that [m + p <= n] implies that [m <= n - p]. Note
+ that this lemma is similar to ssreflect's lemma [leq_subRL];
+ however, the current lemma has no precondition [n <= p], since it
+ has only one direction. *)
+ Lemma leq_subRL_impl:
forall m n p,
- m + p <= n ->
- m <= n - p.
- Proof.
- clear.
- intros.
- 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.
-
- (* Simplify [n + a - b + b - a = n] if [n >= b]. *)
+ m + n <= p ->
+ m <= p - n.
+ Proof. by intros; ssrlia. Qed.
+
+ (** Simplify [n + a - b + b - a = n] if [n >= b]. *)
Lemma subn_abba:
forall n a b,
n >= b ->
n + a - b + b - a = n.
- Proof.
- move=> n a b le_bn.
- rewrite subnK;
- first by rewrite -addnBA // subnn addn0 //.
- rewrite -[b]addn0.
- apply leq_trans with (n := n + 0); rewrite !addn0 //.
- apply leq_addr.
- Qed.
-
- Lemma add_subC:
- forall a b c,
- a >= c ->
- b >=c ->
- a + (b - c) = a - c + b.
- Proof.
- intros* AgeC BgeC.
- induction b;induction c;intros;try ssrlia.
- Qed.
-
- (* TODO: remove when mathcomp minimum required version becomes 1.10.0 *)
- Lemma ltn_subLR:
- forall a b c,
- a - c < b ->
- a < b + c.
- Proof.
- intros* AC. ssrlia.
- Qed.
-
- (* We can drop additive terms on the lesser side of an inequality. *)
+ Proof. by intros; ssrlia. Qed.
+
+ (** We can drop additive terms on the lesser side of an inequality. *)
Lemma leq_addk:
forall m n k,
n + k <= m ->
n <= m.
- Proof.
- move=> m n p.
- apply leq_trans.
- by apply leq_addr.
- Qed.
-
- (** For any numbers [a], [b], and [m], either there exists a number [n]
- such that [m = a + n * b] or [m <> a + n * b] for any [n]. *)
+ Proof. by intros; ssrlia. Qed.
+
+ (** For any numbers [a], [b], and [m], either there exists a number
+ [n] such that [m = a + n * b] or [m <> a + n * b] for any [n]. *)
Lemma exists_or_not_add_mul_cases:
forall a b m,
(exists n, m = a + n * b) \/
@@ -83,19 +47,21 @@ Section NatLemmas.
Proof.
move=> a b m.
case: (leqP a m) => LE.
- { case: (boolP(b %| (m - a))) => DIV.
- { left; exists ((m - a) %/ b).
- now rewrite divnK // subnKC //. }
- { right. move=> n EQ.
+ { case: (boolP(b %| (m - a))) => DIV; [left | right].
+ { exists ((m - a) %/ b).
+ by rewrite divnK // subnKC //. }
+ { move => n EQ.
move: DIV => /negP DIV; apply DIV.
rewrite EQ.
rewrite -addnBAC // subnn add0n.
apply dvdn_mull.
- now apply dvdnn. }}
+ by apply dvdnn. }
+ }
{ right; move=> n EQ.
move: LE; rewrite EQ.
- now rewrite -ltn_subRL subnn //. }
- Qed.
+ by rewrite -ltn_subRL subnn //.
+ }
+ Qed.
(** The expression [n2 * a + b] can be written as [n1 * a + b + (n2 - n1) * a]
for any integer [n1] such that [n1 <= n2]. *)
@@ -108,12 +74,12 @@ Section NatLemmas.
rewrite mulnBl.
rewrite addnBA; first by ssrlia.
destruct a; first by ssrlia.
- now rewrite leq_pmul2r.
+ by rewrite leq_pmul2r.
Qed.
- (** Given constants [a, b, c, z] such that [b <= a] and there is no constant [m]
- such that [a = b + m * c], it holds that there is no constant [n] such that
- [a + z * c = b + n * c]. *)
+ (** Given constants [a, b, c, z] such that [b <= a], if there is no
+ constant [m] such that [a = b + m * c], then it holds that there
+ is no constant [n] such that [a + z * c = b + n * c]. *)
Lemma mul_add_neq:
forall a b c z,
b <= a ->
@@ -123,31 +89,34 @@ Section NatLemmas.
intros * LTE NEQ n EQ.
specialize (NEQ (n - z)).
rewrite mulnBl in NEQ.
- now ssrlia.
+ by ssrlia.
Qed.
End NatLemmas.
+(** In this section, we prove a lemma about intervals of natural
+ numbers. *)
Section Interval.
- (* Trivially, points before the start of an interval, or past the end of an
- interval, are not included in the interval. *)
+ (** Trivially, points before the start of an interval, or past the
+ end of an interval, are not included in the interval. *)
Lemma point_not_in_interval:
forall t1 t2 t',
t2 <= t' \/ t' < t1 ->
forall t,
- t1 <= t < t2
- -> t <> t'.
+ t1 <= t < t2 ->
+ t <> t'.
Proof.
- move=> t1 t2 t' EXCLUDED t /andP [GEQ_t1 LT_t2] EQ.
- subst.
- case EXCLUDED => [INEQ | INEQ];
+ move=> t1 t2 t' EXCLUDED t /andP [GEQ_t1 LT_t2] EQ; subst.
+ by case EXCLUDED => [INEQ | INEQ];
eapply leq_ltn_trans in INEQ; eauto;
- by rewrite ltnn in INEQ.
+ rewrite ltnn in INEQ.
Qed.
End Interval.
+(** In the section, we introduce an additional lemma about relation
+ [<] over natural numbers. *)
Section NatOrderLemmas.
(* Mimic the way implicit arguments are used in [ssreflect]. *)
diff --git a/util/nondecreasing.v b/util/nondecreasing.v
index 9bf4cf106a09c01147222379df22f064c1290cc7..722f172ce0ca52f85f9a5ffea7977416cdcb7701 100644
--- a/util/nondecreasing.v
+++ b/util/nondecreasing.v
@@ -880,7 +880,7 @@ Section NondecreasingSequence.
specialize (LE 0); simpl in LE, FLE.
rewrite leqNgt; apply/negP; intros NEQ.
move: LE; rewrite leqNgt; move => /negP LE; apply: LE.
- rewrite -(ltn_add2r x1) subnK // subh1 // -(ltn_add2r y1) subnK.
+ rewrite -(ltn_add2r x1) subnK // addnBAC // -(ltn_add2r y1) subnK.
- by eapply leq_ltn_trans; [erewrite leq_add2l | erewrite ltn_add2r].
- by apply leq_trans with y2; auto using leq_addr.
}
diff --git a/util/sum.v b/util/sum.v
index 30304efae61c4312ef83790d95fe5ee80e226a69..ed0c0bcdd84a037827386dbc38d45bd5eab114b5 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -259,7 +259,7 @@ Section SumsOverSequences.
Proof.
move=> LEQ.
induction r; first by rewrite !big_nil subn0.
- rewrite !big_cons subh2.
+ rewrite !big_cons subnD.
- apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHl.
by intros; apply LEQ; rewrite in_cons; apply/orP; right.
- by apply LEQ; rewrite in_cons; apply/orP; left.