Merge PR #11076: Remove all remaining calls to “omega” from the standard library

Reviewed-by: ejgallego

5 files changed, 34 insertions, 34 deletions

diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index 3ad5bc9f2d..b90e44eed8 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -1,4 +1,4 @@
-Require Import Bool PArith DecidableClass Ring Omega Lia.
+Require Import Bool PArith DecidableClass Ring Lia.
 
 Ltac bool :=
 repeat match goal with
@@ -359,8 +359,8 @@ intros k p var1 var2 Hvar Hv; revert var1 var2 Hvar.
 induction Hv; intros var1 var2 Hvar; simpl; [now auto|].
 rewrite Hvar; [|now auto]; erewrite (IHHv1 var1 var2).
   + erewrite (IHHv2 var1 var2); [ring|].
-    intros; apply Hvar; zify; omega.
-  + intros; apply Hvar; zify; omega.
+    intros; apply Hvar; lia.
+  + intros; apply Hvar; lia.
 Qed.
 
 End Evaluation.
@@ -424,7 +424,7 @@ match goal with
   apply Pos.max_case_strong; intros; lia
 | [ |- (?z < Pos.max ?x ?y)%positive ] =>
   apply Pos.max_case_strong; intros; lia
-| _ => zify; omega
+| _ => lia
 end : core.
 Hint Resolve Pos.le_max_r Pos.le_max_l : core.
 
@@ -488,7 +488,7 @@ induction Hl; intros kr pr Hr; simpl.
     { apply (valid_le_compat (Pos.max i kr)); auto. }
     { apply poly_add_valid_compat; auto.
       now apply poly_mul_mon_valid_compat; intuition. }
-  - repeat apply Pos.max_case_strong; zify; omega.
+  - repeat apply Pos.max_case_strong; lia.
 Qed.
 
 (* Compatibility of linearity wrt to linear operations *)
@@ -497,7 +497,7 @@ Lemma poly_add_linear_compat : forall kl kr pl pr, linear kl pl -> linear kr pr
   linear (Pos.max kl kr) (poly_add pl pr).
 Proof.
 intros kl kr pl pr Hl; revert kr pr; induction Hl; intros kr pr Hr; simpl.
-+ apply (linear_le_compat kr); [|apply Pos.max_case_strong; zify; omega].
++ apply (linear_le_compat kr); [|apply Pos.max_case_strong; lia].
   now induction Hr; constructor; auto.
 + apply (linear_le_compat (Pos.max kr (Pos.succ i))); [|now auto].
   induction Hr; simpl.
@@ -527,17 +527,17 @@ inversion Hv; case_decide; subst.
   destruct (list_nth k var false); ring_simplify; [|now auto].
   rewrite <- (andb_true_l (eval var p1)), <- (andb_true_l (eval var p3)).
   rewrite <- IHp2; auto; rewrite <- IHp1; [ring|].
-  apply (valid_le_compat k); [now auto|zify; omega].
+  apply (valid_le_compat k); [now auto|lia].
 + remember (list_nth k var false) as b; destruct b; ring_simplify; [|now auto].
   case_decide; simpl.
   - rewrite <- (IHp2 p2); [inversion H|now auto]; simpl.
     replace (eval var p1) with (list_nth k var false && eval var p1) by (rewrite <- Heqb; ring); rewrite <- (IHp1 k).
     { rewrite <- Heqb; ring. }
-    { apply (valid_le_compat p2); [auto|zify; omega]. }
+    { apply (valid_le_compat p2); [auto|lia]. }
   - rewrite (IHp2 p2); [|now auto].
     replace (eval var p1) with (list_nth k var false && eval var p1) by (rewrite <- Heqb; ring).
     rewrite <- (IHp1 k); [rewrite <- Heqb; ring|].
-    apply (valid_le_compat p2); [auto|zify; omega].
+    apply (valid_le_compat p2); [auto|lia].
 Qed.
 
 (* Reduction preserves evaluation by boolean assignations *)
@@ -555,10 +555,10 @@ Lemma reduce_aux_le_compat : forall k l p, valid k p -> (k <= l)%positive ->
   reduce_aux l p = reduce_aux k p.
 Proof.
 intros k l p; revert k l; induction p; intros k l H Hle; simpl; auto.
-inversion H; subst; repeat case_decide; subst; try (exfalso; zify; omega).
-+ apply IHp1; [|now auto]; eapply valid_le_compat; [eauto|zify; omega].
+inversion H; subst; repeat case_decide; subst; try lia.
++ apply IHp1; [|now auto]; eapply valid_le_compat; [eauto|lia].
 + f_equal; apply IHp1; auto.
-  now eapply valid_le_compat; [eauto|zify; omega].
+  now eapply valid_le_compat; [eauto|lia].
 Qed.
 
 (* Reduce projects valid polynomials into linear ones *)
@@ -569,13 +569,13 @@ intros i p; revert i; induction p; intros i Hp; simpl.
 + constructor.
 + inversion Hp; subst; case_decide; subst.
   - rewrite <- (Pos.max_id i) at 1; apply poly_add_linear_compat.
-    { apply IHp1; eapply valid_le_compat; [eassumption|zify; omega]. }
+    { apply IHp1; eapply valid_le_compat; [eassumption|lia]. }
     { intuition. }
   - case_decide.
-  { apply IHp1; eapply valid_le_compat; [eauto|zify; omega]. }
-  { constructor; try (zify; omega); auto.
-    erewrite (reduce_aux_le_compat p2); [|assumption|zify; omega].
-    apply IHp1; eapply valid_le_compat; [eauto|]; zify; omega. }
+  { apply IHp1; eapply valid_le_compat; [eauto|lia]. }
+  { constructor; try lia; auto.
+    erewrite (reduce_aux_le_compat p2); [|assumption|lia].
+    apply IHp1; eapply valid_le_compat; [eauto|]; lia. }
 Qed.
 
 Lemma linear_reduce : forall k p, valid k p -> linear k (reduce p).
@@ -583,7 +583,7 @@ Proof.
 intros k p H; induction H; simpl.
 + now constructor.
 + case_decide.
-  - eapply linear_le_compat; [eauto|zify; omega].
+  - eapply linear_le_compat; [eauto|lia].
   - constructor; auto.
     apply linear_reduce_aux; auto.
 Qed.
diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v
index 98f5ab067a..867fe69550 100644
--- a/plugins/btauto/Reflect.v
+++ b/plugins/btauto/Reflect.v
@@ -1,4 +1,4 @@
-Require Import Bool DecidableClass Algebra Ring PArith Omega.
+Require Import Bool DecidableClass Algebra Ring PArith Lia.
 
 Section Bool.
 
@@ -80,7 +80,7 @@ Qed.
 Hint Extern 5 => change 0 with (min 0 0) : core.
 Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat : core.
 Local Hint Constructors valid : core.
-Hint Extern 5 => zify; omega : core.
+Hint Extern 5 => lia : core.
 
 (* Compatibility with validity *)
 
@@ -203,7 +203,7 @@ intros A n; induction n using Pos.peano_rect; intros i x def Hd;
 + unfold make_last; rewrite Pos.peano_rect_succ; fold (make_last n x def).
   induction i using Pos.peano_case.
   - rewrite list_nth_base; reflexivity.
-  - rewrite list_nth_succ; apply IHn; zify; omega.
+  - rewrite list_nth_succ; apply IHn; lia.
 Qed.
 
 Lemma make_last_nth_2 : forall A n x def, list_nth n (@make_last A n x def) def = x.
@@ -226,7 +226,7 @@ intros var; induction var; intros i j x Hd; simpl.
   - rewrite Pos.peano_rect_succ.
     induction i using Pos.peano_rect.
     { rewrite 2list_nth_base; reflexivity. }
-    { rewrite 2list_nth_succ; apply IHvar; zify; omega. }
+    { rewrite 2list_nth_succ; apply IHvar; lia. }
 Qed.
 
 Lemma list_replace_nth_2 : forall var i x, list_nth i (list_replace var i x) false = x.
@@ -251,10 +251,10 @@ intros k p Hl Hp; induction Hl; simpl.
       assert (Hrw : b = true); [|rewrite Hrw; reflexivity]
     end.
     erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto].
-    now intros j Hd; apply list_replace_nth_1; zify; omega.
+    now intros j Hd; apply list_replace_nth_1; lia.
     rewrite list_replace_nth_2, xorb_false_r.
     erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto].
-    now intros j Hd; apply list_replace_nth_1; zify; omega.
+    now intros j Hd; apply list_replace_nth_1; lia.
 Qed.
 
 (* This should be better when using the [vm_compute] tactic instead of plain reflexivity. *)
diff --git a/plugins/micromega/ZifyComparison.v b/plugins/micromega/ZifyComparison.v
index 8a8b40ded8..df75cf2c05 100644
--- a/plugins/micromega/ZifyComparison.v
+++ b/plugins/micromega/ZifyComparison.v
@@ -9,7 +9,8 @@
 (************************************************************************)
 
 Require Import Bool ZArith.
-Require Import ZifyClasses.
+Require Import Zify ZifyClasses.
+Require Import Lia.
 Local Open Scope Z_scope.
 
 (** [Z_of_comparison] is the injection function for comparison *)
@@ -64,11 +65,11 @@ Proof.
   intros.
   destruct (x ?= y) eqn:C; simpl.
   - rewrite Z.compare_eq_iff in C.
-    intuition.
+    lia.
   - rewrite Z.compare_lt_iff in C.
-    intuition.
+    lia.
   - rewrite Z.compare_gt_iff in C.
-    intuition.
+    lia.
 Qed.
 
 Instance ZcompareSpec : BinOpSpec ZcompareZ :=
diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index 58d01c125c..896ee303cc 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -31,6 +31,7 @@ Require Export Ncring_tac.
 Require Export Integral_domain.
 Require Import DiscrR.
 Require Import ZArith.
+Require Import Lia.
 
 Declare ML Module "nsatz_plugin".
 
@@ -413,7 +414,7 @@ Ltac nsatz_generic radicalmax info lparam lvar :=
             try exact integral_domain_minus_one_zero
           || (solve [simpl; unfold R2, equality, eq_notation, addition, add_notation,
                      one, one_notation, multiplication, mul_notation, zero, zero_notation;
-                     discrR || omega]) 
+                     discrR || lia ])
           || ((*simpl*) idtac) || idtac "could not prove discrimination result"
         ]
       ]
@@ -502,7 +503,7 @@ reflexivity. exact Qplus_opp_r.
 Defined.
 
 Lemma Q_one_zero: not (Qeq 1%Q 0%Q).
-unfold Qeq. simpl. auto with *. Qed.
+Proof. unfold Qeq. simpl. lia.  Qed.
 
 Instance Qcri: (Cring (Rr:=Qri)).
 red. exact Qmult_comm. Defined.
@@ -513,8 +514,7 @@ exact Qmult_integral. exact Q_one_zero. Defined.
 
 (* Integers *)
 Lemma Z_one_zero: 1%Z <> 0%Z.
-omega. 
-Qed.
+Proof. lia. Qed.
 
 Instance Zcri: (Cring (Rr:=Zr)).
 red. exact Z.mul_comm. Defined.
diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v
index a0901202f7..8a51bcea02 100644
--- a/plugins/setoid_ring/Rings_Z.v
+++ b/plugins/setoid_ring/Rings_Z.v
@@ -17,8 +17,7 @@ Instance Zcri: (Cring (Rr:=Zr)).
 red. exact Z.mul_comm. Defined.
 
 Lemma Z_one_zero: 1%Z <> 0%Z.
-omega. 
-Qed.
+Proof. discriminate. Qed.
 
 Instance Zdi : (Integral_domain (Rcr:=Zcri)). 
 constructor.