Clean up subcomponent dependencies of lia

Author: andres-erbsen

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

@@ -14,39 +14,37 @@ let
     "classes" = [ "program" "relations" ];
     "bool" = [ "classes" ];
     "structures" = [ "bool" ];
-    "arith-base" = [ "structures" ];
-    "positive" = [ "arith-base" ];
+    "naturals" = [ "structures" ];
     "narith" = [ "ring" ];
-    "zarith-base" = [ "narith-base" ];
-    "narith-base" = [ "positive" ];
-    "lists" = [ "arith-base" ];
-    "ring" = [ "zarith-base" "lists" ];
+    "integers" = [ "naturals" ];
+    "lists" = [ "naturals" ];
+    "ring" = [ "integers" "lists" ];
     "arith" = [ "ring" ];
-    "strings" = [ "arith" ];
-    "lia" = [ "arith" "narith" ];
+    "strings" = [ "integers" "lists" ];
+    "lia" = [ "ring" ];
     "zarith" = [ "lia" ];
     "zmod" = [ "zarith" "sorting" "field" ];
-    "qarith-base" = [ "ring" ];
-    "field" = [ "zarith" ];
+    "qarith-base" = [ "zarith" ];
+    "field" = [ "ring" ];
     "lqa" = [ "field" "qarith-base" ];
     "qarith" = [ "lqa" ];
-    "classical-logic" = [ "arith" ];
+    "classical-logic" = [ "naturals" ];
     "sets" = [ "classical-logic" ];
     "vectors" = [ "lists" ];
     "sorting" = [ "lia" "sets" "vectors" ];
-    "orders-ex" = [ "strings" "sorting" ];
+    "orders-ex" = [ "narith" "strings" "sorting" ];
     "unicode" = [ ];
     "primitive-int" = [ "unicode" "zarith" ];
     "primitive-floats" = [ "primitive-int" ];
     "primitive-array" = [ "primitive-int" ];
     "primitive-string" = [ "primitive-int" "orders-ex" ];
     "reals" = [ "qarith" "classical-logic" "vectors" ];
-    "fmaps-fsets-msets" = [ "orders-ex" "zarith" ];
-    "extraction" = [ "primitive-string" "primitive-array" "primitive-floats" ];
-    "funind" = [ "arith-base" ];
+    "fmaps-fsets-msets" = [ "orders-ex" "zarith" "arith" ];
+    "extraction" = [ "zarith" "primitive-string" "primitive-array" "primitive-floats" ];
+    "funind" = [ "naturals" ];
     "wellfounded" = [ "lists" ];
     "streams" = [ "logic" ];
-    "rtauto" = [ "positive" "lists" ];
+    "rtauto" = [ "integers" "lists" ];
     "compat" = [ "rtauto" "fmaps-fsets-msets" "funind" "extraction" "reals" "zmod" "wellfounded" "streams" ];
     "all" = [ "compat" ];
   };

doc/changelog/01-changed/150-early-lia.rst

@@ -0,0 +1,8 @@
+- Internal dependencies between about 50 stdlib files
+
+  + To diagnose a failing qualified reference use
+    `From Stdlib Require All. Locate My.Qualified.reference.`
+    Then add a Require command for the appropriately granular containing file
+    (`#150 <https://github.com/coq/stdlib/pull/150>`_,
+    by Andres Erbsen).
+

doc/changelog/02-added/150-early-lia.rst

@@ -0,0 +1,12 @@
+- in `ZArithRing`
+
+  + Added `Zpower_theory` to replace the now-deprecated one in `Zpow_def`
+    (`#150 <https://github.com/coq/stdlib/pull/150>`_,
+    by Andres Erbsen).
+
+- in `BinInt`
+
+  + Added lemmas `div_eucl_0_r`, `mod_0_r`, `div_0_r`
+    (`#150 <https://github.com/coq/stdlib/pull/150>`_,
+    by Andres Erbsen).
+

doc/changelog/04-removed/150-early-lia.rst

@@ -0,0 +1,9 @@
+- in `ZMicromega`
+
+  + Support for `EnumProof`s in `ZChecker`.
+    The `lia` plugin does not generate such proofs anymore.
+    If you have a different certificate generator that targets the same
+    checker, please open an issue
+    (`#150 <https://github.com/coq/stdlib/pull/150>`_,
+    by Andres Erbsen).
+

doc/changelog/05-deprecated/150-early-lia.rst

@@ -0,0 +1,23 @@
+- in `ZMicromega`
+
+  + Internal tactics `flatten_bool` and `inv`, definitions `EnumProof`, `isZ0`,
+    `bdepth`, `vars`, and lemmas `eq_le_iff`, `isZ0_0`, `isZ0_0`, `isZ0_n0`,
+    `isZ0_n0`, `eq_true_iff_eq`, `max_var_le`, `max_var_correct`,
+    `max_var_nformulae_correct_aux`, `max_var_nformalae_correct`,
+    `ltof_bdepth_split_l`, `ltof_bdepth_split_r`
+    (`#150 <https://github.com/coq/stdlib/pull/150>`_,
+    by Andres Erbsen).
+
+- in `ZMicromega`
+
+  + Misplaced lemma `Zpower_theory`, with replacement in `ZArithRing`
+    (`#150 <https://github.com/coq/stdlib/pull/150>`_,
+    by Andres Erbsen).
+
+- in `Div`
+
+  + Lemmas `Zmod_0_r` and `Zdiv_0_r` in favor of `BinInt.Z.mod_0_r` and
+    `BinInt.Z.div_0_r`
+    (`#150 <https://github.com/coq/stdlib/pull/150>`_,
+    by Andres Erbsen).
+

doc/stdlib/depends.dot

@@ -12,31 +12,31 @@ digraph stdlib_deps {
 	classes -> relations;
 	program -> "corelib-wrapper";
 	program -> logic;
-	strings -> arith;
+	strings -> integers;
+	strings -> lists;
 	reals -> qarith;
 	reals -> vectors;
 	reals -> "classical-logic";
-	"arith-base" -> structures;
+	naturals -> structures;
+	integers -> naturals;
 	zarith -> lia;
 	zmod -> zarith;
 	zmod -> sorting;
 	zmod -> field;
 	qarith -> lqa;
-	positive -> "arith-base";
 	narith -> ring;
 	ring -> lists;
-	ring -> "zarith-base";
+	ring -> integers;
 	arith -> ring;
 	structures -> bool;
-	"narith-base" -> positive;
-	lists -> "arith-base";
-	"zarith-base" -> "narith-base";
+	lists -> naturals;
 	"primitive-int" -> zarith;
 	"primitive-int" -> unicode;
-	lia -> narith;
-	lia -> arith;
+	lia -> ring;
 	"fmaps-fsets-msets" -> zarith;
+	"fmaps-fsets-msets" -> arith;
 	"fmaps-fsets-msets" -> "orders-ex";
+	"orders-ex" -> narith;
 	"orders-ex" -> strings;
 	"orders-ex" -> sorting;
 	sets -> "classical-logic";
@@ -49,22 +49,22 @@ digraph stdlib_deps {
 	"primitive-string" -> "primitive-int";
 	"primitive-string" -> "orders-ex";
 	vectors -> lists;
-	field -> zarith;
+	field -> ring;
 	lqa -> field;
 	lqa -> "qarith-base";
-	"qarith-base" -> ring;
-	"classical-logic" -> arith;
+	"qarith-base" -> zarith;
+	"classical-logic" -> naturals;
+	extraction -> "zarith";
 	extraction -> "primitive-string";
 	extraction -> "primitive-floats";
 	extraction -> "primitive-array";
 	"primitive-array" -> "primitive-int";
 	streams -> logic;
-	funind -> "arith-base";
+	funind -> naturals;
 	compat -> zmod;
 	compat -> reals;
 	compat -> "fmaps-fsets-msets";
 	compat -> wellfounded;
-	compat -> "primitive-string";
 	compat -> extraction;
 	compat -> streams;
 	compat -> funind;

doc/stdlib/hidden-files

@@ -33,8 +33,6 @@ theories/micromega/Env.v
 theories/micromega/EnvRing.v
 theories/micromega/Fourier.v
 theories/micromega/Fourier_util.v
-theories/micromega/Lia.v
-theories/micromega/Lqa.v
 theories/micromega/Lra.v
 theories/micromega/OrderedRing.v
 theories/micromega/Psatz.v
@@ -51,8 +49,7 @@ theories/micromega/ZifyInst.v
 theories/micromega/ZifyBool.v
 theories/micromega/ZifyUint63.v
 theories/micromega/ZifySint63.v
-theories/micromega/ZifyNat.v
-theories/micromega/ZifyN.v
+theories/micromega/SatDivMod.v
 theories/micromega/ZifyComparison.v
 theories/micromega/ZifyClasses.v
 theories/micromega/ZifyPow.v
@@ -66,7 +63,6 @@ theories/setoid_ring/Algebra_syntax.v
 theories/setoid_ring/ArithRing.v
 theories/setoid_ring/BinList.v
 theories/setoid_ring/Cring.v
-theories/setoid_ring/Field.v
 theories/setoid_ring/Field_tac.v
 theories/setoid_ring/Field_theory.v
 theories/setoid_ring/InitialRing.v
@@ -77,7 +73,6 @@ theories/setoid_ring/Ncring_initial.v
 theories/setoid_ring/Ncring_polynom.v
 theories/setoid_ring/Ncring_tac.v
 theories/setoid_ring/RealField.v
-theories/setoid_ring/Ring.v
 theories/setoid_ring/Ring_base.v
 theories/setoid_ring/Ring_polynom.v
 theories/setoid_ring/Ring_tac.v
@@ -163,3 +158,5 @@ theories/ssr/ssrfun.v
 theories/ssr/ssrsetoid.v
 theories/ssr/ssrunder.v
 theories/ssrmatching/ssrmatching.v
+theories/NArith/NArith_base.v
+theories/ZArith/ZArith_base.v