feat(tocslib): stage the free-monad API, loop transport, and order bridge - #185
Draft
dtumad wants to merge 1 commit into
Draft
feat(tocslib): stage the free-monad API, loop transport, and order bridge#185dtumad wants to merge 1 commit into
dtumad wants to merge 1 commit into
Conversation
…idge
Make `ToCslib` the lowest production layer under PolyFun and stage there what
PolyFun will upstream, written so that each upstream pull request is a move:
- `Data/PFunctor/Free/Basic.lean`: an opt-in case principle in the
`(lift a).bind cont` simp normal form, the functor equations `map_pure` /
`map_bind` with their constructor spellings, `bind_eq`, the catamorphism
`foldFreeM` with its universal property, handler fusion `liftM_comp`, the
identity fold `liftM_lift_eq_self`, and naturality `map_liftM` along any
`pure`/`bind`-preserving function; lemmas duplicating cslib#716 are marked;
- `Data/PFunctor/Free/Loops.lean`: interpretation commutes with `forIn'`,
`forIn`, `forM`, `foldlM`, `mapM`, and `PureForIn` containers;
- `Control/Monad/HomTransport.lean`: transport of the same loop combinators
along a function preserving `pure` and `bind`, in hypothesis form so that a
bundled monad homomorphism and cslib's in-flight `IsMonadHom` (cslib#856)
instantiate the same lemmas;
- `Control/ForIn.lean`: `PureForIn` / `PureForIn'` / `LawfulMemForInId`
instances for `Option` and `Vector`, absent from core;
- `Order/LeanOrder.lean`: Mathlib's `CompleteLattice` as core's
`Lean.Order.CompleteLattice`, low priority and definitionally agreeing with
core's own `Prop` and function-space instances.
`PolyFun/PFunctor/Free/Basic.lean` now imports the staged module and drops its
local copies (`map_pure`, `map_liftBind`, `map_lift_bind`, `bind_map_right`,
`map_bind`, `monad_bind_def`, `liftM_lift_eq_self`, `liftM_comp`); the
bundled `liftM_natural` is a corollary of `map_liftM`, and the eleven
`bind_map_right` and five `monad_bind_def` call sites use the staged names.
Infrastructure: `scripts/update-lib.sh` takes a library name and generates
`ToCslib.lean` like `PolyFun.lean`; `scripts/check-imports.sh` checks both
umbrellas; `scripts/check-modules.sh` scans `ToCslib` and enforces the
`Std.Do` quarantine in two tiers (definitions for the program-logic kernel,
tactics for the `Do/` bridge files, neither in `ToCslib`); the docs-integrity
checker covers `ToCslib`. AGENTS.md, the repo map, module-API, pfunctor,
generated-files, quickstart, and gotchas pages describe the layer, the staging
conventions, and the `simp`-index trap on reducible interfaces; the upstream
ledger lists each staged module with its target pull request.
Canaries: `PolyFunTest/ToCslib/{Free,HomTransport,LeanOrder}.lean`,
`PolyFunTest/Do/LeanOrder.lean` (definitional agreement with core's order
instances), and ordinary-import canaries in `PolyFunTest/ModuleAPI/`.
Validated with `./scripts/validate.sh --lint --test --axioms` (lint passes
for `PolyFun` and `ToCslib`; zero sorry/axiom taint).
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Nb4g3Vxgjhnhsca7BzAsFc
dtumad
marked this pull request as draft
September 3, 2026 17:23
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
Stacked on #184 (the v4.34.0-rc2 bump). Makes
ToCslibthe lowest production layer under PolyFun and stages there what PolyFun will upstream, written so that each upstream PR is a move rather than a rewrite:Data/PFunctor/Free/Basic.lean— opt-in case principleFreeM.casesin the(lift a).bind contsimp normal form,map_pure/map_bind(+ constructor spellings),bind_eq, the catamorphismfoldFreeMwithfoldFreeM_unique, handler fusionliftM_comp, the identity foldliftM_lift_eq_self, and naturalitymap_liftMalong anypure/bind-preserving function. Lemmas duplicating cslib#716 carry-- upstream: cslib#716.Data/PFunctor/Free/Loops.lean—liftMcommutes withforIn',forIn,forM,foldlM,mapM, andPureForIncontainers.Control/Monad/HomTransport.lean— transport of those loop combinators along a function preservingpureandbind, in hypothesis form so a bundledMonadHomand cslib's in-flightIsMonadHom(cslib#856) instantiate the same lemmas.Control/ForIn.lean—PureForIn/PureForIn'/LawfulMemForInIdforOptionandVector(absent from core).Order/LeanOrder.lean— MathlibCompleteLattice→ coreLean.Order.CompleteLattice, low priority, definitionally agreeing with core'sPropand function-space instances (pinned byPolyFunTest/Do/LeanOrder.lean).PolyFun/PFunctor/Free/Basic.leanimports the staged module and drops its local copies; call sites use the staged names (bind_map_right→map_bind,monad_bind_def→bind_eq).Ownership and layering
cslib + Mathlib + core Std.Internal → ToCslib → PolyFun.ToCslibnever imports PolyFun,Std.Do,Std.Internal.Do, orStd.Tactic.Do. Not stageable downstream: theliftBindnormal-form tax behind the sevenattribute [local implicit_reducible] PFunctor.FreeM.bindsites needs the attribute at the definition in cslib (Lean rejects global/scoped reducibility attributes on imported declarations); recorded in the ledger.Infrastructure
scripts/update-lib.sh [ToCslib]generates either umbrella;check-imports.shchecks both;check-modules.shscansToCsliband enforces theStd.Doquarantine in two tiers (definitions: program-logic kernel +PolyFunTest/Do/; tactics:Control/Do/,PFunctor/Free/Do.lean,PolyFunTest/Do/); docs-integrity coversToCslib.simplemmas overFreeMdo not fire onabbrevinterfaces because the discrimination tree reducescoinP.B atoBool), and the upstream ledger.Validation
./scripts/validate.sh --lint --test --axioms— lint passes forPolyFunandToCslib; 10941 declarations, zero sorry/axiom taintPolyFunTest/ToCslib/{Free,HomTransport,LeanOrder}.lean,PolyFunTest/Do/LeanOrder.lean,PolyFunTest/ModuleAPI/PFunctor.lean🤖 Generated with Claude Code
https://claude.ai/code/session_01Nb4g3Vxgjhnhsca7BzAsFc