# Type Class Generalization `AutoGeneralization` currently generalizes type class assumptions only. The same analysis is shared by the linter and command frontends. ## One-step pipeline `analyzeClosed` opens a theorem once, then calls `selectProposal` independently for each instance binder returned by `classSources`. ```mermaid flowchart LR A["analyzeClosed"] --> B["classSources"] B --> C["selectProposal"] C --> D["EvidenceGraph.create"] D --> E["shared lazy node cache"] E --> F["cut probe / full cut search"] E --> G["complete candidate registry"] F --> H["candidate-plan groups"] G --> I["singleton groups"] H --> J["proposal builders"] I --> J J --> K["closeAndValidateProposal"] K --> L["selection and ambiguity resolution"] ``` Search only proposes candidate groups. Both builders are partial functions and may reject them. Selection sees only `CheckedProposal`s that have already passed closed-term, replay, and kernel validation. `selectProposal` creates one source-specific `EvidenceGraph`. A completed cut search returns both its plans and the complete candidate registry accumulated during the same traversal. Only an exhausted probe starts the independent all-or-nothing registry traversal. The main objects shared between stages are: | Object | Meaning | | --- | --- | | `TheoremContext` | The opened telescope, conclusion, and proof term. | | `ClassSource` | One instance binder being considered for removal. | | `EvidenceCandidate` | A reusable evidence term, its WHNF class type, and the recorded class name. | | `EvidenceNode` | One cached candidate classification and its source-dependent syntax children. | | `EvidenceGraph` | A source-specific lazy view of the evidence DAG and its analysis roots. | | `CandidateRegistryResult` | Complete singleton-anchor coverage or explicit exhaustion. | | `CandidatePlan` | A candidate group plus the outer evidence bypassed to reach it. | | `CheckedProposal` | A closed generalized type and proof that replay the source theorem. | ## Search Evidence inspection and registry coverage are in `TypeClass/EvidenceGraph.lean`. Bounded candidate-cut enumeration remains in `TypeClass/Search.lean`. ### Evidence graph and candidate registry - `candidateAt?` recognizes a fully applied class-evidence term. It accepts an `extends` projection or an application whose head is a registered instance. It rejects the original source class and the theorem proposition itself. - `EvidenceGraph.inspect` applies that classification at most once per expression and caches its immediate source-dependent syntax children. - `EvidenceGraph.dependsOnSource` computes source occurrence bottom-up and memoizes every visited subexpression. - `EvidenceGraph.sameEvidence` memoizes metavariable-free defeq comparisons for the lifetime of one source analysis. The probe, registry, and full search share this cache. - `EvidenceGraph.collectCandidates` visits later binder types, the conclusion, and the proof. It also follows each candidate's inferred type because a dependency can occur only there, for example `C (A.toB source)`. - Collection returns individual resynthesis anchors, not combinations. It is independent of cut conflicts, pruning, and plan caps. Candidate inferred types remain attached to `candidate?`, separate from `EvidenceNode.termChildren`, because cut search traverses these two edge kinds differently. A completed cut traversal itself proves complete coverage; otherwise the dedicated registry must finish. Exhaustion exposes no partial registry: missing one equally small signature could turn a real ambiguity into an apparent unique result. ### Candidate-plan search `EvidenceGraph.searchCandidatePlansResult` runs `cutPlans` over: 1. every binder type after the source; 2. the theorem conclusion; 3. the proof term. Candidate recognition rejects the theorem proposition itself, so a class-valued proof root cannot become a new assumption. Evidence used inside the proof remains searchable. At a reusable evidence expression, `cutPlans` has two meaningful choices: - keep the outer evidence as a candidate at zero additional cost; - descend to concrete child evidence and record the outer term in `bypassed`. `CandidatePlan.cost` is the number of definitionally distinct bypassed outer terms. It prefers cuts that preserve useful outer evidence; it is not the number of generated binders. If a source-dependent subtree has no visible exact cut, `cutPlans` returns the neutral plan `{}` instead of deleting the complete parent plan. This is a deferred branch: it preserves candidates collected from sibling uses, but makes no correctness claim. For example: ```lean theorem deepFromSource [Source α] : Deep α := ... instance [B α] [C α] : Deep α := ... ``` Even though `deepFromSource` is not a registered instance, sibling uses of `source.toB` and `source.toC` can still produce the group `[B α, C α]`. `buildResynthesizedProposal` later decides whether that group really rebuilds `Deep α`. To avoid turning every projection into a powerset branch, descending below an already usable candidate is retained only when it finds a concrete inner candidate. An empty deferred descent is discarded because keeping the outer candidate gives the resynthesis scheduler at least as much information. ### Search pruning The search uses the following pruning rules: | Rule | Function or state | Effect | | --- | --- | --- | | Source-free short circuit | `cutPlans`, `collectAt` | Skips subtrees that do not mention the source. | | Dependency cache | `EvidenceGraph.dependsOnSource` | Computes and caches source occurrence for every recursively visited node. | | Lazy node cache | `EvidenceGraph.inspect` | Infers and classifies each expression at most once per source. | | Shared defeq cache | `EvidenceGraph.sameEvidence` | Reuses stable evidence comparisons across plan merges and search passes. | | Class-name filter | `EvidenceCandidate.className` | Rejects evidence from different classes before an expensive defeq check. | | Theorem-class filter | `candidateAt?` | Skips theorem-type defeq unless the candidate has the same class head. | | Candidate interning | `registerCandidate` | Assigns search-local IDs to defeq candidate terms. | | Work budget | `takeWork`, `SearchState.work` | Bounds source-relevant visits and Cartesian plan merges. | | Registry DAG memoization | `RegistryState.visited` | Charges each source-relevant expression once during registry coverage. | | Cycle guard | `cutPlans` with `active` | Stops a recursive evidence cycle with a neutral deferred branch. | | Evidence deduplication | `addCandidate`, `addBypassed` | Collapses definitionally equal candidate or bypass terms. | | Same-class conflict | `addCandidate` | Rejects only a plan containing two distinct dictionaries for one anonymous binder type. | | Bypass antichain | `pushPlan` | Drops a plan when the same candidate set already has a subset of its bypass evidence. | | Plan cap | `maxCandidatePlans` | Exhausts the search before an additional plan is retained. | | Combination budget | `combinePlanSets` | Charges every pair considered during a Cartesian merge. | | Join ordering | `searchCandidatePlansResult` | Combines smaller root plan sets first, then restores candidate discovery order. | | Completed-plan minimization | `minimizeCompletedPlans` | Keeps the cheapest bypass set for each candidate set. | | Deferred-branch pruning | `cutPlans` | Drops empty descent below an already usable candidate. | When the probe completes, its traversal registry needs no second budget. Otherwise dedicated registry coverage and full cut search use independent work counters. Sharing the node and evidence-comparison caches avoids repeated inference, instance lookup, expression decomposition, and defeq work. Comparisons containing metavariables are deliberately not cached because later assignments could change their result. An exhausted cut search never exposes partial plans. An exhausted registry never exposes partial candidates and therefore cannot establish fallback uniqueness. Selection may retain an independently exhaustive exact result or run full exact search, but it does not use incomplete singleton information. Thus resource settings affect completeness, not proposal validity. ## Proposal builders ### Exact replacement `buildProposal` in `TypeClass/BuildProposal.lean` preserves the selected evidence graph exactly. 1. `orderEvidenceCandidatesForInsertion` puts nested evidence before its users and preserves source order between independent candidates. 2. `insertReadyCandidates` waits until a candidate type no longer contains the source and no longer depends on a future theorem binder. 3. `rewriteExpr` uses `kabstract` with proof irrelevance disabled to replace all definitionally equal occurrences of each evidence term. 4. `withRebuiltBinders` removes the source and rebuilds every retained binder under the rewritten types. 5. Any remaining source occurrence, conflicting dictionary, or solved candidate metavariable rejects the proposal. Fresh evidence metavariables are finally abstracted as instance-implicit binders. If an earlier exact replacement already made a later candidate source-free, that later candidate is marked handled and introduces no binder. ### Multi-candidate binder-ready resynthesis `buildResynthesizedProposal` in `TypeClass/Resynthesize.lean` allows only source-dependent class evidence to be synthesized again. `resynthesizeSourceEvidence` traverses an expression bottom-up. Whenever a subexpression still mentions the removed source and its inferred type is a class, it asks `synthInstance?` for replacement evidence. This applies to any class-valued term, including a theorem such as `deepFromSource`; candidate registry entries remain restricted to projections and registered instances. At each telescope boundary, `withReadyCandidates` repeatedly calls `candidateAction`: | Action | Condition | Result | | --- | --- | --- | | `blocked` | Transformation still needs the source, leaves metavariables, or depends on a future binder. | Wait for another candidate or a later boundary. | | `synthesized` | The candidate class is already available in the rebuilt local-instance context. | Mark it handled without adding a binder. | | `introduce type` | The class is ready but cannot be synthesized. | Add a real instance binder and restart the scan. | The scan restart is what makes joint resynthesis work. Introducing `[B α]` may unlock `[C α]`, and together they may synthesize `Deep α`; the explicit `Deep` candidate then becomes redundant. `withLocalDecl` is nested through a continuation, so every introduced class remains registered as a local instance while later candidates, binders, the conclusion, and the proof are rebuilt. `withResynthesizedBinders` calls this scheduler before every original binder and once after the telescope. Therefore a candidate `PointWeak α x` is blocked before `x`, then inserted immediately after `x`. Candidate checks run under `withoutModifyingMCtx`, and only metavariable-free candidate types escape the check. The old local context remains available for reading original expressions, but the local-instance vector is cleared. This prevents typeclass search from silently reusing the source dictionary that the proposal is supposed to remove. ## Selection `selectProposal` in `TypeClass/SelectProposal.lean` combines bounded search and the two builders. 1. When complete iteration permits unused removal, first try `buildProposal opened source #[]`. A checked zero-binder result is final. 2. Create one lazy `EvidenceGraph` for the selected source. 3. Run cut search on that graph with `min exactProbeWork maxSearchWork`. 4. If the probe completes, `selectExactPlans` validates plans in ascending cost. The first cost tier producing checked proposals becomes the exact baseline, but does not bypass fallback merely because it introduces one binder. 5. Use the complete registry returned by the finished cut traversal. Registry singleton groups use `allowExact := true`; cut-plan groups use resynthesis fallback only. Identical groups combine these permissions. 6. If the probe was exhausted, validate complete-registry singletons first. A unique singleton result avoids full cut search; otherwise run full cut search on the same graph with `maxSearchWork`. The completed full search supplies a complete registry even if the dedicated registry exhausted. Changing `exactProbeWork` therefore changes which path computes coverage, not the selected checked result. `selectExactPlans` is cost-first. `selectFallback` instead minimizes `proposal.introducedIndices.size`, because resynthesis is intended to remove redundant evidence binders. `pushChecked` merges only definitionally equal generated signatures. Among equivalent signatures it chooses: 1. exact replacement over resynthesis; 2. otherwise the smaller structural `CandidateGroup.key`. The key is `(term size, abstracted candidate type, abstracted candidate term)`. Theorem free variables are abstracted before comparison, making the choice stable across fresh local contexts. This key belongs only to selection: generated binder order is controlled separately by `orderEvidenceCandidatesForInsertion`. Definitionally distinct signatures are never made equivalent by canonical ordering. They remain ambiguous. Exact and resynthesized builder results are cached by structural candidate-group key for the lifetime of one source selection. Probe fallback, singleton fallback, and full search therefore do not rebuild and revalidate the same group. When an exact baseline exists, fallback must introduce strictly fewer binders to affect the final choice. The resynthesis scheduler receives that exclusive bound and stops before proof rewriting as soon as another candidate binder would make improvement impossible. `resolveChoice` applies the final policy: | Exact baseline | Fallback | Result | | --- | --- | --- | | unique | unique and strictly fewer binders | fallback | | unique | absent, ambiguous, equal, or larger | exact | | absent | unique | fallback | | ambiguous | unique and smaller than every exact alternative | fallback | | ambiguous | otherwise | no proposal | This preserves an exact, checked signature when several incomparable weaker signatures compete. ### Deliberate future boundaries `cutPlans` is not memoized by expression alone. Candidate-type edges can return to an expression already in the active recursion stack, so such a cache would silently reuse a result computed under a different cycle cut. A future DP pass must first materialize these edges and condense strongly connected components. Binder count is still the fallback cost, not a proof of logical weakness. Witness-based entailment between dependent generated contexts requires keeping the provenance of every retained and introduced binder so the contexts can be aligned before instance synthesis. Until that representation exists, distinct minimal signatures remain ambiguous. ### Why singleton coverage is separate A complete cut can require `[ReplayP α, ReplayQ α]`, while singleton `[ReplayQ α]` lets resynthesis reconstruct `ReplayP α` and introduces only one binder. More importantly, two singleton anchors can produce different, equally small signatures. Complete registry coverage is therefore part of conservative ambiguity detection, not merely a performance fallback. ## Shared validation and correctness boundary Both builders finish through `closeAndValidateProposal`. - `validateClosed` requires a closed, well-typed proposition and proof. - `replaysOriginalType` applies the generalized theorem to the original evidence and retained binders. The resulting type must be definitionally equal to the original theorem statement. - The new proof term need not be definitionally equal to the old proof; it only has to prove the original statement after specialization. Re-synthesis does not permit an arbitrary change of Type-valued dictionary identity. If a retained binder is indexed by old evidence, replay still requires the rebuilt binder type to match definitionally. Prop-valued evidence can differ by proof irrelevance; incompatible data-valued evidence keeps an explicit binder or rejects the proposal. Consequently, search pruning and deferred branches may omit valid proposals, but they cannot make an unchecked proposal valid. ## Worked traces ### Split one source and jointly rebuild hidden evidence Suppose `A α` extends `B α`, `C α`, and `D α`; the theorem uses `source.toB` and `source.toC`, while a retained binder contains non-instance evidence `deepFromSource source : Deep α`. There is also a registered conversion `[B α] [C α] → Deep α`. | Stage | State | | --- | --- | | Cut search | Finds `source.toB` and `source.toC`; the non-instance deep term contributes a neutral deferred branch. | | Candidate group | `[B α, C α]`; unused `D α` never enters the group. | | Source boundary | Introduces `B α`, restarts, then introduces `C α`. | | Retained binder | `resynthesizeSourceEvidence` rebuilds `Deep α` from the two new local instances. | | Checked result | `[A α]` becomes `[B α] [C α]`; neither `D α` nor an explicit `Deep α` binder remains. | No single candidate is sufficient. The group from cut search is what lets the resynthesis scheduler observe both instances simultaneously. ### Wait for a later ordinary binder For a source followed by `(x : α)`, a candidate `PointWeak α x` cannot be inserted at the source position. | Boundary | `candidateAction` | | --- | --- | | Before `x` | `blocked`, because the candidate type contains a future binder. | | Rebuild `x` | Adds the fresh version of `x` to the new telescope. | | After `x` | `introduce (PointWeak α x)`. | | Later dependent class | Re-synthesizes its stored view from the new `PointWeak` instance. | The resulting order is `(x : α) [PointWeak α x] ...`, not a candidate moved blindly to the old source position. ## `#autogeneralize!` `#autogeneralize!` applies the same checked step iteratively. After replacing one source binder—possibly with several dependent evidence binders—it opens the new closed theorem and searches again. Reanalysis is essential because a split can change later instance types or make a previously blocked source removable. Among the proposals currently valid, the command prefers the latest source binder. Later binders may depend on earlier instances, so discharging them first often removes transient evidence from an earlier split. Each iteration therefore examines sources in reverse and stops at the first unseen checked proposal, instead of constructing proposals for earlier binders that cannot be selected. It stops at a fixed point; definitionally repeated signatures guard against cycles. `#autogeneralize!` also removes an earlier source that becomes unused after a later instance is generalized. `#autogeneralize` and the linter report only nonempty replacements. If the ordinary command finds only checked removals, it reports that no nonempty generalization exists and points to `#autogeneralize!`. Every intermediate step passes closed validation and, when specialized, proves the preceding theorem statement. The final proof therefore remains connected to the original theorem without imposing an irrelevant proof-term equality. Generated source normally keeps instance binders anonymous. If ordinary type class synthesis would reconstruct different evidence, the command assigns collision-free `evidenceN` names and prints only the affected applications with explicit instance arguments. This keeps mixed cuts exact without making every generated theorem verbose. This pass introduces only type class binders. It does not abstract an ordinary term such as `s.size` into a new `Nat` parameter. For every checked proposal, the core also closes the removed source class over the generalized telescope and asks typeclass synthesis for a witness. Success proves operationally that the new assumptions still reconstruct the old class. The command keeps the proposal but annotates it; the linter suppresses it. This test is sound when it succeeds, but failure is not a proof of mathematical non-derivability because an implication need not be registered as an instance. The linter applies this check and its exclusion policy after analysis. Global source and target exclusions are `NameSet`s; directed exclusions are a `NameMap NameSet`. The linter collects every introduced class into one `NameSet`; if any target is excluded for the source, the whole proposal is suppressed. The same policy therefore covers proposals that replace one instance with several. These policies affect diagnostics without weakening the reusable engine. ## Search configuration The public Meta API takes a `SearchConfig := {}` at each search and analysis entry point. Its fields and defaults are: - `maxCandidatePlans := 128`: maximum plans retained at one merge; - `exactProbeWork := 256`: work allowed for the inexpensive exact probe; - `maxSearchWork := 4096`: work allowed independently for complete registry coverage and each full cut search. The probe is also bounded by `maxSearchWork`. `maxCandidatePlans` limits only cut-plan search, never registry coverage. Reaching a limit discards that stage's partial result. These settings therefore trade search completeness for runtime; they do not weaken closed-term, type-replay, or kernel validation. Commands and the linter currently use the defaults. Meta callers can override individual fields with, for example, `(config := { maxSearchWork := 8192 })`. ## Imported theorem implementations Within its defining module, a theorem has `thmInfo` and a proof value. An ordinary downstream import exposes it as `axiomInfo`. Because Lean records imports in the module header, a command cannot safely upgrade that import after elaboration has started: the generated proof may depend on private helpers from the defining module. The command therefore locates the module that supplied an imported `axiomInfo` and requests `import all Module.Name`. On the next elaboration Lean loads the complete module implementation, the declaration is available as `thmInfo`, and the normal checked analysis applies without a separate wrapper. Known built-in axioms are rejected directly. If an `import all` declaration still has `axiomInfo`, the command also reports that no proof term exists instead of recommending the same import again. ## Executable examples `AutoGeneralizationTest/Examples.lean` keeps the user-facing cases executable: - `lexicographicSelf` wraps Mathlib's `Prod.Lex.toLex_le_toLex` and replaces one `Preorder` with the `LT` and `LE` capabilities used by that theorem. - `coprimeIffOverField` wraps Mathlib's `Semifield.isCoprime_iff` with a deliberately stronger `Field` assumption. The registered `Field.toSemifield` conversion recovers the useful `Semifield` signature. - `selfAdjointDivOverField` keeps `StarRing` while replacing `Field` with `Semifield`; rebuilding the retained class requires re-synthesizing algebraic evidence selected in the old `Field` context. - `lexicographicPair` applies `#autogeneralize!` to two independent `Preorder` sources, retaining `LT` for the first component and `LE` for the second. - `topologicalInvComponent` recreates the assumptions that `inv_mem_connectedComponent_one` had before [Mathlib PR #23193](https://github.com/leanprover-community/mathlib4/pull/23193). The ordinary command finds `ContinuousInv`; the complete command then weakens `Group` to `DivisionMonoid`. ## Files - `AutoGeneralization/TypeClass.lean` is the public import facade for the core. - `AutoGeneralization/TypeClass/Basic.lean` contains the shared theorem, evidence, and source-binder data structures. - `AutoGeneralization/TypeClass/EvidenceGraph.lean` caches source-specific evidence inspection and provides all-or-nothing candidate-registry coverage. - `AutoGeneralization/TypeClass/Search.lean` defines `SearchConfig`, selects source binders, and enumerates bounded candidate cuts over the shared graph. - `AutoGeneralization/TypeClass/Validation.lean` closes rebuilt telescopes, performs shared kernel and type-replay validation, and is the only module that can construct a `CheckedProposal`. - `AutoGeneralization/TypeClass/BuildProposal.lean` inserts a ready candidate group by exact evidence replacement. - `AutoGeneralization/TypeClass/Resynthesize.lean` schedules binder-ready candidate groups and rebuilds proposals in a clean local-instance context. - `AutoGeneralization/TypeClass/SelectProposal.lean` combines bounded search, proposal validation, fallback selection, pruning, and ambiguity handling. - `AutoGeneralization/TypeClass/Recoverability.lean` checks whether the generalized context can synthesize the removed source class. - `AutoGeneralization/TypeClass/Analyze.lean` opens closed theorems, analyzes each source binder, and builds the iterative complete-generalization chain. - `AutoGeneralization/Linter.lean` renders type class diagnostics and applies the linter policy. - `AutoGeneralization/Command.lean` defines the command frontends and assembles analysis results into code-action suggestions. - `AutoGeneralization/Command/PrettyPrint.lean` pretty-prints exact theorem source while preserving noncanonical instance evidence. - `AutoGeneralizationTest/TypeClass.lean` contains the core regression tests, including multi-evidence, dependent-candidate, dependent-binder, binder-reordering, interaction, ambiguity, and rejection cases. - `AutoGeneralizationTest/EvidenceGraph.lean` fixes registry coverage, cut-plan separation, ambiguity-sensitive singleton coverage, and budget behavior. - `AutoGeneralizationTest/Examples.lean` contains public command and linter examples without metaprogramming code. - `AutoGeneralizationTest/ImportedCommand.lean` checks direct analysis through `import all`; `ImportedCommandFailure.lean` checks the ordinary-import hint.