Merge PR #8425: Deprecate romega in favor of lia

7 files changed, 49 insertions, 37 deletions

diff --git a/CHANGES b/CHANGES
index 81693a8166..bca4788058 100644
--- a/CHANGES
+++ b/CHANGES
@@ -57,6 +57,8 @@ Tactics
   may need to add `Require Import Lra` to your developments. For compatibility,
   we now define `fourier` as a deprecated alias of `lra`.
 
+- The `romega` tactics have been deprecated; please use `lia` instead.
+
 Focusing
 
 - Focusing bracket `{` now supports named goal selectors,
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 1e92d01125..f7a431ef29 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -26,7 +26,9 @@ Description of ``omega``
 .. tacv:: romega
    :name: romega
 
-   To be documented.
+   .. deprecated:: 8.9
+
+      Use :tacn:`lia` instead.
 
 Arithmetical goals recognized by ``omega``
 ------------------------------------------
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index ee7341a4a2..f1095fc9f1 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -1,4 +1,4 @@
-Require Import Bool PArith DecidableClass Omega ROmega.
+Require Import Bool PArith DecidableClass Omega Lia.
 
 Ltac bool :=
 repeat match goal with
@@ -84,9 +84,9 @@ Ltac case_decide := match goal with
   let H := fresh "H" in
   define (@decide P D) b H; destruct b; try_decide
 | [ |- context [Pos.compare ?x ?y] ] =>
-  destruct (Pos.compare_spec x y); try (exfalso; zify; romega)
+  destruct (Pos.compare_spec x y); try lia
 | [ X : context [Pos.compare ?x ?y] |- _ ] =>
-  destruct (Pos.compare_spec x y); try (exfalso; zify; romega)
+  destruct (Pos.compare_spec x y); try lia
 end.
 
 Section Definitions.
@@ -325,13 +325,13 @@ Qed.
 
 Lemma linear_le_compat : forall k l p, linear k p -> (k <= l)%positive -> linear l p.
 Proof.
-intros k l p H; revert l; induction H; constructor; eauto; zify; romega.
+intros k l p H; revert l; induction H; constructor; eauto; lia.
 Qed.
 
 Lemma linear_valid_incl : forall k p, linear k p -> valid k p.
 Proof.
 intros k p H; induction H; constructor; auto.
-eapply valid_le_compat; eauto; zify; romega.
+eapply valid_le_compat; eauto; lia.
 Qed.
 
 End Validity.
@@ -417,13 +417,13 @@ Qed.
 Hint Extern 5 =>
 match goal with
 | [ |- (Pos.max ?x ?y <= ?z)%positive ] =>
-  apply Pos.max_case_strong; intros; zify; romega
+  apply Pos.max_case_strong; intros; lia
 | [ |- (?z <= Pos.max ?x ?y)%positive ] =>
-  apply Pos.max_case_strong; intros; zify; romega
+  apply Pos.max_case_strong; intros; lia
 | [ |- (Pos.max ?x ?y < ?z)%positive ] =>
-  apply Pos.max_case_strong; intros; zify; romega
+  apply Pos.max_case_strong; intros; lia
 | [ |- (?z < Pos.max ?x ?y)%positive ] =>
-  apply Pos.max_case_strong; intros; zify; romega
+  apply Pos.max_case_strong; intros; lia
 | _ => zify; omega
 end.
 Hint Resolve Pos.le_max_r Pos.le_max_l.
@@ -445,8 +445,8 @@ intros kl kr pl pr Hl Hr; revert kr pr Hr; induction Hl; intros kr pr Hr; simpl.
       now rewrite <- (Pos.max_id i); intuition.
     destruct (Pos.compare_spec i i0); subst; try case_decide; repeat (constructor; intuition).
       + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto.
-      + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; zify; romega.
-      + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; zify; romega.
+      + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; lia.
+      + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; lia.
       + apply (valid_le_compat (Pos.max (Pos.succ i) i0)); intuition.
       + apply (valid_le_compat (Pos.max i (Pos.succ i0))); intuition.
 }
@@ -456,7 +456,7 @@ Lemma poly_mul_cst_valid_compat : forall k v p, valid k p -> valid k (poly_mul_c
 Proof.
 intros k v p H; induction H; simpl; [now auto|].
 case_decide; [|now auto].
-eapply (valid_le_compat i); [now auto|zify; romega].
+eapply (valid_le_compat i); [now auto|lia].
 Qed.
 
 Lemma poly_mul_mon_null_compat : forall i p, null (poly_mul_mon i p) -> null p.
diff --git a/plugins/romega/g_romega.mlg b/plugins/romega/g_romega.mlg
index c1ce30027e..ac4f30b1db 100644
--- a/plugins/romega/g_romega.mlg
+++ b/plugins/romega/g_romega.mlg
@@ -41,14 +41,22 @@ let romega_tactic unsafe l =
        (Tactics.intros)
        (total_reflexive_omega_tactic unsafe))
 
+let romega_depr =
+  Vernacinterp.mk_deprecation
+    ~since:(Some "8.9")
+    ~note:(Some "Use lia instead.")
+    ()
+
 }
 
 TACTIC EXTEND romega
+DEPRECATED { romega_depr }
 |  [ "romega" ] -> { romega_tactic false [] }
 |  [ "unsafe_romega" ] -> { romega_tactic true [] }
 END
 
 TACTIC EXTEND romega'
+DEPRECATED { romega_depr }
 | [ "romega" "with" ne_ident_list(l) ] ->
     { romega_tactic false (List.map Names.Id.to_string l) }
 | [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] }
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 3452967821..c0db8646c7 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -27,7 +27,7 @@
 
 *)
 
-Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega.
+Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -39,7 +39,7 @@ Import Raw.Proofs.
 Local Open Scope pair_scope.
 Local Open Scope Int_scope.
 
-Ltac omega_max := i2z_refl; romega with Z.
+Ltac omega_max := i2z_refl; lia.
 
 Section Elt.
 Variable elt : Type.
@@ -697,7 +697,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   end.
   Proof.
   intros; unfold cardinal_e_2; simpl;
-  abstract (do 2 rewrite cons_cardinal_e; romega with * ).
+  abstract (do 2 rewrite cons_cardinal_e; lia ).
   Defined.
 
   Definition Cmp c :=
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index ec480bb1eb..4a1f24b95e 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -21,7 +21,7 @@ Require Import Znumtheory.
 Require Import Zgcd_alt.
 Require Import Zpow_facts.
 Require Import CyclicAxioms.
-Require Import ROmega.
+Require Import Lia.
 
 Local Open Scope nat_scope.
 Local Open Scope int31_scope.
@@ -1237,7 +1237,7 @@ Section Int31_Specs.
   destruct (Z_lt_le_dec (X+Y) wB).
   contradict H1; auto using Zmod_small with zarith.
   rewrite <- (Z_mod_plus_full (X+Y) (-1) wB).
-  rewrite Zmod_small; romega.
+  rewrite Zmod_small; lia.
 
  generalize (Z.compare_eq ((X+Y) mod wB) (X+Y)); intros Heq.
  destruct Z.compare; intros;
@@ -1261,7 +1261,7 @@ Section Int31_Specs.
   destruct (Z_lt_le_dec (X+Y+1) wB).
   contradict H1; auto using Zmod_small with zarith.
   rewrite <- (Z_mod_plus_full (X+Y+1) (-1) wB).
-  rewrite Zmod_small; romega.
+  rewrite Zmod_small; lia.
 
  generalize (Z.compare_eq ((X+Y+1) mod wB) (X+Y+1)); intros Heq.
  destruct Z.compare; intros;
@@ -1299,8 +1299,8 @@ Section Int31_Specs.
   unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
   destruct (Z_lt_le_dec (X-Y) 0).
   rewrite <- (Z_mod_plus_full (X-Y) 1 wB).
-  rewrite Zmod_small; romega.
-  contradict H1; apply Zmod_small; romega.
+  rewrite Zmod_small; lia.
+  contradict H1; apply Zmod_small; lia.
 
  generalize (Z.compare_eq ((X-Y) mod wB) (X-Y)); intros Heq.
  destruct Z.compare; intros;
@@ -1318,8 +1318,8 @@ Section Int31_Specs.
   unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros.
   destruct (Z_lt_le_dec (X-Y-1) 0).
   rewrite <- (Z_mod_plus_full (X-Y-1) 1 wB).
-  rewrite Zmod_small; romega.
-  contradict H1; apply Zmod_small; romega.
+  rewrite Zmod_small; lia.
+  contradict H1; apply Zmod_small; lia.
 
  generalize (Z.compare_eq ((X-Y-1) mod wB) (X-Y-1)); intros Heq.
  destruct Z.compare; intros;
@@ -1356,7 +1356,7 @@ Section Int31_Specs.
  change [|1|] with 1; change [|0|] with 0.
  rewrite <- (Z_mod_plus_full (0-[|x|]) 1 wB).
  rewrite Zminus_mod_idemp_l.
- rewrite Zmod_small; generalize (phi_bounded x); romega.
+ rewrite Zmod_small; generalize (phi_bounded x); lia.
  Qed.
 
  Lemma spec_pred_c : forall x, [-|sub31c x 1|] = [|x|] - 1.
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index e93ebb1ad5..0c9aca2657 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Nnat ZArith_base ROmega ZArithRing Zdiv Morphisms.
+Require Import Nnat ZArith_base Lia ZArithRing Zdiv Morphisms.
 
 Local Open Scope Z_scope.
 
@@ -129,33 +129,33 @@ Qed.
 Theorem Zrem_lt_pos a b : 0<=a -> b<>0 -> 0 <= Z.rem a b < Z.abs b.
 Proof.
   intros; generalize (Z.rem_nonneg a b) (Z.rem_bound_abs a b);
-   romega with *.
+    lia.
 Qed.
 
 Theorem Zrem_lt_neg a b : a<=0 -> b<>0 -> -Z.abs b < Z.rem a b <= 0.
 Proof.
   intros; generalize (Z.rem_nonpos a b) (Z.rem_bound_abs a b);
-   romega with *.
+   lia.
 Qed.
 
 Theorem Zrem_lt_pos_pos a b : 0<=a -> 0<b -> 0 <= Z.rem a b < b.
 Proof.
-  intros; generalize (Zrem_lt_pos a b); romega with *.
+  intros; generalize (Zrem_lt_pos a b); lia.
 Qed.
 
 Theorem Zrem_lt_pos_neg a b : 0<=a -> b<0 -> 0 <= Z.rem a b < -b.
 Proof.
-  intros; generalize (Zrem_lt_pos a b); romega with *.
+  intros; generalize (Zrem_lt_pos a b); lia.
 Qed.
 
 Theorem Zrem_lt_neg_pos a b : a<=0 -> 0<b -> -b < Z.rem a b <= 0.
 Proof.
-  intros; generalize (Zrem_lt_neg a b); romega with *.
+  intros; generalize (Zrem_lt_neg a b); lia.
 Qed.
 
 Theorem Zrem_lt_neg_neg a b : a<=0 -> b<0 -> b < Z.rem a b <= 0.
 Proof.
-  intros; generalize (Zrem_lt_neg a b); romega with *.
+  intros; generalize (Zrem_lt_neg a b); lia.
 Qed.
 
 
@@ -171,12 +171,12 @@ Lemma Remainder_equiv : forall a b r,
  Remainder a b r <-> Remainder_alt a b r.
 Proof.
   unfold Remainder, Remainder_alt; intuition.
-  - romega with *.
-  - romega with *.
-  - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; romega.
+  - lia.
+  - lia.
+  - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; lia.
   - assert (0 <= Z.sgn r * Z.sgn a).
     { rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto. }
-    destruct r; simpl Z.sgn in *; romega with *.
+    destruct r; simpl Z.sgn in *; lia.
 Qed.
 
 Theorem Zquot_mod_unique_full a b q r :
@@ -185,7 +185,7 @@ Proof.
   destruct 1 as [(H,H0)|(H,H0)]; intros.
   apply Zdiv_mod_unique with b; auto.
   apply Zrem_lt_pos; auto.
-  romega with *.
+  lia.
   rewrite <- H1; apply Z.quot_rem'.
 
   rewrite <- (Z.opp_involutive a).
@@ -193,7 +193,7 @@ Proof.
   generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Z.rem (-a) b)).
   generalize (Zrem_lt_pos (-a) b).
   rewrite <-Z.quot_rem', Z.mul_opp_r, <-Z.opp_add_distr, <-H1.
-  romega with *.
+  lia.
 Qed.
 
 Theorem Zquot_unique_full a b q r :