Forward-port to Lean/mathlib v4.31.0 - #7
Closed
gotrevor wants to merge 4 commits into
Closed
Conversation
Forward-ports the library from Lean/mathlib v4.29.0 to v4.31.0 on top of current master (which already includes the FormalizedFormalLogic#794 FirstOrder redesign and the FormalizedFormalLogic#829 ProvabilityLogic removal). - Config bump: lean-toolchain, lakefile.toml (mathlib + doc-gen4 pinned to v4.31.0), lake-manifest.json regenerated. - Source changes to build green on v4.31.0. Whole library builds green (1730/1730 targets). No new proof holes: the sorry/admit count is unchanged versus the base commit. Recurring change patterns: - `simpa … using X` -> `simpa … using! X` (v4.31 needs the defeq-close hatch where the elaborated term is defeq but not syntactically equal to the goal). - `coe_injective'` -> `coe_injective` on mathlib FunLike/SetLike instance bodies (field renamed upstream). - Bare `zero_le a` -> `Arithmetic.zero_le a` across the arithmetic tree (mathlib's `zero_le` now shadows the protected Foundation lemma). - `instance` -> `lemma`/`def` where v4.31's stricter instance checker rejects a non-typeclass return type (`.Nonempty`, `.Countable`) or a hypothesis it cannot infer. - `Function.comp_def` added to simp sets for `f ∘ v` vs pointwise mismatches. - `Nat.testBit` / `Nat.bitIndices` API update in Proof/Coding. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Owner
Author
|
merged upstream: FormalizedFormalLogic#830 |
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.
Forward-ports FormalizedFormalLogic/Foundation from Lean/mathlib v4.29.0 → v4.31.0, on top of current upstream master (
c089e7ab, which already includes FormalizedFormalLogic#794 FirstOrder redesign and FormalizedFormalLogic#829 ProvabilityLogic removal).Base: this PR targets
v4.31-port-base, a branch pinned to the exact upstream-master commitc089e7ab, so the diff is only the port.masteris left untouched.What changed
lean-toolchain,lakefile.toml(mathlib + doc-gen4 → v4.31.0),lake-manifest.jsonregenerated.Foundation.lean: regenerated vialake exe mk_all --module(v4.31 module-system header).Verification
axiom/sorry/admit. The only additions are 5 small proved helpers/compat-shims; severalinstances becamedef/lemma(same names) under v4.31's stricter instance checker.Recurring change patterns
simpa … using e→simpa … using! e— v4.31 tightenedsimpa's final match to reducible transparency;using!opts back into semireducible, so goals that hold only up to unfolding a semireducible def still close.coe_injective'→coe_injective(mathlib FunLike/SetLike field rename).zero_le a→Arithmetic.zero_le a(mathlib'szero_lenow shadows the protected lemma).instance→lemma/defwhere v4.31's instance checker rejects a non-typeclass return type or an uninferable hypothesis.Function.comp_defadded to simp sets;Nat.testBit/Nat.bitIndicesAPI update inProof/Coding.Related work
Semiterm.Operator.val) rather thanusing!. Both approaches are valid; posting this as an alternative, not a replacement.🤖 Generated with Claude Code