doc: record the Array.ofFn call-site audit, and add ofFn' compatibility lemmas - #9048
Merged
Conversation
Decides whether the tree should adopt the ofFn shim ahead of the upstream fix. It should not. Of 297 raw occurrences, only ~100 are in definition bodies, where kernel reduction is actually affected. The defect is real: Hex.Vector.unit in the released hex-matrix is @[expose], built with core Vector.ofFn, and does not reduce from a downstream module. But a blanket migration of the 62 mechanically reachable sites produces 29 build errors in three classes: files that are not module files at all, rfl proofs that break because ofFn is not defeq to ofFn, and proofs that break because the core getElem_ofFn/size_ofFn lemmas do not apply to the shim. Each migrated site costs proof churn proportional to how much its callers reason about the array contents. So migrate per-definition only where something concretely needs reduction, and fix the upstream gap instead. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0188fgvPvjbcXhvTYVSATLhv
Review of the first draft was right on two counts. The counts were wrong: a plain grep counts matching lines, including prose and the primed shim names. Stripping comments and matching the exact core identifiers gives 255 references, of which 66 are in definition bodies (not ~106) and 9 of those are `*Impl` definitions that must keep core `ofFn`. HexPoly has 3, all `*Impl`, not 13. And the blanket-migration experiment tested the wrong population. It rewrote `*Impl` definitions the recommendation says to leave alone, non-exposed definitions where reduction stops earlier anyway, and a file that is not a module file at all. Its failures are therefore not evidence that a targeted migration is costly, and the note no longer claims they are. Most of the churn it did show was a missing shim API rather than an inherent cost, so `HexBasic.OfFn` now provides `Array.size_ofFn'`, `Array.getElem_ofFn'`, `Vector.getElem_ofFn'`, and `Vector.toArray_ofFn'`. The conclusion stands but for a better reason: `import all Init.Data.Array.Basic` in the *consuming* module fixes the reduction with no change to any definition, which is cheaper than migrating anything. Verified against the `Vector.unit` probe. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0188fgvPvjbcXhvTYVSATLhv
kim-em
changed the title
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.
This PR records the outcome of auditing whether the tree should adopt the
ofFnshim ahead of the upstream fix in leanprover/lean4#14270. It should not, and the reasoning is worth keeping so it is not relitigated.The defect is real rather than hypothetical.
Hex.Vector.unitinHexMatrix.Basicis@[expose], is built with coreVector.ofFn, and does not reduce in the kernel from a downstream module;hex-matrixis a released library, so that ships. Switching that single definition toofFn'fixes it.The scale is smaller than the raw grep suggests. Of 297 occurrences across 48 files, only about 100 sit in
def/abbrev/instancebodies, which is the only position where kernel reduction is affected; the rest are theorem statements.A blanket migration of the 62 mechanically reachable sites was attempted and produces 29 build errors in three classes, each of which is a reason not to do it: some files are not module files at all, so
public importis a syntax error there;ofFn'is only propositionally equal toofFn, sorflproofs that went throughsimp only [..., Vector.getElem_ofFn, ...]break; and the shim has no lemma ecosystem, so anything reasoning about a migrated definition's contents needsofFn'_eq_ofFnthreaded in by hand. Each migrated site therefore costs proof churn proportional to how much its callers reason about the array.The recommendation is to fix it upstream and migrate individual definitions only where something concretely needs them to reduce, repairing their lemma uses at the same time, and never to migrate
*Impldefinitions, which are runtime implementations behind@[csimp]where coreofFnis correct.Documentation only; no code changes.
🤖 Prepared with Claude Code