refactor: golf wrapper proofs#1332
Open
Vilin97 wants to merge 499 commits into
Open
Conversation
Contributor
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
Vilin97
changed the title
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Restore the local Relative entropy kernel witness that a previous golf left referenced, and avoid the recursive Pinching unfold while keeping the channel proof reductions. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Compress a mirrored matrix-basis reconstruction and direct small Lorentz, entropy, and purity witnesses. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Replace small local exact wrappers with direct proof terms in list, entropy, and Hermitian matrix witnesses. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Replace five bundled channel extensionality by-exact wrappers with direct proof terms. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Replace complex tensor metric and unit invariance tactic wrappers with direct invariant proof terms. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Replace six complex tensor unit fromConstPair wrappers with direct rfl proofs. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Compress metric fromConstPair identities, real tensor metric invariance, and Wick contraction permutation reflexivity. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Use direct equality and invariant proof terms for Wick contraction permutations, exchange signs, and tensor invariance wrappers. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
# Conflicts: # Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean # Physlib/Relativity/Tensors/RealTensor/Matrix/Pre.lean # Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Basic.lean # Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Contraction.lean
Member
|
@Vilin97 I think there is some merge error going on now, as your PR is showing changes from other PRs which have already been merged. |
Contributor
Author
🏌️ check-golf reportComparing base Result: ✅ Statements preserved. Every changed declaration kept its statement; only proofs / bodies changed.
Of the golfed proofs/bodies above, the trivial reshapes were:
🔧 Definition bodies changed (data may have changed, type unchanged) (41)The defining term outside
✅ Proofs golfed (1322)
✅ Embedded proofs golfed (type unchanged) (1)
✅ Definition proofs golfed (data unchanged) (69)
↩️ Only a newline removed (tokens unchanged) (518)
Generated by |
The automated golf over-shortened many proofs, breaking compilation. Each fix is surgical: restore only the broken proof/step from master while preserving all other golf in the file. Key root-cause fix: several @[simp] coercion lemmas (HermitianMat.val_eq_coe, mat_smul, mat_cfc, MState.mat_M) were golfed from `:= by rfl` to `:= rfl`, which makes them eligible for `dsimp` definitional rewriting. That caused `dsimp` calls in downstream proofs (Pinching, SteinsLemma) to over-normalize goals — unfolding `↑(c • A)`, `↑A`, `↑(A.cfc f)` — so subsequent `rw`s no longer matched, and produced dsimp recursion-depth loops. Reverting those specific lemmas to `by rfl` restores the intended non-dsimp semantics. All CI steps pass locally: lake build -KCI (Physlib + QuantumInfo), check_file_imports, check_dup_tags, sorry_lint, runPhyslibLinters, PhyslibAlpha build + runPhyslibAlphaLinters, lint-style.sh, codespell. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YRA4h6VJRALwaZK1xeUsg3
Member
|
@Vilin97 What was the command you ran locally to get this golf report (struggling to find the right base and head) |
Member
|
One thing which would also slow this review down is the 110 changes to the definition body. But I'm also worried about the increase in heartbeats on some of the files (but it is nice that this scripts picks this up!) |
Contributor
Author
Member
|
@Vilin97 Sure, but when you ran it locally, what arguments did you use for --head and --base? |
Vilin97
added a commit
to Vilin97/physlib
that referenced
this pull request
Jul 3, 2026
A `def`/`instance`/`abbrev` often carries proof obligations discharged by `by` blocks. Golfing only those does not change the definition's data, so it should not read as "the definition changed". The report now masks a definition's `by` proof blocks and splits its changes into: - "definition proofs golfed" (data unchanged), and - "definition values changed" (the defining term changed outside proofs). On PR leanprover-community#1332 this moves 76 of the 110 former "definition body" changes into the proof-only bucket, leaving 34 genuine value changes. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjiv6nckrp5cJT9rpgZaKT
Contributor
Author
Also, re: the definitions that got changed -- they got changed because the proofs inside of them got golfed. E.g. in This can affect things like rfl and defeq despite the def's type not changing. |
This was referenced Jul 4, 2026
Contributor
Author
|
Lmk when it's good to merge or if you want me to change anything |
jstoobysmith
pushed a commit
that referenced
this pull request
Jul 5, 2026
* feat: add /check-golf bot verifying statements are unchanged Add scripts/check_golf.py and a check-golf GitHub workflow. When a `/check-golf` comment is posted on a PR, the bot compares the PR's base and head, checks that no declaration statement (signature/type) changed and only proofs/bodies changed, and upserts a single findings comment (posting it once, editing it on later runs). The Lean sources are parsed textually (no build): comments and whitespace are ignored, declarations are segmented on column-0 command starts, each statement is split from its body at the top-level `:=`, `where`, or equation `|` arm, and `by` proof terms embedded inside a type are treated as proof-irrelevant. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjiv6nckrp5cJT9rpgZaKT * feat: break golfs down by trivial shape (newline removed, `;`-joins) The report now also counts, among statement-preserving changes: - proofs where only a newline was removed (identical tokens, fewer lines), which were previously not surfaced at all; and - proofs where tactics were crammed onto one line with a `;` (excluding the `<;>` combinator), with the number of joins introduced. Also relabel "definition bodies changed" to "definition values changed" and spell out in the footer that it means a def/instance/abbrev whose type is unchanged but whose defining term changed. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjiv6nckrp5cJT9rpgZaKT * feat: split definition changes into proof-only vs value changed A `def`/`instance`/`abbrev` often carries proof obligations discharged by `by` blocks. Golfing only those does not change the definition's data, so it should not read as "the definition changed". The report now masks a definition's `by` proof blocks and splits its changes into: - "definition proofs golfed" (data unchanged), and - "definition values changed" (the defining term changed outside proofs). On PR #1332 this moves 76 of the 110 former "definition body" changes into the proof-only bucket, leaving 34 genuine value changes. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjiv6nckrp5cJT9rpgZaKT * fix: treat whole-body `by` defs as value changes, not proof golfs A `def foo : T := by refine …` builds its *value* with tactics, so a change inside that `by` block can change the definition itself, not just a discharged proof obligation. Masking it as a proof made such edits look like harmless proof golfs. Only classify a changed def body as "proof golfed" when the term outside `by` proof blocks is identical AND the body is not itself a single `by` block (mask != "<by>"). Otherwise report it as a definition-value change. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjiv6nckrp5cJT9rpgZaKT * report: soften "definition values changed" to "bodies changed (may have changed)" The bucket mixes genuine defining-term changes with defs where only proof parts changed but that can't be proven textually — e.g. a `def := by refine … ?_` whose data is untouched, or a structure-instance whose proof fields were rewritten from tactic to term mode. Asserting "data changed" over-claims those. Relabel to "Definition bodies changed (data *may* have changed, type unchanged)" and add an explanatory note; the high-confidence "Definition proofs golfed (data unchanged)" bucket is unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Vjiv6nckrp5cJT9rpgZaKT --------- Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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.
Summary
rflchurn inPhyslib/ClassicalMechanics/HarmonicOscillator/Basic.lean.by rflsplit regressions, zero files with nonnegative net Lean line delta, and zero non-shrinking sequence edit blocks.Added/Removed Declarations
Reviewer Map
Verification
lake env lean QuantumInfo/ForMathlib/HermitianMat/LogExp.lean;lake env lean Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/HyperCharge.lean;lake env lean Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.leangit diff --check;./scripts/lint-style.sh.oleandependencies such asPhyslib/SpaceAndTime/SpaceTime/Derivatives.olean,Physlib/Units/WithDim/Speed.olean, andQuantumInfo/ForMathlib/HayataGroup/TraceInequality/LiebAndoTrace.olean.