Constant space machines - #182
Draft
crei wants to merge 81 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>
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
Moves `.github/copilot-instructions.md` to `AGENTS.md` for better compatibility with AI development tools, and improves instructions to use our READMEs.
…#768) Some useful lemmas about how the tapes are modified during the execution of Turing machines, some lemmas about halting behaviour and some about space usage (partly just moved). This has been split out from leanprover#767
The current definition requires a global bound, which seems wrong. At least it is misleading as a reader of the documentation, perhaps it is intended and the documentation simply confused me.
This PR adds a first formalisation of Stateful Processes (for now without recursion), the textbook process calculus for reasoning about implementation of choreographies (syntactic descriptions of concurrent/distributed protocols). It includes both syntax and semantics of the calculus. The semantics is split into symbolic (e.g., `x := e; P` evolves to `P` by performing a transition with label `x := e`) and concrete (which equips programs with memory and thus the same action would update variable `x` with the value computed from `e`). One reason for this modularisation is future reuse: having a symbolic semantics is the basis to formulate extraction algorithms that infer the protocol executed by a network of process programs (choreography extraction in the literature). Another reason is that it is known to simplify some proofs of correctness for compilers from choreographies to processes, which is a future aim (see the README in `Mech`). Choreographic languages will be part of future PRs.
…ny non-zero number of faults is impossible (leanprover#765) This PR completes the proof that asynchronous distributed consensus tolerating any non-zero number of faults is impossible. The main theorem `OnePseudoConsensus.not_terminating` shows that every 1-tolerant pseudo-consensus algorithm has a fair execution which doesn't contain any fault but never reaches a consensus, which then implies that there cannot be a consensus algorithm that can tolerate even a single fault. This fair execution is constructed using the results obtained in `FLP/OnePseudoConsensus.lean` and the technical machinery developed in `FLP/FairScheduler.lean`. --------- Co-authored-by: Fabrizio Montesi <fm@fabriziomontesi.com>
This PR introduces typeclasses for logical operators (connectives and modalities) and refactors modal and propositional logics with appropriate instances to these. Co-authored-by: Thomas Waring <thomas.waring99@gmail.com> --------- Co-authored-by: twwar <tom.waring@unimelb.edu.au> Co-authored-by: Fabrizio Montesi <fabrizio.montesi@pm.me> Co-authored-by: Maximiliano Onofre Martínez <maxonomar@ciencias.unam.mx> Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com> Co-authored-by: lyj <sjtu5140809011@gmail.com> Co-authored-by: Garmelon <joscha@plugh.de> Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.com> Co-authored-by: VitaliPath <168389478+VitaliPath@users.noreply.github.com> Co-authored-by: Sean Stoneburner <litholight@gmail.com> Co-authored-by: Chi-Yun Hsu <116553435+chiyunhsu@users.noreply.github.com> Co-authored-by: Chi-Yun Hsu <chiyunhsu@users.noreply.github.com> Co-authored-by: Brooke Gill <96643991+brooke-gill@users.noreply.github.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: 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: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Alexandre Rademaker <arademaker@gmail.com> Co-authored-by: Felix Pernegger <s59fpern@uni-bonn.de>
This PR adds a first language for choreographies -- syntactic descriptions of communication protocols. It includes syntax, notation, and basic definitions. Future PRs will add semantics, further constructs (for more nondeterministic behaviours, etc.), and compilers to distributed implementations. Depends on leanprover#754
…eworks, with associated refactorings (leanprover#753) This PR introduces several improvements to the frameworks based on `InferenceSystem` and `Congruence`. 1. `InferenceSystem.Default⇓a` is now pretty-printed to `⇓a` (which is what users write). 2. Introduces a parametric congruence notation, since terms of the same type can have multiple congruences. Consequently, the same type can now also have multiple logical equivalences (which is important, since these may be parametric as we have, e.g., in modal and propositional logics). 3. Introduces a `DefaultCongruence` class to define the 'canonical' congruence for a type. 3. Separates classes for accessing congruence notation from that to prove that a congruence is lawful (`LawfulCongruence`). 4. Simplifies instantiating `Context` by making the term type parameter implicit. 5. Introduces the first examples of rewritings based on `LogicalEquivalence` in `CslibTests`. Both a manual proof based on contexts and one based on grind are provided. In the future, we should explore ways to plug such rewritings into Lean's and Mathlib's frameworks for congruences (perhaps by autogenerating lemmas and/or checks from inductive types). The PR also refactors CLL, HML, and Modal Logic to be in line with all these recent developments. This is a step towards the formulation of general patterns for modal logics (left to future work). Some tests to prevent future breakage are introduced as well. Depends on leanprover#607. --------- Co-authored-by: twwar <tom.waring@unimelb.edu.au> Co-authored-by: Fabrizio Montesi <fabrizio.montesi@pm.me> Co-authored-by: Maximiliano Onofre Martínez <maxonomar@ciencias.unam.mx> Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com> Co-authored-by: lyj <sjtu5140809011@gmail.com> Co-authored-by: Garmelon <joscha@plugh.de> Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.com> Co-authored-by: VitaliPath <168389478+VitaliPath@users.noreply.github.com> Co-authored-by: Sean Stoneburner <litholight@gmail.com> Co-authored-by: Chi-Yun Hsu <116553435+chiyunhsu@users.noreply.github.com> Co-authored-by: Chi-Yun Hsu <chiyunhsu@users.noreply.github.com> Co-authored-by: Brooke Gill <96643991+brooke-gill@users.noreply.github.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: 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: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Alexandre Rademaker <arademaker@gmail.com> Co-authored-by: Felix Pernegger <s59fpern@uni-bonn.de>
Bump `mathlib` dependency to [3069656](leanprover-community/mathlib4@3069656): feat: `haveI`/`letI` tactic linter (#41657) (2026-07-29) Previously at: [169c26b](leanprover-community/mathlib4@169c26b): refactor: rename restrict to domRestrict (#25980) (2026-07-20) Closes leanprover#756 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/30557581998/artifacts/8765719469) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`3069656`) 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/30579241439)._ --------- 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: Joscha <joscha@plugh.de>
Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
Introduces leftmost reduction `⭢ℓ`, a beta-step contracting the redex at position 0, together with normal forms, and proves the Leftmost Reduction Theorem: if a term beta-reduces to a normal form, the leftmost strategy reaches it too. The result falls out of standardization, following Copes (2018). Builds on top of leanprover#679 --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
…ver#735) - Drop `M.LC` param from `step_abs_close`, `redex_abs_close`, `redex_abs_cong`, `step_open_cong_r`, `step_subst_cong_r`, `steps_open_cong_r`, `steps_subst_cong_r`, `FullBeta.steps_open_cong_l_abs` - Add `@[scoped grind →]` to `FullEta.step_lc_l`
…#736) Reprove `SN.isNormalizable to move SN-related theorems adjacent Old proof use `Terminating.subtype_sn` New proof just `by_cases (∃ y, r x y)`
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>
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: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.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: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@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>
Bump `mathlib` dependency to [52ee81c](leanprover-community/mathlib4@52ee81c): chore: delete deprecated declarations/modules from January 2026 (#42075) (2026-08-11) Previously at: [de5ce8a](leanprover-community/mathlib4@de5ce8a): chore: bump toolchain to v4.34.0-rc1 (#42619) (2026-08-11) Closes leanprover#793 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/31506420845/artifacts/9107753650) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`52ee81c`) 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/31531956820)._ --------- 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 [77cbcbc](leanprover-community/mathlib4@77cbcbc): feat: make `TFAE.out` 1-indexed (#42663) (2026-08-12) Previously at: [52ee81c](leanprover-community/mathlib4@52ee81c): chore: delete deprecated declarations/modules from January 2026 (#42075) (2026-08-11) Closes leanprover#795 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/31611692361/artifacts/9148164906) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`77cbcbc`) 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/31636655080)._ --------- Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
…ce and capture-avoiding substitution) (leanprover#458) Named representation of untyped lambda calculus. # Basic.lean First, we define a naive variable renaming. Second, we define alpha-equivalence according to "Gabbay and Pitts, A New Approach to Abstract Syntax with Variable Binding, 2002". Third, we define capture-avoiding substitution. # Properties.lean AlphaEquiv.refl: reflexivity of alpha-equivalence AlphaEquiv.symm: symmetry of alpha-equivalence AlphaEquiv.trans: transitivity of alpha-equivalence Subst.relation_iff_function: the relational and functional definition of capture-avoiding substitution are equivalent, modulo alpha-equivalence subst.commutativity: commutativity of substitution, more commonly known as "substitution lemma (e.g. in Barendregt 1984)" --------- Co-authored-by: Chris Henson <chrishenson.net@gmail.com> Co-authored-by: Fabrizio Montesi <famontesi@gmail.com>
…of infinite sequences (leanprover#704) This PR formalizes some results in the following classic paper: Alpern, Bowen; Schneider, Fred B. (1985). "Defining liveness". Information Processing Letters. 21 (4): 181–185. To wit: * By viewing an infinite sequence as an infinite product, we define a topology on infinite sequences using the product topology. * We identify safety and liveness properties with closed and dense sets in this topology and justify these identifications. * We prove that every property is the intersection of a safety property and a liveness property and give explicit formulas for both. Zulip discussion: [#CSLib: PR reviews > leanprover#704: Topological characterization of safety and liveness](https://leanprover.zulipchat.com/#narrow/channel/605128-CSLib.3A-PR-reviews/topic/.23704.3A.20Topological.20characterization.20of.20safety.20and.20liveness/with/609302284) --------- Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
This PR formalises Milner's classical Vending Machine example for CCS and adds general utilities to LTS, bisimulation, and CCS that have been very useful in developing the example. One of the reasons to develop this is to test the new AI instructions in leanprover#763. Albeit all code is manually written, interacting with the AI to see where it got stuck has been very informative for finding missing utilities. Depends on leanprover#763. --------- Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
…ver#775) Proves that A^R = {w^R | w ∈ A} is regular if A is regular, i.e regular languages are closed under reversal. The proof takes the NFA for A and constructs a new NFA by swapping the accept and start states and reversing all the transition arrows. `Reverse.lean` defines the reversal of a `FinAcc` and proves that it accepts the reverse of the language accepted by the original automaton. The Language reversal is defined in mathlib. Added a theorem `IsRegular.reverse` in `RegularLanguage.lean` to prove that regular languages are closed under reversal. AI Usage : I wrote down all the theorem statements and initial proofs with minimal. I then used claude to rewrite proofs for style compliance. --------- Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Bump `mathlib` dependency to [29e0104](leanprover-community/mathlib4@29e0104): feat(Data/List): add TFAE lemmas for append and permutations (#41022) (2026-08-16) Previously at: [77cbcbc](leanprover-community/mathlib4@77cbcbc): feat: make `TFAE.out` 1-indexed (#42663) (2026-08-12) Closes leanprover#811 Failure log from the validation run: [download](https://github.com/leanprover-community/downstream-reports/actions/runs/31990754158/artifacts/9275474067) _(link expires after 1 year)_ --- This PR bumps `mathlib` to an identified incompatible (first-known-bad) commit (`29e0104`) 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/32063971301)._ --------- 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 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
19 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.