Merge pull request #155 from andres-erbsen/split-nsatz

split nsatz into per-domain pieces

Author: andres-erbsen

.nix/rocq-overlays/stdlib-subcomponents/default.nix

@@ -30,7 +30,6 @@ let
     "field" = [ "zarith" ];
     "lqa" = [ "field" "qarith-base" ];
     "qarith" = [ "lqa" ];
-    "nsatz" = [ "zarith" "qarith-base" ];
     "classical-logic" = [ "arith" ];
     "sets" = [ "classical-logic" ];
     "vectors" = [ "lists" ];
@@ -41,7 +40,7 @@ let
     "primitive-floats" = [ "primitive-int" ];
     "primitive-array" = [ "primitive-int" ];
     "primitive-string" = [ "primitive-int" "orders-ex" ];
-    "reals" = [ "nsatz" "qarith" "classical-logic" "vectors" ];
+    "reals" = [ "qarith" "classical-logic" "vectors" ];
     "fmaps-fsets-msets" = [ "orders-ex" "zarith" ];
     "extraction" = [ "primitive-string" "primitive-array" "primitive-floats" ];
     "funind" = [ "arith-base" ];

doc/changelog/01-changed/155-split-nsatz.rst

@@ -0,0 +1,7 @@
+- in `NsatzTactic.v`
+
+  + Split NsatzTactic into a smaller `NsatzTactic` that only depends on
+    `setoid_ring`, and per-domain files `ZNsatz`, `QNsatz`, and `RNsatz`
+    (`#155 <https://github.com/coq/stdlib/pull/155>`_,
+    by Andres Erbsen).
+

doc/stdlib/depends.dot

@@ -16,7 +16,6 @@ digraph stdlib_deps {
 	reals -> qarith;
 	reals -> vectors;
 	reals -> "classical-logic";
-	reals -> nsatz;
 	"arith-base" -> structures;
 	zarith -> lia;
 	zmod -> zarith;
@@ -55,8 +54,6 @@ digraph stdlib_deps {
 	lqa -> "qarith-base";
 	"qarith-base" -> ring;
 	"classical-logic" -> arith;
-	nsatz -> zarith;
-	nsatz -> "qarith-base";
 	extraction -> "primitive-string";
 	extraction -> "primitive-floats";
 	extraction -> "primitive-array";

doc/stdlib/index-list.html.template

@@ -295,6 +295,7 @@ through the <tt>From Stdlib Require Import</tt> command.</p>
     theories/ZArith/Zdiv_facts.v
     theories/ZArith/Zbitwise.v
     theories/ZArith/ZModOffset.v
+    theories/ZArith/ZNsatz.v
     theories/Numbers/DecimalFacts.v
     theories/Numbers/DecimalNat.v
     theories/Numbers/DecimalPos.v
@@ -528,6 +529,7 @@ through the <tt>From Stdlib Require Import</tt> command.</p>
     theories/QArith/Qabs.v
     (theories/QArith/QArith.v)
     theories/QArith/Qcabs.v
+    theories/QArith/QNsatz.v
     theories/Numbers/DecimalQ.v
     theories/Numbers/HexadecimalQ.v
   </dd>
@@ -609,6 +611,7 @@ through the <tt>From Stdlib Require Import</tt> command.</p>
     theories/Reals/SeqSeries.v
     theories/Reals/Sqrt_reg.v
     theories/Reals/Rlogic.v
+    theories/Reals/RNsatz.v
     theories/Reals/Rregisternames.v
     (theories/Reals/Reals.v)
     theories/Reals/Runcountable.v

test-suite/output/NsatzGuessOnce.out

@@ -0,0 +1,2 @@
+Debug: 1: looking for Integral_domain with backtracking
+Debug: 1.1: exact Zdi on Integral_domain, 0 subgoal(s)

test-suite/output/NsatzGuessOnce.v

@@ -0,0 +1,4 @@
+From Stdlib Require Import Integral_domain ZArith ZNsatz.
+Set Typeclasses Debug.
+Lemma test (x y : Z) : x = y -> y = x.
+Proof. nsatz. Qed.