Generalize CMvPolynomial coefficient universes#178
Merged
dhsorens merged 4 commits intodhsorens/bump_to_4.29.0-rc6from Mar 31, 2026
Merged
Generalize CMvPolynomial coefficient universes#178dhsorens merged 4 commits intodhsorens/bump_to_4.29.0-rc6from
dhsorens merged 4 commits intodhsorens/bump_to_4.29.0-rc6from
Conversation
🤖 Gemini PR SummaryUniverse Generalization
Typeclass and Elaboration Refinement
Dependencies and API Alignment
Statistics
Lean Declarations ✏️ **Removed:** 20 declaration(s)
✏️ **Added:** 1 declaration(s)
✏️ **Affected:** 50 declaration(s) (line number changed)
🎨 **Style Guide Adherence**The following review is based on the provided style guide and the code changes in the diff. There are 24 violations of the style guide. They are grouped by rule below:
📄 **Per-File Summaries**
Last updated: 2026-03-31 19:17 UTC. |
Build Timing Report
Incremental Rebuild Signal
This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark. Slowest Current Clean-Build FilesShowing 20 slowest current targets, with comparison against the selected baseline when available.
|
🤖 Initial AI review without external context🤖 AI ReviewOverall Summary: TL;DRThis PR is in excellent shape, successfully applying standard Mathlib best practices across the board by generalizing universe levels (from Checklist CoverageNo explicit specification checklist was provided for this review. Key Lean 4 / Mathlib IssuesNone found. The refactoring perfectly aligns with Lean 4 and Mathlib conventions for universe polymorphism and minimal typeclasses. Nitpicks & Minor Observations
Overall VerdictApproved (Fantastic work on the cleanup—the typeclass minimization and universe polymorphism refactors are exactly what we look for in Lean 4 library development!) 📄 **Review for `CompPoly/Multivariate/CMvMonomial.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: 📄 **Review for `CompPoly/Multivariate/CMvPolynomial.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: (The change from 📄 **Review for `CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: 📄 **Review for `CompPoly/Multivariate/FinSuccEquiv.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: 📄 **Review for `CompPoly/Multivariate/Lawful.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: 📄 **Review for `CompPoly/Multivariate/MvPolyEquiv/Core.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: 📄 **Review for `CompPoly/Multivariate/MvPolyEquiv/Eval.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks:
📄 **Review for `CompPoly/Multivariate/MvPolyEquiv/Instances.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: (Note: Generalizing the universe levels by replacing 📄 **Review for `CompPoly/Multivariate/Operations.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: (The changes correctly generalize the universe levels of 📄 **Review for `CompPoly/Multivariate/Rename.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: 📄 **Review for `CompPoly/Multivariate/Restrict.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: 📄 **Review for `CompPoly/Multivariate/Unlawful.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: (Additional Context): 📄 **Review for `CompPoly/Multivariate/VarsDegrees.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: 📄 **Review for `lakefile.lean`**Verdict: Approved Critical Misformalizations: Lean 4 / Mathlib Issues: Nitpicks: |
dhsorens
reviewed
Mar 31, 2026
Collaborator
dhsorens
left a comment
dhsorens
left a comment
There was a problem hiding this comment.
as long as this doesn't negatively affect performance, I'm happy with this but it might be nice to get a review/approval from @Julek just in case. @quangvdao do you have a specific use case in mind for making CMvPolynomial polymorphic over universes?
Collaborator
Author
|
None right now, though this brings the multivariate case on par with univariate case that is already universe polymorphic. And I don't think we have any perf regression |
dhsorens
approved these changes
Mar 31, 2026
Collaborator
dhsorens
left a comment
dhsorens
left a comment
There was a problem hiding this comment.
please see some minor comments but otherwise I'm happy with this!
Comment on lines
+1
to
+10
| /- | ||
| Copyright (c) 2026 CompPoly. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Quang Dao | ||
| -/ | ||
| import CompPoly.Multivariate.FinSuccEquiv | ||
| import CompPoly.Multivariate.Operations | ||
| import CompPoly.Univariate.ToPoly.Impl | ||
|
|
||
| /-! |
Collaborator
There was a problem hiding this comment.
is this a duplicate of the file already merged in? possibly this branch needs rebasing?
CompPoly/Multivariate/Unlawful.lean
Outdated
Comment on lines
+107
to
+105
| ⟨λ (m, c) => repr c ++ " * " ++ repr m⟩ | ||
| ⟨fun (m, c) ↦ repr c ++ " * " ++ repr m⟩ |
Collaborator
There was a problem hiding this comment.
this is a kind of funny change - should we choose either \lambda and \mapsto together, or fun and => together?
CompPoly/Multivariate/Unlawful.lean
Outdated
| lemma filter_get {R : Type} [BEq R] [LawfulBEq R] {v : R} {m : CMvMonomial n} (a : Unlawful n R) : | ||
| (ExtTreeMap.filter (fun _ c => c != v) a)[m]?.getD v = a[m]?.getD v := by | ||
| lemma filter_get {R : Type*} [BEq R] [LawfulBEq R] {v : R} {m : CMvMonomial n} (a : Unlawful n R) : | ||
| (ExtTreeMap.filter (fun _ c ↦ c != v) a)[m]?.getD v = a[m]?.getD v := by |
Collaborator
There was a problem hiding this comment.
in this spirit, if we're changing => to \mapsto, shall we also change fun to \lambda?
docs/wiki/repo-map.md
Outdated
Comment on lines
+39
to
+41
| - Working on the dedicated one-variable | ||
| `CMvPolynomial 1 R ≃+* CPolynomial R` bridge: | ||
| start in `CompPoly/Multivariate/UnivariateEquiv.lean`. |
Collaborator
There was a problem hiding this comment.
another instance of probably needing to rebase
Collaborator
There was a problem hiding this comment.
there are more in the other wiki docs but I won't comment them all
lakefile.lean
Outdated
| require "leanprover-community" / mathlib @ git "v4.28.0" | ||
|
|
||
| require ExtTreeMapLemmas from git "https://github.com/Verified-zkEVM/ExtTreeMapLemmas"@"v4.28.0-patch-1" | ||
| require ExtTreeMapLemmas from git "https://github.com/quangvdao/ExtTreeMapLemmas"@"ed753cfcaa1ad3699e204899a0136ffa2383526c" |
Collaborator
There was a problem hiding this comment.
re this dependency change - I just merged your PR in ExtTreeMapLemmas and issued a new tag, v4.29.0-rc6-patch-1 - can we please us that here? hopefully 4.29.0-rc6 works as a dependency
on a separate note it might be nice to consider just putting ExtTreeMapLemmas into CompPoly since it's small and a sort of annoying dependency
Collaborator
Author
There was a problem hiding this comment.
Yeah fully support moving that into CompPoly. Can be an internal detail of CMvPolynomial
quangvdao
force-pushed
the
quang/cmvpoly-type-universe
branch
from
2d5d34c to
5f1f193
Compare
quangvdao
force-pushed
the
quang/cmvpoly-type-universe
branch
from
5f1f193 to
7f3ab20
Compare
Collaborator
Author
|
Posted by Cursor assistant (model: GPT-5) on behalf of the user (Quang Dao) with approval. Thanks for the review. I addressed the minor comments and cleaned up the branch shape:
While restacking onto the 4.29 branch, a few small proof adjustments were needed for Lean 4.29 in:
Revalidated with:
So at this point the PR is aligned with the 4.29 base and the upstream dependency tag. |
dhsorens
approved these changes
Mar 31, 2026
Collaborator
dhsorens
left a comment
dhsorens
left a comment
There was a problem hiding this comment.
great, thanks! happy with this
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
2 participants
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.
Posted by Cursor assistant (model: GPT-5.4) on behalf of the user (Quang Dao) with approval.
Summary
Validation