diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4b055e3d372ad0e736b3d2cc30695e9559b34488..afc6289e54ed0383c228d9022ca70bd85318b499 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -41,6 +41,7 @@ stages:
extends:
- .preferred-stable-version
script:
+ - opam install coq-mathcomp-zify
- ./create_makefile.sh --without-classic
- make -j ${NJOBS}
@@ -49,6 +50,7 @@ stages:
extends:
- .preferred-stable-version
script:
+ - opam install coq-mathcomp-zify
- ./create_makefile.sh --only-classic
- make -j ${NJOBS}
@@ -85,6 +87,7 @@ stages:
- .preferred-stable-version
stage: process
script:
+ - opam install coq-mathcomp-zify
- make html -j ${NJOBS}
- mv html with-proofs
- make gallinahtml -j ${NJOBS}
@@ -170,6 +173,7 @@ validate:
dependencies:
- compile
script:
+ - opam install coq-mathcomp-zify
- make -j ${NJOBS} # CI gotcha — get any spurious recompilation out of the way
- make validate 2>&1 | tee validation-results.txt
- scripts/check-validation-output.sh validation-results.txt
@@ -182,7 +186,9 @@ validate-classic:
needs: ["compile-classic"]
dependencies:
- compile-classic
- script: make validate
+ script:
+ - opam install coq-mathcomp-zify
+ - make validate
doc:
extends:
@@ -220,6 +226,7 @@ proof-state:
image: bbbrandenburg/alectryon-ci:1.14.0-coq-8.15.0
script:
- eval $(opam env "--switch=${COMPILER_EDGE}" --set-switch)
+ - opam install coq-mathcomp-zify
- ./create_makefile.sh --without-classic
- make -j ${NJOBS} alectryon
artifacts:
diff --git a/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
index 2e68fdeffccfe0ba1c93643e9cef22586bc02a0b..bfbeb31c08cacf6e8c2f497d786fb441cd9b8127 100644
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -359,7 +359,7 @@ Section Abstract_RTA.
have HH : task_rtct tsk <= F.
{ move: H_A_F_fixpoint => EQ.
have L1 := relative_arrival_le_interference_bound.
- ssrlia.
+ lia.
}
apply leq_trans with F; auto.
Qed.
@@ -371,7 +371,7 @@ Section Abstract_RTA.
have HH : task_rtct tsk <= F.
{ move: H_A_F_fixpoint => EQ.
have L1 := relative_arrival_le_interference_bound.
- ssrlia.
+ lia.
}
by apply leq_trans with (task_rtct tsk); first rewrite /optimism leq_subr.
Qed.
diff --git a/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v
index 606b9313544325289f16af364f2627121f3b7d42..44639d4683907ba20235cd4116dde3463c1ce9bf 100644
--- a/analysis/facts/behavior/arrivals.v
+++ b/analysis/facts/behavior/arrivals.v
@@ -162,7 +162,7 @@ Section ArrivalSequencePrefix.
Proof.
intros P t t1 t2 INEQ.
rewrite -filter_cat.
- now rewrite -arrivals_between_cat => //; ssrlia.
+ now rewrite -arrivals_between_cat => //; lia.
Qed.
(** The same observation applies to membership in the set of
@@ -339,7 +339,7 @@ Section ArrivalSequencePrefix.
apply mem_bigcat_nat_exists in J2ARR; move : J2ARR => [i [J2_IN INEQ]].
apply mem_bigcat_nat with (j := i) => //.
apply H_consistent_arrival_times in J2_IN; rewrite J2_IN in ARR_LT.
- now ssrlia.
+ now lia.
Qed.
End ArrivalTimes.
diff --git a/analysis/facts/behavior/service.v b/analysis/facts/behavior/service.v
index 94d0d4fc46a7223b1a0b2e43a5a8052e93724b04..4558a0782652dc72817372893ed685241e04d928 100644
--- a/analysis/facts/behavior/service.v
+++ b/analysis/facts/behavior/service.v
@@ -184,8 +184,8 @@ Section UnitService.
Ï <= delta.
Proof.
induction delta; intros ? LE.
- - by rewrite service_during_geq in LE; ssrlia.
- - rewrite addnS -service_during_last_plus_before in LE; last by ssrlia.
+ - by rewrite service_during_geq in LE; lia.
+ - rewrite addnS -service_during_last_plus_before in LE; last by lia.
destruct (service_is_zero_or_one (t + delta)) as [EQ|EQ]; rewrite EQ in LE.
+ rewrite addn0 in LE.
by apply IHdelta in LE; rewrite (leqRW LE).
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index b8d88135e0c806873c5434bb19bdc1dbb51acacd..d1a8964e4ab2ec14a6da7d0b3ff40a25f9b8e6f7 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -627,7 +627,7 @@ Section PriorityInversionIsBounded.
by inversion SCHED2.
}
{ have EX: exists sm, sm.+1 = fpt.
- { exists fpt.-1. ssrlia. }
+ { exists fpt.-1. lia. }
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/hyperperiod.v b/analysis/facts/hyperperiod.v
index 1915643296c3fb6e24f1edb7df85be841b1c97d6..644ff743122c668f9abf03bfcae2f13955162378 100644
--- a/analysis/facts/hyperperiod.v
+++ b/analysis/facts/hyperperiod.v
@@ -95,13 +95,14 @@ Section PeriodicLemmas.
job_task (corresponding_job_in_hyperperiod ts arr_seq j1
(starting_instant_of_corresponding_hyperperiod ts j2) (job_task j1)) = job_task j1.
Proof.
+ clear H_task_in_ts H_valid_period.
intros *.
set ARRIVALS := (task_arrivals_between arr_seq (job_task j1) (starting_instant_of_hyperperiod ts (job_arrival j2))
(starting_instant_of_hyperperiod ts (job_arrival j2) + HP)).
set IND := (job_index_in_hyperperiod ts arr_seq j1 (starting_instant_of_hyperperiod ts (job_arrival j1)) (job_task j1)).
have SIZE_G : size ARRIVALS <= IND -> job_task (nth j1 ARRIVALS IND) = job_task j1 by intro SG; rewrite nth_default.
- case: (boolP (size ARRIVALS == IND)) => [/eqP EQ|NEQ]; first by apply SIZE_G; ssrlia.
- move : NEQ; rewrite neq_ltn; move => /orP [LT | G]; first by apply SIZE_G; ssrlia.
+ case: (boolP (size ARRIVALS == IND)) => [/eqP EQ|NEQ]; first by apply SIZE_G; lia.
+ move : NEQ; rewrite neq_ltn; move => /orP [LT | G]; first by apply SIZE_G; lia.
set jb := nth j1 ARRIVALS IND.
have JOB_IN : jb \in ARRIVALS by apply mem_nth.
rewrite /ARRIVALS /task_arrivals_between mem_filter in JOB_IN.
@@ -139,8 +140,8 @@ Section PeriodicLemmas.
rewrite mulnA /HP /jobs_in_hyperperiod !size_of_task_arrivals_between.
erewrite big_sum_eq_in_eq_sized_intervals => //; intros g G_LT.
have OFF_G : task_offset tsk <= O_max by apply max_offset_g.
- have FG : forall v b n, v + b + n = v + n + b by intros *; ssrlia.
- erewrite eq_size_of_task_arrivals_seperated_by_period => //; last by ssrlia.
+ have FG : forall v b n, v + b + n = v + n + b by intros *; lia.
+ erewrite eq_size_of_task_arrivals_seperated_by_period => //; last by lia.
now rewrite FG.
Qed.
@@ -154,9 +155,9 @@ Section PeriodicLemmas.
intros *.
case : (boolP (n1 == n2)) => [/eqP EQ | NEQ]; first by rewrite EQ.
move : NEQ; rewrite neq_ltn; move => /orP [LT | LT].
- + now apply eq_size_hyp_lt => //; ssrlia.
+ + now apply eq_size_hyp_lt => //; lia.
+ move : (eq_size_hyp_lt n2 n1) => EQ_S.
- now feed_n 1 EQ_S => //; ssrlia.
+ now feed_n 1 EQ_S => //; lia.
Qed.
(** Consider any two jobs [j1] and [j2] that stem from the arrival sequence
@@ -189,11 +190,11 @@ Section PeriodicLemmas.
move : NTH_IN => [i [NJ_IN INEQ]]; apply H_consistent_arrivals in NJ_IN; rewrite -NJ_IN in INEQ.
apply /andP; split => //.
rewrite ltnS.
- apply leq_trans with (n := (job_arrival j2 - O_max) %/ HP * HP + O_max + HP); first by ssrlia.
+ apply leq_trans with (n := (job_arrival j2 - O_max) %/ HP * HP + O_max + HP); first by lia.
rewrite leq_add2r.
have O_M : (job_arrival j2 - O_max) %/ HP * HP <= job_arrival j2 - O_max by apply leq_trunc_div.
have ARR_G : job_arrival j2 >= O_max by auto.
- now ssrlia.
+ now lia.
Qed.
(** We show that job [j1] arrives in its own hyperperiod. *)
@@ -207,7 +208,7 @@ Section PeriodicLemmas.
+ specialize (div_floor_add_g (job_arrival j1 - O_max) HP) => AB.
feed_n 1 AB; first by apply valid_periods_imply_pos_hp => //.
rewrite ltn_subLR // in AB.
- now rewrite -/(HP); ssrlia.
+ now rewrite -/(HP); lia.
Qed.
(** We show that the [corresponding_job_in_hyperperiod] of [j1] in [j2]'s hyperperiod
diff --git a/analysis/facts/job_index.v b/analysis/facts/job_index.v
index 1c14706282884fadc7db9ae94d7adba2863f185d..b12e0041585a1f270b21cd9e7c537c72d048586d 100644
--- a/analysis/facts/job_index.v
+++ b/analysis/facts/job_index.v
@@ -81,9 +81,9 @@ Section JobIndexLemmas.
j1 = j2.
Proof.
case: (ltngtP (job_arrival j1) (job_arrival j2)) => [LT|GT|EQ].
- - now apply case_arrival_lte_implies_equal_job; ssrlia.
- - now apply case_arrival_gt_implies_equal_job; ssrlia.
- - now apply case_arrival_lte_implies_equal_job; ssrlia.
+ - now apply case_arrival_lte_implies_equal_job; lia.
+ - now apply case_arrival_gt_implies_equal_job; lia.
+ - now apply case_arrival_lte_implies_equal_job; lia.
Qed.
End EqualJobIndex.
@@ -114,7 +114,7 @@ Section JobIndexLemmas.
move : T; rewrite mem_filter => /andP [/eqP SM_TSK JB_IN_ARR].
apply mem_bigcat_nat_exists in JB_IN_ARR; move : JB_IN_ARR => [ind [JB_IN IND_INTR]].
erewrite H_consistent_arrivals in IND_INTR; eauto 2.
- now ssrlia.
+ now lia.
Qed.
(** Given jobs [j1] and [j2] in [arrivals_between_P arr_seq P t1 t2], the fact that
@@ -133,7 +133,7 @@ Section JobIndexLemmas.
apply mem_bigcat_nat_exists in J2ARR; move : J2ARR => [i [J2_IN INEQ]].
apply mem_bigcat_nat with (j := i) => //.
apply H_consistent_arrivals in J2_IN; rewrite J2_IN in ARR_LT.
- now ssrlia.
+ now lia.
Qed.
(** We show that jobs in the sequence [arrivals_between_P] are ordered by their arrival times, i.e.,
@@ -155,7 +155,7 @@ Section JobIndexLemmas.
rewrite index_mem.
now eapply arrival_lt_implies_job_in_arrivals_between_P; eauto.
- apply Bool.not_true_is_false; intro T.
- now apply job_arrival_between in T; try ssrlia.
+ now apply job_arrival_between in T; try lia.
Qed.
(** We observe that index of job [j1] is same in the
@@ -188,14 +188,14 @@ Section JobIndexLemmas.
intros IND_LT.
rewrite /job_index in IND_LT.
move_neq_up ARR_GT; move_neq_down IND_LT.
- rewrite job_index_same_in_task_arrivals /task_arrivals_up_to_job_arrival; try by ssrlia.
- rewrite -> task_arrivals_cat with (t_m := job_arrival j1); try by ssrlia.
+ rewrite job_index_same_in_task_arrivals /task_arrivals_up_to_job_arrival; try by lia.
+ rewrite -> task_arrivals_cat with (t_m := job_arrival j1); try by lia.
rewrite -H_same_task !index_cat ifT; try by apply arrives_in_task_arrivals_up_to.
rewrite ifF.
- now eapply leq_trans;
[apply index_job_lt_size_task_arrivals_up_to_job | rewrite leq_addr].
- apply Bool.not_true_is_false; intro T.
- now apply job_arrival_between in T; try ssrlia.
+ now apply job_arrival_between in T; try lia.
Qed.
(** We show that if job [j1] arrives earlier than job [j2]
@@ -214,7 +214,7 @@ Section JobIndexLemmas.
Lemma job_index_minus_one_lt_size_task_arrivals_up_to:
job_index arr_seq j1 - 1 < size (task_arrivals_up_to_job_arrival arr_seq j1).
Proof.
- apply leq_ltn_trans with (n := job_index arr_seq j1); try by ssrlia.
+ apply leq_ltn_trans with (n := job_index arr_seq j1); try by lia.
now apply index_job_lt_size_task_arrivals_up_to_job.
Qed.
@@ -271,7 +271,7 @@ Section PreviousJob.
index (prev_job arr_seq j) (task_arrivals_up_to_job_arrival arr_seq j) = job_index arr_seq j - 1.
Proof.
apply index_uniq; last by apply uniq_task_arrivals.
- apply leq_ltn_trans with (n := job_index arr_seq j); try by ssrlia.
+ apply leq_ltn_trans with (n := job_index arr_seq j); try by lia.
now apply index_job_lt_size_task_arrivals_up_to_job.
Qed.
@@ -302,7 +302,7 @@ Section PreviousJob.
rewrite mem_filter in PREV_JOB_IN; move : PREV_JOB_IN => /andP [TSK PREV_IN].
apply mem_bigcat_nat_exists in PREV_IN; move : PREV_IN => [i [PREV_IN INEQ]].
apply H_consistent_arrivals in PREV_IN; rewrite -PREV_IN in INEQ.
- now ssrlia.
+ now lia.
Qed.
(** We show that for any job [j] the job index of [prev_job j] is one less
@@ -331,7 +331,7 @@ Section PreviousJob.
- rewrite EQ.
apply/eqP/negPn/negP; rewrite -has_filter => /hasP [j' IN /eqP TASK].
apply mem_bigcat_nat_exists in IN; move : IN => [i [J'_IN ARR_INEQ]].
- now ssrlia.
+ now lia.
- apply/eqP/negPn/negP; rewrite -has_filter => /hasP [j3 IN /eqP TASK].
apply mem_bigcat_nat_exists in IN; move : IN => [i [J3_IN ARR_INEQ]].
have J3_ARR : (arrives_in arr_seq j3) by apply in_arrseq_implies_arrives with (t := i).
@@ -340,7 +340,7 @@ Section PreviousJob.
apply (earlier_arrival_implies_lower_index arr_seq H_consistent_arrivals _ _) in PJ_L_J3 => //; try by
rewrite prev_job_task.
+ apply (earlier_arrival_implies_lower_index arr_seq H_consistent_arrivals _ _) in J3_L_J => //.
- now rewrite prev_job_index_j in PJ_L_J3; try by ssrlia.
+ now rewrite prev_job_index_j in PJ_L_J3; try by lia.
+ now apply prev_job_arr.
Qed.
@@ -355,6 +355,7 @@ Section PreviousJob.
arrives_in arr_seq j' /\
job_index arr_seq j' = k.
Proof.
+ clear H_positive_job_index.
intros k K_LT.
exists (nth j (task_arrivals_up_to_job_arrival arr_seq j) k).
set (jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k).
@@ -371,12 +372,12 @@ Section PreviousJob.
{ rewrite -> diff_jobs_iff_diff_indices => //; eauto.
rewrite /job_index; rewrite [in X in _ <> X] (job_index_same_in_task_arrivals _ _ jk j) => //.
- rewrite index_uniq -/(job_index arr_seq j)=> //; last by apply uniq_task_arrivals.
- now ssrlia.
+ now lia.
- apply H_consistent_arrivals in JK_IN; rewrite -JK_IN in I_INEQ.
- now ssrlia. }
+ now lia. }
{ rewrite /job_index; rewrite [in X in X = _] (job_index_same_in_task_arrivals _ _ jk j) => //.
apply H_consistent_arrivals in JK_IN; rewrite -JK_IN in I_INEQ.
- now ssrlia. }
+ now lia. }
Qed.
End PreviousJob.
diff --git a/analysis/facts/model/offset.v b/analysis/facts/model/offset.v
index c19f246cb91b341a16677a90b61e709f773b9bb9..ed0acbdfa09f46eb48a4fe8ce11f8657018416f0 100644
--- a/analysis/facts/model/offset.v
+++ b/analysis/facts/model/offset.v
@@ -42,7 +42,7 @@ Section OffsetLemmas.
- have IND_LTE : (job_index arr_seq j <= job_index arr_seq j') by rewrite INDX N.
apply index_lte_implies_arrival_lte in IND_LTE => //; last by rewrite TSK.
now apply/eqP; rewrite eqn_leq; apply/andP; split;
- [ssrlia | apply H_valid_offset].
+ [lia | apply H_valid_offset].
Qed.
(** Consider any task set [ts]. *)
diff --git a/analysis/facts/model/task_arrivals.v b/analysis/facts/model/task_arrivals.v
index ee44311df2053760b9beab7009733a7ba71fee2a..83ed2581f90b8a169d9f15ecd194bdc0c2c83efd 100644
--- a/analysis/facts/model/task_arrivals.v
+++ b/analysis/facts/model/task_arrivals.v
@@ -72,7 +72,7 @@ Section TaskArrivals.
move : ARR => [t ARR]; move : (ARR) => EQ.
apply H_consistent_arrivals in EQ.
rewrite (mem_bigcat_nat _ (fun t => arrivals_at arr_seq t) j 0 _ (job_arrival j)) // EQ //.
- now ssrlia.
+ now lia.
Qed.
(** Also, any job [j] from the arrival sequence is contained in
@@ -192,7 +192,7 @@ Section TaskArrivals.
apply /negP; rewrite mem_filter => /andP [_ IN].
apply mem_bigcat_nat_exists in IN; move : IN => [t' [IN NEQt']].
rewrite -(H_consistent_arrivals j t') in NEQt' => //.
- now ssrlia.
+ now lia.
Qed.
(** We show that for any two jobs [j1] and [j2], task arrivals up to arrival of job [j1] form a
@@ -211,9 +211,9 @@ Section TaskArrivals.
split.
- move: (in_nil j2) => /negP => JIN NIL.
rewrite -NIL in JIN; contradict JIN.
- now apply job_in_task_arrivals_between => //; ssrlia.
+ now apply job_in_task_arrivals_between => //; lia.
- rewrite /task_arrivals_up_to_job_arrival TSK1 TSK2.
- now rewrite -task_arrivals_cat; try by ssrlia.
+ now rewrite -task_arrivals_cat; try by lia.
Qed.
(** For any job [j2] with [job_index] equal to [n], the nth job
diff --git a/analysis/facts/model/workload.v b/analysis/facts/model/workload.v
index 6ad3ed36768cccbfb131ba84ff70eff76996dce8..bf520a8c89a682449ff297938ffe6e3dd77c5c7c 100644
--- a/analysis/facts/model/workload.v
+++ b/analysis/facts/model/workload.v
@@ -86,6 +86,7 @@ Section WorkloadFacts.
workload_of_jobs (fun j => (job_arrival j <= t) && P j) (arrivals_between t1 t2)
<= workload_of_jobs (fun j => P j) (arrivals_between t1 (t + ε)).
Proof.
+ clear H_jobs_uniq H_j_in_jobs H_t1_le_t2.
rewrite /workload_of_jobs big_seq_cond.
rewrite -[in X in X <= _]big_filter -[in X in _ <= X]big_filter.
apply leq_sum_sub_uniq; first by apply filter_uniq, arrivals_uniq.
@@ -94,7 +95,7 @@ Section WorkloadFacts.
apply job_in_arrivals_between; eauto.
- by eapply in_arrivals_implies_arrived; eauto 2.
- apply in_arrivals_implies_arrived_between in A; auto; move: A => /andP [A E].
- by unfold ε; apply/andP; split; ssrlia.
+ by unfold ε; apply/andP; split; lia.
Qed.
End Subset.
diff --git a/analysis/facts/periodic/arrival_separation.v b/analysis/facts/periodic/arrival_separation.v
index 0849781ea5ad9067ee93757ead04147fb138bf89..46af75dbfe4b35415f53043de5e535662a5629c3 100644
--- a/analysis/facts/periodic/arrival_separation.v
+++ b/analysis/facts/periodic/arrival_separation.v
@@ -48,11 +48,11 @@ Section JobArrivalSeparation.
job_arrival j2 = job_arrival j1 + task_period tsk.
Proof.
move : (H_periodic_model j2) => PERIODIC.
- feed_n 3 PERIODIC => //; first by rewrite H_consecutive_jobs; ssrlia.
+ feed_n 3 PERIODIC => //; first by rewrite H_consecutive_jobs; lia.
move : PERIODIC => [pj' [ARR_IN_PJ' [INDPJ'J' [TSKPJ' ARRPJ']]]].
rewrite H_consecutive_jobs addnK in INDPJ'J'.
apply equal_index_implies_equal_jobs in INDPJ'J' => //; last by rewrite TSKPJ'.
- now rewrite INDPJ'J' in ARRPJ'; ssrlia.
+ now rewrite INDPJ'J' in ARRPJ'; lia.
Qed.
End ConsecutiveJobSeparation.
@@ -91,29 +91,29 @@ Section JobArrivalSeparation.
{ intros j1 j2 TSKj1 TSKj2 STEP LT ARRj1 ARRj2; exfalso.
specialize (earlier_arrival_implies_lower_index arr_seq H_consistent_arrivals j1 j2) => LT_IND.
feed_n 4 LT_IND => //; first by rewrite TSKj2.
- now ssrlia.
+ now lia.
}
{ intros j1 j2 TSKj1 TSKj2 STEP LT ARRj2 ARRj1.
specialize (exists_jobs_before_j
arr_seq H_consistent_arrivals H_uniq_arrseq j2 ARRj2 (job_index arr_seq j2 - s)) => BEFORE.
destruct s.
- exists 1; repeat split.
- now rewrite (consecutive_job_separation j1) //; ssrlia.
- - feed BEFORE; first by ssrlia.
+ now rewrite (consecutive_job_separation j1) //; lia.
+ - feed BEFORE; first by lia.
move : BEFORE => [nj [NEQNJ [TSKNJ [ARRNJ INDNJ]]]]; rewrite TSKj2 in TSKNJ.
- specialize (IHs nj j2); feed_n 6 IHs => //; first by ssrlia.
+ specialize (IHs nj j2); feed_n 6 IHs => //; first by lia.
{ by apply (lower_index_implies_earlier_arrival _ H_consistent_arrivals tsk);
- eauto with basic_facts; ssrlia.
+ eauto with basic_facts; lia.
}
move : IHs => [n [NZN ARRJ'NJ]].
- move: (H_periodic_model nj) => PERIODIC; feed_n 3 PERIODIC => //; first by ssrlia.
+ move: (H_periodic_model nj) => PERIODIC; feed_n 3 PERIODIC => //; first by lia.
move : PERIODIC => [sj [ARR_IN_SJ [INDSJ [TSKSJ ARRSJ]]]]; rewrite ARRSJ in ARRJ'NJ.
- have INDJ : (job_index arr_seq j1 = job_index arr_seq j2 - s.+2) by ssrlia.
+ have INDJ : (job_index arr_seq j1 = job_index arr_seq j2 - s.+2) by lia.
rewrite INDNJ -subnDA addn1 -INDJ in INDSJ.
apply equal_index_implies_equal_jobs in INDSJ => //; last by rewrite TSKj1 => //.
- exists (n.+1); split; try by ssrlia.
+ exists (n.+1); split; try by lia.
rewrite INDSJ in ARRJ'NJ; rewrite mulSnr.
- now ssrlia.
+ now lia.
}
Qed.
diff --git a/analysis/facts/periodic/arrival_times.v b/analysis/facts/periodic/arrival_times.v
index 3c5afc4996ce6c2017866d05864199e72d9066de..b85f7d42449eedfa88020ef4af55b4ac8fcb61dc 100644
--- a/analysis/facts/periodic/arrival_times.v
+++ b/analysis/facts/periodic/arrival_times.v
@@ -43,10 +43,10 @@ Section PeriodicArrivalTimes.
}
{ intros j ARR TSK_IN JB_INDEX.
move : (H_task_respects_periodic_model j ARR) => PREV_JOB.
- feed_n 2 PREV_JOB => //; first by ssrlia.
+ feed_n 2 PREV_JOB => //; first by lia.
move : PREV_JOB => [pj [ARR' [IND [TSK ARRIVAL]]]].
- specialize (IHn pj); feed_n 3 IHn => //; first by rewrite IND JB_INDEX; ssrlia.
- rewrite ARRIVAL IHn; ssrlia.
+ specialize (IHn pj); feed_n 3 IHn => //; first by rewrite IND JB_INDEX; lia.
+ rewrite ARRIVAL IHn; lia.
}
Qed.
@@ -77,19 +77,19 @@ Section PeriodicArrivalTimes.
induction n.
+ intros * ARR_J TSK ARR.
destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]] => //.
- now apply periodic_arrival_times in SUCC => //; ssrlia.
+ now apply periodic_arrival_times in SUCC => //; lia.
+ intros * ARR_J TSK ARR.
specialize (H_task_respects_periodic_model j); feed_n 3 H_task_respects_periodic_model => //.
{ rewrite lt0n; apply /eqP; intro EQ.
apply (first_job_arrival _ H_consistent_arrivals tsk) in EQ => //.
- now rewrite EQ in ARR; ssrlia.
+ now rewrite EQ in ARR; lia.
}
move : H_task_respects_periodic_model => [j' [ARR' [IND' [TSK' ARRIVAL']]]].
- specialize (IHn j'); feed_n 3 IHn => //; first by rewrite ARR in ARRIVAL'; ssrlia.
+ specialize (IHn j'); feed_n 3 IHn => //; first by rewrite ARR in ARRIVAL'; lia.
rewrite IHn in IND'.
- destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]]; last by ssrlia.
+ destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]]; last by lia.
rewrite (first_job_arrival arr_seq _ tsk)// in ARR.
- ssrlia.
+ by lia.
Qed.
End PeriodicArrivalTimes.
diff --git a/analysis/facts/periodic/max_inter_arrival.v b/analysis/facts/periodic/max_inter_arrival.v
index 4b115615a6a3fbf26976b869057cab8b813a3f93..cd6830f242682be0e7b4897f9a60b33dc25d2fda 100644
--- a/analysis/facts/periodic/max_inter_arrival.v
+++ b/analysis/facts/periodic/max_inter_arrival.v
@@ -44,11 +44,11 @@ Section PeriodicTasksRespectMaxInterArrivalModel.
exists j'; repeat split => //.
{ case: (boolP (j == j')) => [/eqP EQ|NEQ].
- have EQ_IND : (job_index arr_seq j' = job_index arr_seq j) by apply f_equal => //.
- now exfalso; ssrlia.
+ now exfalso; lia.
- now apply /eqP. }
{ have NZ_PERIOD : (task_period tsk > 0) by apply VALID_PERIOD.
rewrite /max_inter_eq_period /task_max_inter_arrival_time ARRJ'.
- now ssrlia. }
+ now lia. }
Qed.
End PeriodicTasksRespectMaxInterArrivalModel.
diff --git a/analysis/facts/periodic/sporadic.v b/analysis/facts/periodic/sporadic.v
index 07bc889a7e99682b32cddb50f7c1443e8cf5e9bd..2a4f509e17d60390ac3869b6de712bfc1b648ddc 100644
--- a/analysis/facts/periodic/sporadic.v
+++ b/analysis/facts/periodic/sporadic.v
@@ -48,18 +48,18 @@ Section PeriodicTasksAsSporadicTasks.
have IND_LT : job_index arr_seq j1 < job_index arr_seq j2.
{ rewrite -> diff_jobs_iff_diff_indices in NEQ => //; eauto; last by rewrite TSK.
move_neq_up IND_LTE; move_neq_down ARR_LT.
- specialize (H_PERIODIC j1); feed_n 3 H_PERIODIC => //; try by ssrlia.
+ specialize (H_PERIODIC j1); feed_n 3 H_PERIODIC => //; try by lia.
move : H_PERIODIC => [pj [ARR_PJ [IND_PJ [TSK_PJ PJ_ARR]]]].
- have JB_IND_LTE : job_index arr_seq j2 <= job_index arr_seq pj by ssrlia.
+ have JB_IND_LTE : job_index arr_seq j2 <= job_index arr_seq pj by lia.
apply index_lte_implies_arrival_lte in JB_IND_LTE => //; try by rewrite TSK_PJ.
rewrite PJ_ARR.
have POS_PERIOD : task_period tsk > 0 by auto.
- now ssrlia. }
- specialize (H_PERIODIC j2); feed_n 3 H_PERIODIC => //; try by ssrlia.
+ now lia. }
+ specialize (H_PERIODIC j2); feed_n 3 H_PERIODIC => //; try by lia.
move: H_PERIODIC => [pj [ARR_PJ [IND_PJ [TSK_PJ PJ_ARR]]]].
- have JB_IND_LTE : job_index arr_seq j1 <= job_index arr_seq pj by ssrlia.
+ have JB_IND_LTE : job_index arr_seq j1 <= job_index arr_seq pj by lia.
apply index_lte_implies_arrival_lte in JB_IND_LTE => //; try by rewrite TSK_PJ.
- now rewrite PJ_ARR; ssrlia.
+ now rewrite PJ_ARR; lia.
Qed.
(** For convenience, we state these obvious correspondences also at the level
diff --git a/analysis/facts/periodic/task_arrivals_size.v b/analysis/facts/periodic/task_arrivals_size.v
index 63fb3fc1a2a41f4e356af1eeddf00f79355676fb..8d3b831fe49ffa503a18926061d278dca5cc075b 100644
--- a/analysis/facts/periodic/task_arrivals_size.v
+++ b/analysis/facts/periodic/task_arrivals_size.v
@@ -70,11 +70,11 @@ Section TaskArrivalsSize.
have SPO : respects_sporadic_task_model arr_seq tsk; try by auto with basic_facts.
have EQ_ARR_A : (job_arrival a = t) by apply H_consistent_arrivals.
have EQ_ARR_B : (job_arrival b = t) by apply H_consistent_arrivals.
- specialize (SPO a b); feed_n 6 SPO => //; try by ssrlia.
+ specialize (SPO a b); feed_n 6 SPO => //; try by lia.
rewrite EQ_ARR_A EQ_ARR_B in SPO.
rewrite /task_min_inter_arrival_time /periodic_as_sporadic in SPO.
have POS : task_period tsk > 0 by auto.
- now ssrlia.
+ now lia.
Qed.
(** We show that the size of task arrivals (strictly) between two consecutive arrival
@@ -92,7 +92,7 @@ Section TaskArrivalsSize.
move : INEQ => /andP [INEQ1 INEQ2].
rewrite ltn_add2l ltn_mul2r in INEQ1; rewrite ltn_add2l ltn_mul2r in INEQ2.
move : INEQ1 INEQ2 => /andP [A B] /andP [C D].
- now ssrlia.
+ now lia.
Qed.
(** In this section we show some properties of task arrivals in case
@@ -144,7 +144,7 @@ Section TaskArrivalsSize.
have Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0.
{ rewrite size_of_task_arrivals_between big_nat_eq0 => //; intros t T_EQ.
rewrite task_arrivals_size_at_non_arrival => //; intros n EQ.
- now ssrlia.
+ now lia.
}
rewrite Z add0n /task_arrivals_between /arrivals_between big_nat1.
specialize (task_arrivals_at_size 0) => AT_SIZE.
@@ -165,17 +165,17 @@ Section TaskArrivalsSize.
intros l r.
specialize (task_arrivals_cat arr_seq tsk (task_offset tsk + n * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk)) => CAT.
- feed_n 1 CAT; first by ssrlia.
+ feed_n 1 CAT; first by lia.
rewrite CAT size_cat IHn.
specialize (task_arrivals_between_cat arr_seq tsk (task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) (task_offset tsk + n.+1 * task_period tsk).+1) => S_CAT.
- feed_n 2 S_CAT; try by ssrlia.
+ feed_n 2 S_CAT; try by lia.
{ rewrite ltn_add2l ltn_mul2r.
now apply /andP; split => //.
}
rewrite S_CAT size_cat /task_arrivals_between /arrivals_between big_nat1.
rewrite size_task_arrivals_between_eq0 task_arrivals_at_size => //.
- now ssrlia.
+ now lia.
Qed.
(** We show that the number of jobs released by task [tsk] at any instant [t]
@@ -190,7 +190,7 @@ Section TaskArrivalsSize.
destruct (exists_or_not_add_mul_cases (task_offset tsk) (task_period tsk) t) as [[n1 JB_ARR] | JB_NOT_ARR].
+ have EXISTS_N : exists nn, t + n * task_period tsk = task_offset tsk + nn * task_period tsk.
{ exists (n1 + n).
- now rewrite JB_ARR; ssrlia.
+ now rewrite JB_ARR; lia.
}
move : EXISTS_N => [nn JB_ARR'].
now rewrite JB_ARR' JB_ARR !task_arrivals_at_size => //.
diff --git a/analysis/facts/preemption/rtc_threshold/job_preemptable.v b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 8f8a503d721b99723395bf7f62c8f0ed024ba81e..69778b68d180aa6cf4bb88d784ba2e9a7c17de46 100644
--- a/analysis/facts/preemption/rtc_threshold/job_preemptable.v
+++ b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -199,7 +199,7 @@ Section RunToCompletionThreshold.
intros COST; unfold job_rtct, ε.
have N1 := job_last_nonpreemptive_segment_positive COST.
have N2 := job_last_nonpreemptive_segment_le_job_cost.
- ssrlia.
+ lia.
Qed.
(** Next we show that the run-to-completion threshold is at most
@@ -218,7 +218,7 @@ Section RunToCompletionThreshold.
Proof.
move => Ï /andP [GE LT].
apply/negP; intros C.
- have POS : 0 < job_cost j; first by ssrlia.
+ have POS : 0 < job_cost j; first by lia.
rewrite /job_rtct subnBA in GE; last by apply job_last_nonpreemptive_segment_positive.
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.
diff --git a/analysis/facts/preemption/rtc_threshold/limited.v b/analysis/facts/preemption/rtc_threshold/limited.v
index b6c1111d30ebb54ebd13c10b40e69be1af78766a..4e560671a0316aed259af94e44c74da1cc6f8076 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; 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 F := number_of_preemption_points_in_task_at_least_two; lia.
+ - rewrite [in X in X - 1]size_of_seq_of_distances; [lia | apply number_of_preemption_points_in_task_at_least_two].
+ } lia.
}
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/priority/fifo.v b/analysis/facts/priority/fifo.v
index d3b8aeedce19151980208f098d49d1b28dc2ad29..3228d7e60937e1ffa6352f7b3407f4afa44bc09b 100644
--- a/analysis/facts/priority/fifo.v
+++ b/analysis/facts/priority/fifo.v
@@ -119,7 +119,7 @@ Section BasicLemmas.
- do 2 (apply /andP; split; last by done).
eapply scheduled_implies_pending in SCHED1; try eauto with basic_facts.
move : SCHED1 => /andP [HAS COMPL].
- by apply leq_trans with t.-1; [exact HAS| ssrlia].
+ by apply leq_trans with t.-1; [exact HAS| lia].
- move: SCHEDj_other IDLE.
rewrite scheduled_at_def => /eqP SCHED /eqP IDLE.
by rewrite IDLE in SCHED. }
@@ -132,7 +132,7 @@ Section BasicLemmas.
rewrite /hep_job /fifo.FIFO -ltnNge in HEP.
eapply (early_hep_job_is_scheduled arr_seq ) in SCHED1; try eauto 2 with basic_facts.
- apply scheduled_implies_not_completed in INTER; eauto with basic_facts.
- by eapply (incompletion_monotonic sched s t.-1 t) in INTER; [move: INTER => /negP|ssrlia].
+ by eapply (incompletion_monotonic sched s t.-1 t) in INTER; [move: INTER => /negP|lia].
- by move=> ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=]. }
Qed.
diff --git a/analysis/facts/priority/sequential.v b/analysis/facts/priority/sequential.v
index 54acdac9705efc410fb65308ba6fc4d343146407..06bcf3ac4fc8ff1d301fb4c8b558f8d5443f5fd0 100644
--- a/analysis/facts/priority/sequential.v
+++ b/analysis/facts/priority/sequential.v
@@ -66,7 +66,7 @@ Section SequentialJLFP.
specialize (ALL_SCHED pt); feed ALL_SCHED; first by apply/andP; split.
have PEND1: pending sched j1 pt.
{ apply/andP; split.
- - by rewrite /has_arrived; ssrlia.
+ - by rewrite /has_arrived; lia.
- by move: NCOMPL; apply contra, completion_monotonic.
}
apply H_job_ready in PEND1 => //; destruct PEND1 as [j3 [ARR3 [READY3 HEP3]]].
diff --git a/analysis/facts/readiness/sequential.v b/analysis/facts/readiness/sequential.v
index 9330505d73ee702b3ffdfcd6900a4810fff87eac..8614b72c8a9f1965a714fa4d08e0fe06a5bd6c29 100644
--- a/analysis/facts/readiness/sequential.v
+++ b/analysis/facts/readiness/sequential.v
@@ -98,7 +98,7 @@ Section SequentialTasksReadiness.
have PEND' : pending sched j' t.
{ apply/andP; split; last by done.
move: PEND => /andP [LE _].
- by unfold has_arrived in *; ssrlia.
+ by unfold has_arrived in *; lia.
}
specialize (IHk j' LE' t ARR' PEND').
destruct IHk as [j'' [ARR'' [READY'' HEP'']]].
diff --git a/analysis/facts/shifted_job_costs.v b/analysis/facts/shifted_job_costs.v
index 5cd9b2c620a6009f9502fdf9b0f6cace5c047538..03ad3562c00d90ebb7788f1fdfd36a184bd18457 100644
--- a/analysis/facts/shifted_job_costs.v
+++ b/analysis/facts/shifted_job_costs.v
@@ -83,7 +83,7 @@ Section ValidJobCostsShifted.
+ now apply H_valid_offsets_in_taskset.
+ now apply H_valid_periods_in_taskset.
+ now apply H_periodic_taskset.
- + now ssrlia.
+ + now lia.
Qed.
End ValidJobCostsShifted.
diff --git a/analysis/facts/sporadic.v b/analysis/facts/sporadic.v
index 24afade5787d4f9eb926c353c02ab61cb0216362..1ac074ec9f148975a82df4477ebd17d8d6fbc95b 100644
--- a/analysis/facts/sporadic.v
+++ b/analysis/facts/sporadic.v
@@ -46,12 +46,12 @@ Section SporadicModelIndexLemmas.
intro IND.
move: (H_sporadic_model j1 j2) => SPORADIC; feed_n 6 SPORADIC => //.
- rewrite -> diff_jobs_iff_diff_indices => //; eauto.
- + now ssrlia.
+ + now lia.
+ now rewrite H_j1_task.
- apply (index_lte_implies_arrival_lte arr_seq); try eauto.
now rewrite H_j1_task.
- have POS_IA : task_min_inter_arrival_time tsk > 0 by auto.
- now ssrlia.
+ now lia.
Qed.
End SporadicModelIndexLemmas.
@@ -97,8 +97,8 @@ Section DifferentJobsImplyDifferentArrivalTimes.
intros UNEQ EQ_ARR.
rewrite -> diff_jobs_iff_diff_indices in UNEQ => //; eauto; last by rewrite H_j1_task.
move /neqP: UNEQ; rewrite neq_ltn => /orP [LT|LT].
- all: try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; ssrlia ) ||
- now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; ssrlia.
+ all: try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; lia ) ||
+ now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; lia.
Qed.
(** We prove a stronger version of the above lemma by showing
@@ -113,7 +113,7 @@ Section DifferentJobsImplyDifferentArrivalTimes.
case: (boolP (j1 == j2)) => [/eqP EQ | /eqP NEQ]; first by auto.
rewrite -> diff_jobs_iff_diff_indices in NEQ => //; eauto; last by rewrite H_j1_task.
move /neqP: NEQ; rewrite neq_ltn => /orP [LT|LT].
- all: try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; ssrlia ) || now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; ssrlia.
+ all: try ( now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; lia ) || now apply lower_index_implies_earlier_arrival with (tsk := tsk) in LT => //; lia.
Qed.
End DifferentJobsImplyDifferentArrivalTimes.
@@ -239,7 +239,7 @@ Section SporadicArrivals.
- now apply prev_job_task.
- intro EQ.
have SM_IND: job_index arr_seq j1 - 1 = job_index arr_seq j1 by rewrite -prev_job_index // EQ.
- now ssrlia.
+ now lia.
Qed.
(** We show that task arrivals at [job_arrival j1] is the
diff --git a/analysis/facts/tdma.v b/analysis/facts/tdma.v
index aca8b5cc0ee81813407bb27ecc3af2cd5b8d72a6..6d0bde3b7f0297f0c655e615457f762d09dad08d 100644
--- a/analysis/facts/tdma.v
+++ b/analysis/facts/tdma.v
@@ -136,11 +136,11 @@ 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 ssrlia.
+ case (O1 <= t %% cycle) eqn:O1T; case (O2 <= t %% cycle) eqn:O2T; intros G1 G2; try lia.
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.
+ all: by apply relation_offset in order; fold O1 O2 in order; try lia; auto; apply/eqP; auto.
Qed.
End TimeSlotOrderFacts.
diff --git a/classic/analysis/apa/interference_bound_edf.v b/classic/analysis/apa/interference_bound_edf.v
index 8b10fba0ed7471d16cb9347e8afff3dd7f7305cc..a7bde7f42ae1379c1c2839ffd495eb9bc209af9c 100644
--- a/classic/analysis/apa/interference_bound_edf.v
+++ b/classic/analysis/apa/interference_bound_edf.v
@@ -808,6 +808,7 @@ Module InterferenceBoundEDF.
Lemma interference_bound_edf_many_periods_in_between :
a_lst - a_fst >= num_mid_jobs.+1 * p_k.
Proof.
+ clear H_at_least_one_cpu H_tsk_i_in_task_set H_delta_le_deadline.
unfold a_fst, a_lst, j_fst, j_lst.
assert (EQnk: num_mid_jobs.+1=(size sorted_jobs).-1).
by rewrite H_at_least_two_jobs.
@@ -841,7 +842,7 @@ Module InterferenceBoundEDF.
{
apply H_sporadic_tasks; try (by done).
unfold cur, next, not; intro EQ; move: EQ => /eqP EQ.
- rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; try ssrlia.
+ rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; try lia.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
diff --git a/classic/analysis/apa/workload_bound.v b/classic/analysis/apa/workload_bound.v
index 9bd2aef4cb190275588b05be16c0aece6ce641fc..faa6d8582babf00177598085b5406f6e5787868a 100644
--- a/classic/analysis/apa/workload_bound.v
+++ b/classic/analysis/apa/workload_bound.v
@@ -548,7 +548,7 @@ Module WorkloadBound.
{
apply H_sporadic_tasks; try (by done).
unfold cur, next, not; intro EQ; move: EQ => /eqP EQ.
- rewrite nth_uniq in EQ; first move: EQ => /eqP EQ; try ssrlia.
+ rewrite nth_uniq in EQ; first move: EQ => /eqP EQ; try lia.
by rewrite sort_uniq -/scheduled_jobs filter_uniq // undup_uniq.
by rewrite CURtsk.
}
diff --git a/classic/analysis/global/basic/interference_bound_edf.v b/classic/analysis/global/basic/interference_bound_edf.v
index c7acc1cbabbc23946c94eb4fa7c44535afe1bbcf..9e8f0bb64e4769244de2c091b27e119b697e621c 100644
--- a/classic/analysis/global/basic/interference_bound_edf.v
+++ b/classic/analysis/global/basic/interference_bound_edf.v
@@ -806,6 +806,7 @@ Module InterferenceBoundEDF.
Lemma interference_bound_edf_many_periods_in_between :
a_lst - a_fst >= num_mid_jobs.+1 * p_k.
Proof.
+ clear H_at_least_one_cpu H_tsk_i_in_task_set H_delta_le_deadline.
unfold a_fst, a_lst, j_fst, j_lst.
assert (EQnk: num_mid_jobs.+1=(size sorted_jobs).-1).
by rewrite H_at_least_two_jobs.
@@ -839,7 +840,7 @@ Module InterferenceBoundEDF.
{
apply H_sporadic_tasks; try (by done).
unfold cur, next, not; intro EQ; move: EQ => /eqP EQ.
- rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; ssrlia.
+ rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; lia.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
diff --git a/classic/analysis/global/basic/workload_bound.v b/classic/analysis/global/basic/workload_bound.v
index e0806cef23dc937bfc1cf9882d608f9ed848fec9..b08d6d6778bfc0b13e1f636f3b06d81e997e5207 100644
--- a/classic/analysis/global/basic/workload_bound.v
+++ b/classic/analysis/global/basic/workload_bound.v
@@ -551,7 +551,7 @@ Module WorkloadBound.
{
apply H_sporadic_tasks; try (by done).
unfold cur, next, not; intro EQ; move: EQ => /eqP EQ.
- rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; try ssrlia.
+ rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; try lia.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/scheduled_jobs filter_uniq // undup_uniq.
diff --git a/classic/analysis/global/jitter/interference_bound_edf.v b/classic/analysis/global/jitter/interference_bound_edf.v
index 4948f71ee887f30b0c6d769a034825934dc16ba2..89347396fe765da5e7a4360e5a1e8e8205d4b4f6 100644
--- a/classic/analysis/global/jitter/interference_bound_edf.v
+++ b/classic/analysis/global/jitter/interference_bound_edf.v
@@ -893,6 +893,8 @@ Module InterferenceBoundEDFJitter.
Lemma interference_bound_edf_many_periods_in_between :
a_lst - a_fst >= num_mid_jobs.+1 * p_k.
Proof.
+ clear H_tsk_k_in_task_set.
+ clear H_at_least_one_cpu H_tsk_i_in_task_set H_delta_le_deadline.
unfold a_fst, a_lst, j_fst, j_lst.
assert (EQnk: num_mid_jobs.+1=(size sorted_jobs).-1).
by rewrite H_at_least_two_jobs.
@@ -935,7 +937,7 @@ Module InterferenceBoundEDFJitter.
{
apply H_sporadic_tasks; try (by done).
unfold cur, next, not; intro EQ; move: EQ => /eqP EQ.
- rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; ssrlia.
+ rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; lia.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
diff --git a/classic/analysis/global/jitter/workload_bound.v b/classic/analysis/global/jitter/workload_bound.v
index 463f35ccc19bdfe3397d22357aa71cd128f2b556..2224ddcf75a5773c77b83314bc03d85a40620ada 100644
--- a/classic/analysis/global/jitter/workload_bound.v
+++ b/classic/analysis/global/jitter/workload_bound.v
@@ -569,7 +569,7 @@ Module WorkloadBoundJitter.
{
apply H_sporadic_tasks; try (by done).
unfold cur, next, not; intro EQ; move: EQ => /eqP EQ.
- rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; ssrlia.
+ rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; lia.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/scheduled_jobs filter_uniq // undup_uniq.
diff --git a/classic/analysis/global/parallel/interference_bound_edf.v b/classic/analysis/global/parallel/interference_bound_edf.v
index 75187d19d69cfed98c580ea7394b893120d34607..92e6925ef9ea43d7237469f791f6a7e08f418c16 100644
--- a/classic/analysis/global/parallel/interference_bound_edf.v
+++ b/classic/analysis/global/parallel/interference_bound_edf.v
@@ -606,6 +606,8 @@ Module InterferenceBoundEDF.
Lemma interference_bound_edf_many_periods_in_between :
a_lst - a_fst >= num_mid_jobs.+1 * p_k.
Proof.
+ clear H_tsk_k_in_task_set.
+ clear H_at_least_one_cpu H_tsk_i_in_task_set H_delta_le_deadline.
unfold a_fst, a_lst, j_fst, j_lst.
assert (EQnk: num_mid_jobs.+1=(size sorted_jobs).-1).
by rewrite H_at_least_two_jobs.
@@ -639,7 +641,7 @@ Module InterferenceBoundEDF.
{
apply H_sporadic_tasks; try (by done).
unfold cur, next, not; intro EQ; move: EQ => /eqP EQ.
- rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; ssrlia.
+ rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; lia.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
diff --git a/classic/analysis/global/parallel/workload_bound.v b/classic/analysis/global/parallel/workload_bound.v
index c20dc4eca1ba0a24c6760ea14414ce2ed047d298..f70b6dfb9807070a48bd95e26b89884879510b05 100644
--- a/classic/analysis/global/parallel/workload_bound.v
+++ b/classic/analysis/global/parallel/workload_bound.v
@@ -410,7 +410,7 @@ Module WorkloadBound.
{
apply H_sporadic_tasks; try (by done).
unfold cur, next, not; intro EQ; move: EQ => /eqP EQ.
- rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; ssrlia.
+ rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; lia.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/scheduled_jobs filter_uniq // undup_uniq.
diff --git a/classic/analysis/uni/basic/tdma_rta_theory.v b/classic/analysis/uni/basic/tdma_rta_theory.v
index 21fe61975f8aa59b50e44e1dafe67c9607b2cdf5..f931c2203dbe628f68aa3b0b17a82415078f5464 100644
--- a/classic/analysis/uni/basic/tdma_rta_theory.v
+++ b/classic/analysis/uni/basic/tdma_rta_theory.v
@@ -140,7 +140,7 @@ Module ResponseTimeAnalysisTDMA.
with (task_deadline:=task_deadline)
(arr_seq:=arr_seq)(job_deadline:=job_deadline)
(job_task:=job_task)(slot_order:=slot_order) );eauto 2.
- intros. apply H_arrival_times_are_consistent in ARR. ssrlia.
+ intros. apply H_arrival_times_are_consistent in ARR. lia.
- have INJ: arrives_in arr_seq j by exists n.+1.
try ( apply completion_monotonic
with (t0:=job_arrival j + WCRT task_cost task_time_slot ts tsk);auto ) ||
@@ -157,13 +157,13 @@ 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. ssrlia.
+ have JO:job_arrival j_other = job_arrival j by f_equal. lia.
try ( apply completion_monotonic with (t0:= job_arrival j_other +
task_period (job_task j_other)); auto ) ||
apply completion_monotonic with (t:= 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. ssrlia.
+ apply (IHt (job_arrival j_other));auto. lia.
destruct H0 as [tj AAJO]. have CONSIST: job_arrival j_other =tj by auto.
by subst. by subst.
Qed.
@@ -182,7 +182,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. ssrlia.
+ have JO:job_arrival j_other = job_arrival j by f_equal. lia.
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 0075cfbf39a274bf2aa765a10af569ac1933e3a4..768409251c5720aa219d81fe96b3ad303dfb29ca 100644
--- a/classic/analysis/uni/basic/tdma_wcrt_analysis.v
+++ b/classic/analysis/uni/basic/tdma_wcrt_analysis.v
@@ -1,5 +1,5 @@
Require Import Arith Nat.
-Require Import prosa.classic.util.all.
+Require Import prosa.classic.util.all prosa.classic.util.ssrlia.
Require Import prosa.classic.model.arrival.basic.job
prosa.classic.model.arrival.basic.task_arrival
prosa.classic.model.schedule.uni.schedulability
@@ -389,15 +389,14 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
repeat rewrite subn0.
case Hc_slot:(c < time_slot); rewrite /duration_to_finish_from_start_of_slot_with.
* by rewrite ceil_eq1 //; ssrlia.
- * rewrite ceil_suba //; try ssrlia.
+ * rewrite ceil_suba //; [|ssrlia].
rewrite subn1 mulnBl mul1n addnA -addSn addn1.
- apply/eqP. rewrite eqn_add2l subnBA // addnA. repeat rewrite addnBA; try ssrlia.
+ apply/eqP. rewrite eqn_add2l subnBA // addnA. repeat rewrite addnBA; [| |ssrlia].
-- by rewrite addKn addnAC addnK.
-- apply leq_trans with (n:=tdma_cycle - time_slot + time_slot).
- ++ ssrlia.
- ++ apply leq_add.
- ** apply leq_pmull, ceil_neq0; try ssrlia. rewrite ltn_subRL addn0. ssrlia.
- ** apply leqnn.
+ ++ ssrlia.
+ ++ apply leq_add; [|ssrlia].
+ apply leq_pmull, ceil_neq0; lia.
- rewrite Hcases. repeat rewrite addnA. apply/eqP. repeat rewrite eqn_add2r.
rewrite -addn1 -addnA eqn_add2l /to_next_slot /from_start_of_slot.
move:Hcases. repeat rewrite -addnBA //. intro Hcases.
@@ -443,9 +442,10 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
rewrite ltn_subRL addSn in Hc1. rewrite ltn_subRL addnS -addnBA // in Hc.
ssrlia.
* repeat rewrite -addnBA //.
- case (c < time_slot - ((t.+1 + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle)) eqn:Hc1; try ssrlia.
+ case (c < time_slot - ((t.+1 + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle)) eqn:Hc1; [ssrlia|].
rewrite prednK // in mod_case. destruct mod_case.
- rewrite addSn in Hc1. ssrlia.
+ rewrite addSn in Hc1.
+ ssrlia.
- destruct c; repeat rewrite -addnBA // in Hc;rewrite -addnBA // in NSLOT;simpl.
+ ssrlia.
+ repeat rewrite -addnBA // addSn.
@@ -489,7 +489,6 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
rewrite addSn case1 case2 add0n subn0 add0n.
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.
diff --git a/classic/implementation/uni/basic/schedule_tdma.v b/classic/implementation/uni/basic/schedule_tdma.v
index 6f82352bfb344179294ed7643e3e23187ae70006..0b53ea6c8e724280bdbea93327f397343c93478c 100644
--- a/classic/implementation/uni/basic/schedule_tdma.v
+++ b/classic/implementation/uni/basic/schedule_tdma.v
@@ -99,7 +99,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 ssrlia.
+ rewrite ->big_cat_nat with (n:=arrj.+1) in LEQ;try lia.
rewrite filter_cat find_cat /=in LEQ.
rewrite find_cat /= in LEQ.
have F: (has (fun job : Job => job == j')
@@ -111,7 +111,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.
- ssrlia.
+ lia.
have TT: (has (fun job : Job => job == j)
[seq j <- \big[cat/[::]]_(0 <= i < arrj.+1)
jobs_arriving_at arr_seq i
@@ -123,7 +123,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. ssrlia.
+ rewrite F TT in LEQ. lia.
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 403c393bf0508cfb478f208b60eeaae71fecf9e8..f409eb8e820a5c5a573f161738c24ff3d6d83a5e 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. ssrlia.
+ intros t1 t2 t3 IN1 IN2. lia.
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 ssrlia.
+ have EQ: task_id x = task_id y by lia.
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.
@@ -145,7 +145,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. ssrlia.
+ apply ts_has_valid_parameters,periodic_arrivals_all_jobs_from_taskset. lia.
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 5d6bd08fb6c7cb768332a1378d4ac6c2e91e2737..194f2293a597ba364375bba2e394517597ac4686 100644
--- a/classic/model/policy_tdma.v
+++ b/classic/model/policy_tdma.v
@@ -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 ssrlia.
+ case (O1 <= t%%cycle)eqn:O1T;case (O2 <= t %%cycle)eqn:O2T;intros G1 G2;try lia.
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.
+ fold O1 O2 in order;try lia;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 ca412336dabd038d6702dfad83d6e33e9e0c583b..482dce9b7b79a964be1384e3afe6d59677b6b0b7 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]; ssrlia.
+ induction G as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre]; lia.
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]; ssrlia.
+ induction h1 as [t|t c e Hcase1 Hpre |t c e Hcase2 Hpre]; lia.
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.
- ssrlia.
+ lia.
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. ssrlia.
+ + inversion Hpre. apply big_geq. lia.
+ 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 ssrlia.
+ apply leq_ltn_trans with (n:= (job_cost job).-1); last lia.
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. ssrlia.
+ destruct ht2 as [p [ht21 ht22]]. exists p. lia.
- 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 ssrlia.
- symmetry. apply big_cat_nat; ssrlia.
+ (\big[addn_monoid/0]_(t' <= i < t'+delta) service_at sched job i)); simpl; try lia.
+ symmetry. apply big_cat_nat; lia.
Qed.
End Lemmas.
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 4cb4c88081c823295c361d3cbcc435d51d954686..0cdc3e9f19495372ce804f13f57e5f2caf6744c3 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
@@ -223,7 +223,7 @@ Module RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
rewrite addn1 addnS in H.
rewrite -subn_gt0 in H0.
apply ltn_trans with (a - c + b); last by done.
- ssrlia.
+ lia.
}
eapply F; eauto 2.
}
diff --git a/classic/util/all.v b/classic/util/all.v
index 963ee97a5752c530cb5f0882fc8198fa0a0f8350..e0385af9f681dffc0d096322bb606493657ccb3c 100644
--- a/classic/util/all.v
+++ b/classic/util/all.v
@@ -1,3 +1,4 @@
+Require Export mathcomp.zify.zify.
Require Export prosa.classic.util.tactics.
Require Export prosa.classic.util.notation.
Require Export prosa.classic.util.bigcat.
@@ -17,4 +18,3 @@ 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.ssrlia.
diff --git a/classic/util/div_mod.v b/classic/util/div_mod.v
index 59eee12dedb1656d3447912c91e150ee88d38e40..acbdd2e26e244bff3ab176709fe302d58b89e929 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 Nat.
-Require Import prosa.classic.util.tactics prosa.util.ssrlia prosa.classic.util.nat.
+Require Import prosa.classic.util.tactics mathcomp.zify.zify 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 ssrlia.
+ assert (X:n<n.+1) by lia.
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. ssrlia.
+ + assert (X: a%%n.+1 < n.+1). by apply ltn_pmod. lia.
- 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. ssrlia.
- - right. apply modnS_eq. ssrlia.
+ - assert (X: a%%n.+1 < n.+1). by apply ltn_pmod. lia.
+ - right. apply modnS_eq. lia.
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; ssrlia.
+ destruct c; lia.
- 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 //; ssrlia).
+ assert (X:a=a-c+c) by (rewrite subnK //; lia).
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).
- ssrlia.
+ lia.
Qed.
diff --git a/classic/util/nat.v b/classic/util/nat.v
index 81961b7a6077466eca106fabee9cffa3b8f46d22..c152181db4d3f2161171a5bef8589b222a7005fc 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.ssrlia.
+Require Import prosa.classic.util.tactics mathcomp.zify.zify.
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; ssrlia.
+ by split; ins; lia.
Qed.
Lemma addmovl:
@@ -38,7 +38,7 @@ Section NatLemmas.
m >= n ->
(p = m - n <-> p + n = m).
Proof.
- by split; ins; ssrlia.
+ by split; ins; lia.
Qed.
Lemma ltSnm : forall n m, n.+1 < m -> n < m.
diff --git a/util/ssrlia.v b/classic/util/ssrlia.v
similarity index 100%
rename from util/ssrlia.v
rename to classic/util/ssrlia.v
diff --git a/classic/util/sum.v b/classic/util/sum.v
index 3a14881e32a53bbf63880a28d34b734e342011cb..2eebe2d4b6937a4023bb833bc95bb90f0682aa81 100644
--- a/classic/util/sum.v
+++ b/classic/util/sum.v
@@ -1,5 +1,5 @@
Require Export prosa.util.sum.
-Require Export prosa.util.ssrlia.
+Require Export mathcomp.zify.zify.
Require Import prosa.classic.util.tactics.
Require Import prosa.classic.util.notation.
diff --git a/coq-prosa.opam b/coq-prosa.opam
index 67939dfa73c6287de7e97b39e4434ee16692d7f8..08a68238bcbe3bbec6e7153715b82e5ed825d1f1 100644
--- a/coq-prosa.opam
+++ b/coq-prosa.opam
@@ -15,6 +15,7 @@ install: [make "install"]
depends: [
"coq" {((>= "8.13" & < "8.16~") | = "dev")}
"coq-mathcomp-ssreflect" {((>= "1.12" & < "1.15~") | = "dev")}
+ "coq-mathcomp-zify"
]
tags: [
diff --git a/doc/tactics.md b/doc/tactics.md
index c93d2d5343fc0211a860c4a43f5f4da21465eb63..126173ba170a4e54899c35a0060c441246a46ea4 100644
--- a/doc/tactics.md
+++ b/doc/tactics.md
@@ -39,5 +39,5 @@ Tactics taken from the standard library of Viktor Vafeiadis.
## Miscellaneous
-- `ssrlia`: Solves arithmetic goals, including ones with `ssreflect`'s definitions.
+- `lia`: Solves arithmetic goals, including ones with `ssreflect`'s definitions.
diff --git a/implementation/facts/extrapolated_arrival_curve.v b/implementation/facts/extrapolated_arrival_curve.v
index 3471c28ff8c4bcd0ca03527b982ce244c9af327b..407816d0f0ba8d706ba042bf761e0cba78bc6df8 100644
--- a/implementation/facts/extrapolated_arrival_curve.v
+++ b/implementation/facts/extrapolated_arrival_curve.v
@@ -14,7 +14,7 @@ Section BasicFacts.
transitive ltn_steps.
Proof.
move=> a b c /andP [FSTab SNDab] /andP [FSTbc SNDbc].
- by apply /andP; split; ssrlia.
+ by apply /andP; split; lia.
Qed.
(** Next, we show that the relation [leq_steps] is reflexive... *)
@@ -31,7 +31,7 @@ Section BasicFacts.
transitive leq_steps.
Proof.
move=> a b c /andP [FSTab SNDab] /andP [FSTbc SNDbc].
- by apply /andP; split; ssrlia.
+ by apply /andP; split; lia.
Qed.
End BasicFacts.
@@ -69,7 +69,7 @@ Section ArrivalCurvePrefixSortedLeq.
move => /andP [ALL SORT].
destruct (leqP (fst (t__c, v__c)) t1) as [R1 | R1], (leqP (fst (t__c, v__c)) t2) as [R2 | R2]; simpl in *.
{ rewrite R1 R2 //=; apply IHsteps; try done. }
- { by ssrlia. }
+ { by lia. }
{ rewrite ltnNge -eqbF_neg in R1; move: R1 => /eqP ->; rewrite R2 //=; apply IHsteps; try done.
- by move: LTN1; rewrite /leq_steps => /andP //= [_ LEc].
- by apply/allP.
@@ -105,7 +105,7 @@ Section ArrivalCurvePrefixSortedLeq.
rewrite [in X in X ++ _](eq_filter (a2 := fun x => fst x <= t)) in LT; last first.
{ clear; intros [a b]; simpl.
destruct (leqP a t).
- - by rewrite Bool.andb_true_r; apply/eqP; ssrlia.
+ - by rewrite Bool.andb_true_r; apply/eqP; lia.
- by rewrite Bool.andb_false_r.
}
{ by rewrite cats0 ltnn in LT. }
@@ -121,7 +121,7 @@ Section ArrivalCurvePrefixSortedLeq.
induction steps; [by done | simpl in *].
move: SORT; rewrite path_sortedE; auto using leq_steps_is_transitive; move => /andP [LE SORT].
apply IHsteps in SORT.
- rewrite path_sortedE; last by intros ? ? ? LE1 LE2; ssrlia.
+ rewrite path_sortedE; last by intros ? ? ? LE1 LE2; lia.
apply/andP; split; last by done.
apply/allP; intros [x y] IN.
by move: LE => /allP LE; specialize (LE _ IN); move: LE => /andP [LT _].
@@ -151,7 +151,7 @@ Section ArrivalCurvePrefixSortedLtn.
destruct l; simpl in *; first by done.
eapply sub_path; last by apply H_sorted_ltn.
intros [a1 b1] [a2 b2] LT.
- by unfold ltn_steps, leq_steps in *; simpl in *; ssrlia.
+ by unfold ltn_steps, leq_steps in *; simpl in *; lia.
Qed.
(** Next, we show that [step_at 0] is equal to [(0, 0)]. *)
@@ -164,7 +164,7 @@ Section ArrivalCurvePrefixSortedLtn.
have EM : [seq step <- steps | fst step <= 0] = [::].
{ apply filter_in_pred0; intros [t' v'] IN.
move: ALL => /allP ALL; specialize (ALL _ IN); simpl in ALL.
- by rewrite -ltnNge //=; move: ALL; rewrite /ltn_steps //= => /andP [T _ ]; ssrlia.
+ by rewrite -ltnNge //=; move: ALL; rewrite /ltn_steps //= => /andP [T _ ]; lia.
}
rewrite EM; destruct (posnP t) as [Z | POS].
{ subst t; simpl.
@@ -222,10 +222,10 @@ Section ExtrapolatedArrivalCurve.
{ by apply/orP; rewrite -leq_eqVlt; apply leq_div2r, ltnW. }
move: ALT => [/eqP EQ | LT].
{ rewrite EQ leq_add2l; apply value_at_monotone => //.
- by apply eqdivn_leqmodn; ssrlia.
+ by apply eqdivn_leqmodn; lia.
}
{ have EQ: exists k, t1 + k = t2 /\ k > 0.
- { exists (t2 - t1); split; ssrlia. }
+ { exists (t2 - t1); split; lia. }
destruct EQ as [k [EQ POS]]; subst t2; clear LTs.
rewrite divnD; last by done.
rewrite !mulnDl -!addnA leq_add2l.
@@ -269,7 +269,7 @@ Section ExtrapolatedArrivalCurve.
s1 < s2 \/ s1 = s2 /\ x < y.
{ clear; intros * LEs LT.
move: LEs; rewrite leq_eqVlt => /orP [/eqP EQ | LTs].
- { by subst s2; rename s1 into s; right; split; [ done | ssrlia]. }
+ { by subst s2; rename s1 into s; right; split; [ done | lia]. }
{ by left. }
}
apply AF with (m := prefix h).
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index a0e1b44b72278d92471fda13b285d39424e13bc3..ceec37fd490691d188145c7395940c5f5ed08a1c 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -189,7 +189,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
by move: JINB; move => /andP [_ T].
}
rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline in NOTHEP.
- rewrite /D; ssrlia.
+ rewrite /D; lia.
}
Qed.
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index f59b44bb98c7b57893fc47d955200ab94e2ee718..59e285a0d729204d461997a0f7d55ed7a23fa5fb 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -252,7 +252,7 @@ Section AbstractRTAforFIFOwithArrivalCurves.
eauto 2 with basic_facts;last by done.
move : H_busy_interval => [ [_ [_ [QUIET /andP [ARR _ ]]]] _].
destruct (leqP t t1) as [LE | LT].
- { have EQ : t = job_arrival j by apply eq_trans with t1; ssrlia.
+ { have EQ : t = job_arrival j by apply eq_trans with t1; lia.
rewrite EQ in COMPL; apply completed_on_arrival_implies_zero_cost in COMPL; eauto with basic_facts.
by move: (H_job_cost_positive); rewrite /job_cost_positive COMPL. }
{ specialize (QUIET t); feed QUIET.
@@ -280,7 +280,7 @@ Section AbstractRTAforFIFOwithArrivalCurves.
move => t1 t2 Δ j ARRj TSKj BUSY IN_BUSY NCOMPL.
move: H_valid_schedule => [READY MUST ].
rewrite /cumul_interference cumulative_interference_split.
- have JPOS: job_cost_positive j by rewrite -ltnNge in NCOMPL; unfold job_cost_positive; ssrlia.
+ have JPOS: job_cost_positive j by rewrite -ltnNge in NCOMPL; unfold job_cost_positive; lia.
move: (BUSY) => [ [ /andP [LE GT] [QUIETt1 _ ] ] [QUIETt2 EQNs]].
erewrite (cumulative_priority_inversion_is_bounded j ARRj JPOS t1 t2); rewrite //= add0n.
rewrite (instantiated_cumulative_interference_of_hep_jobs_equal_total_interference_of_hep_jobs arr_seq) //=;
@@ -293,7 +293,7 @@ Section AbstractRTAforFIFOwithArrivalCurves.
{ apply leq_trans with (task_rbf ε).
( try ( apply (task_rbf_1_ge_task_cost arr_seq) with (j0 := j) => //= ) ||
apply (task_rbf_1_ge_task_cost arr_seq) with (j := j) => //=); first by auto.
- by apply task_rbf_monotone; [apply H_valid_arrival_curve | ssrlia]. }
+ by apply task_rbf_monotone; [apply H_valid_arrival_curve | lia]. }
{ eapply leq_trans; last first.
by erewrite leq_add2l; eapply task_rbf_excl_tsk_bounds_task_workload_excl_j; eauto 1.
rewrite addnBA.
@@ -383,14 +383,14 @@ Section AbstractRTAforFIFOwithArrivalCurves.
- destruct H_valid_run_to_completion_threshold as [TASKvalid JOBvalid].
by apply TASKvalid.
- rewrite addnBA; first by rewrite leq_sub2r // leq_add2l.
- have GE: task_cost tsk <= R; last by ssrlia.
+ have GE: task_cost tsk <= R; last by lia.
rewrite !add0n in LE1.
rewrite -(leqRW LE2) -(leqRW LE1).
by eapply (task_cost_le_sum_rbf arr_seq); eauto with basic_facts. }
{ rewrite subnK; first by done.
rewrite !add0n in LE1. apply leq_trans with F; last by done.
apply leq_trans with (\sum_(tsko <- ts) rbf tsko ε); last by done.
- apply leq_trans with (task_cost tsk); first by ssrlia.
+ apply leq_trans with (task_cost tsk); first by lia.
eapply task_cost_le_sum_rbf; eauto with basic_facts. }
Qed.
diff --git a/scripts/known-long-proofs.json b/scripts/known-long-proofs.json
index a5e0cc60aae214f74c4e17c8b2f669ba42da80be..9374c63cac604f3151bd83f3943fdfa035156a20 100644
--- a/scripts/known-long-proofs.json
+++ b/scripts/known-long-proofs.json
@@ -32,7 +32,7 @@
},
"./classic/analysis/apa/interference_bound_edf.v": {
"interference_bound_edf_holds_for_single_job_that_completes_on_time": 90,
- "interference_bound_edf_many_periods_in_between": 40
+ "interference_bound_edf_many_periods_in_between": 41
},
"./classic/analysis/apa/workload_bound.v": {
"W_monotonic": 51,
@@ -62,7 +62,7 @@
},
"./classic/analysis/global/basic/interference_bound_edf.v": {
"interference_bound_edf_holds_for_single_job_that_completes_on_time": 100,
- "interference_bound_edf_many_periods_in_between": 40
+ "interference_bound_edf_many_periods_in_between": 41
},
"./classic/analysis/global/basic/workload_bound.v": {
"W_monotonic": 51,
@@ -94,7 +94,7 @@
"interference_bound_edf_holds_for_single_job_that_completes_on_time": 132,
"interference_bound_edf_holds_for_single_job_with_small_slack": 57,
"interference_bound_edf_j_fst_completed_on_time": 48,
- "interference_bound_edf_many_periods_in_between": 49
+ "interference_bound_edf_many_periods_in_between": 51
},
"./classic/analysis/global/jitter/workload_bound.v": {
"W_monotonic": 51,
@@ -122,7 +122,7 @@
"bertogna_fp_all_cpus_are_busy": 81
},
"./classic/analysis/global/parallel/interference_bound_edf.v": {
- "interference_bound_edf_many_periods_in_between": 40,
+ "interference_bound_edf_many_periods_in_between": 42,
"interference_bound_edf_n_k_covers_all_jobs": 47
},
"./classic/analysis/uni/arrival_curves/workload_bound.v": {
@@ -137,7 +137,7 @@
"uniprocessor_response_time_bound_fp": 46
},
"./classic/analysis/uni/basic/tdma_wcrt_analysis.v": {
- "formula_not_sched_St": 45,
+ "formula_not_sched_St": 44,
"formula_sched_St": 100,
"response_time_le_WCRT": 52
},
diff --git a/util/all.v b/util/all.v
index 7d5fd95d0a83d0753eb4cb565fca888db95b5e9b..ca17d35f789556b7d9020055c01caa96c222569a 100644
--- a/util/all.v
+++ b/util/all.v
@@ -1,10 +1,10 @@
+Require Export mathcomp.zify.zify.
Require Export prosa.util.tactics.
Require Export prosa.util.notation.
Require Export prosa.util.bigcat.
Require Export prosa.util.div_mod.
Require Export prosa.util.list.
Require Export prosa.util.nat.
-Require Export prosa.util.ssrlia.
Require Export prosa.util.sum.
Require Export prosa.util.seqset.
Require Export prosa.util.unit_growth.
diff --git a/util/bigcat.v b/util/bigcat.v
index 0ae2586bb9180621de5b110befa574487d11ae9e..98a919e363004bb9af1d936b72d9efb721ede0ed 100644
--- a/util/bigcat.v
+++ b/util/bigcat.v
@@ -1,6 +1,7 @@
+Require Export mathcomp.zify.zify.
Require Export prosa.util.tactics prosa.util.notation.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-Require Export prosa.util.tactics prosa.util.ssrlia prosa.util.list.
+Require Export prosa.util.tactics prosa.util.list.
(** In this section, we introduce lemmas about the concatenation
operation performed over arbitrary sequences. *)
@@ -156,13 +157,13 @@ Section BigCatNatLemmas.
Proof.
intros.
specialize (leq_total t1 t2) => /orP [T1_LT | T2_LT].
- + have EX: exists Δ, t2 = t1 + Δ by simpl; exists (t2 - t1); ssrlia.
+ + have EX: exists Δ, t2 = t1 + Δ by simpl; exists (t2 - t1); lia.
move: EX => [Δ EQ]; subst t2.
induction Δ.
{ by rewrite addn0 !big_geq => //. }
{ rewrite addnS !big_nat_recr => //=; try by rewrite leq_addr.
rewrite filter_cat IHΔ => //.
- by ssrlia. }
+ by lia. }
+ by rewrite !big_geq => //.
Qed.
@@ -175,12 +176,12 @@ Section BigCatNatLemmas.
Proof.
intros.
specialize (leq_total t1 t2) => /orP [T1_LT | T2_LT].
- - have EX: exists Δ, t2 = t1 + Δ by simpl; exists (t2 - t1); ssrlia.
+ - have EX: exists Δ, t2 = t1 + Δ by simpl; exists (t2 - t1); lia.
move: EX => [Δ EQ]; subst t2.
induction Δ.
{ by rewrite addn0 !big_geq => //. }
{ rewrite addnS !big_nat_recr => //=; try by rewrite leq_addr.
- by rewrite size_cat IHΔ => //; ssrlia. }
+ by rewrite size_cat IHΔ => //; lia. }
- by rewrite !big_geq => //.
Qed.
diff --git a/util/div_mod.v b/util/div_mod.v
index eed01ed2ba33b2296b68843ed3eada4bcb3e9d27..aa417e75b569f83f6b21ca482e36405c58d200d7 100644
--- a/util/div_mod.v
+++ b/util/div_mod.v
@@ -16,9 +16,9 @@ Section DivMod.
destruct (posnP h) as [Z | POSh].
{ by subst; rewrite !modn0. }
{ have EX: exists k, t1 + k = t2.
- { exists (t2 - t1); ssrlia. }
+ { exists (t2 - t1); lia. }
destruct EX as [k EX]; subst t2; clear LT.
- rewrite modnD //; replace (h <= t1 %% h + k %% h) with false; first by ssrlia.
+ rewrite modnD //; replace (h <= t1 %% h + k %% h) with false; first by lia.
symmetry; apply/negP/negP; rewrite -ltnNge.
symmetry in EQ; rewrite divnD // in EQ; move: EQ => /eqP.
rewrite -{2}[t1 %/ h]addn0 -addnA eqn_add2l addn_eq0 => /andP [_ /eqP Z2].
@@ -45,7 +45,7 @@ Section DivMod.
- by apply dvdn_mull, dvdnn.
- by apply dvdnn.
}
- { by move: LT; rewrite -addn1 leq_add2r leqNgt ltn_pmod //; ssrlia. }
+ { by move: LT; rewrite -addn1 leq_add2r leqNgt ltn_pmod //; lia. }
}
Qed.
@@ -60,7 +60,7 @@ Section DivMod.
intros x h POS EQ.
rewrite !addnS !addn0.
rewrite addnS divnS // addn0 in EQ.
- destruct (h %| x.+1) eqn:DIV ; rewrite /= in EQ; first by ssrlia.
+ destruct (h %| x.+1) eqn:DIV ; rewrite /= in EQ; first by lia.
by rewrite modnS DIV.
Qed.
@@ -119,7 +119,7 @@ Section DivFloorCeil.
move => d m n LEQ.
rewrite /div_ceil.
have LEQd: m %/ d <= n %/ d by apply leq_div2r.
- destruct (d %| m) eqn:Mm; destruct (d %| n) eqn:Mn => //; first by ssrlia.
+ destruct (d %| m) eqn:Mm; destruct (d %| n) eqn:Mn => //; first by lia.
rewrite ltn_divRL //.
apply ltn_leq_trans with m => //.
move: (leq_trunc_div m d) => LEQm.
@@ -139,8 +139,7 @@ Section DivFloorCeil.
have lkc: (Δ - T) %/ T < Δ %/ T.
{ rewrite divnBr; last by auto.
rewrite divnn POS.
- rewrite ltn_psubCl //; try ssrlia.
- by rewrite divn_gt0.
+ rewrite ltn_psubCl //; lia.
}
destruct (T %| Δ) eqn:EQ1.
{ have divck: (T %| Δ) -> (T %| (Δ - T)) by auto.
@@ -160,15 +159,15 @@ Section DivFloorCeil.
- have DIVab: T %| a + b by apply dvdn_add.
by rewrite /div_ceil DIVa DIVb DIVab divnDl.
- have DIVab: T %| a+b = false by rewrite -DIVb; apply dvdn_addr.
- by rewrite /div_ceil DIVa DIVb DIVab divnDl //=; ssrlia.
+ by rewrite /div_ceil DIVa DIVb DIVab divnDl //=; lia.
- have DIVab: T %| a+b = false by rewrite -DIVa; apply dvdn_addl.
- by rewrite /div_ceil DIVa DIVb DIVab divnDr //=; ssrlia.
+ by rewrite /div_ceil DIVa DIVb DIVab divnDr //=; lia.
- destruct (T %| a + b) eqn:DIVab.
+ rewrite /div_ceil DIVa DIVb DIVab.
- apply leq_trans with (a %/ T + b %/T + 1); last by ssrlia.
+ apply leq_trans with (a %/ T + b %/T + 1); last by lia.
by apply leq_divDl.
+ rewrite /div_ceil DIVa DIVb DIVab.
- apply leq_ltn_trans with (a %/ T + b %/T + 1); last by ssrlia.
+ apply leq_ltn_trans with (a %/ T + b %/T + 1); last by lia.
by apply leq_divDl.
Qed.
@@ -195,12 +194,12 @@ Section DivFloorCeil.
(a + c - b) %% c = if a %% c >= b then (a %% c - b) else (a %% c + c - b).
Proof.
intros * BC.
- have POS : c > 0 by ssrlia.
+ have POS : c > 0 by lia.
have G : a %% c < c by apply ltn_pmod.
case (b <= a %% c) eqn:CASE; rewrite -addnBA; auto; rewrite -modnDml.
- rewrite addnABC; auto.
- by rewrite -modnDmr modnn addn0 modn_small; auto; ssrlia.
- - by rewrite modn_small; ssrlia.
+ by rewrite -modnDmr modnn addn0 modn_small; auto; lia.
+ - by rewrite modn_small; lia.
Qed.
End DivFloorCeil.
diff --git a/util/list.v b/util/list.v
index ebceb3a85e7a8d782e9a5079aa60c89733568cff..f399c9b26eafdbe9d580b9504c52e80a370ebd5e 100644
--- a/util/list.v
+++ b/util/list.v
@@ -1,5 +1,7 @@
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-Require Import prosa.util.ssrlia prosa.util.tactics.
+Require Export mathcomp.zify.zify.
+
+Require Import prosa.util.tactics.
Require Export prosa.util.supremum.
(** We define a few simple operations on lists that return zero for
@@ -565,7 +567,7 @@ Section Sorted.
Proof.
clear; induction xs; intros * SORT; simpl in *; first by done.
have TR : transitive (T:=X) (fun x y : X => f x <= f y).
- { intros ? ? ? LE1 LE2; ssrlia. }
+ { intros ? ? ? LE1 LE2; lia. }
destruct (P a) eqn:Pa, (leqP (f a) t) as [R1 | R1]; simpl.
{ erewrite IHxs; first by reflexivity.
by eapply path_sorted; eauto. }
@@ -573,7 +575,7 @@ Section Sorted.
replace ([seq x <- xs | P x & f x <= t]) with (@nil X); first by done.
symmetry; move: SORT; rewrite path_sortedE // => /andP [ALL SORT].
apply filter_in_pred0; intros ? IN; apply/negP; intros H; move: H => /andP [Px LEx].
- by move: ALL => /allP ALL; specialize (ALL _ IN); simpl in ALL; ssrlia.
+ by move: ALL => /allP ALL; specialize (ALL _ IN); simpl in ALL; lia.
}
{ by eapply IHxs, path_sorted; eauto. }
{ by eapply IHxs, path_sorted; eauto. }
@@ -717,7 +719,7 @@ Section IotaRange.
intros * LE.
interval_to_duration n_le n k.
rewrite iotaD.
- by replace (_ + _ - _) with k; last ssrlia.
+ by replace (_ + _ - _) with k; last lia.
Qed.
(** Next, we prove that [index_iota a b = a :: index_iota a.+1 b]
@@ -759,7 +761,7 @@ Section IotaRange.
{ exists (b-a); by simpl. }
destruct EX as [k BO].
revert x a b BO; induction k; move => x a b BO /andP [GE LT].
- { by exfalso; move: BO; rewrite leqn0 subn_eq0; move => BO; ssrlia. }
+ { by exfalso; move: BO; rewrite leqn0 subn_eq0; move => BO; lia. }
{ destruct a.
{ destruct b; first by done.
rewrite index_iota_lt_step //; simpl.
@@ -767,15 +769,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; ssrlia.
+ - by apply IHk; lia.
}
- rewrite index_iota_lt_step; last by ssrlia.
+ rewrite index_iota_lt_step; last by lia.
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 //; ssrlia.
+ - by rewrite IHk //; lia.
}
Qed.
@@ -808,7 +810,7 @@ Section IotaRange.
induction xs as [ | y' xs]; first by done.
rewrite in_cons IHxs; simpl; clear IHxs.
destruct (y == y') eqn:EQ1, (y' == x) eqn:EQ2; auto.
- - by exfalso; move: EQ1 EQ2 => /eqP EQ1 /eqP EQ2; subst; ssrlia.
+ - by exfalso; move: EQ1 EQ2 => /eqP EQ1 /eqP EQ2; subst; lia.
- by move: EQ1 => /eqP EQ1; subst; rewrite in_cons eq_refl.
- by rewrite in_cons EQ1.
Qed.
@@ -829,7 +831,7 @@ Section IotaRange.
{ exists (b-a); by 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; ssrlia.
+ - by move_neq_down BO; lia.
- move: LE; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT].
+ subst.
rewrite index_iota_lt_step //.
@@ -843,7 +845,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 ssrlia.
+ + rewrite index_iota_lt_step //; last by lia.
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.
@@ -859,7 +861,7 @@ Section IotaRange.
apply in_rem_all in C.
by move_neq_down LT; apply MIN.
}
- by rewrite IHk //; ssrlia.
+ by rewrite IHk //; lia.
Qed.
(** For convenience, we define a special case of
@@ -897,9 +899,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 ssrlia.
+ apply IHk; try lia.
by rewrite index_iota_lt_step // //= PA //= in LT2.
- * apply IHk; try ssrlia.
+ * apply IHk; try lia.
by rewrite index_iota_lt_step // //= PA //= in LT2.
Qed.
diff --git a/util/nat.v b/util/nat.v
index 36d335e52d2a86f57b468c53e64bc30621eaca0c..3a02c22c1f0177042af0aae03fd0dcf202afdeec 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -1,5 +1,7 @@
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
-Require Export prosa.util.tactics prosa.util.ssrlia.
+Require Export mathcomp.zify.zify.
+
+Require Export prosa.util.tactics.
(** Additional lemmas about natural numbers. *)
Section NatLemmas.
@@ -12,7 +14,7 @@ Section NatLemmas.
m1 >= m2 ->
n1 >= n2 ->
(m1 + n1) - (m2 + n2) = (m1 - m2) + (n1 - n2).
- Proof. by ins; ssrlia. Qed.
+ Proof. by ins; lia. Qed.
(** Next, we show that [m + p <= n] implies that [m <= n - p]. Note
that this lemma is similar to ssreflect's lemma [leq_subRL];
@@ -22,21 +24,21 @@ Section NatLemmas.
forall m n p,
m + n <= p ->
m <= p - n.
- Proof. by intros; ssrlia. Qed.
+ Proof. by intros; lia. 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. by intros; ssrlia. Qed.
+ Proof. by intros; lia. 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. by intros; ssrlia. Qed.
+ Proof. by intros; lia. 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]. *)
@@ -72,8 +74,8 @@ Section NatLemmas.
Proof.
intros * LT.
rewrite mulnBl.
- rewrite addnBA; first by ssrlia.
- destruct a; first by ssrlia.
+ rewrite addnBA; first by lia.
+ destruct a; first by lia.
by rewrite leq_pmul2r.
Qed.
@@ -89,7 +91,7 @@ Section NatLemmas.
intros * LTE NEQ n EQ.
specialize (NEQ (n - z)).
rewrite mulnBl in NEQ.
- by ssrlia.
+ by lia.
Qed.
End NatLemmas.
diff --git a/util/nondecreasing.v b/util/nondecreasing.v
index f55b3c7b82aa7badd7e1aae899328b3cb8b6701c..5cb772d091fb071e8e973cbc6c33d72eb2862c78 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.
by rewrite index_iota_lt_step // //= PA //= in LT.
- * apply IHk; try ssrlia.
+ * apply IHk; try lia.
apply/andP; split; first by done.
by rewrite index_iota_lt_step // //= PA //= in LT.
- + apply IHk; try ssrlia.
+ + apply IHk; try lia.
apply/andP; split; first by done.
by rewrite index_iota_lt_step // //= PA //= in LT.
}
@@ -353,7 +353,7 @@ Section NondecreasingSequence.
apply/eqP; rewrite eqbF_neg.
apply nondecreasing_sequence_cons in H0.
apply/negP; intros ?; eauto 2.
- by eapply nondecreasing_sequence_cons_min in H0; eauto 2; ssrlia.
+ by eapply nondecreasing_sequence_cons_min in H0; eauto 2; lia.
Qed.
(** Next we show that function [undup] doesn't change
@@ -626,10 +626,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 + Δ; [by exists (indy - indx); ssrlia | move: EQ => [Δ EQ]; subst indy].
+ have EQ: exists Δ, indy = indx + Δ; [by exists (indy - indx); lia | 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 ssrlia.
+ induction Δ; intros; first by lia.
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|].
diff --git a/util/sum.v b/util/sum.v
index febadac56b77143f068469f784681530c4834df7..6eaed4066211af0caf920f80f83548a425176b73 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -179,7 +179,7 @@ Section SumsOverSequences.
rewrite big_seq_cond [\sum_(_ <- _| P _)_]big_seq_cond.
rewrite eqn_leq; apply /andP; split.
all: apply leq_sum; move => j /andP [IN H].
- all: by move:(EQ j IN H) => LEQ; ssrlia.
+ all: by move:(EQ j IN H) => LEQ; lia.
Qed.
(** Assume that [P1] implies [P2] in all the points contained in
@@ -227,7 +227,7 @@ Section SumsOverSequences.
apply H1; last by done.
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 by intros; ssrlia.
+ have EqLeq: forall a b c d, a + b = c + d -> a <= c -> b >= d by intros; lia.
move: IN; rewrite in_cons; move => /orP [/eqP EQ | IN].
{ subst a.
rewrite PX in H2.
@@ -289,7 +289,7 @@ Section SumsOverRanges.
Proof.
move=> t Δ.
rewrite big_const_nat iter_addn_0.
- by ssrlia.
+ by lia.
Qed.
(** Next, we show that a sum of natural numbers equals zero if and only
@@ -394,8 +394,8 @@ Section SumOfTwoIntervals.
\sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t.
Proof.
induction d; first by rewrite !addn0 !big_geq.
- rewrite !addnS !big_nat_recr => //; try by ssrlia.
- rewrite IHn //=; last by move=> g G_LTl; apply (equal_before_d g); ssrlia.
+ rewrite !addnS !big_nat_recr => //; try by lia.
+ rewrite IHn //=; last by move=> g G_LTl; apply (equal_before_d g); lia.
by rewrite equal_before_d.
Qed.
diff --git a/util/superadditivity.v b/util/superadditivity.v
index 71de032a55cc7f257970843697564c00f42d96db..4c8afba8c7f9920c073b67f0c4715ec32a096ec4 100644
--- a/util/superadditivity.v
+++ b/util/superadditivity.v
@@ -69,7 +69,7 @@ Section Superadditivity.
specialize (SUPER 0 0 (addn0 0)).
contradict SUPER.
apply /negP; rewrite -ltnNge.
- by ssrlia.
+ by lia.
Qed.
(** In this section, we show some of the properties of superadditive functions. *)
@@ -84,9 +84,9 @@ Section Superadditivity.
Proof.
move=> x y LEQ.
apply leq_trans with (f x + f (y - x)).
- - by ssrlia.
+ - by lia.
- apply h_superadditive.
- by ssrlia.
+ by lia.
Qed.
(** Next, we prove that moving any factor [m] outside of the arguments
@@ -96,7 +96,7 @@ Section Superadditivity.
m * f n <= f (m * n).
Proof.
move=> n m.
- elim: m=> [| m IHm]; first by ssrlia.
+ elim: m=> [| m IHm]; first by lia.
rewrite !mulSnr.
apply leq_trans with (f (m * n) + f n).
- by rewrite leq_add2r.
@@ -189,17 +189,17 @@ Section Superadditivity.
rewrite -SUM.
destruct a as [|a'] eqn:EQa; destruct b as [|b'] eqn:EQb => //=.
{ rewrite add0n eq_refl superadditive_first_zero; first by rewrite add0n.
- by apply h_superadditive_until; ssrlia. }
+ by apply h_superadditive_until; lia. }
{ rewrite addn0 eq_refl superadditive_first_zero; first by rewrite addn0.
- by apply h_superadditive_until; ssrlia. }
+ by apply h_superadditive_until; lia. }
{ rewrite -!EQa -!EQb eq_refl //=.
rewrite -{1}(addn0 a) eqn_add2l {1}EQb //=.
rewrite -{1}(add0n b) eqn_add2r {2}EQa //=.
rewrite /minimal_superadditive_extension.
apply in_max0_le.
apply /mapP; exists a.
- - by rewrite mem_iota; ssrlia.
- - by have -> : a + b - a = b by ssrlia. }
+ - by rewrite mem_iota; lia.
+ - by have -> : a + b - a = b by lia. }
Qed.
(** And finally, we prove that [f'] is superadditive until [h.+1]. *)
@@ -209,9 +209,9 @@ Section Superadditivity.
move=> t LEQh a b SUM.
destruct (ltngtP t h) as [LT | GT | EQ].
- rewrite !h_f'_min_extension.
- rewrite !ltn_eqF; try ssrlia.
+ rewrite !ltn_eqF; try lia.
by apply h_superadditive_until.
- - by ssrlia.
+ - by lia.
- rewrite EQ in SUM; rewrite EQ.
by apply minimal_extension_superadditive_at_horizon.
Qed.