Repository navigation
refactor(MultiTape): simulate machines through adapters - #32
Merged
Merged
Conversation
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
from
October 11, 2026 13:56
7653687 to
e2d87e8
Compare
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
2 times, most recently
from
October 13, 2026 20:29
29e1c83 to
6f1be88
Compare
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
from
October 13, 2026 22:10
6f1be88 to
222bcc1
Compare
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
from
October 13, 2026 22:23
222bcc1 to
068b321
Compare
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
from
October 13, 2026 22:31
068b321 to
61f42f4
Compare
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
from
October 14, 2026 13:28
61f42f4 to
3398d6f
Compare
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
from
October 14, 2026 16:00
3398d6f to
5f98b5a
Compare
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
5 times, most recently
from
October 14, 2026 16:48
9b297bb to
0d93c15
Compare
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
from
October 14, 2026 23:08
0d93c15 to
d4e415c
Compare
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
2 times, most recently
from
October 19, 2026 13:46
5a4c95c to
21b4e08
Compare
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
2 times, most recently
from
October 21, 2026 08:09
f33ed1b to
7c214a5
Compare
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
from
October 24, 2026 20:50
7c214a5 to
192855e
Compare
barni120400
changed the title
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
from
October 27, 2026 00:31
192855e to
c2d2b0d
Compare
barni120400
changed the base branch from
refactor/multitape-single-space-api
to
main
October 27, 2026 00:32
Without this change, the bench suite will crash as soon as any part of `lake build` tries to use a `cc` compiler or other tools required for compiling: Since we're overriding the toolchain directory lake uses to provide our own `lean` wrapper, we need to also provide the other tools lake expects (though without custom wrappers). I forgot to include this in leanprover#1165 even though the PR description mentions it, so here it is in a separate PR.
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
2 times, most recently
from
October 28, 2026 00:03
d0bfa21 to
9b2a4eb
Compare
Take care of the linter messages from the [weekly linting report](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Weekly.20linting.20log/near/634853991). Profiling results against `main` (mean of 5 runs): * `vm_ltsD_ltsND_not_bisim`: 41 ms → 43 ms (1029 → 1110 heartbeats) * `exists_full_synthesis_finset`: 70 ms → 50 ms (1289 → 1044 heartbeats) Profiled using `set_option trace.profiler true in`, heartbeats from `#count_heartbeats in`.
Bump `mathlib` dependency to [7ed8b09](leanprover-community/mathlib4@7ed8b09): feat(Topology/Algebra/InfiniteSum): Deprecate generalized ENNReal lemmas (#38193) (2026-10-27) Previously at: [625d891](leanprover-community/mathlib4@625d891): chore: bump toolchain to v4.36.0-rc1 (#44879) (2026-10-16) Closes leanprover#1171 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/40624676977/artifacts/12791455952) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`7ed8b09`) so you can reproduce and fix the incompatibility locally by checking out this branch. _Opened automatically by [downstream-reports/track-incompatibility](https://github.com/leanprover-community/downstream-reports) via [this workflow run](https://github.com/leanprover/cslib/actions/runs/40760536941)._ --------- Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
Bump `mathlib` dependency to [6955275](leanprover-community/mathlib4@6955275): chore(Data/Nat/Init): rename recursor arguments (#43848) (2026-10-27) Previously at: [9d581df](leanprover-community/mathlib4@9d581df): chore: bump toolchain to v4.36.0-rc2 (#45383) (2026-10-27) Closes leanprover#1174 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/40897888966/artifacts/12908103845) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`6955275`) so you can reproduce and fix the incompatibility locally by checking out this branch. _Opened automatically by [downstream-reports/track-incompatibility](https://github.com/leanprover-community/downstream-reports) via [this workflow run](https://github.com/leanprover/cslib/actions/runs/40946293027)._ --------- Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
This PR adds Thompson's construction, which converts regular expressions to ε-NAs: `RegularExpression.toEpsilonNA r : εNA.FinAcc r.State α`, with `RegularExpression.language_toEpsilonNA : language r.toEpsilonNA = r.matches'`. It then uses the construction to prove `IsRegular.char`, `IsRegular.mul`, `IsRegular.kstar` and `IsRegular.regex`. - `LTS/Simulation.lean`: `IsSimulationMap` (a map of states that sends transitions to transitions) and `IsSimulationMap.sim_trace` (it sends runs to runs), as a special case of simulation through `IsSimulationMap.isSimulation`. - `LTS/Union.lean`: the transitions and runs of `LTS.unionSum` (`unionSum_tr_inl_inl`, `unionSum_mTr_inl_iff`, …). - `LTS/HasTau.lean`: `τSTr_iff_exists_mTr_replicate` and `sMTr_iff_exists_mTr_filter` (a saturated run along a τ-free list is a plain run whose labels, once the τs are dropped, are that list). - `Languages/LanguageHom.lean`: `Language.Hom.reduceOption`, dropping the `none`s of a list as a language homomorphism. - `EpsilonNA/Basic.lean`: `εNA.FinAcc.mem_language_iff` (acceptance through plain runs) and `DecidableEqTau (Option α)`. - `EpsilonNA/ToSingleStartAccept.lean` (formerly `ToSingleAccept.lean`): `toSingleStartAccept` adds a start state without incoming transitions and an accept state without outgoing transitions, on `Bool ⊕ State`. It replaces `toSingleAccept`. - `NA/ToEpsilonNA.lean`: `NA.toEpsilonNA` through `LTS.mapHom` and `Language.Hom.reduceOption`, so its ε-transitions are self-loops, and `NA.FinAcc.toEpsilonNAFinAcc`, with the same language. - `EpsilonNA/ThompsonConstruction.lean`: the building blocks and their languages: - `zero`, `epsilon` and `char`; - `sum`, both automata side by side through `LTS.unionSum`; - `union := (sum a b).toSingleStartAccept`; - `concat`, with ε-transitions from the accepting states of the first automaton to the initial states of the second; - `star`, with a fresh hub state that is both initial and accepting. - `EpsilonNA/OfRegularExpression.lean`: `RegularExpression.State` (with a `Finite` instance), `toEpsilonNA` and `language_toEpsilonNA`. - `Languages/RegularLanguage.lean`: `IsRegular.iff_epsilon_nfa`. `IsRegular.char`, `IsRegular.mul` and `IsRegular.kstar` now come from the blocks above, without a case split on an empty alphabet, and `IsRegular.regex` from `language_toEpsilonNA`. Relation to existing code: CSLib has concatenation and star for ε-free `NA` (`NA.FinAcc.finConcat`, `NA.FinAcc.finLoop`), which need `[Inhabited Symbol]`. Thompson's construction is a specific ε-NA instead: every `r.toEpsilonNA` has one initial state and at most one accepting state, and each constructor of `r` adds at most two states. NFA-simulation algorithms work on exactly this automaton. Following the [discussion on Zulip](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Thompson.27s.20construction.2C.20.CE.B5-NA.20simulation.20and.20repeats.20in.20word/with/631341023), the union is built on `toSingleStartAccept`. This complements leanprover#887 (Kleene's algorithm, the converse direction), and leanprover#625 named the construction as a target. AI disclosure: written with Anthropic's Claude Code Opus 5.5, which drafted the Lean code under my direction. I chose the design, reviewed every definition and proof, and ran the checks. --------- Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Adds Basic Temporal Logic (BTL), following Blackburn et al.'s presentation of the basic temporal language. The PR also shows that BTL is essentially a thin layer to reason about frames with two operators that have inverse diagonals. AI disclosure: the BTL tests are largely AI generated. Depends on leanprover#863.
) This PR adds adapters, a common way to say that one machine runs another step by step. An adapter computes what the inner machine reads from the symbols under the outer heads, and turns each inner action into an outer one. A configuration map that agrees with the adapter then maps each step to a step (`Follows.step`), so it maps whole run paths (`Follows.stepHom`, `Follows.runningStepHom`). The plumbing is rebuilt on top of this. `extendTapes`, `outputToTape` and `inputFromTape` now use `adapt`. `seq` and `repeatUntilBlank` use the new `combine`, which runs two machines on the same tapes. Each construction loses its hand-written step lemmas, and the proofs that use them get shorter. I used Claude Code to help write the Lean code and this description. --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Co-authored-by: crei <crei.github@gmail.com>
barni120400
force-pushed
the
refactor/multitape-shared-simulations
branch
from
November 1, 2026 16:53
9cca087 to
ee99dd3
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
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.
Lets a machine follow another: it performs each transition of the inner machine through an adapter, which computes what the inner machine reads from the symbols under the outer heads (
HeadSymbols) and gives the outer action performing each inner action.Follows.runningStepHomandFollows.stepHomturn a configuration map that agrees with the adapter into a homomorphism of step relations, so it maps run paths.Defines
extendTapes,outputToTapeandinputFromTapeas the machine run through an adapter (MultiTapeTM.adapt), so their homomorphisms come fromfollows_adapt.seqandrepeatUntilBlankrelabel the actions of their inner machines withAction.mapStateand follow them by definition, andprependOutputHomfollows the machine itself. This replaces the step lemmas of each simulation and the deterministicstepHomandrunningStepHom, and shortens the proofs that use them.Depends on #31 (upstream leanprover#1122). Upstream: leanprover#1151.
Composed with Claude Code.