From 66fe09108aefc314c6da2b5195574bf353d04ca4 Mon Sep 17 00:00:00 2001
From: Marco Maida <>
Date: Wed, 5 Aug 2020 14:47:48 +0200
Subject: [PATCH] Replaced `omega` with `lia`
---
analysis/abstract/abstract_rta.v | 4 +-
.../facts/busy_interval/priority_inversion.v | 2 +-
.../rtc_threshold/job_preemptable.v | 4 +-
.../facts/preemption/rtc_threshold/limited.v | 6 +-
analysis/facts/tdma.v | 4 +-
classic/analysis/uni/basic/tdma_rta_theory.v | 8 +-
.../analysis/uni/basic/tdma_wcrt_analysis.v | 94 +++++++++----------
.../implementation/uni/basic/schedule_tdma.v | 6 +-
.../uni/basic/tdma_rta_example.v | 6 +-
classic/model/policy_tdma.v | 6 +-
classic/model/schedule/uni/end_time.v | 16 ++--
classic/util/all.v | 2 +-
classic/util/div_mod.v | 16 ++--
classic/util/nat.v | 6 +-
classic/util/sum.v | 2 +-
results/edf/rta/bounded_nps.v | 2 +-
util/all.v | 2 +-
util/div_mod.v | 4 +-
util/list.v | 22 ++---
util/nat.v | 10 +-
util/nondecreasing.v | 15 ++-
util/{ssromega.v => ssrlia.v} | 6 +-
util/sum.v | 2 +-
23 files changed, 122 insertions(+), 123 deletions(-)
rename util/{ssromega.v => ssrlia.v} (95%)
diff --git a/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
index f8e8764a9..234a2e309 100644
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -355,7 +355,7 @@ Section Abstract_RTA.
have HH : task_run_to_completion_threshold tsk <= F.
{ move: H_A_F_fixpoint => EQ.
have L1 := relative_arrival_le_interference_bound.
- ssromega.
+ ssrlia.
}
apply leq_trans with F; auto.
Qed.
@@ -367,7 +367,7 @@ Section Abstract_RTA.
have HH : task_run_to_completion_threshold tsk <= F.
{ move: H_A_F_fixpoint => EQ.
have L1 := relative_arrival_le_interference_bound.
- ssromega.
+ ssrlia.
}
by apply leq_trans with (task_run_to_completion_threshold tsk); first rewrite /optimism leq_subr.
Qed.
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index 173658b44..361712d0d 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -723,7 +723,7 @@ Section PriorityInversionIsBounded.
by inversion SCHED2.
}
{ have EX: exists sm, sm.+1 = fpt.
- { exists fpt.-1. ssromega. }
+ { exists fpt.-1. ssrlia. }
destruct EX as [sm EQ2]. rewrite -EQ2.
rewrite addnS.
move: ((proj1 CORR) s' (H_jobs_come_from_arrival_sequence _ _ Sched_s')) => T.
diff --git a/analysis/facts/preemption/rtc_threshold/job_preemptable.v b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 1f5ea86a0..60b3ecafb 100644
--- a/analysis/facts/preemption/rtc_threshold/job_preemptable.v
+++ b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -200,7 +200,7 @@ Section RunToCompletionThreshold.
intros COST; unfold job_run_to_completion_threshold, ε.
have N1 := job_last_nonpreemptive_segment_positive COST.
have N2 := job_last_nonpreemptive_segment_le_job_cost.
- ssromega.
+ ssrlia.
Qed.
(** Next we show that the run-to-completion threshold is at most
@@ -219,7 +219,7 @@ Section RunToCompletionThreshold.
Proof.
move => Ï /andP [GE LT].
apply/negP; intros C.
- have POS : 0 < job_cost j; first by ssromega.
+ have POS : 0 < job_cost j; first by ssrlia.
rewrite /job_run_to_completion_threshold 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 job_cost_is_last_element_of_preemption_points in LT, GE.
diff --git a/analysis/facts/preemption/rtc_threshold/limited.v b/analysis/facts/preemption/rtc_threshold/limited.v
index 1d09527ff..742963e38 100644
--- a/analysis/facts/preemption/rtc_threshold/limited.v
+++ b/analysis/facts/preemption/rtc_threshold/limited.v
@@ -111,9 +111,9 @@ Section TaskRTCThresholdLimitedPreemptions.
rewrite last0_nth; apply T6; eauto 2.
have F: 1 <= size (distances (task_preemption_points tsk)).
{ apply leq_trans with (size (task_preemption_points tsk) - 1).
- - have F := number_of_preemption_points_in_task_at_least_two; ssromega.
- - rewrite [in X in X - 1]size_of_seq_of_distances; [ssromega | apply number_of_preemption_points_in_task_at_least_two].
- } ssromega.
+ - have F := number_of_preemption_points_in_task_at_least_two; ssrlia.
+ - rewrite [in X in X - 1]size_of_seq_of_distances; [ssrlia | apply number_of_preemption_points_in_task_at_least_two].
+ } ssrlia.
}
have J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
by eapply job_last_nonpreemptive_segment_le_job_cost; eauto using valid_fixed_preemption_points_model_lemma.
diff --git a/analysis/facts/tdma.v b/analysis/facts/tdma.v
index 3a8808b8a..db99d8a91 100644
--- a/analysis/facts/tdma.v
+++ b/analysis/facts/tdma.v
@@ -135,10 +135,10 @@ Section TDMAFacts.
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 ssromega.
+ 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 ssromega;auto. by move/eqP in NEQ. apply /eqP;auto.
+ fold O1 O2 in order;try ssrlia;auto. by move/eqP in NEQ. apply /eqP;auto.
Qed.
End TimeSlotOrderFacts.
diff --git a/classic/analysis/uni/basic/tdma_rta_theory.v b/classic/analysis/uni/basic/tdma_rta_theory.v
index 8257106e0..e3e232b2d 100644
--- a/classic/analysis/uni/basic/tdma_rta_theory.v
+++ b/classic/analysis/uni/basic/tdma_rta_theory.v
@@ -137,7 +137,7 @@ Module ResponseTimeAnalysisTDMA.
with (task_deadline0:=task_deadline)
(arr_seq0:=arr_seq)(job_deadline0:=job_deadline)
(job_task0:=job_task)(slot_order0:=slot_order);eauto 2.
- intros. apply H_arrival_times_are_consistent in ARR. ssromega.
+ intros. apply H_arrival_times_are_consistent in ARR. ssrlia.
- have INJ: arrives_in arr_seq j by exists n.+1.
apply completion_monotonic
with (t0:=job_arrival j + WCRT task_cost task_time_slot ts tsk);auto.
@@ -148,11 +148,11 @@ Module ResponseTimeAnalysisTDMA.
intros.
have PERIOD: job_arrival j_other + task_period (job_task j_other)<= job_arrival j.
apply H_sporadic_tasks;auto. case (j==j_other)eqn: JJ;move/eqP in JJ;last auto.
- have JO:job_arrival j_other = job_arrival j by f_equal. ssromega.
+ have JO:job_arrival j_other = job_arrival j by f_equal. ssrlia.
apply completion_monotonic with (t0:= job_arrival j_other +
task_period (job_task j_other)); auto.
have ARRJ: job_arrival j = n.+1 by auto.
- apply (IHt (job_arrival j_other));auto. ssromega.
+ apply (IHt (job_arrival j_other));auto. ssrlia.
destruct H0 as [tj AAJO]. have CONSIST: job_arrival j_other =tj by auto.
by subst. by subst.
Qed.
@@ -171,7 +171,7 @@ Module ResponseTimeAnalysisTDMA.
intros.
have PERIOD: job_arrival j_other + task_period (job_task j_other)<= job_arrival j.
apply H_sporadic_tasks;auto. case (j==j_other)eqn: JJ;move/eqP in JJ;last auto.
- have JO:job_arrival j_other = job_arrival j by f_equal. ssromega.
+ have JO:job_arrival j_other = job_arrival j by f_equal. ssrlia.
apply completion_monotonic with (t:=job_arrival j_other + task_period (job_task j_other));auto.
apply any_job_completed_before_period;auto. by subst.
Qed.
diff --git a/classic/analysis/uni/basic/tdma_wcrt_analysis.v b/classic/analysis/uni/basic/tdma_wcrt_analysis.v
index fd5de0054..4c53d9cf3 100644
--- a/classic/analysis/uni/basic/tdma_wcrt_analysis.v
+++ b/classic/analysis/uni/basic/tdma_wcrt_analysis.v
@@ -222,7 +222,7 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
- rewrite /has_arrived; auto.
- rewrite /completed_by /service /service_during big_nat_recr /service_at /=;
rewrite /is_scheduled_at in SCHED. rewrite SCHED /= -COST; apply/eqP;
- rewrite /service /service_during /service_at;ssromega. trivial.
+ rewrite /service /service_during /service_at;ssrlia. trivial.
Qed.
End BasicLemmas.
@@ -254,8 +254,8 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
fold cycle_sub. repeat rewrite ltn_subRL.
rewrite addSn addnS.
case (modulo_cases (t + cycle_sub) tdma_cycle.-1); intros h1 h2.
- - rewrite prednK // in h1. ssromega.
- - destruct h1 as [h1 _]. rewrite prednK // in h1. ssromega.
+ - rewrite prednK // in h1. ssrlia.
+ - destruct h1 as [h1 _]. rewrite prednK // in h1. ssrlia.
Qed.
(* Lemma: if the duration to next start of slot is a+b at instant t
@@ -298,8 +298,8 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
rewrite /to_next_slot /from_start_of_slot -addnBA in h2.
- fold cycle_sub in h2. rewrite ltn_subRL in h2.
case (modulo_cases (t + cycle_sub) tdma_cycle.-1).
- + intros h3 h4. rewrite prednK // in h3. rewrite h3. ssromega.
- + intros [h31 h32] h4. rewrite prednK // in h32. ssromega.
+ + intros h3 h4. rewrite prednK // in h3. rewrite h3. ssrlia.
+ + intros [h31 h32] h4. rewrite prednK // in h32. ssrlia.
- by apply ltnW, ltn_pmod.
Qed.
@@ -317,7 +317,7 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
induction d as [| d' IHd'];intros t PEN.
- by rewrite addn0.
- rewrite addnS -addSn. intros NSCHED SD. apply IHd'. by apply pendingSt.
- apply S_t_not_sched;auto. ssromega. by apply lt_to_next_slot_1LR.
+ apply S_t_not_sched;auto. ssrlia. by apply lt_to_next_slot_1LR.
Qed.
(* Lemma: if the job is pending but cannot be scheduled at instant t
@@ -333,7 +333,7 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
apply duration_not_sched with (d:= (to_next_slot t).-1)in PEN.
replace (to_next_slot t) with ((to_next_slot t).-1 .+1).
rewrite addnS. apply pendingSt. apply PEN. apply PEN.
- ssromega. auto. ssromega.
+ ssrlia. auto. ssrlia.
Qed.
(* Lemma: It must be schedulable at next start of its time slot *)
@@ -380,21 +380,21 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
- rewrite -addnBA // in NSLOT. rewrite -addnBA // in Hcases.
case (modulo_cases (t + (tdma_cycle - slot_offset %% tdma_cycle)) tdma_cycle.-1); intro mod_case;
repeat (rewrite prednK // in mod_case).
- + rewrite addSn mod_case in Hcases. ssromega.
+ + rewrite addSn mod_case in Hcases. ssrlia.
+ destruct mod_case as [case1 case2].
rewrite /to_next_slot /from_start_of_slot. repeat (rewrite -addnBA //).
rewrite case2 Hcases. repeat rewrite addSn case1 -subn1 subKn //.
repeat rewrite subn0.
case Hc_slot:(c < time_slot); rewrite /duration_to_finish_from_start_of_slot_with.
- * by rewrite ceil_eq1 //; ssromega.
- * rewrite ceil_suba //; try ssromega.
+ * by rewrite ceil_eq1 //; ssrlia.
+ * rewrite ceil_suba //; try ssrlia.
rewrite subn1 mulnBl mul1n addnA -addSn addn1.
- apply/eqP. rewrite eqn_add2l subnBA // addnA. repeat rewrite addnBA; try ssromega.
+ apply/eqP. rewrite eqn_add2l subnBA // addnA. repeat rewrite addnBA; try ssrlia.
-- by rewrite addKn addnAC addnK.
-- apply leq_trans with (n:=tdma_cycle - time_slot + time_slot).
- ++ ssromega.
+ ++ ssrlia.
++ apply leq_add.
- ** apply leq_pmull, ceil_neq0; try ssromega. rewrite ltn_subRL addn0. ssromega.
+ ** apply leq_pmull, ceil_neq0; try ssrlia. rewrite ltn_subRL addn0. ssrlia.
** apply leqnn.
- rewrite Hcases. repeat rewrite addnA. apply/eqP. repeat rewrite eqn_add2r.
rewrite -addn1 -addnA eqn_add2l /to_next_slot /from_start_of_slot.
@@ -407,7 +407,7 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
by rewrite subnDA subn1 addn1 prednK // ltn_subRL addn0 ltn_mod.
+ destruct mod_case as [case1 case2].
rewrite addSn case1 in Hcases.
- assert (H_slot_pos: time_slot > 0) by assumption. ssromega.
+ assert (H_slot_pos: time_slot > 0) by assumption. ssrlia.
Qed.
(* Lemma: if the job can be scheduled at instant t and its residue cost is not
@@ -434,22 +434,22 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
rewrite /from_start_of_slot.
case (c < time_slot - (t + tdma_cycle - slot_offset %% tdma_cycle) %% tdma_cycle) eqn: Hc.
- destruct c; simpl.
- + ssromega.
+ + ssrlia.
+ case (modulo_cases (t + (tdma_cycle - slot_offset %% tdma_cycle)) tdma_cycle.-1); intro mod_case.
* repeat rewrite -addnBA //. rewrite prednK // in mod_case. repeat rewrite addSn mod_case.
- case (c < time_slot - ((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1) eqn:Hc1; try ssromega.
+ case (c < time_slot - ((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1) eqn:Hc1; try ssrlia.
rewrite ltn_subRL addSn in Hc1. rewrite ltn_subRL addnS -addnBA // in Hc.
- ssromega.
+ ssrlia.
* repeat rewrite -addnBA //.
- case (c < time_slot - ((t.+1 + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle)) eqn:Hc1; try ssromega.
+ case (c < time_slot - ((t.+1 + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle)) eqn:Hc1; try ssrlia.
rewrite prednK // in mod_case. destruct mod_case.
- rewrite addSn in Hc1. ssromega.
+ rewrite addSn in Hc1. ssrlia.
- destruct c; repeat rewrite -addnBA // in Hc;rewrite -addnBA // in NSLOT;simpl.
- + ssromega.
+ + ssrlia.
+ repeat rewrite -addnBA // addSn.
case (modulo_cases (t + (tdma_cycle - slot_offset %% tdma_cycle)) tdma_cycle.-1);
intro mod_case; rewrite prednK // in mod_case.
- * case (c < time_slot - ((t + (tdma_cycle - slot_offset %% tdma_cycle)).+1 %% tdma_cycle)) eqn:Hc1; try ssromega.
+ * case (c < time_slot - ((t + (tdma_cycle - slot_offset %% tdma_cycle)).+1 %% tdma_cycle)) eqn:Hc1; try ssrlia.
rewrite /to_next_slot /from_start_of_slot. repeat rewrite -addnBA //. rewrite addSn.
rewrite mod_case -addSn addnA addnA.
replace (t.+1 +(tdma_cycle - ((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1)) with
@@ -459,66 +459,66 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
(c.+1 - (time_slot - ((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1)); trivial.
symmetry.
replace ((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1 with
- (((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle)+1) by ssromega.
- rewrite subnDA. repeat (rewrite subnBA;try ssromega).
+ (((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle)+1) by ssrlia.
+ rewrite subnDA. repeat (rewrite subnBA;try ssrlia).
by rewrite addn1.
-- rewrite -addn1. apply/eqP. rewrite -addnA eqn_add2l.
replace ((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1 with
- (((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle)+1) by ssromega.
+ (((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle)+1) by ssrlia.
rewrite subnDA addnC addnBA.
++ rewrite add1n subn1 //.
++ rewrite ltn_subRL addn0. by apply ltn_pmod.
* case (c < time_slot - ((t + (tdma_cycle - slot_offset %% tdma_cycle)).+1 %% tdma_cycle)) eqn:Hc1;
destruct mod_case as [case1 case2].
-- rewrite leq_eqVlt in H_tdma_cycle_ge_slot. revert H_tdma_cycle_ge_slot.
- move/orP. intros [Hts | Hts]; try ssromega.
+ move/orP. intros [Hts | Hts]; try ssrlia.
move/eqP in Hts. rewrite case2.
rewrite /duration_to_finish_from_start_of_slot_with Hts.
- replace (tdma_cycle - tdma_cycle) with 0 by ssromega.
+ replace (tdma_cycle - tdma_cycle) with 0 by ssrlia.
rewrite muln0 /to_next_slot /from_start_of_slot -addnBA // case2.
- replace (tdma_cycle - tdma_cycle.-1) with 1 by ssromega. ssromega.
+ replace (tdma_cycle - tdma_cycle.-1) with 1 by ssrlia. ssrlia.
-- rewrite case1 case2. rewrite leq_eqVlt in H_tdma_cycle_ge_slot.
revert H_tdma_cycle_ge_slot. move/orP.
- intros [Hts | Hts]; try ssromega. move/eqP in Hts. apply /eqP.
+ intros [Hts | Hts]; try ssrlia. move/eqP in Hts. apply /eqP.
rewrite -addnS eqn_add2l /duration_to_finish_from_start_of_slot_with /to_next_slot /from_start_of_slot.
repeat rewrite Hts.
- replace (tdma_cycle - tdma_cycle) with 0 by ssromega.
+ replace (tdma_cycle - tdma_cycle) with 0 by ssrlia.
repeat rewrite muln0 -addnBA //.
rewrite addSn case1 case2 add0n subn0 add0n.
- replace (tdma_cycle - tdma_cycle.-1) with 1 by ssromega.
- rewrite add1n subn1 //= addnBA; try ssromega.
+ replace (tdma_cycle - tdma_cycle.-1) with 1 by ssrlia.
+ rewrite add1n subn1 //= addnBA; try ssrlia.
by rewrite addKn.
- move/negP /negP in Hcases. rewrite -ltnNge in Hcases. rewrite -addnBA in NSLOT.
rewrite /from_start_of_slot.
case (c < time_slot - (t + tdma_cycle - slot_offset %% tdma_cycle) %% tdma_cycle)eqn:Hc.
- + destruct c; simpl; try ssromega.
+ + destruct c; simpl; try ssrlia.
rewrite /to_next_slot /from_start_of_slot.
case (modulo_cases (t + (tdma_cycle - slot_offset %% tdma_cycle)) tdma_cycle.-1); intro mod_case;
rewrite prednK // in mod_case. rewrite addSn mod_case leq_eqVlt in Hcases.
- move: Hcases => /orP [Hcase | Hcase]; try ssromega.
+ move: Hcases => /orP [Hcase | Hcase]; try ssrlia.
* rewrite -addn1 in Hcase.
replace ((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+2 with
- (((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1 +1) in Hcase; try ssromega.
+ (((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1 +1) in Hcase; try ssrlia.
rewrite eqn_add2r in Hcase. move/eqP in Hcase.
- rewrite Hcase -addnBA // subSnn in Hc. ssromega.
+ rewrite Hcase -addnBA // subSnn in Hc. ssrlia.
* destruct mod_case as [case1 case2].
- rewrite addSn case1 in Hcases. ssromega.
+ rewrite addSn case1 in Hcases. ssrlia.
+ destruct c; simpl.
- * rewrite ltn_subRL addn0 -addnBA // in Hc. ssromega.
+ * rewrite ltn_subRL addn0 -addnBA // in Hc. ssrlia.
* rewrite /to_next_slot /from_start_of_slot.
case (modulo_cases (t + (tdma_cycle - slot_offset %% tdma_cycle)) tdma_cycle.-1) ;intro mod_case;
rewrite prednK // in mod_case.
-- rewrite addSn mod_case leq_eqVlt in Hcases.
- move:Hcases =>/orP [Hcase|Hcase]; try ssromega.
+ move:Hcases =>/orP [Hcase|Hcase]; try ssrlia.
rewrite -addn1 in Hcase.
replace ((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+2 with
- (((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1 +1) in Hcase; try ssromega.
+ (((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1 +1) in Hcase; try ssrlia.
rewrite eqn_add2r in Hcase.
move/eqP in Hcase.
repeat rewrite -addnBA //.
rewrite addSn addSn mod_case Hcase subSnn subn1 /= subnS -addnS -addSn prednK // ltn_subRL addn0.
by apply ltn_pmod.
- -- destruct mod_case as [case1 _]. rewrite addSn case1 in Hcases. ssromega.
+ -- destruct mod_case as [case1 _]. rewrite addSn case1 in Hcases. ssrlia.
+ trivial.
Qed.
@@ -554,10 +554,10 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
- rewrite formula_not_sched_St.
+ replace (t + (to_next_slot t).-1).+1 with (t + to_next_slot t).
* reflexivity.
- * rewrite -addnS. ssromega.
- + apply duration_not_sched;auto. ssromega.
- + apply duration_not_sched;auto. ssromega.
- - ssromega.
+ * rewrite -addnS. ssrlia.
+ + apply duration_not_sched;auto. ssrlia.
+ + apply duration_not_sched;auto. ssrlia.
+ - ssrlia.
Qed.
(* Lemma: if the job cannot be scheduled at instant t and its residue cost is not
@@ -684,7 +684,7 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
-- by apply pendingSt_Sched with (c:=c).
-- rewrite /is_scheduled_at in l;
rewrite -SC /service /service_during /service_at big_nat_recr //.
- rewrite l /=;ssromega.
+ rewrite l /=;ssrlia.
+ apply end_time_predicate_eq;try exact l.
* exact PEN.
* destruct c as [|c];rewrite job_not_sched_to_cunsume_1unit //.
@@ -696,7 +696,7 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
by rewrite service_is_zero_in_Nsched_duration.
++ rewrite <-service_is_zero_in_Nsched_duration with (d:=to_next_slot ARR) in SC;auto.
rewrite -SC /service /service_during /service_at big_nat_recr;auto. rewrite SCHED /=.
- ssromega.
+ ssrlia.
Qed.
End formula_predicate_eq.
@@ -808,7 +808,7 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
- apply decPcases in gt_ref.
destruct (TDMA_policy_case_RT_le_Period (job_arrival j)) as [hj |hj]. apply pendingArrival.
unfold in_time_slot_at in hj.
- + rewrite /from_start_of_slot in gt_ref. rewrite /from_start_of_slot in EXISTS. case (_ < _) in gt_ref;try ssromega.
+ + rewrite /from_start_of_slot in gt_ref. rewrite /from_start_of_slot in EXISTS. case (_ < _) in gt_ref;try ssrlia.
+ 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.
diff --git a/classic/implementation/uni/basic/schedule_tdma.v b/classic/implementation/uni/basic/schedule_tdma.v
index b77338776..1a075dccb 100644
--- a/classic/implementation/uni/basic/schedule_tdma.v
+++ b/classic/implementation/uni/basic/schedule_tdma.v
@@ -97,7 +97,7 @@ Module ConcreteSchedulerTDMA.
have BIGJ': j' \in [seq j <- \big[cat/[::]]_(arrj.+1 <= i < t.+1)
jobs_arriving_at arr_seq i | is_pending j t]
by rewrite mem_filter;apply /andP.
- rewrite ->big_cat_nat with (n:=arrj.+1) in LEQ;try ssromega.
+ rewrite ->big_cat_nat with (n:=arrj.+1) in LEQ;try ssrlia.
rewrite filter_cat find_cat /=in LEQ.
rewrite find_cat /= in LEQ.
have F: (has (fun job : Job => job == j')
@@ -109,7 +109,7 @@ Module ConcreteSchedulerTDMA.
jobs_arriving_at arr_seq i
| is_pending j t]);auto.
rewrite -filter_cat -big_cat_nat;auto. apply pending_jobs_uniq.
- ssromega.
+ ssrlia.
have TT: (has (fun job : Job => job == j)
[seq j <- \big[cat/[::]]_(0 <= i < arrj.+1)
jobs_arriving_at arr_seq i
@@ -121,7 +121,7 @@ Module ConcreteSchedulerTDMA.
[seq j <- \big[cat/[::]]_(0 <= t < arrj.+1)
jobs_arriving_at arr_seq t
| is_pending j t]). by rewrite -has_find.
- rewrite F TT in LEQ. ssromega.
+ rewrite F TT in LEQ. ssrlia.
Qed.
Lemma pending_job_in_penging_list:
diff --git a/classic/implementation/uni/basic/tdma_rta_example.v b/classic/implementation/uni/basic/tdma_rta_example.v
index c469297a2..fd9363a42 100644
--- a/classic/implementation/uni/basic/tdma_rta_example.v
+++ b/classic/implementation/uni/basic/tdma_rta_example.v
@@ -92,14 +92,14 @@ Module ResponseTimeAnalysisExemple.
slot_order_is_transitive slot_order.
Proof.
rewrite /slot_order.
- intros t1 t2 t3 IN1 IN2. ssromega.
+ intros t1 t2 t3 IN1 IN2. ssrlia.
Qed.
Fact slot_order_antisymmetric:
slot_order_is_antisymmetric_over_task_set ts slot_order.
Proof.
intros x y IN1 IN2. rewrite /slot_order. intros O1 O2.
- have EQ: task_id x = task_id y by ssromega.
+ have EQ: task_id x = task_id y by ssrlia.
case (x==y)eqn:XY;move/eqP in XY;auto.
repeat (move:IN2=> /orP [/eqP TSK2 |IN2]); repeat (move:IN1=>/orP [/eqP TSK1|IN1];subst);compute ;try done.
Qed.
@@ -142,7 +142,7 @@ Module ResponseTimeAnalysisExemple.
apply (respects_FIFO ) in FIND;auto.
apply periodic_arrivals_are_sporadic with (ts:=ts) in FIND;auto.
have PERIODY:task_period (job_task y)>0 by
- apply ts_has_valid_parameters,periodic_arrivals_all_jobs_from_taskset. ssromega.
+ apply ts_has_valid_parameters,periodic_arrivals_all_jobs_from_taskset. ssrlia.
apply job_arrival_times_are_consistent.
apply periodic_arrivals_is_a_set,ts_has_valid_parameters.
split;auto.
diff --git a/classic/model/policy_tdma.v b/classic/model/policy_tdma.v
index 9a270f405..5cd2450f9 100644
--- a/classic/model/policy_tdma.v
+++ b/classic/model/policy_tdma.v
@@ -12,7 +12,7 @@ Module PolicyTDMA.
Section TDMA.
(* The TDMA policy is based on two properties.
(1) Each task has a fixed, reserved time slot for execution;
- (2) These time slots are ordered in sequence to form a TDMA cycle, which repeats along the timeline.
+ (2) These time slots are ordered in sequence to form a TDMA cycle, which repeats along the timeline.
An example of TDMA schedule is illustrated in the following.
______________________________
| s1 | s2 |s3| s1 | s2 |s3|...
@@ -197,10 +197,10 @@ Module PolicyTDMA.
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 ssromega.
+ 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.
destruct (slot_order_total tsk1 tsk2) as [order |order];auto;apply relation_offset in order;
- fold O1 O2 in order;try ssromega;auto. by move/eqP in NEQ. apply /eqP;auto.
+ fold O1 O2 in order;try ssrlia;auto. by move/eqP in NEQ. apply /eqP;auto.
Qed.
End InTimeSlotUniq.
diff --git a/classic/model/schedule/uni/end_time.v b/classic/model/schedule/uni/end_time.v
index c41dd513a..ca412336d 100644
--- a/classic/model/schedule/uni/end_time.v
+++ b/classic/model/schedule/uni/end_time.v
@@ -199,7 +199,7 @@ Module end_time.
forall t c e, job_end_time_p t c e -> t <= e.
Proof.
intros* G.
- induction G as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre]; ssromega.
+ induction G as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre]; ssrlia.
Qed.
(* the sum of job arrival and job cost is less than or equal to
@@ -210,7 +210,7 @@ Module end_time.
t+c<=e.
Proof.
intros* h1.
- induction h1 as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre]; ssromega.
+ induction h1 as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre]; ssrlia.
Qed.
(* The servive received between the job arrival
@@ -254,7 +254,7 @@ Module end_time.
unfold job_completed_by, completed_by, service, service_during in h1.
destruct job_end; trivial.
rewrite big_geq // in h1.
- ssromega.
+ ssrlia.
Qed.
(* The service received between job arrival and the previous instant
@@ -273,7 +273,7 @@ Module end_time.
rewrite big_ltn // IHHpre /service_at /service_during.
case C:(scheduled_at sched job t);done.
- destruct c.
- + inversion Hpre. apply big_geq. ssromega.
+ + inversion Hpre. apply big_geq. ssrlia.
+ apply arrival_add_cost_le_end, leq_sub2r with (p:=1) in Hpre.
rewrite subn1 addnS //= addSn subn1 in Hpre.
apply leq_ltn_trans with (m:=t) in Hpre; try (apply leq_addr).
@@ -289,17 +289,17 @@ Module end_time.
Proof.
intros job_cmplted t' [ht1 ht2].
assert (H_slot: job_cost job > 0) by (apply H_valid_job).
- apply leq_ltn_trans with (n:= (job_cost job).-1); last ssromega.
+ apply leq_ltn_trans with (n:= (job_cost job).-1); last ssrlia.
rewrite -job_uncompletes_at_end_time_sub_1 // /job_service_during /service_during.
assert (H_lt: exists delta, t' + delta = job_end.-1).
- move/leP:ht2 => ht2.
apply Nat.le_exists_sub in ht2.
- destruct ht2 as [p [ht21 ht22]]. exists p. ssromega.
+ destruct ht2 as [p [ht21 ht22]]. exists p. ssrlia.
- destruct H_lt as [delta ht']. rewrite -ht'.
replace (\sum_(job_arrival job <= t < t' + delta) service_at sched job t)
with (addn_monoid(\big[addn_monoid/0]_(job_arrival job <= i < t') service_at sched job i)
- (\big[addn_monoid/0]_(t' <= i < t'+delta) service_at sched job i)); simpl; try ssromega.
- symmetry. apply big_cat_nat; ssromega.
+ (\big[addn_monoid/0]_(t' <= i < t'+delta) service_at sched job i)); simpl; try ssrlia.
+ symmetry. apply big_cat_nat; ssrlia.
Qed.
End Lemmas.
diff --git a/classic/util/all.v b/classic/util/all.v
index 7c7e47674..963ee97a5 100644
--- a/classic/util/all.v
+++ b/classic/util/all.v
@@ -17,4 +17,4 @@ Require Export prosa.classic.util.minmax.
Require Export prosa.classic.util.seqset.
Require Export prosa.classic.util.step_function.
Require Export prosa.util.epsilon.
-Require Export prosa.util.ssromega.
+Require Export prosa.util.ssrlia.
diff --git a/classic/util/div_mod.v b/classic/util/div_mod.v
index 64bd60948..4782e4b9d 100644
--- a/classic/util/div_mod.v
+++ b/classic/util/div_mod.v
@@ -1,7 +1,7 @@
Require Export prosa.util.div_mod.
Require Import Arith Omega Nat.
-Require Import prosa.classic.util.tactics prosa.util.ssromega prosa.classic.util.nat.
+Require Import prosa.classic.util.tactics prosa.util.ssrlia prosa.classic.util.nat.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
@@ -160,7 +160,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop d
rewrite -(modnn (n.+1)).
change (a.+1) with (1+a).
change (n.+1) with (1+n).
- assert (X:n<n.+1) by ssromega.
+ assert (X:n<n.+1) by ssrlia.
apply modn_small in X.
split; intros* G.
- apply eq_modDl in G.
@@ -179,7 +179,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop d
by rewrite -G -addn1 -modnDml addn1.
- destruct n.
+ left. reflexivity.
- + assert (X: a%%n.+1 < n.+1). by apply ltn_pmod. ssromega.
+ + assert (X: a%%n.+1 < n.+1). by apply ltn_pmod. ssrlia.
- right. destruct n.
+ discriminate G.
+ apply modnS_eq. by injection G.
@@ -191,8 +191,8 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop d
destruct (ltngtP ((a%%n.+1).+1) (n.+1)) as [G|G|G].
- left. apply modn_small in G.
by rewrite -G -addn1 -modnDml addn1.
- - assert (X: a%%n.+1 < n.+1). by apply ltn_pmod. ssromega.
- - right. apply modnS_eq. ssromega.
+ - assert (X: a%%n.+1 < n.+1). by apply ltn_pmod. ssrlia.
+ - right. apply modnS_eq. ssrlia.
Qed.
(* Old version of the lemma which is now covered by modnSor and modnS_eq *)
@@ -211,14 +211,14 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop d
rewrite leq_eqVlt. move/orP => [G2|G2].
- move/eqP :G2 => G2. subst.
rewrite dvdnn. rewrite divnn.
- destruct c; ssromega.
+ destruct c; ssrlia.
- rewrite gtnNdvd // divn_small //.
Qed.
Lemma ceil_suba: forall a c, c > 0 -> a > c -> div_ceil a c = (div_ceil (a-c) c).+1.
Proof.
intros* G1 G2. unfold div_ceil.
- assert (X:a=a-c+c) by (rewrite subnK //; ssromega).
+ assert (X:a=a-c+c) by (rewrite subnK //; ssrlia).
case E1:(c %| a); case E2:(c %| a - c); rewrite {1} X.
- rewrite divnDl //. rewrite divnn. by rewrite G1 addn1.
- rewrite X in E1. apply dvdn_add_eq in E1.
@@ -232,5 +232,5 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop d
Proof.
intros.
rewrite {2}(divn_eq a b).
- ssromega.
+ ssrlia.
Qed.
diff --git a/classic/util/nat.v b/classic/util/nat.v
index e6a46d406..81961b7a6 100644
--- a/classic/util/nat.v
+++ b/classic/util/nat.v
@@ -1,6 +1,6 @@
Require Export prosa.util.nat.
-Require Import prosa.classic.util.tactics prosa.util.ssromega.
+Require Import prosa.classic.util.tactics prosa.util.ssrlia.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
(* Additional lemmas about natural numbers. *)
@@ -30,7 +30,7 @@ Section NatLemmas.
m >= n ->
(m - n = p <-> m = p + n).
Proof.
- by split; ins; ssromega.
+ by split; ins; ssrlia.
Qed.
Lemma addmovl:
@@ -38,7 +38,7 @@ Section NatLemmas.
m >= n ->
(p = m - n <-> p + n = m).
Proof.
- by split; ins; ssromega.
+ by split; ins; ssrlia.
Qed.
Lemma ltSnm : forall n m, n.+1 < m -> n < m.
diff --git a/classic/util/sum.v b/classic/util/sum.v
index 66be428eb..f5539c82a 100644
--- a/classic/util/sum.v
+++ b/classic/util/sum.v
@@ -1,5 +1,5 @@
Require Export prosa.util.sum.
-Require Export prosa.util.ssromega.
+Require Export prosa.util.ssrlia.
Require Import prosa.classic.util.tactics.
Require Import prosa.classic.util.notation.
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index 1c048c5ca..a9a9d4e01 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -197,7 +197,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
by move: JINB; move => /andP [_ T].
}
rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline in NOTHEP.
- rewrite /D; ssromega.
+ rewrite /D; ssrlia.
}
Qed.
diff --git a/util/all.v b/util/all.v
index 8e4014180..c80df7935 100644
--- a/util/all.v
+++ b/util/all.v
@@ -5,7 +5,7 @@ Require Export prosa.util.counting.
Require Export prosa.util.div_mod.
Require Export prosa.util.list.
Require Export prosa.util.nat.
-Require Export prosa.util.ssromega.
+Require Export prosa.util.ssrlia.
Require Export prosa.util.sum.
Require Export prosa.util.seqset.
Require Export prosa.util.step_function.
diff --git a/util/div_mod.v b/util/div_mod.v
index 5c3e19d47..af257be9d 100644
--- a/util/div_mod.v
+++ b/util/div_mod.v
@@ -14,7 +14,7 @@ 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;ssromega.
- - rewrite modn_small;try ssromega.
+ - rewrite add_subC;auto. rewrite -modnDmr modnn addn0 modn_small;auto;ssrlia.
+ - rewrite modn_small;try ssrlia.
Qed.
diff --git a/util/list.v b/util/list.v
index dd2efd28a..85f33ef78 100644
--- a/util/list.v
+++ b/util/list.v
@@ -1,4 +1,4 @@
-Require Import prosa.util.ssromega prosa.util.tactics.
+Require Import prosa.util.ssrlia prosa.util.tactics.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** We define a few simple operations on
@@ -526,7 +526,7 @@ Section IotaRange.
induction k.
{ move => x a b BO /andP [GE LT]; exfalso.
move: BO; rewrite leqn0 subn_eq0; move => BO.
- by ssromega.
+ by ssrlia.
}
{ move => x a b BO /andP [GE LT].
destruct a.
@@ -536,15 +536,15 @@ Section IotaRange.
- move: EQ => /eqP EQ; subst x.
rewrite filter_in_pred0 //.
by intros x; rewrite mem_index_iota -lt0n; move => /andP [T1 _].
- - by apply IHk; ssromega.
+ - by apply IHk; ssrlia.
}
- rewrite index_iota_lt_step; last by ssromega.
+ rewrite index_iota_lt_step; last by ssrlia.
simpl; destruct (a.+1 == x) eqn:EQ.
- move: EQ => /eqP EQ; subst x.
rewrite filter_in_pred0 //.
intros x; rewrite mem_index_iota; move => /andP [T1 _].
by rewrite neq_ltn; apply/orP; right.
- - by rewrite IHk //; ssromega.
+ - by rewrite IHk //; ssrlia.
}
Qed.
@@ -579,7 +579,7 @@ Section IotaRange.
destruct (y == y') eqn:EQ1, (y' == x) eqn:EQ2; auto.
- exfalso.
move: EQ1 EQ2 => /eqP EQ1 /eqP EQ2; subst.
- by ssromega.
+ by ssrlia.
- move: EQ1 => /eqP EQ1; subst.
by rewrite in_cons eq_refl.
- by rewrite in_cons EQ1.
@@ -601,7 +601,7 @@ Section IotaRange.
{ exists (b-a); now simpl. } destruct EX as [k BO].
revert x xs a b B MIN BO.
induction k; move => x xs a b /andP [LE GT] MIN BO.
- - by move_neq_down BO; ssromega.
+ - by move_neq_down BO; ssrlia.
- move: LE; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT].
+ subst.
rewrite index_iota_lt_step //.
@@ -615,7 +615,7 @@ Section IotaRange.
replace (@in_mem nat x (@mem nat (seq_predType nat_eqType) (@rem_all nat_eqType x xs))) with false; last first.
apply/eqP; rewrite eq_sym eqbF_neg. apply/negP; apply nin_rem_all.
reflexivity.
- + rewrite index_iota_lt_step //; last by ssromega.
+ + rewrite index_iota_lt_step //; last by ssrlia.
replace ([seq Ï <- a :: index_iota a.+1 b | Ï \in x :: xs])
with ([seq Ï <- index_iota a.+1 b | Ï \in x :: xs]); last first.
{ simpl; replace (@in_mem nat a (@mem nat (seq_predType nat_eqType) (@cons nat x xs))) with false; first by done.
@@ -631,7 +631,7 @@ Section IotaRange.
apply in_rem_all in C.
by move_neq_down LT; apply MIN.
}
- by rewrite IHk //; ssromega.
+ by rewrite IHk //; ssrlia.
Qed.
(** For convenience, we define a special case of
@@ -669,9 +669,9 @@ Section IotaRange.
+ rewrite index_iota_lt_step; last by done.
simpl in *; destruct (P a) eqn:PA.
* destruct idx; simpl; first by done.
- apply IHk; try ssromega.
+ apply IHk; try ssrlia.
by rewrite index_iota_lt_step // //= PA //= in LT2.
- * apply IHk; try ssromega.
+ * apply IHk; try ssrlia.
by rewrite index_iota_lt_step // //= PA //= in LT2.
Qed.
diff --git a/util/nat.v b/util/nat.v
index 16bc5f715..b267c5cb8 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -1,4 +1,4 @@
-Require Export prosa.util.tactics prosa.util.ssromega.
+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. *)
@@ -8,14 +8,14 @@ Section NatLemmas.
forall m n p,
m >= n ->
m - n + p = m + p - n.
- Proof. by ins; ssromega. Qed.
+ Proof. by ins; ssrlia. Qed.
Lemma subh2 :
forall m1 m2 n1 n2,
m1 >= m2 ->
n1 >= n2 ->
(m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2).
- Proof. by ins; ssromega. Qed.
+ Proof. by ins; ssrlia. Qed.
Lemma subh3:
forall m n p,
@@ -51,7 +51,7 @@ Section NatLemmas.
a + (b - c ) = a - c + b.
Proof.
intros* AgeC BgeC.
- induction b;induction c;intros;try ssromega.
+ induction b;induction c;intros;try ssrlia.
Qed.
(* TODO: remove when mathcomp minimum required version becomes 1.10.0 *)
@@ -60,7 +60,7 @@ Section NatLemmas.
a - c < b ->
a < b + c.
Proof.
- intros* AC. ssromega.
+ intros* AC. ssrlia.
Qed.
(* We can drop additive terms on the lesser side of an inequality. *)
diff --git a/util/nondecreasing.v b/util/nondecreasing.v
index 5ee910da9..9bf4cf106 100644
--- a/util/nondecreasing.v
+++ b/util/nondecreasing.v
@@ -65,10 +65,10 @@ Section NondecreasingSequence.
+ destruct n1, n2; try done; simpl.
* apply iota_filter_gt; first by done.
rewrite index_iota_lt_step // //= PA //= in LT.
- * apply IHk; try ssromega.
+ * apply IHk; try ssrlia.
apply/andP; split; first by done.
rewrite index_iota_lt_step // //= PA //= in LT.
- + apply IHk; try ssromega.
+ + apply IHk; try ssrlia.
apply/andP; split; first by done.
rewrite index_iota_lt_step // //= PA //= in LT.
}
@@ -660,10 +660,10 @@ Section NondecreasingSequence.
{ rewrite ltnNge; apply/negP; intros CONTR.
subst x y; move: LT; rewrite ltnNge; move => /negP T; apply: T.
by apply SIZE; apply/andP. }
- have EQ: exists Δ, indy = indx + Δ. exists (indy - indx); ssromega. move: EQ => [Δ EQ]; subst indy.
+ have EQ: exists Δ, indy = indx + Δ. exists (indy - indx); ssrlia. move: EQ => [Δ EQ]; subst indy.
have F: exists ind, indx <= ind < indx + Δ /\ xs[|ind|] < xs[|ind.+1|].
{ subst x y; clear SIZEx SIZEy; revert xs indx LTind SIZE LT.
- induction Δ; intros; first by ssromega.
+ induction Δ; intros; first by ssrlia.
destruct (posnP Δ) as [ZERO|POS].
{ by subst Δ; exists indx; split; [rewrite addn1; apply/andP | rewrite addn1 in LT]; auto. }
have ALT: xs[|indx + Δ|] == xs[|indx + Δ.+1|] \/ xs[|indx + Δ|] < xs[|indx + Δ.+1|].
@@ -809,7 +809,7 @@ Section NondecreasingSequence.
rewrite {1}range_iota_filter_step //. rewrite distances_unfold_2cons. rewrite {1}range_iota_filter_step //.
}
Qed.
-
+
(** Let [xs] again be a non-decreasing sequence. We prove that
distances of sequence [undup xs] coincide with
sequence of positive distances of [xs]. *)
@@ -820,8 +820,7 @@ Section NondecreasingSequence.
Proof.
intros ? NonDec.
rewrite -(distances_iota_filtered _ (max0 xs)); [ | by apply in_max0_le | by done].
- have T: forall {X Y : Type} (x y : X) (f : X -> Y), x = y -> f x = f y.
- { by intros; subst. } apply T; clear T.
+ enough ([seq Ï <- index_iota 0 (max0 xs).+1 | Ï \in xs] = (undup xs)) as IN; first by rewrite IN.
have EX: exists len, size xs <= len.
{ exists (size xs); now simpl. } destruct EX as [n BO].
revert xs NonDec BO; induction n.
@@ -904,4 +903,4 @@ Section NondecreasingSequence.
End DistancesOfNonDecreasingSequence.
-End NondecreasingSequence.
\ No newline at end of file
+End NondecreasingSequence.
diff --git a/util/ssromega.v b/util/ssrlia.v
similarity index 95%
rename from util/ssromega.v
rename to util/ssrlia.v
index dc1977142..e24e726fc 100644
--- a/util/ssromega.v
+++ b/util/ssrlia.v
@@ -1,5 +1,5 @@
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-Require Import Omega.
+Require Import Lia.
(* Adopted from http://github.com/pi8027/formalized-postscript/blob/master/stdlib_ext.v *)
@@ -24,7 +24,7 @@ Ltac arith_goal_ssrnat2coqnat :=
| |- is_true (_ < _) => try apply/ltP
end.
-Ltac ssromega :=
+Ltac ssrlia :=
repeat arith_hypo_ssrnat2coqnat;
arith_goal_ssrnat2coqnat; simpl;
- omega.
\ No newline at end of file
+ lia.
diff --git a/util/sum.v b/util/sum.v
index fa2a4a7bd..e18e3cbf5 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -161,7 +161,7 @@ Section ExtraLemmas.
by rewrite in_cons; apply/orP; right. }
rewrite big_cons [RHS]big_cons in H2.
have EqLeq: forall a b c d, a + b = c + d -> a <= c -> b >= d.
- { clear; intros; ssromega. }
+ { clear; intros; ssrlia. }
move: IN; rewrite in_cons; move => /orP [/eqP EQ | IN].
{ subst a.
rewrite PX in H2.
--
GitLab