Merge PR #11018: “auto with zarith”: use “lia” rather than “omega”

Ack-by: Zimmi48
Reviewed-by: anton-trunov
Ack-by: jfehrle
Reviewed-by: maximedenes

4 files changed, 38 insertions, 32 deletions

diff --git a/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst b/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst
new file mode 100644
index 0000000000..d510416990
--- /dev/null
+++ b/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst
@@ -0,0 +1,7 @@
+- **Changed:** The :g:`auto with zarith` tactic and variations (including :tacn:`intuition`)
+  may now call the :tacn:`lia` tactic instead of :tacn:`omega`
+  (when the `Omega` module is loaded);
+  more goals may be automatically solved,
+  fewer section variables will be captured spuriously
+  (`#11018 <https://github.com/coq/coq/pull/11018>`_,
+  by Vincent Laporte).
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 1c790a37a0..f6b2544b6e 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -2226,7 +2226,7 @@ Section Int31_Specs.
       < ([|iter312_sqrt n rec ih il j|] + 1) ^ 2.
  Proof.
  revert rec ih il j; elim n; unfold iter312_sqrt; fold iter312_sqrt; clear n.
- intros rec ih il j Hi Hj Hij Hrec; apply sqrt312_step_correct; auto with zarith.
+ intros rec ih il j Hi Hj Hij Hrec; apply sqrt312_step_correct. 1-3: lia.
  intros; apply Hrec. 2: rewrite Z.pow_0_r. 1-3: lia.
  intros n Hrec rec ih il j Hi Hj Hij HHrec.
  apply sqrt312_step_correct; auto.
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index a8c645deb2..c4f738ac39 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -1316,9 +1316,8 @@ Lemma iter_sqrt_correct n rec i j: 0 < φ i -> 0 < φ j ->
   φ (iter_sqrt n rec i j) ^ 2 <= φ i < (φ (iter_sqrt n rec i j) + 1) ^ 2.
 Proof.
  revert rec i j; elim n; unfold iter_sqrt; fold iter_sqrt; clear n.
- intros rec i j Hi Hj Hij H31 Hrec; apply sqrt_step_correct; auto with zarith.
- intros; apply Hrec; auto with zarith.
- rewrite Zpower_0_r; auto with zarith.
+ intros rec i j Hi Hj Hij H31 Hrec; apply sqrt_step_correct. 1-4: lia.
+ intros; apply Hrec; only 2: rewrite Zpower_0_r; auto with zarith.
  intros n Hrec rec i j Hi Hj Hij H31 HHrec.
  apply sqrt_step_correct; auto.
  intros j1 Hj1  Hjp1; apply Hrec; auto with zarith.
@@ -1516,9 +1515,8 @@ Lemma iter2_sqrt_correct n rec ih il j:
       < (φ (iter2_sqrt n rec ih il j) + 1) ^ 2.
 Proof.
  revert rec ih il j; elim n; unfold iter2_sqrt; fold iter2_sqrt; clear n.
- intros rec ih il j Hi Hj Hij Hrec; apply sqrt2_step_correct; auto with zarith.
- intros; apply Hrec; auto with zarith.
- rewrite Zpower_0_r; auto with zarith.
+ intros rec ih il j Hi Hj Hij Hrec; apply sqrt2_step_correct. 1-3: lia.
+ intros; apply Hrec; only 2: rewrite Zpower_0_r; auto with zarith.
  intros n Hrec rec ih il j Hi Hj Hij HHrec.
  apply sqrt2_step_correct; auto.
  intros j1 Hj1  Hjp1; apply Hrec; auto with zarith.
diff --git a/theories/omega/Omega.v b/theories/omega/Omega.v
index 9c2e8a9212..10a5aa47b3 100644
--- a/theories/omega/Omega.v
+++ b/theories/omega/Omega.v
@@ -19,6 +19,7 @@
 Require Export ZArith_base.
 Require Export OmegaLemmas.
 Require Export PreOmega.
+Require Import Lia.
 
 Declare ML Module "omega_plugin".
 
@@ -28,28 +29,28 @@ Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l
 
 Require Export Zhints.
 
-Hint Extern 10 (_ = _ :>nat) => abstract omega: zarith.
-Hint Extern 10 (_ <= _) => abstract omega: zarith.
-Hint Extern 10 (_ < _) => abstract omega: zarith.
-Hint Extern 10 (_ >= _) => abstract omega: zarith.
-Hint Extern 10 (_ > _) => abstract omega: zarith.
-
-Hint Extern 10 (_ <> _ :>nat) => abstract omega: zarith.
-Hint Extern 10 (~ _ <= _) => abstract omega: zarith.
-Hint Extern 10 (~ _ < _) => abstract omega: zarith.
-Hint Extern 10 (~ _ >= _) => abstract omega: zarith.
-Hint Extern 10 (~ _ > _) => abstract omega: zarith.
-
-Hint Extern 10 (_ = _ :>Z) => abstract omega: zarith.
-Hint Extern 10 (_ <= _)%Z => abstract omega: zarith.
-Hint Extern 10 (_ < _)%Z => abstract omega: zarith.
-Hint Extern 10 (_ >= _)%Z => abstract omega: zarith.
-Hint Extern 10 (_ > _)%Z => abstract omega: zarith.
-
-Hint Extern 10 (_ <> _ :>Z) => abstract omega: zarith.
-Hint Extern 10 (~ (_ <= _)%Z) => abstract omega: zarith.
-Hint Extern 10 (~ (_ < _)%Z) => abstract omega: zarith.
-Hint Extern 10 (~ (_ >= _)%Z) => abstract omega: zarith.
-Hint Extern 10 (~ (_ > _)%Z) => abstract omega: zarith.
-
-Hint Extern 10 False => abstract omega: zarith.
+Hint Extern 10 (_ = _ :>nat) => abstract lia: zarith.
+Hint Extern 10 (_ <= _) => abstract lia: zarith.
+Hint Extern 10 (_ < _) => abstract lia: zarith.
+Hint Extern 10 (_ >= _) => abstract lia: zarith.
+Hint Extern 10 (_ > _) => abstract lia: zarith.
+
+Hint Extern 10 (_ <> _ :>nat) => abstract lia: zarith.
+Hint Extern 10 (~ _ <= _) => abstract lia: zarith.
+Hint Extern 10 (~ _ < _) => abstract lia: zarith.
+Hint Extern 10 (~ _ >= _) => abstract lia: zarith.
+Hint Extern 10 (~ _ > _) => abstract lia: zarith.
+
+Hint Extern 10 (_ = _ :>Z) => abstract lia: zarith.
+Hint Extern 10 (_ <= _)%Z => abstract lia: zarith.
+Hint Extern 10 (_ < _)%Z => abstract lia: zarith.
+Hint Extern 10 (_ >= _)%Z => abstract lia: zarith.
+Hint Extern 10 (_ > _)%Z => abstract lia: zarith.
+
+Hint Extern 10 (_ <> _ :>Z) => abstract lia: zarith.
+Hint Extern 10 (~ (_ <= _)%Z) => abstract lia: zarith.
+Hint Extern 10 (~ (_ < _)%Z) => abstract lia: zarith.
+Hint Extern 10 (~ (_ >= _)%Z) => abstract lia: zarith.
+Hint Extern 10 (~ (_ > _)%Z) => abstract lia: zarith.
+
+Hint Extern 10 False => abstract lia: zarith.