Require NsatzTactic: nsatz support for Z and Q

The purpose of `NsatzTactic` is to allow using `nsatz` without the
dependency on real axioms. So we declare the instances for `Z` and `Q`
in that file, so that users don't have to re-create them.

Fixes #12860

5 files changed, 64 insertions, 41 deletions

diff --git a/doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst b/doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst
new file mode 100644
index 0000000000..41359098e3
--- /dev/null
+++ b/doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst
@@ -0,0 +1,7 @@
+- **Changed:**
+  ``Require Import Coq.nsatz.NsatzTactic`` now allows using :tacn:`nsatz`
+  with `Z` and `Q` without having to supply instances or using ``Require Import Coq.nsatz.Nsatz``, which
+  transitively requires unneeded files declaring axioms used in the reals
+  (`#12861 <https://github.com/coq/coq/pull/12861>`_,
+  fixes `#12860 <https://github.com/coq/coq/issues/12860>`_,
+  by Jason Gross).
diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst
index ed2e1ea58c..ed93145622 100644
--- a/doc/sphinx/addendum/nsatz.rst
+++ b/doc/sphinx/addendum/nsatz.rst
@@ -34,6 +34,12 @@ Nsatz: tactics for proving equalities in integral domains
 
    You can load the ``Nsatz`` module with the command ``Require Import Nsatz``.
 
+   Alternatively, if you prefer not to transitively depend on the
+   files declaring the axioms used to define the real numbers, you can
+   ``Require Import NsatzTactic`` instead; this will still allow
+   :tacn:`nsatz` to solve goals defined about :math:`\mathbb{Z}`,
+   :math:`\mathbb{Q}` and any user-registered rings.
+
 More about `nsatz`
 ---------------------
 
@@ -85,4 +91,4 @@ performed using :ref:`typeclasses`.
      then `lvar` is replaced by all the variables which are not in
      `parameters`.
 
-See the file `Nsatz.v` for many examples, especially in geometry.
+See the test-suite file `Nsatz.v <https://github.com/coq/coq/blob/master/test-suite/success/Nsatz.v>`_ for many examples, especially in geometry.
diff --git a/test-suite/bugs/closed/bug_12860.v b/test-suite/bugs/closed/bug_12860.v
new file mode 100644
index 0000000000..243aeceba2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12860.v
@@ -0,0 +1,10 @@
+Require Import Coq.nsatz.NsatzTactic.
+Require Import Coq.ZArith.ZArith Coq.QArith.QArith.
+
+Goal forall x y : Z, (x + y = y + x)%Z.
+  intros; nsatz.
+Qed.
+
+Goal forall x y : Q, Qeq (x + y) (y + x).
+  intros; nsatz.
+Qed.
diff --git a/theories/nsatz/Nsatz.v b/theories/nsatz/Nsatz.v
index 70180f47c7..b684775bb4 100644
--- a/theories/nsatz/Nsatz.v
+++ b/theories/nsatz/Nsatz.v
@@ -75,43 +75,3 @@ red. exact Rmult_comm. Defined.
 Instance Rdi : (Integral_domain (Rcr:=Rcri)).
 constructor.
 exact Rmult_integral. exact R_one_zero. Defined.
-
-(* Rational numbers *)
-Require Import QArith.
-
-Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq).
-Defined.
-
-Instance Qri : (Ring (Ro:=Qops)).
-constructor.
-try apply Q_Setoid.
-apply Qplus_comp.
-apply Qmult_comp.
-apply Qminus_comp.
-apply Qopp_comp.
- exact Qplus_0_l. exact Qplus_comm. apply Qplus_assoc.
- exact Qmult_1_l.  exact Qmult_1_r. apply Qmult_assoc.
- apply Qmult_plus_distr_l.  intros. apply Qmult_plus_distr_r.
-reflexivity. exact Qplus_opp_r.
-Defined.
-
-Lemma Q_one_zero: not (Qeq 1%Q 0%Q).
-Proof. unfold Qeq. simpl. lia.  Qed.
-
-Instance Qcri: (Cring (Rr:=Qri)).
-red. exact Qmult_comm. Defined.
-
-Instance Qdi : (Integral_domain (Rcr:=Qcri)).
-constructor.
-exact Qmult_integral. exact Q_one_zero. Defined.
-
-(* Integers *)
-Lemma Z_one_zero: 1%Z <> 0%Z.
-Proof. lia. Qed.
-
-Instance Zcri: (Cring (Rr:=Zr)).
-red. exact Z.mul_comm. Defined.
-
-Instance Zdi : (Integral_domain (Rcr:=Zcri)).
-constructor.
-exact Zmult_integral. exact Z_one_zero. Defined.
diff --git a/theories/nsatz/NsatzTactic.v b/theories/nsatz/NsatzTactic.v
index db7dab2c46..0d24de39d1 100644
--- a/theories/nsatz/NsatzTactic.v
+++ b/theories/nsatz/NsatzTactic.v
@@ -447,3 +447,43 @@ Tactic Notation "nsatz" "with"
     repeat equalities_to_goal;
     nsatz_generic radicalmax info lparam lvar
   end.
+
+(* Rational numbers *)
+Require Import QArith.
+
+Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq).
+Defined.
+
+Instance Qri : (Ring (Ro:=Qops)).
+constructor.
+try apply Q_Setoid.
+apply Qplus_comp.
+apply Qmult_comp.
+apply Qminus_comp.
+apply Qopp_comp.
+ exact Qplus_0_l. exact Qplus_comm. apply Qplus_assoc.
+ exact Qmult_1_l.  exact Qmult_1_r. apply Qmult_assoc.
+ apply Qmult_plus_distr_l.  intros. apply Qmult_plus_distr_r.
+reflexivity. exact Qplus_opp_r.
+Defined.
+
+Lemma Q_one_zero: not (Qeq 1%Q 0%Q).
+Proof. unfold Qeq. simpl. lia.  Qed.
+
+Instance Qcri: (Cring (Rr:=Qri)).
+red. exact Qmult_comm. Defined.
+
+Instance Qdi : (Integral_domain (Rcr:=Qcri)).
+constructor.
+exact Qmult_integral. exact Q_one_zero. Defined.
+
+(* Integers *)
+Lemma Z_one_zero: 1%Z <> 0%Z.
+Proof. lia. Qed.
+
+Instance Zcri: (Cring (Rr:=Zr)).
+red. exact Z.mul_comm. Defined.
+
+Instance Zdi : (Integral_domain (Rcr:=Zcri)).
+constructor.
+exact Zmult_integral. exact Z_one_zero. Defined.