feat: prove that regular languages are closed under Kleene star (leanprover#241) This patch proves that regular languages are closed under Kleene star. The proof technique is similar to the one used in PR leanprover#239 and re-uses much of the infrastructure introduce in that PR. --------- Co-authored-by: Chris Henson <chrishenson.net@gmail.com> chore: weekly lints for 2026-01-05 (leanprover#245) As identified by [this workflow](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Weekly.20linting.20log/near/566277830). feat: adding free reader monad API and minor edits to free writer and free cont (leanprover#247) This PR adds an API for the `Reader` monad represented as a free monad, to the list of existing free effects. Also made some minor changes to the `Writer` and `Cont` APIs in this same file chore: cleanup of `Cslib.Languages.LambdaCalculus.LocallyNameless.*` (leanprover#250) With the somewhat recent change to allow passing arbitrary expressions to `grind` and other improvements, some cleanup of locally nameless lambda calculus is possible. chore: add radar benchmark suite (leanprover#267) This PR adds the benchmark suite to cslib that radar has already been using for a while. It can also be run standalone following the instructions in `scripts/bench/README.md`. Radar will automatically switch to this suite once merged. There have been some small changes to bring the benchmark suite in line with the mathlib benchmark suite, but nothing that should affect the results. Revert to FreeM, but use extra type param Some progress on the example Dangers of using only pure ops experiments Simple example Simple example Developing array sort example Developing array sort example Vectors Vectors Made coercions work. Added custom cost structures Comment out mergesort.lean for now Comment out mergesort.lean for now Comment out mergesort.lean for now Comment out mergesort.lean for now Try removing #evals to check build remove #evals Model is a structure now Remove redundant TimeM interpretation in the beginning. The TimeM section suffices Cslib.Init imports Set up linear search example. Only theorem statements. Proofs come later extra space removed Let's tail-recursive linear search. It is still monadic Author and license stuff Another attempt at proofs Let's count pure oerations as well Let's count pure oerations as well Add missing public annotation to import in CSLib Address some review comments List linear search proofs were simpler Try Vector proofs by list induction Split the files Add copyright header Improve docs Circuit complexitygit add *! add copyright comment to CircuitProgs.lean Circuits with automatic IDs Eric's suggestion Done Circuits works Circuits works Organise: Fix stuff AddCommSemigroup is the right Cost structure AddCommSemigroup chore: upload lakeprof report (leanprover#272) This PR makes the bench suite upload the lakeprof report it collected while building cslib. The report will be accessible through the "Lakeprof report" button in radar when viewing a commit (as long as the benchmark run for the commit has completed successfully). feat: Adding some `CompRel` lemmas to Relation for symmetric closure support (leanprover#276) This PR adds some preliminary support for [`CompRel`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Comparable.html#CompRel) in `Relation.lean`, as it doesn't currently have a concrete notion of symmetric closure. In particular, we add: - Helper lemmas for symmetry relationships between `ReflGen`, `ReflTransGen`, and `CompRel` - A theorem showing `EqvGen r = ReflTransGen (CompRel r)`, bridging the gap between `Gen` structures. This should hopefully help with future development surrounding symmetric closures in `Relation.lean`. --------- Co-authored-by: Chris Henson <chrishenson.net@gmail.com> feat: add notion of finite execution for LTS (leanprover#258) This PR adds a notion of finite execution for LTS analogous to the infinite counterpart. --------- Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.com> feat: add time step counting for relations (leanprover#270) This PR adds `Reduction.relates{In,Within}Steps`, functions that communicate whether a relation forms a directed path of length (at most) `n` between two elements. Specifically, it includes: * Definitions of these functions * Theorems about reflexivity and transitivity * Theorems that track the growth of ancillary functions with respect to the relation These are a prerequisite to defining time bounds, perhaps for multiple models of computation, but in particular for Turing machines, see PR --------- Co-authored-by: Chris Henson <chrishenson.net@gmail.com> chore: add .claude to .gitignore (leanprover#282) This one-line PR adds `.claude` to the `.gitignore`. In the course of using tools from the Anthropic ecosystem, the user may want to add personalized permissions or scripts, which can appear in the `.claude` folder. Adding this to the `.gitignore` would make it easier to use these tools in this repository without accidentally committing a personalized setting. fix: address shellcheck warnings in create-adaptation-pr.sh (leanprover#203) Fixes leanprover#202 Addresses all shellcheck warnings in `scripts/create-adaptation-pr.sh`: - Quote variables to prevent globbing/word splitting ([SC2086](https://www.shellcheck.net/wiki/SC2086)) - Use `$(...)` instead of legacy backticks ([SC2006](https://www.shellcheck.net/wiki/SC2006)) - Add `-r` flag to `read` commands ([SC2162](https://www.shellcheck.net/wiki/SC2162)) Co-authored-by: Chris Henson <chrishenson.net@gmail.com> chore: bump toolchain to v4.27.0 (leanprover#287) Co-authored-by: Chris Henson <chrishenson.net@gmail.com> feat(CI): add shellcheck workflow for shell scripts (leanprover#229) Adds a CI workflow that runs shellcheck on shell scripts in `scripts/`. Related to leanprover#202. fix: prevent duplicate Zulip posts in nightly failure workflow (leanprover#290) This PR fixes a bug in the `report_failures_nightly-testing.yml` workflow where duplicate messages were being posted to Zulip for the same nightly date. The deduplication logic compared the first 160 characters of the message, but the GitHub Actions run ID appears within those characters. Different workflow runs have different IDs, so the comparison always failed and duplicates were posted. Now we extract and compare the nightly date and bump branch explicitly using regex, which correctly identifies duplicate messages. See https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Cslib.20bump.20branch.20reminders/near/569853848 for context. 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> fix: look for last bot message when deduplicating Zulip posts (leanprover#291) This PR improves the Zulip deduplication logic by fetching the last 20 messages and finding the most recent one from the bot, rather than just checking the single most recent message. This handles the case where human replies appear between bot messages, which would previously cause duplicates to be posted. Suggested by Chris Henson: https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Cslib.20bump.20branch.20reminders/near/569945200 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> chore: bump toolchain to v4.28.0-rc1 (leanprover#292) Co-authored-by: Chris Henson <chrishenson.net@gmail.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.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: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.com> fix: use sender narrow filter for Zulip deduplication (leanprover#295) This PR uses Zulip's sender narrow filter to fetch only bot messages directly, rather than fetching multiple messages and filtering client-side. This fixes the bug where leanprover#291 was finding the oldest bot message instead of the newest due to message ordering in the Zulip API response. Suggested by Bryan Gin-ge Chen: leanprover-community/mathlib4#34398 (comment) 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com> feat: syntactic contexts and congruence relations (leanprover#284) This PR introduces notions of (single hole) syntactic contexts (`HasContext`) and congruence relations (`Congruence`), along with the standard notation `c[t]` for 'fill the hole in the context `c` with term `t`'. The development of CCS is adapted accordingly and should hold for many other calculi. The idea actually comes from an ongoing development on the generalisation of sequent calculi and logics, but these require more concepts. Also, in the future, it might be interesting to study approaches similar to `HasContext` in semantics that use different kinds of contexts. The PR also scopes the `grind` annotations in CCS. chore: unpin the Mathlib revision (leanprover#293) See [this Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/.60lake.20update.60.20in.20CsLib/with/569849603). Instead of accumulating changes required for Mathlib compatibility in `nightly-testing`, we will more frequently run `lake update` and PR to the `main` branch. I plan for there to be a workflow to semi-automate these PRs. In the meantime `nightly-testing` will still report any issues and prompt me to make a PR manually. feat: Bisimilarity can be characterized through symmetric simulation relations (leanprover#273) In formalized proofs, the characterization of bisimilarity through symmetric simulations often is more convenient than the one through bisimulation relations. (The reason is that paper proofs about bisimulation often say “the converse case is analogous,” which is not possible in proof assistants. The background usually is that the witness simulation is symmetric or can easily be adapted to be symmetric, which can usually be handled conveniently in a proof assistant.) Being about alternative characterizations of bisimilarity notions, the PR also proposes to remove the `SWBisimilarity` relation and only see `SWBisimulation` as an alternative characterization mechanism for `WeakBisimilarity`. The thought behind this is that there usually are many ways of characterizing the same notion of equivalence. Especially the weak spectrum has rich aliasing of notions, e.g. with a range of different definitions all leading to the same branching bisimilarity relation. It seems impractical to grant each equivalent definition its own relation symbol. Also, some proofs are shortened a bit using `grind`. feat: add several definitions and theorems about reduction systems (leanprover#211) This PR adds some additional API to `ReductionSystem`. While it duplicates from the relation namespace, this seems like an acceptable tradeoff for unifying proofs that use the corresponding notation, and ultimately a user can still simplify to the underlying relation if they desire. (description added by Chris Henson) --------- Co-authored-by: Chris Henson <chrishenson.net@gmail.com> feat: prove that an omega-language is regular iff it is a finite union of omega-languages of a special form (leanprover#249) This PR proves that an ω-language is regular iff it is the finite union of ω-languages of the form `L * M^ω`, where all `L`s and `M`s are regular languages. In addition to being of independent interest, thiss result will also be used in proving that ω-regular languages are closed under complementation, where the complement of an ω-regular language will be given as a finite union of this form. As part of this PR, we prove the theorem `LTS.ωTr.flatten`, which says that an infinite sequence of finite executions of a LTS connecting an infinite sequence of intermediate states can be concatenated into an infinite execution of the LTS. We also use this theorem to simplify the proof of `loop_run_exists` in Loop.lean. --------- Co-authored-by: Fabrizio Montesi <famontesi@gmail.com> feat: prepare for proving the closure of omega-regular languages under complementation (leanprover#268) This PR lays some groundwork for proving the closure of omega-regular languages under complementation. The main result is `IsRegular.fin_cover_saturates_compl` in `OmegaRegularLanguage.lean`, which depends on the definition and theorems in `Saturation.lean`. In future work we will construct a right congruence of finite index on finite words so that the index type `I` in `IsRegular.fin_cover_saturates_compl` consists of pairs of equivalence classes of this congruence. feat: add linear logic tests/benchmark (leanprover#302) For all logics that are likely to be implemented, it would be interesting to have a test suite that not only demonstrates how the definitions of syntax and semantics work, but also serves a didactic purpose through concrete instantiations of the logic. In this PR, I suggest some initial tests for the linear logic already implemented in CSLib. In addition to tests for syntax and trivial equivalences, I present a proof of a linear logic theorem that I picked at random from https://arxiv.org/abs/1904.06850. From this PR onward, we can think about more systematic methods for constructing proof benchmarks. ``` @Article{Olarte_2019, title={The ILLTP Library for Intuitionistic Linear Logic}, volume={292}, ISSN={2075-2180}, url={http://dx.doi.org/10.4204/EPTCS.292.7}, DOI={10.4204/eptcs.292.7}, journal={Electronic Proceedings in Theoretical Computer Science}, publisher={Open Publishing Association}, author={Olarte, Carlos and de Paiva, Valeria and Pimentel, Elaine and Reis, Giselle}, year={2019}, month=apr, pages={118–132}} ``` chore: simplify the connection between `HasFresh` and `Infinite` (leanprover#303) This PR adds an instance directly showing that `HasFresh` implies `Infinite`. This replaces `HasFresh.not_of_finite` which triggered a linter and is now equivalent to just `not_finite`. `HasFresh.of_infinite` is also changed to an instance with a slightly more direct definition. feat: copilot instructions (leanprover#310) Add a first version of copilot instructions to support pre- and post-PR reviewing. See, e.g., [copilot cli](https://github.com/github/copilot-cli). chore: `lake update` for 2026-02-02 (leanprover#313) Addresses an instance removed in leanprover-community/mathlib4#32984. chore: migrate nightly-testing workflows to GitHub App (leanprover#314) This PR migrates the nightly-testing workflows from using `NIGHTLY_TESTING` token (from `leanprover-community-mathlib4-bot`) to the `mathlib-nightly-testing` GitHub App. Affected workflows: - `bump_toolchain_nightly-testing.yml` - `merge_main_into_nightly-testing.yml` - `report_failures_nightly-testing.yml` I have installed all the secrets and github app required. 🤖 Prepared with Claude Code feat(Foundations/Semantics/ReductionSystem): extend `ReductionSystem` (leanprover#304) - Add more definitions and theorems about reduction systems - Use namespace `ReductionSystem` - Add sections feat: TimeM is a LawfulMonad (leanprover#316) feat: TimeM is an instance of LawfulMonad This PR provides the code showing that TimeM is an instance of LawfulMonad refactor: Update TimeM to match the version in the whitepaper (leanprover#321) Most notably this removes the global `[simp]` attribute from `Bind.bind` and `Pure.pure`, which breaks monadic reasoning about all other monads. The changes here were discussed during review of the whitepaper. fix: do not redefine clog2 (leanprover#322) This already exists in mathlib Co-authored-by: Chris Henson <chrishenson.net@gmail.com> feat: Hennessy-Milner logic (leanprover#319) This PR adds Hennessy-Milner Logic (HML) in its general form (parameterised over any LTS). We have proven the correctness of denotational semantics and its key result (the Hennessy-Milner theorem, stating that theory equivalence coincides with bisimilarity). --------- Co-authored-by: Alexandre Rademaker <arademaker@gmail.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com> chore: `lake update` for 2026-02-06 (leanprover#326) Addresses a deprecation from leanprover-community/mathlib4#34428. chore: remove `ReductionSystem` (leanprover#320) See [this Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/unbundling.20.60ReductionSystem.60/with/572059244). This PR: - completely removes `ReductionSystem` - renames the `reduction_sys` attribute to `reduction` and moves it to `Cslib.Foundations.Data.Relation` - changes the notation for reduction to use the unbundled relation and reflexive transitive closure - adds a definition that was accidentally only present for `ReductionSystem` to `Cslib.Foundations.Data.Relation` Some more work could be done to bring the SKI modules in line with what we have in `Cslib.Foundations.Data.Relation`, but this should be done in a follow up PR. I have left a few TODO comments to open issues. feat(Computability): add Unlimited Register Machines (leanprover#299) This PR introduces Unlimited Register Machines (URMs) and extends `ReductionSystem` with general termination concepts. **Core definitions** (`Defs.lean`): - `Instr`: The four instruction types (Z, S, T, J) - `Program`: Lists of instructions - `Regs`: Register contents as `ℕ → ℕ` - `State`: Machine configuration (program counter + registers) **Basic lemmas** (`Basic.lean`): - Register read/write lemmas, state lemmas - Jump instruction predicates and bounded jump targets **Execution semantics** (`Execution.lean`): - `Step`/`Steps`: Single-step and multi-step execution - `stepRs`: ReductionSystem integration - `Halts`, `Diverges`, `HaltsWithResult`: Defined via `ReductionSystem.Terminates`/`Diverges` - `eval`: Evaluation as a partial function - `ProgramEquiv`: Program equivalence with `Setoid` instance - Notation: `p ↓ inputs`, `p ↑ inputs`, `p ↓ inputs ≫ result`, `s ⭢ᵉ s'`, `s ↠ᵉ s'` **Computability** (`Computable.lean`): - `Computes`, `Computable`: URM-computability definitions **Straight-line programs** (`StraightLine.lean`): - `IsStraightLine`, `straight_line_halts` **Standard form** (`StandardForm.lean`): - `IsStandardForm`, `toStandardForm`, equivalence and idempotence theorems - `Deterministic` class: each term has at most one successor - `Terminates(Halted, t)`: term can reach a halted state - `Diverges(Halted, t)`: term cannot reach any halted state - `Deterministic.unique_halted`: uniqueness of reachable halted states - `Trapped`: state cannot reach terminated state (corresponds to `Diverges`) - `Functional`: at most one successor regardless of label (corresponds to `Deterministic`) - `toReductionSystem`: convert LTS to ReductionSystem by forgetting labels - Equivalence theorems: `MayTerminate ↔ Terminates`, `Trapped ↔ Diverges` - 0-indexed registers (Lean/Mathlib convention) - Functional register representation (`Regs := ℕ → ℕ`) - Relational semantics following Mathlib's Turing machine style - URM `Halts`/`Diverges` defined via general `ReductionSystem` concepts --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com> feat: An Alternative Definition of the Locally Closed Term of Locally Nameless LC Using `LcAt` (leanprover#336) In [A. Chargueraud, The Locally Nameless Representation](https://chargueraud.org/research/2009/ln/main.pdf), which is the primary reference of implementation, several different definitions of “locally closed” are proposed. One of them is using "lc_at". ``` lc_at 0 M ↔ M.LC ``` This is somewhat useful in proving strong normalizing property and maybe other theorems related to locally closed terms. Also it is straightforward to defining an algorithm later to decide whether certain term is locally closed on not. --------- Co-authored-by: Chris Henson <chrishenson.net@gmail.com> feat: define BuchiCongruence and prove that it is a right congruence of finite index (leanprover#278) This PR defines the notion of a "right congruence", which is an equivalence relation between finite words that is preserved by concatenation on the right, and proves its basic properties: - There is a natural deterministic automaton corresponding to each right congruence whose states are the equivalence classes of the congruence and whose transitions correspond to concatenation on the right of the input symbols. - If a right congruence is of finite index, then each of its equivalence classes is a regular language. Furthermore, this PR also defines a special type of right congruences introduced by J.R. Buchi and proves that it is of finite index if the underlying Buchi automaton is finite-state. The purpose of Buchi congruence is to prove the closure of ω-regular languages under complementation. But more work will be needed before we reach that goal. The old PR leanprover#265 has been absorbed into this PR. --------- Co-authored-by: Fabrizio Montesi <famontesi@gmail.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com> chore: bump toolchain to v4.28.0 (leanprover#339) chore: use authenticated gh api in nightly bump workflow (leanprover#341) This PR replaces unauthenticated `curl` calls to the GitHub API with `gh api` in the nightly bump workflow. The `gh api` command automatically uses the app token already generated in the workflow, avoiding transient failures from the unauthenticated rate limit (60 req/hour). See [this mathlib4-nightly-testing failure](https://github.com/leanprover-community/mathlib4-nightly-testing/actions/runs/22084056453/job/63814863096) for an example of the problem: the API returned a rate-limit error object instead of the expected array, and `jq` crashed trying to index it. Corresponding PRs: - leanprover-community/mathlib4#35427 - leanprover-community/batteries#1678 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> chore: create GitHub releases from version tags (leanprover#340) This PR adds a GitHub Actions workflow that automatically creates GitHub releases when version tags are pushed, mirroring the existing functionality in batteries. See also leanprover-community/mathlib4#35425 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> chore: weekly linting for 2026-02-02 (leanprover#312) As identified by [this workflow](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Weekly.20linting.20log/near/571350271). chore(CombinatoryLogic): use Relation infrastructure (leanprover#342) ... plus some small golfing & style. closes leanprover#333 closes leanprover#334 closes leanprover#335 --------- Co-authored-by: twwar <tom.waring@unimelb.edu.au> pull main branch Sorry out proofs for now The proof of insertOrd_complexity_upper_bound is AI slop. But it suggests some useful API lemmas The proof of insertOrd_complexity_upper_bound is AI slop. But it suggests some useful API lemmas Extract nice lemmas Extract nice lemmas Insertion Sort done Remove #checks Clean up merge sort Clean up merge sort More work to be done More work to be done Simplify this PR. Use AddCommMonoid for now feat(CombinatoryLogic): add Church-encoded list infrastructure for SKI terms (leanprover#331) Adds Church-encoded list operations (nil, cons, head, tail) for SKI combinatory logic, along with conversions to/from Church numerals and helper combinators (PrependZero, SuccHead). Head is defined via a general HeadD that takes an arbitrary default value; Head specializes to default 0. This is a stepping stone toward proving the equivalence of SKI combinatory logic with Mathlib's Turing machines. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> chore: bump toolchain to v4.29.0-rc1 (leanprover#344) 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: 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: Ching-Tsun Chou <chingtsun.chou@gmail.com> Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Alexandre Rademaker <arademaker@gmail.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: Claude Opus 4.6 <noreply@anthropic.com> chore(CombinatoryLogic): miscellaneous grind golfing (leanprover#345) Low priority --------- Co-authored-by: twwar <tom.waring@unimelb.edu.au> Co-authored-by: Chris Henson <chrishenson.net@gmail.com> feat: deterministic relations (leanprover#353) ... aka `Relator.RightUnique`. The proof pattern of deterministic -> confluent in `URM/Execution` seemed common enough to deserve generalisation. If appropriate this predicate could get a cslib-specific abbrev to improve discoverability. --------- Co-authored-by: twwar <tom.waring@unimelb.edu.au> Co-authored-by: Chris Henson <chrishenson.net@gmail.com> doc: update CONTRIBUTING.md (leanprover#356) Updated to include the `--module` flag for `mk_all` and remove the outdated `shake` description pending this being re-enabled in CI. ci: allow ci prefix in PR titles (leanprover#355) ...as confirmed for this very PR. fix: specify `-X GET` in `gh api` call (leanprover#354) This workflow has been failing since leanprover#341, as the `-f per_page=1` is incorrectly interpreted without the `GET` HTTP verb. I have manually triggered a run from this branch to ensure this is working. feat: prove the Ramsey theorem for infinite graphs (leanprover#281) This PR proves the Ramsey theorem for infinite graphs, which will be needed in Buchi's proof that omega-regular languages are closed under complementation. Ideally, this result should be in mathlib, but it is not and I don't know when it will be: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Infinite.20Ramsey.20theory/with/568507228 So I now prove what I will need. Once mathlib has the desired result, this proof can be deprecated. --------- Co-authored-by: Fabrizio Montesi <famontesi@gmail.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com> Toolchain update Remove graph files remove extraneous TimeM.lean Restore the OG TimeM under Lean subfolder Remove changes in Free/Effects.lean Check toplevel file Changes to import paths of TimeM Only mergeSort_complexity remains Build okay Done Lint passes locally Ran lake exe mk_all --module Remove Dead Code Fix docstring of mergeNaive Use the ML definition-by-match-expression formal for defining evalQuery and cost everywhere Fix Indent in Prog Fix line breaks Fix line breaks Fix line breaks OrderedInsert fixed All ready All ready Take the example suggestion. But this kinda defeats the point of that example feat: add background and orientation information on how to contribute to CSLib (leanprover#358) This PR adds more references and details on the structure of CSLib. feat: generalize `TimeM` to arbitrary cost types providing `AddZero` (leanprover#357) This also fixes some insufficiently-general `simp` lemmas about `seqLeft`, `seqRight`, and `seq`. Discussed in [#CSLib > Lightweight algorithms in CSLib :Cslib#275 @ 💬](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Lightweight.20algorithms.20in.20CSLib.20.3ACslib.23275/near/574964064); whatever we end up doing with leanprover#275, this change is a natural generalization and can be used to experiment with cleanups in leanprover#275. If we ultimately converge on dropping `TimeM`, then we can drop this generalization along with the rest of `TimeM` at that time. Some indentation rule fixes Round one nlinarith not needed. linarith is enough insertOrd_complexity_upper_bound has a shorter proof use simp only's Golf some mergeSort proofs with grind Golf some mergeSort proofs with grind fix naming in test files Fix names Linebreak acsSortOps Instances improved. API lemmas for sortOps moved to sortops file remove Id.run and pure and bind from simp lemma sets Fix docblame error TimeM abbrev added. Prog.time untouched One sorry remains Apparently induction syntax is better sorry free again sorry free again sorry free again sorry free again fix: generalize time_tick and ret_tick (leanprover#362) This was a mistake in my leanprover#357 docstring Docstring Some review fixes Other review fixes Other review fixes Manual inlines rfls rfls rfls remove some instance names fix correctness as a single theorem correctness as a single theorem fewer intros in insertOrd Unname instances Removed (m := Id) in favour of Id.run) Using Equiv instance for SortOpsCost with Nat pair Simplify Prog.bind_pure and Prog.pure_bind BEq can be better that decidableEq for equality BEq can be better that decidableEq for equality simps simps simps Remove mergeNaive Fix instruction docs made mergeSortNaive private fix doc typo naming Fix induction proofs and add missing pures substantially golf proofs chore: golf proofs about merge (leanprover#323) The lemmas this golfs are now unused, and could also be deleted. golf more golf more mergeSortNaive_Perm mergeSort_Perm mergeSort_Perm golf further generalize to total partial orders, to allow stability claims fix whitespace, use notation whitespace and docstrings . in docstrings generalize theorems Deduplicate proofs Use SortOpsNat with only cmpLE for mergeSort Use SortOpsCmp with only cmpLE for mergeSort Fix line lengths in linear search insertOrd module docstring insertionSort module docstring mergeSort module docstring mergeSort module docstring linear search docstring linear search docstring Fix comments fix style in tests Universe generalizations deduplicate example code style tweaks and typo further deduplicate tests simp in examples

	-- TODO: `SKI.redexFree_iff` and related theorems should use `Relation.Normal`
	/-- A term is redex free iff it has no one-step reductions. -/

SKI.redexFree_iff and related theorems should use Relation.Normal #335

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

`SKI.redexFree_iff` and related theorems should use `Relation.Normal` #335