clean up component dependencies of lia

dev/tools/subcomponents.py

@@ -26,7 +26,7 @@ def dfs(target, comp, html, dot):
     if target in component.keys():
         assert comp_requires(comp, component[target]),\
                f"{target} (from component {component[target]}) used in {comp}"+\
-               f"but {comp} does not require {component[target]}"
+               f" but {comp} does not require {component[target]}"
         return
     component[target] = comp
     for dep in compdeps[target]:
@@ -108,5 +108,12 @@ def dfs(target, comp, html, dot):
           continue
       assert component.get(target) not in [None, top],\
               f"{target} does not belong to any component"
+      if not is_component(target):
+        continue
+      for dep in sorted(dependencies[target]):
+        if is_component(dep):
+          continue
+        assert component[dep] == target,\
+            f"{dep} listed in {target} is used earlier in {component[dep]}"
   print("</dl>", file=html)
   print("}", file=dot)

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).
+

subcomponents/arith.v

@@ -1,2 +1,7 @@
 From subcomponents Require ring.
 From Stdlib Require Arith.Arith.
+From Stdlib Require Arith.Cantor.
+From Stdlib Require Arith.Compare.
+From Stdlib Require Arith.Euclid.
+From Stdlib Require Arith.Zerob.
+From Stdlib Require Classes.SetoidDec.

subcomponents/classical_logic.v

@@ -1,4 +1,4 @@
-From subcomponents Require arith.
+From subcomponents Require naturals.
 From Stdlib Require Logic.IndefiniteDescription.
 From Stdlib Require Logic.Classical_Pred_Type.
 From Stdlib Require Logic.Classical_Prop.

subcomponents/compat.v

@@ -1,4 +1,3 @@
-From subcomponents Require rtauto.
 From subcomponents Require fmaps_fsets_msets.
 From subcomponents Require funind.
 From subcomponents Require extraction.
@@ -8,4 +7,21 @@ From subcomponents Require wellfounded.
 From subcomponents Require streams.
 From Stdlib Require Compat.AdmitAxiom.
 From Stdlib Require Compat.Stdlib818.
-From Stdlib Require Reals.Nsatz.
+From Stdlib Require Numbers.AltBinNotations.
+From Stdlib Require Numbers.NaryFunctions.
+From Stdlib Require Numbers.NatInt.NZDomain.
+From Stdlib Require Numbers.NatInt.NZProperties.
+From Stdlib Require Numbers.Natural.Abstract.NStrongRec.
+From Stdlib Require Numbers.Natural.Abstract.NDefOps.
+From Stdlib Require Numbers.Natural.Abstract.NIso.
+From Stdlib Require rtauto.Bintree.
+From Stdlib Require rtauto.Rtauto.
+From Stdlib Require micromega.Ztac.
+From Stdlib Require ZNatPairs.
+From Stdlib Require ZBinary.
+From Stdlib Require ZDivEucl.
+From Stdlib Require NBinary.
+From Stdlib Require Bool_nat.
+From Stdlib Require Nsatz.
+From Stdlib Require Bvector.
+From Stdlib Require Zeuclid.

subcomponents/extraction.v

@@ -1,3 +1,4 @@
+From subcomponents Require arith.
 From subcomponents Require primitive_string.
 From subcomponents Require primitive_array.
 From subcomponents Require primitive_floats.

subcomponents/field.v

@@ -1,2 +1,2 @@
-From subcomponents Require zarith.
+From subcomponents Require ring.
 From Stdlib Require setoid_ring.Field.

subcomponents/fmaps_fsets_msets.v

@@ -1,4 +1,5 @@
 From subcomponents Require orders_ex.
+From subcomponents Require arith.
 From subcomponents Require zarith.
 From Stdlib Require FSets.FMapInterface.
 From Stdlib Require FSets.FSetInterface.

subcomponents/funind.v

@@ -1,3 +1,4 @@
-From subcomponents Require arith_base.
+From subcomponents Require naturals.
+From subcomponents Require lists.
 From Stdlib Require funind.FunInd.
 From Stdlib Require funind.Recdef.

subcomponents/zarith_base.v → subcomponents/integers.v

@@ -1,39 +1,22 @@
-From subcomponents Require narith_base.
-From Stdlib Require Numbers.Integer.Abstract.ZSgnAbs.
+From subcomponents Require naturals.
 From Stdlib Require Numbers.Integer.Abstract.ZAxioms.
+From Stdlib Require Numbers.Integer.Abstract.ZBase.
+From Stdlib Require Numbers.Integer.Abstract.ZAdd.
+From Stdlib Require Numbers.Integer.Abstract.ZMul.
+From Stdlib Require Numbers.Integer.Abstract.ZLt.
 From Stdlib Require Numbers.Integer.Abstract.ZAddOrder.
-From Stdlib Require Numbers.Integer.Abstract.ZProperties.
-From Stdlib Require Numbers.Integer.Abstract.ZDivTrunc.
+From Stdlib Require Numbers.Integer.Abstract.ZMulOrder.
+From Stdlib Require Numbers.Integer.Abstract.ZSgnAbs.
+From Stdlib Require Numbers.Integer.Abstract.ZDivFloor.
 From Stdlib Require Numbers.Integer.Abstract.ZParity.
-From Stdlib Require Numbers.Integer.Abstract.ZMul.
 From Stdlib Require Numbers.Integer.Abstract.ZPow.
-From Stdlib Require Numbers.Integer.Abstract.ZAdd.
-From Stdlib Require Numbers.Integer.Abstract.ZDivFloor.
-From Stdlib Require Numbers.Integer.Abstract.ZMulOrder.
-From Stdlib Require Numbers.Integer.Abstract.ZDivEucl.
-From Stdlib Require Numbers.Integer.Abstract.ZMaxMin.
+From Stdlib Require Numbers.Integer.Abstract.ZBits.
+From Stdlib Require Numbers.Integer.Abstract.ZDivTrunc.
 From Stdlib Require Numbers.Integer.Abstract.ZGcd.
-From Stdlib Require Numbers.Integer.Abstract.ZLt.
 From Stdlib Require Numbers.Integer.Abstract.ZLcm.
-From Stdlib Require Numbers.Integer.Abstract.ZBase.
-From Stdlib Require Numbers.Integer.Abstract.ZBits.
+From Stdlib Require Numbers.Integer.Abstract.ZMaxMin.
+From Stdlib Require Numbers.Integer.Abstract.ZProperties.
 From Stdlib Require ZArith.BinIntDef.
 From Stdlib Require ZArith.BinInt.
-From Stdlib Require ZArith.Zcompare.
-From Stdlib Require ZArith.Zorder.
-From Stdlib Require ZArith.Zminmax.
-From Stdlib Require ZArith.Zmin.
-From Stdlib Require ZArith.Zmax.
-From Stdlib Require ZArith.Znat.
 From Stdlib Require ZArith.ZArith_dec.
-From Stdlib Require ZArith.Zabs.
-From Stdlib Require ZArith.auxiliary.
-From Stdlib Require ZArith.Zbool.
-From Stdlib Require ZArith.Zmisc.
-From Stdlib Require ZArith.Wf_Z.
-From Stdlib Require ZArith.Zhints.
-From Stdlib Require ZArith.ZArith_base.
-From Stdlib Require ZArith.Zeven.
-From Stdlib Require ZArith.Zpow_alt.
-From Stdlib Require ZArith.Zeuclid.
-From Stdlib Require ZArith.Int.
+From Stdlib Require PArith.POrderedType.

subcomponents/lia.v

@@ -1,25 +1,11 @@
-From subcomponents Require arith.
-From subcomponents Require narith.
-From Stdlib Require omega.OmegaLemmas.
-From Stdlib Require omega.PreOmega.
-From Stdlib Require micromega.ZifyN.
-From Stdlib Require micromega.ZifyComparison.
+From subcomponents Require ring.
+From Stdlib Require micromega.Lia.
+From Stdlib Require micromega.SatDivMod.
+From Stdlib Require micromega.Zify.
+From Stdlib Require micromega.ZifyBool.
 From Stdlib Require micromega.ZifyClasses.
+From Stdlib Require micromega.ZifyComparison.
+From Stdlib Require micromega.ZifyInst.
+From Stdlib Require micromega.ZifyN.
 From Stdlib Require micromega.ZifyNat.
 From Stdlib Require micromega.ZifyPow.
-From Stdlib Require micromega.ZifyBool.
-From Stdlib Require micromega.Zify.
-From Stdlib Require micromega.ZifyInst.
-From Stdlib Require micromega.DeclConstantZ.
-From Stdlib Require micromega.OrderedRing.
-From Stdlib Require micromega.Tauto.
-From Stdlib Require micromega.Env.
-From Stdlib Require micromega.Refl.
-From Stdlib Require micromega.ZArith_hints.
-From Stdlib Require micromega.ZMicromega.
-From Stdlib Require micromega.EnvRing.
-From Stdlib Require micromega.Lia.
-From Stdlib Require micromega.VarMap.
-From Stdlib Require micromega.Ztac.
-From Stdlib Require micromega.ZCoeff.
-From Stdlib Require micromega.RingMicromega.

subcomponents/lists.v

@@ -1,10 +1,9 @@
-From subcomponents Require arith_base.
-From Stdlib Require Lists.ListDec.
+From subcomponents Require naturals.
 From Stdlib Require Lists.List.
+From Stdlib Require Classes.EquivDec.
+From Stdlib Require Lists.ListDec.
+From Stdlib Require Lists.Finite.
 From Stdlib Require Lists.ListSet.
 From Stdlib Require Lists.ListTactics.
-From Stdlib Require Lists.Finite.
-From Stdlib Require Sorting.Permutation.
-From Stdlib Require Numbers.NaryFunctions.
 From Stdlib Require Logic.WKL.
-From Stdlib Require Classes.EquivDec.
+From Stdlib Require Sorting.Permutation.

subcomponents/lqa.v

@@ -1,8 +1,9 @@
 From subcomponents Require field.
-From subcomponents Require qarith_base.
-From Stdlib Require micromega.QMicromega.
-From Stdlib Require micromega.Lqa.
-From Stdlib Require micromega.DeclConstant.
+From subcomponents Require rationals.
 From Stdlib Require QArith.Qfield.
 From Stdlib Require QArith.Qring.
+From Stdlib Require micromega.DeclConstantZ.
+From Stdlib Require micromega.DeclConstant.
+From Stdlib Require micromega.QMicromega.
+From Stdlib Require micromega.Lqa.
 From Stdlib Require setoid_ring.Rings_Q.

subcomponents/arith_base.v → subcomponents/naturals.v

@@ -1,54 +1,48 @@
-From subcomponents Require structures.
-From Stdlib Require Arith.Arith_base.
-From Stdlib Require Arith.Between.
-From Stdlib Require Arith.Bool_nat.
-From Stdlib Require Arith.Cantor.
-From Stdlib Require Arith.Compare.
-From Stdlib Require Arith.Compare_dec.
-From Stdlib Require Arith.EqNat.
-From Stdlib Require Arith.Euclid.
-From Stdlib Require Arith.Factorial.
-From Stdlib Require Arith.PeanoNat.
-From Stdlib Require Arith.Peano_dec.
-From Stdlib Require Arith.Wf_nat.
-From Stdlib Require Arith.Zerob.
+From subcomponents Require orders.
 From Stdlib Require Numbers.NumPrelude.
+From Stdlib Require Numbers.NatInt.NZAxioms.
 From Stdlib Require Numbers.NatInt.NZBase.
+From Stdlib Require Numbers.NatInt.NZAdd.
+From Stdlib Require Numbers.NatInt.NZMul.
 From Stdlib Require Numbers.NatInt.NZOrder.
-From Stdlib Require Numbers.NatInt.NZProperties.
+From Stdlib Require Numbers.NatInt.NZAddOrder.
+From Stdlib Require Numbers.NatInt.NZMulOrder.
 From Stdlib Require Numbers.NatInt.NZDiv.
-From Stdlib Require Numbers.NatInt.NZParity.
 From Stdlib Require Numbers.NatInt.NZPow.
-From Stdlib Require Numbers.NatInt.NZSqrt.
-From Stdlib Require Numbers.NatInt.NZGcd.
-From Stdlib Require Numbers.NatInt.NZBits.
-From Stdlib Require Numbers.NatInt.NZDomain.
-From Stdlib Require Numbers.NatInt.NZAxioms.
-From Stdlib Require Numbers.NatInt.NZAddOrder.
-From Stdlib Require Numbers.NatInt.NZMul.
 From Stdlib Require Numbers.NatInt.NZLog.
-From Stdlib Require Numbers.NatInt.NZAdd.
-From Stdlib Require Numbers.NatInt.NZMulOrder.
-From Stdlib Require Numbers.Natural.Abstract.NStrongRec.
-From Stdlib Require Numbers.Natural.Abstract.NAdd.
+From Stdlib Require Numbers.NatInt.NZParity.
+From Stdlib Require Numbers.NatInt.NZBits.
+From Stdlib Require Numbers.NatInt.NZGcd.
+From Stdlib Require Numbers.NatInt.NZSqrt.
 From Stdlib Require Numbers.Natural.Abstract.NAxioms.
-From Stdlib Require Numbers.Natural.Abstract.NDefOps.
-From Stdlib Require Numbers.Natural.Abstract.NSqrt.
-From Stdlib Require Numbers.Natural.Abstract.NDiv0.
-From Stdlib Require Numbers.Natural.Abstract.NBits.
-From Stdlib Require Numbers.Natural.Abstract.NGcd.
-From Stdlib Require Numbers.Natural.Abstract.NParity.
-From Stdlib Require Numbers.Natural.Abstract.NProperties.
-From Stdlib Require Numbers.Natural.Abstract.NMaxMin.
-From Stdlib Require Numbers.Natural.Abstract.NDiv.
-From Stdlib Require Numbers.Natural.Abstract.NPow.
+From Stdlib Require Numbers.Natural.Abstract.NBase.
+From Stdlib Require Numbers.Natural.Abstract.NAdd.
+From Stdlib Require Numbers.Natural.Abstract.NOrder.
 From Stdlib Require Numbers.Natural.Abstract.NAddOrder.
-From Stdlib Require Numbers.Natural.Abstract.NLcm0.
-From Stdlib Require Numbers.Natural.Abstract.NLog.
 From Stdlib Require Numbers.Natural.Abstract.NMulOrder.
-From Stdlib Require Numbers.Natural.Abstract.NIso.
 From Stdlib Require Numbers.Natural.Abstract.NSub.
-From Stdlib Require Numbers.Natural.Abstract.NBase.
+From Stdlib Require Numbers.Natural.Abstract.NDiv.
+From Stdlib Require Numbers.Natural.Abstract.NParity.
+From Stdlib Require Numbers.Natural.Abstract.NPow.
+From Stdlib Require Numbers.Natural.Abstract.NLog.
+From Stdlib Require Numbers.Natural.Abstract.NBits.
+From Stdlib Require Numbers.Natural.Abstract.NDiv0.
+From Stdlib Require Numbers.Natural.Abstract.NGcd.
 From Stdlib Require Numbers.Natural.Abstract.NLcm.
-From Stdlib Require Numbers.Natural.Abstract.NOrder.
-From Stdlib Require Classes.SetoidDec.
+From Stdlib Require Numbers.Natural.Abstract.NLcm0.
+From Stdlib Require Numbers.Natural.Abstract.NMaxMin.
+From Stdlib Require Numbers.Natural.Abstract.NSqrt.
+From Stdlib Require Numbers.Natural.Abstract.NProperties.
+From Stdlib Require Arith.PeanoNat.
+From Stdlib Require Arith.Between.
+From Stdlib Require Arith.Compare_dec.
+From Stdlib Require Arith.EqNat.
+From Stdlib Require Arith.Factorial.
+From Stdlib Require Arith.Peano_dec.
+From Stdlib Require Arith.Wf_nat.
+From Stdlib Require Arith.Arith_base.
+From Stdlib Require PArith.BinPosDef.
+From Stdlib Require PArith.BinPos.
+From Stdlib Require NArith.BinNatDef.
+From Stdlib Require NArith.BinNat.
+From Stdlib Require NArith.Nnat.

subcomponents/qarith.v

@@ -1,3 +1,4 @@
+From subcomponents Require zarith.
 From subcomponents Require lqa.
 From Stdlib Require QArith.Qcabs.
 From Stdlib Require QArith.Qround.

subcomponents/reals.v

@@ -1,3 +1,4 @@
+From subcomponents Require arith.
 From subcomponents Require qarith.
 From subcomponents Require classical_logic.
 From subcomponents Require vectors.
@@ -9,7 +10,6 @@ From Stdlib Require Reals.ClassicalConstructiveReals.
 From Stdlib Require Reals.Machin.
 From Stdlib Require Reals.Rminmax.
 From Stdlib Require Reals.Rlogic.
-From Stdlib Require Reals.Nsatz.
 From Stdlib Require setoid_ring.Rings_R.
 From Stdlib Require micromega.Psatz.
 From Stdlib Require Numbers.DecimalR.