Conversation
crei
force-pushed
the
pr/transforms-tapes
branch
3 times, most recently
from
September 11, 2026 09:28
e1c93f6 to
ea033d9
Compare
Introduce the word-level interface through which control-flow combinators use machines, the space-accounting lemmas it rests on, and sequential composition as the first non-trivial combinator over it. * `Plumbing/TransformsTapes.lean`: `tapeOfList` (a tape holding exactly a word), `wordsCfg` (a configuration whose tapes hold given words), `TransformsTapes` (started on word-holding tapes, halt in the normal form `wordsCfg input none ws' out` with the new words related to the old by a postcondition, within given time/space), its `.imp` weakening, and `exists_transformsTapes_nop` as the inhabiting example. * `Plumbing/Sequential.lean`: `transformsTapes_seq`, running one transformer then another. The halting configuration of the first is a valid starting configuration for the second, so the two chain by rewriting with the normal-form equality. * `TapeLemmas.lean`: add the visited-set / space-usage lemmas the interface needs (`visitedByTapeHead_add`, `spaceUsed_add_le`, `spaceUsed_eq_of_workTapePos`, `exists_visitedByTapeHead_eq_Icc`, `spaceUsed_le_of_one_moving`, ...). * `Configuration.lean`: add the state-remap embeddings `Cfg.mapState` and `Cfg.withState`, used to place a sub-machine's configurations into a larger one. * `Deterministic.lean`: add `runFrom_eq_of_halt` and `exists_minimal_halting_time`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
crei
force-pushed
the
pr/transforms-tapes
branch
from
September 11, 2026 09:46
ea033d9 to
def5ea2
Compare
The step where we inject `TEST_ARGS` into the `GITHUB_ENV` environment variable was a workaround for a bug in `lean-action`, in which it ignored its own `test-args` input. That fix landed in leanprover/lean-action#153 and is included in `lean-action` since v1.6.0, which is what we pick up here on the CSLib side.
…ver#747) Fixes the definition of consistency to have realizability as a precondition.
Add Xueying Qin as reviewer.
We show that various list operations are preserved under monad morphisms, and that FreeM.liftM is. Note that [PolyFun already has the _bundled_ version](https://github.com/Verified-zkEVM/PolyFun/blob/main/PolyFun/Control/Monad/Hom.lean), but having the unbundled version now does not preclude adding the bundled version later. --------- Co-authored-by: Fabrizio Montesi <fm@fabriziomontesi.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
…ence to commutation (leanprover#880) This PR generalises many results from confluent to commuting relations, and obtains the classical case as a specialisation. We add `HJoin` and `MHJoin` — heterogenous versions of `Join` and `MJoin` — and associated API for them and related relational constructions. NB: the theorem `confluent_equivalents` is now public, and the `TFAE` has been extended with certain other properties which generalise better to the heterogenous case. --------- Co-authored-by: twwar <tom.waring@unimelb.edu.au>
Adds notation for CCS processes and updates the vending machine example to use it.
Bump `mathlib` dependency to [87befc8](leanprover-community/mathlib4@87befc8): doc(DerivNotation): remove stale "future work" note (#43662) (2026-09-13) Previously at: [950d270](leanprover-community/mathlib4@950d270): feat(TacticAnalysis): suggest `rwa` for `rw` followed by `assumption` (#42732) (2026-09-04) --- This is an automated dependency bump to the latest commit this project is known to build against (its **last-known-good** commit). `lake build` was run against the new commit before this PR was opened and succeeded, so it should be mergeable as-is. Only `lake build` is checked, though — if your own CI does more (linting, failing on warnings, downstream tests, …), run it on this PR before merging. _This PR was last updated on 2026-09-13 by [this workflow run](https://github.com/leanprover/cslib/actions/runs/34779898369). It is an automated bump using [downstream-reports/open-bump-pr](https://github.com/leanprover-community/downstream-reports)._ Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
…configurations reachable in bounded space (leanprover#772) Proves an upper bound on the number of configurations reachable in bounded space on a multi-tape TM. The proof introduces the concept of `Storage`, the projection of `Cfg` that only contain the state and the work tapes. It shows that if the TM uses at most `s` space, there is an injection to a structure that only uses `[-s, s]` to index the tape. --------- Co-authored-by: Fabrizio Montesi <famontesi@gmail.com>
…s is computable in constant time and space (leanprover#854) This is a starting point of a Turing machine combinator library, it adds one of the leaves: Any function that is constant with finitely many exceptions is computable in constant time and zero space, relative to any encoding. The same holds for any function with a finite domain. This result captures many functions we want to compose later or with a combinator library: Any function on tuples of `Bool`, for example and "equality comparison with a constant". Together with a "fold" and "composition" combinators, this already allows us to evaluate CNFs or compute `Nat.succ` on binary encoded numbers.
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com> Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Alexandre Rademaker <arademaker@gmail.com> Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Fabrizio Montesi <famontesi@gmail.com> Co-authored-by: downstream-lean4[bot] <296232862+downstream-lean4[bot]@users.noreply.github.com> Co-authored-by: downstream-lean4[bot] <downstream-lean4[bot]@users.noreply.github.com>
Add `.github/dependabot.yml` covering the two dependency sources CI actually has. Adding this will enable automatically created PRs if updates (checked weekly) are available, coming from two sources: - GitHub Actions - pip. Look only for minor and patch bumps. (Major versions are excluded, for now.) Related to leanprover#894, which introduces the requirements file the pip entry watches. But mechanically, either one can merge first.
Replace the bare `pip install zulip` calls with a pinned `.github/requirements.txt`. This is pretty small on its own (effectively a no-op), but pinning a version increases reproducibility and helps track issues upstream, should they arise. This also gives Dependabot something to watch, once we've set that up.
Adds a workflow that runs actionlint over the `.github/workflows` directory whenever those files change. actionlint checks expression types (used in the little GitHub Action DSL), undefined step/output references and needs/if conditions, and runs shellcheck over every `run:` shell block and [pyflakes](https://github.com/PyCQA/pyflakes) over `shell: python` chunks. To make sure that adding this workflow does not immediately break the build, I did a manual one-off run and found one thing, which is fixed here: an `echo | sed` pipeline that is now a parameter expansion.
…olating into script text (leanprover#889) Move the key into the step's `env:` block and reference it as a shell variable, matching how the step already receives its other values.
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
8 participants
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.
Introduce the word-level interface through which control-flow combinators will use machines, together with the space-accounting lemmas it rests on.
Plumbing/TransformsTapes.lean:tapeOfList(a tape holding exactly a word),wordsCfg(a configuration whose tapes hold given words),TransformsTapes(started on word-holding tapes, halt in a configuration of the same shape with the new words related to the old by a postcondition, within given time/space), its.impweakening, andexists_transformsTapes_nopas the inhabiting example.TapeLemmas.lean: add the visited-set / space-usage lemmas the interface needs (visitedByTapeHead_add,spaceUsed_add_le,spaceUsed_eq_of_workTapePos,exists_visitedByTapeHead_eq_Icc,spaceUsed_le_of_one_moving, ...); drop two unused lemmas.Configuration.lean: addCfg.mapState, the state-remap embedding used bymapState_wordsCfg.