Prepare move of ring/field and micromega computational part to Corelib

[proux01]

So that this can be used in other libraries.
This also factors some common code between ring/field and micromega (maybe proofs could also be factored further)

Overlay (to be merged before the current PR)

• Adapt to https://github.com/rocq-prover/stdlib/pull/207 math-comp/algebra-tactics#126

Overlays (ot be merged in sync with the current PR)

• Adapt to https://github.com/rocq-prover/stdlib/pull/207 smtcoq/smtcoq#155
• Adapt to https://github.com/rocq-prover/stdlib/pull/207 MetaRocq/metarocq#1204

[andres-erbsen]

What other libraries do you have in mind? Is this for mathcomp?

I don't object to this change in particular, but it sure seems like a great demonstration why having stdlib separate from the main repository is a bad idea. If polynomials, boolean algebra, and cutting planes belong in corelib, what doesn't? Developing theories split across repositories like this is harder than when they are together. For example, consider the workflow and release schedule for removing EnumProof.

EDIT: Added to Rocq-Call-2025-09-16

[proux01]

What other libraries do you have in mind? Is this for mathcomp?

Virtually any library, maybe HoTT, Unimath or whatnnot. I already tested it successfully in MathComp.

I don't object to this change in particular, but it sure seems like a great demonstration why having stdlib separate from the main repository is a bad idea. If polynomials, boolean algebra, and cutting planes belong in corelib, what doesn't? Developing theories split across repositories like this is harder than when they are together.

The important part in the PR title is "computational part". In particular, I don't want to move any of the following, that are library specific: reificator (still in the OCaml plugin for now), theories or glue tactic. More precisely you can look at rocq-prover/rocq#21080 to see what I'd like to retrieve in Corelib: this is only generic code, independent from any library theory, and doesn't contain any proof.
More importantly, for micromega, having this material closer from the OCaml plugin will ease further developments.

[andres-erbsen]

The alternative I proposed on the call today is to move the definitions and soundness proof of the lia proof procedure into corelib:

This would mean that tightly-coupled active development remains within corelib, with lra being a part of reals (not moved) and instantiating the proof machinery using this interface.

[proux01]

Beyond the fact that it's a very large chunk of stdlib, we won't move to Corelib every theory out there that would want to use micromega.
The point of Corelib is to share some basic definitions between libraries that can build their own theories on top of them, not to host whole theories.

[andres-erbsen]

Yeah, we disagree here -- moving all of stdlib back would be even better.

[andres-erbsen]

If "very large chunk" is primarily about build time, we should seriously consider composed build approaches such as BRiCk/dune or fiat-crypto/Makefile.composed. This way, projects that only need lia don't need to build e.g. reals.

[proux01]

Anyway, we could consider merging the current PR whatever we eventually decide to do about rocq-prover/rocq#21080 since it's bringing general cleanup: removal of duplications, added documentation,...