Landau calculus - #181
Draft
crei wants to merge 61 commits into
Draft
Conversation
…eanprover#610) Adds new area maintainers for algorithms and logic, resp. @sorrachai and @arademaker. --------- Co-authored-by: Alexandre Rademaker <arademaker@gmail.com>
Some of the arguments in `Bisimulation` can be simplified by symmetry and use of API lemmas. --------- Co-authored-by: twwar <tom.waring@unimelb.edu.au>
A previous modification to CODEOWNERS had the unintended consequence that chenson2018 couldn't approve PRs to logic any longer, which is too restrictive until we get more logic maintainers.
Adds logical equivalence for modal logic, proving that it is a `Congruence` (for any modal logic, regardless of the class of models considered) and a `LogicalEquivalence` (for logic K, i.e., when considering the class of all models). The PR also renames `Proposition.neg` to `Proposition.not` and adds a useful lemma on `Proposition.iff`. Depends on leanprover#528. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
I forgot `declare_term_config_elab` generated these for Boolean options when writing this documentation.
Bump `mathlib` dependency to [8589236](leanprover-community/mathlib4@8589236): chore: move Data/Nat/Lattice to Order (#39990) (2026-06-09) Previously at: [d90090f](leanprover-community/mathlib4@d90090f): chore: bump toolchain to v4.31.0-rc2 (#40358) (2026-06-08) Closes leanprover#627 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/27253259444/artifacts/7526847935) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`8589236`) 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/27305770390)._ --------- Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
…er#477) ## Summary - Port `PFunctor.FreeM` from [VCV-io](https://github.com/dtumad/VCV-io) (`ToMathlib/PFunctor/Free.lean`) to cslib. - The free monad on a polynomial functor extends the W-type construction with an extra `pure` constructor, yielding a lawful monad that is free over `P : PFunctor`. ### Main definitions - `PFunctor.FreeM`: inductive type with `pure` and `roll` constructors - `FreeM.lift` / `FreeM.liftA`: lifting from the base polynomial functor - `Monad` and `LawfulMonad` instances - `FreeM.inductionOn` / `FreeM.construct`: propositional and dependent eliminators - `FreeM.mapM`: canonical interpretation into any target monad, with `simp` lemmas for `bind`, `map`, `seq`, etc. ### Notes - The `MonadHom`-related definitions (`mapMHom`, `mapMHom'`) from the original VCV-io source are omitted since cslib does not have `MonadHom` infrastructure. These can be added later if cslib gains monad homomorphism support. - File placed at `Cslib/Foundations/Data/PFunctor/FreeM.lean` as a foundation for future polynomial functor work. - Builds cleanly with no linter warnings. Posted by Cursor assistant (model: claude-4.6-opus-high-thinking) on behalf of the user (Quang Dao) with approval. Made with [Cursor](https://cursor.com) --------- Co-authored-by: Cursor <cursoragent@cursor.com>
Bump `mathlib` dependency to [73b2611](leanprover-community/mathlib4@73b2611): chore(Order/Defs/Unbundled): deprecate `def Symmetric` in favor of `class Std.Symm` (#38092) (2026-06-10) Previously at: [8589236](leanprover-community/mathlib4@8589236): chore: move Data/Nat/Lattice to Order (#39990) (2026-06-09) Closes leanprover#639 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/27427486135/artifacts/7596930467) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`73b2611`) 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/27442101619)._ --------- 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 was already at ~1000 lines and growing. I've split this without making any other changes with one exception: the `CoeDep` instances previously specific to `dom` and `cod` are generalized as this makes imports less awkward (and is also useful for another PR I will make soon).
Follow-up to cslib#613 adding API & simplifying arguments related to trace equivalence. --- - [ ] depends on: cslib#613 --------- Co-authored-by: twwar <tom.waring@unimelb.edu.au>
…e systems (leanprover#536) We amend the definitions of `IsClassical` and `IsIntuitionistic` in `Logics.Propositional.Defs` to refer to an inference system, rather than a theory. This makes inhabitation of these typeclasses independent of the chosen axiomatisation, so, for instance, we can define `instance instIsIntuitionisticOfIsClassical [IsClassical Atom T] : IsIntuitionistic Atom T`, which before was impossible. We describe some common alternative axiom systems for classical logic, and introduce some derived rules. --------- Co-authored-by: twwar <tom.waring@unimelb.edu.au>
…hen there is no fault (leanprover#619) This PR presents an asynchronous distributed consensus algorithm and proves that it achieves consensus when there is no fault. This result is not needed for proving the FLP impossibility result, but is included to show that the notion of an algorithm defined in `Algorithm.lean` is not vacuous, in the sense that it does allow a working asynchronous consensus algorithm when there is no fault. Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Impossibility.20of.20distributed.20consensus/with/592462001
…ise TM tapes to arbitrary universes, fix EpsilonNA, and introduce their single-accept transformation (leanprover#625) This PR: - Fixes a bug in the formulation of EpsilonNA by adopting a new saturated multistep transition LTS.SMTr for LTS, which correctly invokes tau-closure for empty strings. - Introduces a `mapLabel` operation for LTS and its properties. - Introduces a new transformation `toSingleAccept` for EpsilonNA.FinAcc, which transforms the automaton into an equivalent one that has a single accept state with no outgoing transitions. - Generalises TM tapes/symbols to arbitrary universes. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Chris Henson <ch3473@drexel.edu>
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: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com> Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.com> Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Alexandre Rademaker <arademaker@gmail.com> Co-authored-by: Fabrizio Montesi <famontesi@gmail.com>
…nprover#666) - New theorem `subst_intro_openRec` - `subst_intro` no longer needs `LC t` - `subst_intro` no longer needs `subst_fresh` - `subst_intro` new proof based on `subst_intro_openRec` - Updated `preservation_open` in STLC to take advantage of the weaker precondition Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
…r#667) `step_subst_cong_l` is the more general version --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
…_openRec_to_subst (leanprover#668) - Renamed the general `close_open_to_subst` (with explicit `k`) to `close_openRec_to_subst` - Added new `close_open_to_subst` that specializes to k = 0 using the `^*` / `^` notation: `(m ^* x) ^ n = m [x := n]` - Added `@[scoped grind =]` to both lemmas for better automation support
A first pass at adding definitions corresponding to the concept of having some property of a (homogeneous) relation over a set restriction, as discussed in [this thread](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/unbundled.20relations.20with.20restricted.20.28co.29domain/with/596236853). I also add lemmas `of_{cod,dom}` for convenience of working in the "constructive" case where we explicitly are given the relation as evidence of the (co)domain.
Bump `mathlib` dependency to [29af524](leanprover-community/mathlib4@29af524): chore: adaptation for batteries#1864 and batteries#1866 (#40821) (2026-06-21) Previously at: [360da6f](leanprover-community/mathlib4@360da6f): chore: bump toolchain to v4.32.0-rc1 (#40732) (2026-06-18) Closes leanprover#669 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/27909093828/artifacts/7776869620) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`29af524`) 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/27916674545)._ --------- Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
…ver#671) This is the first step towards the Standardization Theorem. Instead of the classic (and painful) Barendregt approach, I defined `Standard` reduction relying on `CBN` to find the head redex, which makes the proofs much nicer. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Adds a class for transducers and a first implementation based on `NA`.
…eanprover#682) Add @fmontesi to the "Authors" field of the header of this file.
…eanprover#686) Make sure this job is run only on the main cslib repo `leanprover/cslib'` and not on personal forks.
Bump `mathlib` dependency to [d52d26f](leanprover-community/mathlib4@d52d26f): chore(Logic/Relation): use `≤` to spell subrelation (#30526) (2026-07-01) Previously at: [29af524](leanprover-community/mathlib4@29af524): chore: adaptation for batteries#1864 and batteries#1866 (#40821) (2026-06-21) Closes leanprover#693 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/28530264197/artifacts/8015922463) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`d52d26f`) 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/28546158135)._ --------- Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
…rover#687) Fixes leanprover#631. My PR changes `HasSubstitution` notation from a plain trailing notation to a `syntax`/`macro_rules` form guarded by `noWs`. The substitution spelling remains`t[x := s]`; the spaced receiver spelling `t [x := s]` is migrated internally because it can capture brackets from following syntax. The new regression test checks that a structure field followed by an instance-binder field parses after importing `Cslib.Foundations.Syntax.HasSubstitution`. Co-authored-by: loafer-19 <loafer-19@users.noreply.github.com>
…eanprover#683) - Adds NTMs, defined as nondeterministic automata over `TrLabel` and the usual derived 'yields' relation (`Red`). - Instantiates Acceptor and Transducer for NTM. - Proves characterisation theorems that connect reductions on configurations to single- and multistep transitions of the underlying machine.
…rover#679) This PR proves the standardization theorem: if `M` beta-reduces to `N` in any number of steps, then `N` is reachable from `M` by a standard reduction. Builds on leanprover#671. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
If a term is locally closed at level `i` and `i ≤ j`, then it is also locally closed at level `j`. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
) - Redefine `multiApp` as right-recursive (`multiApp (app f a) as`) instead of left. - Switch several inductions to `List.reverseRecOn` for compatibility with the new recursion. - Add `listFullBeta_cons_r`/`listFullBeta_cons_l`/`multiApp_tail` helpers. - Update related proofs Fixes leanprover#706 --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
… fairness properties (leanprover#612) This PR contains some technical machineries for reasoning about diamond and fairness properties about the distributed algorithms introduced in leanprover#556: * `CanReachVia.lean` defines the notion of reachability via a subset of processes and proves some of its properties, including some diamond properties. * `FairScheduler.lean` contains a technical machinery for constructing fair executions, which will be used in formalizing some arguments which were either only hinted at or completely glossed over in Völzer's paper. Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Impossibility.20of.20distributed.20consensus/with/592462001
This tweak brings the bench suite more in line with the other repos. It should not affect functionality. Follow-up to leanprover#707.
…nprover#675) Addresses leanprover#638. Converts the global well-formed notation to a macro with a `noWs` whitespace guard. This explicitly prevents the postfix parser from greedily consuming the `✓` token across line breaks, resolving the syntax collision with TimeM's prefix tick notation when both modules are imported simultaneously. --------- Co-authored-by: Sean Stoneburner <litholight@gmail.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
… are regular (leanprover#720) Prove languages matching regular expressions are regular in IsRegular.regex. The proof uses existing theorems IsRegular.add, IsRegular.mul, and IsRegular.kstar. Prove remaining key ingredient that the language containing only the one character string is regular in IsRegular.char. Implemented collaboratively by Brooke Gill and Chi-Yun Hsu --------- Co-authored-by: Chi-Yun Hsu <chiyunhsu@users.noreply.github.com> Co-authored-by: Brooke Gill <96643991+brooke-gill@users.noreply.github.com>
… OmegaLanguage (leanprover#722) This PR proves some consequences of an empty alphabet type (denoted by `Symbol`) on Language and OmegaLanguage: (1) The only possible languages over an empty alphabet are {} and {[]}. (2) The only possible omega-language over an empty alphabet is {}. Furthermore, (1) enables the assumption `[Inhabited Symbol]` to be removed from the regular language closure properties `IsRegular.mul` and `IsRegular.kstar`. Now no closure property for regular languages has that assumption.
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: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Chris Henson <chrishenson.net@gmail.com> Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.com> Co-authored-by: Alexandre Rademaker <arademaker@gmail.com> Co-authored-by: Fabrizio Montesi <famontesi@gmail.com>
This PR adds README files to some of the main source code directories, covering explanations on principles and vision for CSLib that I've found myself repeating often in private and public conversations. --------- Co-authored-by: Fabrizio Montesi <fabrizio.montesi@pm.me>
Bump `mathlib` dependency to [d99d52c](leanprover-community/mathlib4@d99d52c): chore(Data): rename `setOf` to `Set.ofPred` (#41507) (2026-07-17) Previously at: [79d0395](leanprover-community/mathlib4@79d0395): chore: bump toolchain to v4.33.0-rc1 (#41779) (2026-07-16) Closes leanprover#727 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/29592162806/artifacts/8412435005) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`d99d52c`) 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/29610863999)._ --------- Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
Bump `mathlib` dependency to [169c26b](leanprover-community/mathlib4@169c26b): refactor: rename restrict to domRestrict (#25980) (2026-07-20) Previously at: [d99d52c](leanprover-community/mathlib4@d99d52c): chore(Data): rename `setOf` to `Set.ofPred` (#41507) (2026-07-17) Closes leanprover#732 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/29755881109/artifacts/8467297013) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`169c26b`) 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/29776447755)._ --------- Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
Adds an AUTHORS.md file explaining where copyright information can be found. --------- Co-authored-by: Fabrizio Montesi <fabrizio.montesi@pm.me>
…ver#730) Follow up to my version space PR. Adds Mitchell (1982) VS lattice and describes it's properties.
## Summary This PR fixes two small typos in the contribution guide. No semantic changes are intended.
This introduces a multi-tape Turing machine built in a similar way to the single-tape Turing machine in leanprover#269 I did not define how a function is computed by a multi-tape Turing machine. Instead I would like to focus on tuples of tapes being transformed by Turing machines. The idea is that this allows us to build complex Turing machines from basic building blocks by composition without the need to serialize and de-serialize all the time. Especially when talking about logarithmic space it will become necessary to define dedicated read-only input and write-only output tapes, but this is not yet included. I have not yet properly combined the common parts between single- and multi-tape Turing machines and am hoping for some ideas there. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
…ring machine (leanprover#745) The configuration should only contain data that influences the future behaviour of the Turing machine. While it is convenient to put the "output so far" in the configuration, it leads to more problems down the line, for example when the number of reachable configurations is determined or if we want to reason about loops in the configuration graph. NB: claude was used for a review of this PR and it did some refactoring.
There is a bug where the input position wraps around instead of getting properly clamped. This PR fixes it and ensures it can't happen again. --------- Co-authored-by: crei <crei.github@gmail.com>
…#719) Restates four reduction inclusions as namespaced relation inequalities. Pointwise use remains available through dot notation without duplicate wrapper theorems. This intentionally removes the old pointwise theorem names; there were no in-repository callers. Closes leanprover#696. [Zulip chat](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Scope.20of.20issue.20.23696/with/609971277) Codex was used for part of the code, I have reviewed all the changes done by it. --------- Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
…prover#740) Replace manual induction + grind with Xi.step_lc_r + grind --------- Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
Fixes the compound modal logics in the cube to include compound sentences instead of the union of sentences from the individual logics.
…nsensus (leanprover#718) This PR defines the notion of a fault-tolerant "pseudo-consensus" algorithm, which is central to Völzer's proof, and proves that every f-tolerant consensus algorithm is also a f-tolerant pseudo-consensus algorithm. This resilt is intuitively obvious and is stated without proof in Völzer's paper, but it turns out to require quite a bit of formal machinery (given in `FairSchedular.ean`) to prove. Zulip discussion: [#CSLib > Impossibility of distributed consensus](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Impossibility.20of.20distributed.20consensus/with/604941788) --------- Co-authored-by: Fabrizio Montesi <fm@fabriziomontesi.com>
This PR fixes various typos; same method as in leanprover-community/mathlib4#42232
… tolerate up to 1 fault (leanprover#755) This PR develops a theory of pseudo-consensus algorithms that can tolerate up to 1 fault, which is the core of Völzer's argument. The central notion is "non-uniformity": a state `s` is non-uniform iff for each boolean value `b`, there exists a process `p` such that there is an execution of the algorithm from `s` that ends up deciding on `b` without the participation of `p`. Then any algorithm that can tolerate up to 1 fault is proved to have two properties: (1) `nonUniform_inp`, which says that there must an initial non-uniform state. (2) `nonUniform_step`, which will be shown in the next PR to guarantee that any execution ending in a non-uniform state can be extended to a longer execution ending in a non-uniform state.
There is no reason for a `refine` to ever be terminal, it should be `exact`
Self explanotory. Additionally, this PR replaces `simpa using X` with `simp [X]` whenever possible. `simpa using` is not very good codestyle for various reasons, but at least in this case there is an easy replacement I did many cleanup PRs like this in mathlib recently and try to repeat the applicable ones here
A theorem shouldnt be tagged with simp, when the LHS can be simplified already, as it will never fire. There is only one exception which is not a false positive in this PR There are two solutions to this: Either untag the theorem or rewrite it as it would be after applying `simp`. I chose the second method, since there is a more general `simp` lemma avaiable. But of course happy to go the other way
Proves bounds on the number of configurations reachable in bounded space and proves complexity-class inclusions from that: DSPACE(s) \subseteq DTIME(n * 2^(O(s))
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
17 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.
No description provided.