stdlib: basic commutative algebra#602
Open
strub wants to merge 19 commits into
Open
Conversation
Member
Author
|
CRT in GCD domains done. |
Member
Author
|
Principal => UFD. |
strub
marked this pull request as ready for review
January 22, 2025 14:53
strub
force-pushed
the
comm-algebra
branch
2 times, most recently
from
July 17, 2026 14:31
b62a91f to
d3a00af
Compare
Introduce comax x y = exists u v, u*x + v*y = oner and restate the CRT cluster against it, before the Euclidean structure: comax_Gauss, comaxMr/Ml/prod, dvdrMl_comax, dvdr_prodl_comax, crt_comax, crt_uniq_comax. These consume co-primality only through the Bezout witnesses, so instances can supply the witnesses directly (e.g. binomial moduli X^n - c1, X^n - c2, whose witnesses are constants) without going through gcds -- i.e. without the Euclide axiom. The generic divisibility lemmas the cluster relies on (dvdr_mul, dvdrD, dvdrN, dvdrB, dvd1r, dvdr_sum, dvdr_prod) move up above the Euclidean axioms, unchanged. comax_coprime is immediate in any domain; coprime_comax is Bezout (comax = coprime characterizes Bezout domains). crt and crt_uniq keep their statements and become corollaries of the witness-level versions.
Base is the ideal-theoretic core over an abstract integral domain: divisibility kit and the witness-level (comax) CRT cluster, with no axiom beyond the ring structure. Euclidean includes Base and adds the weight function with its axioms, gcds, Bezout, coprimality, factorization, and the coprime-phrased CRT corollaries. Instances can thus enter at Base -- e.g. polynomial rings before any division theory is available -- by exhibiting Bezout witnesses directly. The parameterization follows the Poly.ec pattern (top-level type t, named parameter theory ID) rather than an anonymous IDomain clone: overriding an anonymous parameter subtheory referenced by the nested Ideal/BigComRing clones crashes the cloning machinery (ecThCloning.ml:472 assertion). dvdw was inconsistent as stated (y = zeror + dvdr0 + ge0_w + eq0_wP collapse the ring); it now requires both arguments nonzero.
peval was defined and never developed (its only stdlib occurrences were the definition and the root abbrev). Add the morphism kit at the PolyComRing level -- pevalE_ge (range-flexible form), pevalC, peval0, pevalD, pevalN, pevalB, pevalMX, pevalX, pevalZ, pevalM, peval_big -- together with the polyL structure lemmas polyL_nil and polyL_cons that the list inductions rely on. The definition now sums over 0 <= i < deg p: under the deg convention the previous bound deg p + 1 included a guaranteed-zero last term.
IDPoly and ZModpField were cloned with <- bindings, inlining the type and operators: the resulting theories lack their own t/zeror/... and cannot be passed where an IDomain-shaped theory parameter is expected (structural matching fails with unknown symbols). Switch to <=, which keeps the members as aliases, as ZModpRing and the PolyComRing inner instance already do; and clone-export IDPoly so that instances of the IDomain-level Poly theory expose its names unqualified, mirroring the ComRing instance.
peval_prod, the multiplicative companion of peval_big: evaluating a PCM product of polynomials is the BCM product of the evaluations.
Aligns with peval_prod: peval_sum/peval_prod for PCA/PCM bigs.
mprod rs = prod_(r in rs) (X - C r) as a PCM big, with the unfolding lemmas, factorization at a member root (mprod_mem_factor, by perm_to_rem), vanishing at member roots (mprod_root), and the degree computation deg_mprod = 1 + size rs -- the degM_proper side condition is discharged by monicity (lc_XC), no domain assumption on the coefficients.
peval_mprod_out, in the IDomain-level theory: evaluating a product of monic linear factors outside the root list is nonzero (coefficient mulf_eq0).
degBl/lcBl (degree and leading coefficient through subtraction of a lower-degree polynomial); degXBC/lcXBC replace deg_XC/lc_XC, stated with the early deg/lc lemmas and proved without smt; deg_mprod and peval_mprod_out streamlined accordingly (mulf_neq0).
A third floor over PolyComRing / Poly, with Field coefficients. First content: Lagrange interpolation over a uniq root list -- the basis lag (scaled monic products), its evaluation lemmas, interp as a PCA sum realizing any assignment of values at the roots, with degree at most the number of roots.
PolyField.Lagrange holds lag/interp and their lemmas; PolyField imports BigCf/BigPoly so the proofs drop the qualified coefficient and bigop names, and the scripts are shortened (&-combinators, ler_trans chains instead of smt).
BR is declared before the Ideal clone and substituted for its BigDom with <-, so the nested copy vanishes and instances only ever substitute top-level theories (ID, BR). This replaces the previous op-level aliasing of BR onto I.BigDom, and retires the FIXME unfoldings that aliasing required in the proofs.
IDomainMixin and FieldMixin take their parent ComRing as a named parameter (referenced, not copied). IDomainMixin carries mulf_eq0 and the domain lemma library. FieldMixin is a factory: its single axiom is that units are exactly the nonzero elements; mulf_eq0 is derived generically (retiring ZModP's 'FIXME: should be generic') and its nested Dom is a fully realized IDomainMixin over the same parent, so consumers expecting the domain layer accept F.Dom. ZModP pilots the architecture: ZModpFieldMx is a FieldMixin over ZModpRing realized by the single lemma unitE -- versus the bundled ZModpField clone (kept for compatibility during migration), which re-clones Ring.Field and re-realizes nine ComRing axioms by delegation. One ring library on zmod; the field level a pure delta.
IDomainBundle and FieldBundle package one slot per structure level (carrier, ComRing, mixin), coherently threaded, with no library of their own: consumers declare a single bundle parameter and instances substitute a single theory. A FieldBundle yields an IDomainBundle by construction through the factory's Dom. ZModpFieldBd is the zmod instance.
The Poly theory now takes its coefficients as CR : ComRing plus CoeffDom : IDomainMixin, realizes PolyComRing's unit/invr definitionally in the include (discharging the three unit axioms, previously left unproven and cleared), and grows the domain level as a delta-only IDomainMixin (IDPoly) over the one PolyComRing object: no duplicate ring object, no clear. PolyField takes the coefficient field as a single FieldBundle parameter K, pierced slot-by-slot into Poly. mul_lc/degM_le/degM_proper move above the inner ring clone (which they never needed) so the include's realize obligations can use them.
The field level keeps the one ring object (ZModpRing) and gets its field structure from the ZModpFieldMx mixin / ZModpFieldBd bundle. The old Ring.Field clone's import role is preserved by importing ZModpRing and the mixin at the same spot, so downstream vocabulary is unchanged; exp_mod bridges its one unit side-goal with unitE (the style exp_pow already used). Field-requesting consumers (DHIES, SchnorrPK, elgamal, cramer-shoup, UC/dh_enc) clone the field bundle; Group's g_neq0 hint becomes oner_neq0.
Ideal.Ideal and CommAlgebra.Base now take R : ComRing plus
Dom : IDomainMixin instead of a fresh IDomain object: Ideal's
op-by-op push-down into IdealComRing (with its twelve delegated
realizes and clear) collapses to the single substitution
theory IComRing <- R. Base keeps owning BR and pushes R/Dom/BR into
its Ideal clone.
Poly's BigPoly binds its CR slot with <= instead of <-, keeping the
alias navigable so BigPoly is substitutable from outside.
With this, the previously-blocked instantiation goes through as one
coherent substitution --
clone CommAlgebra.Base as ZqCA with
type t <= ZqP.poly,
theory R <= ZqP.PolyComRing,
theory Dom <= ZqP.IDPoly,
theory BR <= ZqP.BigPoly { rename "BAdd" as "PCA"
"BMul" as "PCM" }.
-- and the bigop sharing ZqCA.BR.BMul.big = ZqP.BigPoly.PCM.big is
definitional (closed by reflexivity).
Base gets the modulus-parametric congruence eqm m x y, an abbreviation for m %| (x - y) (so it converts freely with the divisibility form), together with its kit: eqmP (Bezout-witness form), eqm_refl/sym/trans, eqm_eq, eqm_mod0, the ring-operation congruences eqmD/N/B/M, and the CRT-tree descend eqm_mulm. This is the generic content of the peqm kit that lived in the ML-DSA development.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.