Bump Lean to v4.33.0 - #128
Merged
Merged
Conversation
quangvdao
pushed a commit
that referenced
this pull request
Aug 12, 2026
* fix(pfunctor): replace global reducible overrides with implicit_reducible Lean 4.33 split the transparency ladder (reducible < instances < implicit < default) and now compares assigned metavariable types at implicit transparency. The v4.33 migration compensated by marking upstream declarations globally reducible under allowUnsafeReducibility, which perturbs simp and typeclass discrimination-tree indexing for every downstream module and forced the removal of valid simp lemmas. - PFunctor.Obj (Mathlib): demote the global override to implicit_reducible, its minimal sufficient tier, with a justification comment; restore the @[simp] on M.dest_inj that the reducible override had invalidated. - FreeM.bind / FreeM.map (cslib): drop the global overrides entirely. The four consumers that actually need implicit-transparency unfolding now declare an option-free `attribute [local implicit_reducible]` scoped to their own file, and proofs deleted by the migration are restored where they again close. - Display/Category.lean: replace the allowUnsafeReducibility local reducible block on FreeP.substMonoid with the option-free local implicit_reducible form. The reducible version over-unfolded typeclass goals, breaking Monad (Extension _) resolution once Obj is no longer globally reducible. - SubstMonoid/Extension.lean: restore the original term-mode LawfulMonad proofs, which elaborate again under this attribute regime. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * fix(cofree): convert Universal.lean to implicit_reducible, restore simp API Replace the three allowUnsafeReducibility local-reducible blocks with one option-free `attribute [local implicit_reducible]` block, and demote the def-site @[reducible] on unfoldShape / unfoldRootDirection / unfoldDirection / unfoldLens to @[implicit_reducible]. Because implicit_reducible does not unfold at reducible transparency, the seven rfl simp lemmas the migration had to drop (cogenerator_toFunA, cogenerator_toFunB, cogenerator_comp_map, comonoid_identity, comonoid_target, comonoid_compose, cogenerator_comp_unfoldLens) are valid again and return to the default simp set, and all nine with_unfolding_all escalations revert to the original rw/simpa proofs. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * fix(pfunctor,cofree): convert core transparency workarounds to implicit_reducible Apply the Universal.lean recipe across the PFunctor core, Free, Display, Comonoid, Cofree, and PatternRunsOnMatter subtrees: - every `set_option allowUnsafeReducibility true in attribute [local reducible] ...` block becomes an option-free, commented `attribute [local implicit_reducible] ...` block; - migration-added def-site @[reducible] demotes to @[implicit_reducible], except genuine thin type wrappers (C, selfMonomial, constProd, CofreeC, stateComonoid, Comonoid.unit/tensor) which keep @[reducible]; - the simp attributes the migration dropped return (projectionN_zero, the four LaxMonoidal cogenerator/laxTensor lemmas, the freeM_unfold append_liftBind pair), all passing simpNF; - proofs brute-forced during the migration revert to their original text where they close again; the handful of genuinely Lean-4.33-forced changes (e.g. calc Trans instances resolving below implicit transparency, core's Function.comp demotion) keep the migration's proof with a one-line comment naming the reason. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * fix(dynamical): convert transparency workarounds to implicit_reducible Convert all four allowUnsafeReducibility local-reducible blocks (CofreeMate, Bounded, Termination, Parallel/Behavior) to option-free commented `attribute [local implicit_reducible]` blocks, demote the def-site @[reducible] on DynComputation.mapResult / wrap, restore the four dropped simp attributes (terminatesFrom_return and the three parallelBehavior_answer lemmas), and eliminate all eight with_unfolding_all escalations by restoring the original proofs. Simulation.lean's proof bodies return to their original one-line forms (statements deliberately left for a separate change). The split-calc shapes kept in Responder files carry comments: calc's Trans instance resolves below implicit transparency, a genuine Lean 4.33 constraint. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * fix(itree): restore original proofs under implicit_reducible The migration left no attribute blocks in ITree but bloated proofs instead (+129/-35 in Rec/Facts.lean alone): simp proofs with appended rfl, subst replaced by rw, direct rewrites replaced by fully-ascribed have-then-rw chains, and corecursor step functions inlined into statements. All of it reverts to the original text. The enabling attributes are small and commented: `Sum.elim` needs implicit_reducible for `(P + Q).B (Sum.inl e)` to reduce during implicit-transparency checks in the sum-signature proofs, and `PFunctor.Obj` locally in Bisim/Bind. Unfold.lean and Sim/Facts.lean are again byte-identical to main; the migration's import all additions there are gone. ITree / ExceptE / StateE / Handler keep @[reducible] as genuine thin wrappers; Handler.id and recursiveHandler demote to @[implicit_reducible]. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * fix(interaction): convert transparency workarounds to implicit_reducible Convert all Interaction attribute blocks to option-free commented `attribute [local implicit_reducible]` blocks and demote every migration-added `@[expose, reducible]` to `@[expose, implicit_reducible]` (all ten hold; none needed full reducible). TwoParty/Strategy.lean's +105/-38 of let-barrier / change / manual-calc workarounds revert to the original proofs, as do the UC OpenProcess retyping chains and the Chain/Append proofs, with four of the six dropped simp attributes restored. The two substMonoid_mult projection lemmas stay un-simped with comments: their heads are reducible abbrevs, so simpNF correctly rejects them — a pre-existing latent issue the 4.33 validation now surfaces. Compose.lean keeps its consolidated shape (the one file the migration made shorter) with its block converted option-free. pairedMonadic.map now takes its node argument directly instead of via simpa, removing Eq.mp casts that 4.33 can no longer see through. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * fix(test): convert PolyFunTest transparency workarounds to implicit_reducible Convert all 27 allowUnsafeReducibility local-reducible sites across the test library to option-free local implicit_reducible blocks or def-site @[implicit_reducible] on test-local definitions, and restore the example proofs the migration had rewritten wherever they close again. Every example's assertion is back to its original statement; in particular SimulationExamples.lean is again byte-identical to main, including the Coalg.Hom.id statements the migration had weakened. The state/exception interpreter examples keep the migration's rw chains with comments: the interpState/interpExcept simp lemmas currently key their discrimination-tree entries on an unreduced projection in the Sum.inl binder ascriptions, so simp cannot retrieve them — a follow-up restates those binders to restore the one-liners. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * fix(trace): restore the FreeMonoid-backed TraceList design Return `TraceList P` to its original definition as `FreeMonoid (Idx P)` (reducible, as a type synonym instance resolution must see through), deleting the migration's hand-rolled Monoid instance and `TraceList.lift` in favor of Mathlib's instances and `FreeMonoid.lift`, and restoring the `List.countP` definition of `occurrences` together with the original proofs. The free-monoid universal property is available to traces again, and the module docstring's "definitionally `FreeMonoid (Idx P)`" claim is true once more. The migration's `getAt?` restatement and its cons-lemmas stay: they are a genuine improvement. The enabling attribute is one option-free local block: `FreeMonoid` and `PFunctor.Idx` at implicit_reducible — `event.fst` on `P.Idx` not being type-correct at implicit transparency was the single root cause behind the FreeMonoid retreat. Both migration `import all` lines are deleted: the Mathlib files involved are `@[expose] public section`, so the plain public import already provides the needed bodies. Downstream, the Cursor occurrence-counting proofs return to main's text. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * fix(dynamical,itree): restore Simulation statements and interpreter simp keys Restore the original letI-based `Coalg.Hom p.Obj S₁ S₂'` statements of isSimulation_graph_coalgHom and behavior_coalgHom — the migration's fully explicit `@Coalg.Hom ... D₁.coalg D₂.coalg` spelling changed the public API for what turns out to be no remaining reason. Restate the Sum.inl/Sum.inr binders of the interpState / interpExcept computation rules with explicit component types instead of ascriptions through `(StateE σ + E).A`. The ascribed form froze an unreduced projection into the lemmas' discrimination-tree keys, so simp could never retrieve them — the root cause of the migration's manual rw chains in the interpreter examples. With the keys fixed, the `simp [stateProgram]` style one-liners in PolyFunTest return (two now close goals main still needed congr for). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * chore(pfunctor): deduplicate instance bodies; promote Lens.ext_heq The HAdd/Add instances for PFunctor delegate to `sum` again instead of duplicating its anonymous-constructor body — `sum` is an abbrev, so the instances behave identically while keeping one source of truth for `+`. `Lens.ext_heq`, introduced privately during the migration for the cartesian-closed round-trip proof, moves to Lens/Basic.lean as public API next to `Lens.ext`: heterogeneous extensionality is the natural statement whenever direction families only agree after rewriting along the position map. `exp_direction_components` stays private — it is specific to the exponential. `selfMonomial` keeps the migration's explicit structure literal, now with a docstring explaining why: the mate-object equations in the dynamical layers rewrite through this carrier at implicit transparency, where the literal's projections reduce and the `monomial` spelling does not. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * docs: transparency-attribute policy for Lean 4.33 Add a Transparency Attributes section to CONTRIBUTING.md's module-scopes chapter — when to use implicit_reducible (the standard 4.33 fix), instance_reducible, reducible (thin wrappers only), the option-free `attribute [local implicit_reducible]` form for imported declarations, and the justification-comment requirement for the single sanctioned allowUnsafeReducibility site — and a matching symptom-to-fix table in docs/wiki/gotchas.md covering the 4.33 transparency ladder. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * fix: reconcile rebased transparency work with main's per-file overrides Post-rebase fallout from replaying the implicit_reducible series onto the squashed PR #128, which had independently adopted per-file transparency overrides in place of the dropped global PFunctor.Obj attribute: - deduplicate merged attribute blocks that listed the same constant twice in one file (Free/Cursor.lean, UC/OpenProcess.lean) - add per-file 'attribute [local implicit_reducible] PFunctor.Obj' where restored original proofs previously leaned on the global override (Dynamical/Trajectory.lean, ITree/Unfold.lean, PatternRunsOnMatter/ Module.lean) - drop main's explicit 'map' body in SubstMonoid/Extension.lean instMonad so the restored pre-migration LawfulMonad proofs typecheck again - drop trailing tactics main's migration proofs needed but the restored attribute configuration closes earlier (Display/Free.lean, FreeCursorExamples.lean); keep main's head_extend text in Cofree.lean Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5 <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
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.
Summary
Validation