Results about finite space and regular languages - #180
Draft
crei wants to merge 59 commits into
Draft
Conversation
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
…time and space consumption.
…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>
…make step function total.
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>
…dd generic ComputableInTimeAndSpace definition.
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
10 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.