WIP: Jcb/formalization2 - #4
Open
johnchandlerburnham wants to merge 20 commits into
Open
Conversation
annotatedPiReplay07 and the two aggregator lists it feeds compile fine without the marker; every data field is a plain def. Leftover from an earlier revision where the annotatedPi environment chain was still choice-based.
Add buildExecution totality lemmas at every trace level (positivity, positivity mode, constructor telescope, constructor list, singleton run): a successful checker execution guarantees the transparent decomposition returns .ok. ConstructorValidationRun.of_run now replays buildExecution and discharges the impossible error branch with the totality lemma, replacing its Classical.choice selection. Axiom guards are unchanged; the singleton fixture layer loses its only value-level choice root.
ConstructorCandidateAlignmentTrace.build and
buildConstructorPreFamilySafety already execute the exact audits their
check wrappers erase, so give each a totality lemma (a successful check
guarantees the builder returns .ok) and let the staged D2/D3 owners
match on the builder, discharging the impossible error branch with the
lemma. Both StagedNormalizationCandidate{Post,Pre}FamilyInput.ofRun drop
their Classical.choice selections and become computable.
With of_run and the staged D2/D3 ofRun packagers now replaying their builders, every fixture definition rooted in them compiles: the staged universe/post-family/pre-family inputs, their positivity-alignment helpers, and the cvm/prb test aliases across IndexedVecSemanticReplay, InductiveFixtures, and ConstructorValidityReplay. The definitions still selected through Classical.choice ..._exists generation packages keep their markers; making those computable needs a pure verified Expr-to- VExpr translator.
TrExprS's semantic premises only validate a translation, they never select between candidates, so the strict Theory translation of any IsUnique-fragment expression is computable syntactically. trExprS? is that computation: an env-free structural function over VLCtx that fails only on proj (whose Theory endpoint is an open design decision) and mvar. Agreement replaces soundness: TrExprS.trExprS?_eq proves any derivation's value is exactly the computed one, generalized over the existing value-preserving context alignment so let-bound types stay unconstrained, with literal spines pinned by new toConstructor_eq inversions. The trExprS?_isSome/of_trExprS?_eq wrappers are the replay API for de-choicing the semantic packagers: compute the translation, then transfer the Nonempty witness onto it.
…nslator Assemble the singleton semantic hierarchy choice-free: semanticOfUnique lifts thread trExprS?-computed views from the candidate-expression leaf through constructor, list, family, and normalization layers, with the executable D3 strict-view gate supplying the uniqueness certificates from the staged owner's safety trace. ProducedGenerationShapeCandidate.exactProducedPackage closes the package as data, and all five fixture packages (indexedVec, aliasFormer, annotatedPi, cvm, prb) replay it instead of choosing from their _exists theorems. IndexedVecSemanticReplay, InductiveFixtures, and ConstructorValidityReplay drop every remaining noncomputable marker; the project's survivors are the Experimental classical developments and the recursor-defined spec shims.
johnchandlerburnham
force-pushed
the
jcb/formalization2
branch
from
August 9, 2026 11:29
b7781f6 to
ea73301
Compare
L4L-09A checkpoint. Audit how the implementation stores nested inductives, commit the design decision, and pin both with build-failing probes in Lean4Lean/Verify/Environment/NestedRepresentation.lean; no acceptance behavior changes. The audit: Environment.addInductive flattens nested occurrences into auxiliary families, runs the ordinary mutual path, then restores - the final environment keeps only source families (all = source names, numNested = auxiliary count), restored constructor types, and one recursor per source family plus one per auxiliary family named by appendIndexAfter, all with flattened motive/minor counts and auxiliary rules keyed by previously declared inductives' constructors. No _nested.* constant survives, and the final metadata is independent of auxiliary-name collisions. The decision: the stored Theory payload stays the source VInductDecl with no new field; nested support is an additive artifact coupling the flattened block - which probes show the existing arbitrary-block machinery already accepts - with per-auxiliary specifications (the Theory analog of aux2nested) and a restoration substitution sigma. Probes verify on rose-tree, nested-indexed, and constant-universe fixtures that the port's nested path reproduces Lean's stored metadata exactly and that sigma over the existing flat-block generation artifacts reproduces every stored recursor type and rule RHS, using declaration-world values for constructor types and an instL elimination-offset splice for recursor-world artifacts. Source declarations remain rejected by every current analyzer. Gates: focused, aggregate, and default Lake builds, sorry frontier unchanged (25 known entries), Theory import boundary empty, whitespace clean; Nix proof/dependency build and flake checks run on this committed checkpoint.
L4L-09B checkpoint. Implement the Theory mirror of the kernel's ElimNestedInductive transformation per the committed L4L-09A design. VInductDecl.nestedElimination? (Theory/NestedInductive.lean) flattens a source declaration against caller-supplied, environment-free copies of the nested-into blocks (NestedTargetBlock; NestedTargetBlock.WF ties a copy to a VEnv): target recognition on application spines, the kernel's local-variable rejection for parametric arguments, rewrite without descending into replacements, value-keyed deduplication, auxiliary creation for every family of the target block with level instantiation and simultaneous parameter substitution, canonical appendIndexAfter naming, and a fueled fixpoint over queued auxiliary constructors. nestedStage3 gates acceptance by flattening success plus generation readiness of the flattened block through the unchanged L4L-08 block analyzers; no generated recursor, rule, or replay is claimed. Theory fixtures pin the exact flattened blocks and auxiliary specifications for the rose-tree and nested-indexed fixtures plus four structural negatives. The Verify differential (Verify/Environment/NestedTransformation.lean) proves the Theory flattening equal to the port's ElimNestedInductive output on the three real fixtures - families, constructors, specifications, and stored numNested - ties the hand-written List target block to Lean's stored metadata, and matches kernel accept/reject on the four nearest negatives, pinning the kernel's exact local-variable diagnostic. Gates: focused, aggregate, and default Lake builds, sorry frontier unchanged (25 known entries), Theory import boundary empty, whitespace clean; Nix proof/dependency build and flake checks run on this committed checkpoint.
…saction First L4L-09C sub-checkpoint: the complete generic nested layer. Theory: the total restoration substitution restoreExpr fires bottom-up at each auxiliary spine that completes its block-parameter count - coinciding with restoreNested's top-down pass on generated artifacts - with recursor renaming checked before the constructor-prefix case. NestedBlockChecked.recursors/generatedRules restore the flattened block's generation artifacts onto the appendIndexAfter inventory with declaration-world values instL-spliced by the elimination offset. VEnv.addInductNested inserts source families, source constructors, restored recursors, and restored rules in the four block phases; AddInductNestedTrace pins the exact phase boundaries, and the lemma suite (trace recovery, atomicity, le, freshness, family/ctor/rec lookup, rule membership) mirrors the block transaction through ctorFold_spec/rulesFold_spec. NestedBlockChecked.WF chains per-insertion constant and rule well-formedness along the deterministic phase folds; addInductNested_WF folds it into Ordered preservation, and the new VDecl.WF.inductNested case discharges through VEnv.WF.ordered. Verify: AddInductNestedTrace/AddInductNested alignment mirrors the block trace (real ConstantInfo insertions, TrConstVal translation, RecursorMapKMatches, rule fold), TrEnv' gains the inductNested case, and TrEnv'.wf/aligned/of_value/map_wf/sf_mono are extended. The restoration-parity differential proves the product sigma equal to Lean's stored metadata - every restored recursor name, universe count, and type, and every rule RHS in globally flattened order - on the rose-tree, nested-indexed, and constant-universe fixtures, and the Theory fixtures pin restored names, cleanliness (no auxiliary constant survives), rule counts, and the transaction's final lookups. Environment replay of real Inductive.Add.run output through the new alignment trace remains the open L4L-09C obligation. Gates: focused, aggregate, and default Lake builds, sorry frontier unchanged (25 known entries), Theory import boundary empty, whitespace clean; Nix proof/dependency build and flake checks run on this committed checkpoint.
Second L4L-09C sub-checkpoint. The real-output round-trip runs the port's complete Environment.addInductive on dependency-only kernel environments and compares its entire output - not the ambient elaborator metadata - against the Theory nested artifacts: stored payload families and constructors (universe counts and translated types), numNested against the artifact's auxiliary count, and every emitted recursor's name, universe count, type, K flag, and rule RHSs against the restored inventory in order, on the rose-tree, nested-indexed, and constant-universe fixtures. Nothing on either side is hand-authored: the left side is real Inductive.Add.run-derived output and the right side is computed by nestedBlockChecked?. The roadmap records the L4L-09C position: the generic layer and the metadata round-trip are landed; inhabiting NestedBlockChecked.WF for both ladder fixtures (checker-run certificates on restored artifacts or the general sigma-transport theorem) and driving the replay through TrEnv'.inductNested remain open. Gates: focused, aggregate, and default Lake builds, sorry frontier unchanged (25 known entries), Theory import boundary empty, whitespace clean; Nix proof/dependency build and flake checks run on this committed checkpoint.
Third L4L-09C sub-checkpoint: the sigma-transport core from the L4L-09A design note. Theory/Typing/NestedTransport.lean defines the clean compositional substitution substConst (each interpreted constant replaced by a closed value, level-instantiated per occurrence) with its full commutation calculus against liftN, inst, and instL, plus context-lookup transport. The ConstInterp environment morphism packages what nested restoration provides: interpreted constants become closed values typed at their sigma-image types in the target environment, surviving constants and registered defeqs are sigma-imaged, and the target is Ordered. IsDefEq.substConst proves the typed transport: every Theory judgment of the interpreted environment holds of the sigma-images in the target, with the interpreted-constant case discharged through IsDefEq.instL_r and closed-term weakening, and the extra case through the defeq clause. HasType/IsType/VConstant.WF/VDefEq.WF corollaries give exactly the field shapes of NestedBlockChecked.WF. Remaining transport obligations, recorded in the module docstring and plans/l4l-09c-replay-plan.md: the beta-collapse bridge from substConst to the spine-collapsed restoreExpr on generated artifacts, the per-phase morphism construction for a staged flattened block, and the fixture replays through TrEnv'.inductNested. Gates: focused, aggregate, and default Lake builds, sorry frontier unchanged (25 known entries), Theory import boundary empty, whitespace clean; Nix proof/dependency build and flake checks run on this committed checkpoint.
Fourth L4L-09C sub-checkpoint: the first real nested environment replay. Verify/Environment/NestedReplay.lean replays the stored rose-tree metadata (RoseTree, RoseTree.node, RoseTree.rec, RoseTree.rec_1) over the completed List replay environment. The NestedBlockChecked.WF package is proved outright: every phase constant and every restored rule is typed by direct concrete derivations (type_tac over the staged environments), with the printed artifact literals tied to the computed nestedBlockChecked? artifact by native_decide observations, so the package closure is the standard logical baseline plus the persistent-map container axioms and the named native observations - no sorryAx. The alignment trace inserts the real ConstantInfos with tr_type_expr_tac translations, exact freshness chains, the K-flag agreement, and the literal rule fold, and TrEnv'.inductNested drives the final map and environment into alignment, with Ordered derived and the exact transitional closure guarded. The nested-indexed fixture replay and the milestone close-out remain. Gates: focused, aggregate, and default Lake builds, sorry frontier unchanged (25 known entries), whitespace clean; Nix gates run on this committed checkpoint.
L4L-09C closure checkpoint. The second ladder fixture - the nested-indexed family through PVec - replays from real stored metadata: the PVec family and constructors are staged over the completed Nat replay through TrEnv'.inductStaging (with concrete WF and tr_type_expr_tac translations), and the stored NVTree metadata then drives TrEnv'.inductNested with the complete NestedBlockChecked.WF package proved by direct concrete typing derivations over the exact phase environments, printed artifact literals tied to the computed nestedBlockChecked? artifact by named native_decide observations, exact freshness chains, K-flag agreement, and the literal rule fold. Both package closures carry no sorryAx; the TrEnv' roots carry the usual transitional checker closure, exactly guarded. With both fixtures round-tripping real Inductive.Add.run output through generic packaging and environment replay - comparing every family, constructor, and recursor type and every rule RHS against stored metadata rather than hand-authored declarations - the L4L-09C exit is met and the milestone is pruned from the roadmap ladder: L4L-10A is active. The roadmap records the nested coverage boundary (single-target nesting; breadth belongs to L4L-11) and the proved sigma-hat transport as the generic justification layer. Gates: focused, aggregate, and default Lake builds, sorry frontier unchanged (25 known entries), Theory import boundary empty, whitespace clean; Nix proof/dependency build and flake checks run on this committed checkpoint.
L4L-10A. Every certified mutual block's iota rules are exact SimplePattern.iota patterns, and the block supplies the complete generic Params pattern facts at standard Theory axiom closure. Theory/Typing/Pattern.lean gains the implementation-independent shape layer: HeadConstN/HeadConst spines, of_varN_matches and HeadConstN.matches (varN-tower match inversion/construction), varNPaths capture paths, RecursorIotaPattern with matches_shape/matches_of, bounded subpattern classification (Subpattern.varN_const_le, subpattern_inv, app_subpattern), tower intersection laws (varN_const_inter_some/none, app_inter_varN_const_some, RecursorIotaPattern.inter_some/ inter_varN_const_some), component injectivity (varN_const_inj, RecursorIotaPattern.inj), and Pattern.RHS.appN. Theory/Typing/InductivePattern.lean names the generated rule anatomy (ruleBinders/ruleLhsBody/ruleCtorApp/ruleIdx, rule_lhs by rfl), defines rulePattern (major arity: parameters, motives, minors, and the constructor's result indices; argument arity: parameters plus fields), and matches the exact generated left body against it at the rule's recursor levels (ruleLhsBody_matches). The name-freshness inputs come from the certified blockGeneratedNames nodup bit transported across the normalization boundary (sameTypeHeaders name transport); the major-arity agreement between same-recursor rules is extracted from the analyzer's terminal blockTarget? arity equation through the checked family spine (view_resultIndices_length, env-free). IotaPat couples each rule pattern with an RHS template (the registered right tower applied to the captured common arguments and fields) and a check list (parameter and result-index agreement), closed under a decidable RuleClosure bundle. pat_simple, recover, rule distinctness (rulePattern_inj), pat_uniq, pat_app_l, pat_app_l_uniq, and pat_app_uniq are exactly the Params obligations for the block set, with guarded propext/Quot.sound closures (pat_uniq additionally Classical.choice). No open-environment Params instance is installed. Theory/Typing/InductivePatternFixtures.lean pins two literal-name certified blocks by kernel evaluation: a mutual tree/forest pair (majors 6/6/6, arguments 3/1/3) and a Nat-indexed vector (majors 5/5, arguments 1/4), including RuleClosure by decide and exact pattern inventories. Gates: lake build Lean4Lean.Theory Lean4Lean.Verify, SorryFrontier (25 known, unchanged), and the default build are green; nix gates run on this checkpoint before the bookmark advances. plans/roadmap.md moves the ladder to L4L-10B (pattern soundness and environment assembler).
L4L-10B. A successful match of a certified block rule whose checks hold is definitionally equal to its instantiated RHS template, through the exact rule defeq registered by addInduct, and a block-local assembler builds environments whose defeq sets are exactly generated rules plus separately certified extensions. Theory/Typing/InductivePatternWF.lean builds the typed β-collapse layer at a sorry-free propext/Quot.sound closure: IsDefEq.appN_lamN collapses a lambda telescope applied to a full well-typed spine to the iterated instantiation (instRev) of its body, via instN_lamN/instL_lamN pushes, Ctx.InstN.consTel, OnTel.instN, SpineDefEq with appN_defEq/appN_congr pointwise application congruence, SpineWF.defEq_of_pointwise, and the lamN_wf/forallN_wf tower inversions (clean lam_inv/forallE_inv only). varN_matches_paths reads a match's captures back as the spine arguments; instRev_bvar_lt and map_instRev_bvarRevRange_seg compute instantiation images of reverse bound-variable segments. pat_wf then derives pattern soundness: the redex, decomposed into recursor and constructor spines with spine-form typing and source-pinned major levels (exactly what a verified reduction site holds), is defeq to the applied right tower — by the registered defeq (.extra), spine congruence along the capture spine, per-index tower collapses composed with the parameter/index agreement checks, and the capture computation of the L4L-10A templates. Its guarded closure is exactly the Church-Rosser development's transitional unique-typing closure (propext, sorryAx, Classical.choice, Quot.sound), shedding sorryAx automatically when L4L-16/17 land. Theory/Typing/InductivePatternEnv.lean adds the assembler: CertifiedExtension couples a defeq with its simple pattern, payload, and the spine-level extra_pat coverage equation; assembleEnv runs the block's four insertion phases over a base and folds the extension defeqs; assembleEnv_defeqs/assembleEnv_defeq_cases invert the assembled defeq set exactly (constant phases preserve defeqs, rule and extension folds add exactly their lists); assembleEnv_WF preserves ordering via the block preservation theorem and the rule-fold WF lemma; AssembledPat is the union pattern set with pat_simple and per-extension ext_covers. No global open-environment Params instance is installed: upstream extra_pat demands syntactic pattern matches of registered defeqs, which lambda-tower registrations (including quotDefEq) never satisfy, so the assembler exposes spine-level coverage and pat_wf-derived reduction instead. Fixtures assemble both L4L-10A blocks over the empty base and pin their defeq sets to the generated rules. Gates: lake build Lean4Lean.Theory Lean4Lean.Verify, SorryFrontier (25 known, unchanged), and the default build are green; nix gates run on this checkpoint before the bookmark advances. plans/roadmap.md prunes L4L-10 and moves the ladder to L4L-11.
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.
todo