refactor(control): retire the do-stated monad law helpers - #190
Merged
Merged
Conversation
dtumad
marked this pull request as draft
September 3, 2026 18:31
dtumad
marked this pull request as ready for review
September 3, 2026 18:31
Core's bind_assoc, bind_pure_comp, and bind_map_left close do-stated goals directly (the last two are themselves stated with do), so the Lean 4.29 workaround file has no remaining purpose. - PolyFun/Control/Lawful/Basic.lean deleted; PolyFun.lean regenerated; its four topNamespace nolint entries dropped. - Interaction/TwoParty/Compose.lean uses the core lemmas at every call site; the dependent-pair shape is a congrArg / pure_bind term. - PolyFunTest/Control/LawfulDo.lean pins that the core lemmas apply to do-stated goals by exact. - Docs: gotcha 8 rewritten, repo map and pfunctor page, alignment ledger row. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Nb4g3Vxgjhnhsca7BzAsFc
dtumad
force-pushed
the
lawful/retire-basic
branch
from
September 8, 2026 22:51
aa12458 to
b610dc6
Compare
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.
Two-party strategy composition now uses Lean’s standard
bind_assoc,bind_pure_comp,bind_map_left, andpure_bindlaws directly. The four duplicate helpers inPolyFun.Control.Lawful.Basicand that module’s imports are removed; the composition theorem statements and assumptions are preserved.Ordinary-import canaries exercise the law forms through the public composition module for an arbitrary lawful monad with independent universes. Documentation describes the verified upstream behavior, and Python bytecode caches are ignored. The generated umbrella and obsolete namespace-linter entries are updated.
Validation:
./scripts/validate.sh --lint --test --axioms, an external ordinary-import consumer, andgit diff --checkpassed on the updated main base. The axiom sweep checked 10,904 declarations across 281 modules with zero sorry or non-standard axiom taint. Explicit checks of the two changed composition proofs report onlypropextandQuot.sound.Review: checked the pinned core statements and the dependent-pair equality transport. No references to the removed module or helpers were found in the inspected VCVio and ArkLib source snapshots. Full downstream toolchain upgrades are outside this change.