Landau calculus

.github/CODEOWNERS

@@ -12,6 +12,9 @@
 ### Area access
 # Each area maintainer has access to parts that pertain them. They get automatically asked for
 # reviewing new PRs that touch those areas.
-/Cslib/Languages/LambdaCalculus/ @chenson2018
+/Cslib/Algorithms/ @fmontesi @sorrachai @chenson2018
+/Cslib/Foundations/Logic/ @arademaker @fmontesi @chenson2018
+/Cslib/Logics/ @arademaker @fmontesi @chenson2018
+/Cslib/Languages/LambdaCalculus/ @chenson2018 @fmontesi
 /.github/workflows @kim-em @fmontesi @chenson2018
 /scripts @kim-em @fmontesi @chenson2018

.github/workflows/lake-update.yml

@@ -25,6 +25,7 @@ on:
 jobs:
   bump:
     runs-on: ubuntu-latest
+    if: github.repository == 'leanprover/cslib'
     steps:
       - name: Generate app token
         id: app-token
@@ -52,6 +53,7 @@ jobs:
 
   open-issue:
     runs-on: ubuntu-latest
+    if: github.repository == 'leanprover/cslib'
     permissions:
       issues: write
     steps:

.github/workflows/lean_action_ci.yml

@@ -22,10 +22,10 @@ jobs:
         with:
           build-args: "--wfail --iofail"
           test-args: "--wfail --iofail"
-      - name: "lake exe mk_all --check --module"
+      - name: "lake exe mk_all --check"
         run: |
           set -e
-          lake exe mk_all --check --module
+          lake exe mk_all --check
       #- name: "lake shake"
       #  run: |
       #    set -e

AUTHORS.md

@@ -0,0 +1,15 @@
+# CSLib Authors
+
+## Copyright and Authorship
+
+**Copyright in CSLib is held by the individual authors** who contributed to the code.
+
+Each file in CSLib includes a copyright header that lists the authors who contributed significantly to that specific file (in the opener and in the optional `Authors` field, when there are multiple significant authors). Examples of significant contributions are original creation, major refactoring, or important additions.
+
+To see more people who have contributed to CSLib and own copyright to parts of the codebase, please refer to its Git history (on a web browser, this can be accessed at <https://github.com/leanprover/cslib/commits/main>).
+
+**Note**: Git history may not always be fully comprehensive. In cases where code is co-written, commit messages and copyright headers in files may attribute additional authors beyond the single commit author.
+
+## Co-Authorship
+
+To ensure **all contributors are properly credited**, we strongly encourage the use of GitHub's [commit with multiple authors feature](https://docs.github.com/en/pull-requests/committing-changes-to-your-project/creating-and-editing-commits/creating-a-commit-with-multiple-authors) whenever code is co-written. This helps with maintaining accurate attribution in CSLib's Git history.

CONTRIBUTING.md

@@ -101,7 +101,7 @@ instructions on how to run these locally.
 
 ## Pull Request Titles
 
-It is required that pull request titles begun with one of the following categories followed by a
+It is required that pull request titles begin with one of the following categories followed by a
 colon: `feat`, `fix`, `doc`, `style`, `refactor`, `test`, `chore`, `perf`. These may optionally be followed by a
 parenthetical containing what area of the library the PR is working on.
 
@@ -125,8 +125,8 @@ CSLib uses a number of linters, mostly inherited from Batteries and Mathlib. The
 
 ## Imports
 
-There is a also a test that [Cslib.lean](/Cslib.lean) imports all files. You can ensure this by
-running `lake exe mk_all --module` locally, which will make the required changes.
+There is also a test that [Cslib.lean](/Cslib.lean) imports all files. You can ensure this by
+running `lake exe mk_all` locally, which will make the required changes.
 
 CSLib tests for minimized imports using `lake shake --add-public --keep-implied --keep-prefix`, which also comes with a `--fix` option.
 See `lake shake --help` for the special comment syntax used to preserve imports required for tactics or typeclasses.

Cslib.lean

@@ -11,19 +11,27 @@ public import Cslib.Computability.Automata.DA.Prod
 public import Cslib.Computability.Automata.DA.ToNA
 public import Cslib.Computability.Automata.EpsilonNA.Basic
 public import Cslib.Computability.Automata.EpsilonNA.ToNA
+public import Cslib.Computability.Automata.EpsilonNA.ToSingleAccept
 public import Cslib.Computability.Automata.NA.Basic
 public import Cslib.Computability.Automata.NA.BuchiEquiv
 public import Cslib.Computability.Automata.NA.BuchiInter
 public import Cslib.Computability.Automata.NA.Concat
+public import Cslib.Computability.Automata.NA.EpsilonTransducer
 public import Cslib.Computability.Automata.NA.Hist
 public import Cslib.Computability.Automata.NA.Loop
 public import Cslib.Computability.Automata.NA.Pair
 public import Cslib.Computability.Automata.NA.Prod
 public import Cslib.Computability.Automata.NA.Sum
 public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.NA.Total
+public import Cslib.Computability.Automata.Transducers.Transducer
 public import Cslib.Computability.Distributed.FLP.Algorithm
+public import Cslib.Computability.Distributed.FLP.CanReachVia
 public import Cslib.Computability.Distributed.FLP.Consensus
+public import Cslib.Computability.Distributed.FLP.FairScheduler
+public import Cslib.Computability.Distributed.FLP.OnePseudoConsensus
+public import Cslib.Computability.Distributed.FLP.PseudoConsensus
+public import Cslib.Computability.Distributed.FLP.ZeroConsensus
 public import Cslib.Computability.Languages.Congruences.BuchiCongruence
 public import Cslib.Computability.Languages.Congruences.RightCongruence
 public import Cslib.Computability.Languages.ExampleEventuallyZero
@@ -32,7 +40,14 @@ public import Cslib.Computability.Languages.MyhillNerode
 public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
-public import Cslib.Computability.Machines.SingleTapeTuring.Basic
+public import Cslib.Computability.Machines.Turing.MultiTape.Classes
+public import Cslib.Computability.Machines.Turing.MultiTape.ConfigBound
+public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+public import Cslib.Computability.Machines.Turing.MultiTape.SpaceInTime
+public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas
+public import Cslib.Computability.Machines.Turing.SingleTape.Defs
+public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
+public import Cslib.Computability.Machines.Turing.SingleTape.NonDeterministic
 public import Cslib.Computability.URM.Basic
 public import Cslib.Computability.URM.Computable
 public import Cslib.Computability.URM.Defs
@@ -58,19 +73,26 @@ public import Cslib.Foundations.Data.DecidableEqZero
 public import Cslib.Foundations.Data.FinFun.Basic
 public import Cslib.Foundations.Data.FinFun.Update
 public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Foundations.Data.Nat.BigO
 public import Cslib.Foundations.Data.Nat.Segment
 public import Cslib.Foundations.Data.OmegaSequence.Defs
 public import Cslib.Foundations.Data.OmegaSequence.Flatten
 public import Cslib.Foundations.Data.OmegaSequence.InfOcc
 public import Cslib.Foundations.Data.OmegaSequence.Init
 public import Cslib.Foundations.Data.OmegaSequence.Temporal
+public import Cslib.Foundations.Data.PFunctor.Free
 public import Cslib.Foundations.Data.RelatesInSteps
-public import Cslib.Foundations.Data.Relation
 public import Cslib.Foundations.Data.Set.Saturation
 public import Cslib.Foundations.Data.StackTape
 public import Cslib.Foundations.Lint.Basic
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Cslib.Foundations.Logic.LogicalEquivalence
+public import Cslib.Foundations.Relation.Attr
+public import Cslib.Foundations.Relation.Confluence
+public import Cslib.Foundations.Relation.Defs
+public import Cslib.Foundations.Relation.Domain
+public import Cslib.Foundations.Relation.Euclidean
+public import Cslib.Foundations.Relation.Restriction
 public import Cslib.Foundations.Semantics.FLTS.Basic
 public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
 public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
@@ -81,6 +103,7 @@ public import Cslib.Foundations.Semantics.LTS.Divergence
 public import Cslib.Foundations.Semantics.LTS.Execution
 public import Cslib.Foundations.Semantics.LTS.HasTau
 public import Cslib.Foundations.Semantics.LTS.LTSCat.Basic
+public import Cslib.Foundations.Semantics.LTS.MapLabel
 public import Cslib.Foundations.Semantics.LTS.Notation
 public import Cslib.Foundations.Semantics.LTS.OmegaExecution
 public import Cslib.Foundations.Semantics.LTS.Relation
@@ -116,6 +139,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.StrongNorm
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.CallByName
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
@@ -127,6 +151,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StandardReduction
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
 public import Cslib.Logics.HML.Basic
@@ -139,9 +164,12 @@ public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
 public import Cslib.Logics.Modal.Basic
 public import Cslib.Logics.Modal.Cube
 public import Cslib.Logics.Modal.Denotation
+public import Cslib.Logics.Modal.LogicalEquivalence
 public import Cslib.Logics.Propositional.Defs
 public import Cslib.Logics.Propositional.NaturalDeduction.Basic
+public import Cslib.Logics.Propositional.NaturalDeduction.Theory
 public import Cslib.MachineLearning.PACLearning.Defs
 public import Cslib.MachineLearning.PACLearning.VCDimension
 public import Cslib.MachineLearning.PACLearning.VersionSpace
+public import Cslib.MachineLearning.PACLearning.VersionSpaceLattice
 public import Cslib.Probability.PMF

Cslib/Algorithms/Lean/MergeSort/MergeSort.lean

@@ -8,7 +8,7 @@ module
 
 public import Cslib.Algorithms.Lean.TimeM
 public import Mathlib.Data.Nat.Cast.Order.Ring
-public import Mathlib.Data.Nat.Lattice
+public import Mathlib.Order.Lattice.Nat
 public import Mathlib.Data.Nat.Log
 
 /-!

Cslib/Algorithms/README.md

@@ -0,0 +1,31 @@
+<pre>
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Clark Barrett, Swarat Chaudhuri, Jim Grundy, Fabrizio Montesi, Leonardo de Moura, Alexandre Rademaker, Sorrachai Yingchareonthawornchai
+</pre>
+
+# Algorithms
+
+This directory hosts **algorithms and their properties**. These properties concern functional correctness, complexity, and other relevant results. The directory also includes dedicated facilities for reasoning about algorithms written in Lean.
+
+The broader aim is to develop a library of verified algorithms, both in Lean and in other languages formalised in CSLib. Accordingly, it is in scope to study algorithms implemented as Lean programs as well as algorithms expressed inside one of CSLib's [Languages](../Languages), depending on the purpose of the development.
+All algorithms sit in a language-specific subdirectory depending on the language they are written in, like `Boole`, `Lean`, etc.
+
+## Principles
+
+### Synergies with languages and logics
+
+Important synergies are expected with both [Languages](../Languages) and [Logics](../Logics). Languages provide settings in which algorithms can be written and studied under formal semantics, while logics provide tools for specifying and proving their properties.
+
+One long-term aim is to support principled reasoning pipelines where algorithms are defined in a language, specified through logical notions, and verified inside shared semantic frameworks.
+
+### Dealing with optimisation
+
+Optimising an algorithm can make it harder to reason about it. When this happens, one can prove a relation (e.g., functional or behavioural) to a simpler, less optimised version, and then work by transferring results from it.
+In doing this, we expect contributions to leverage Lean's and CSLib's common infrastructures whenever reasonable.
+
+## Plans and notes
+
+- We aim at developing a comprehensive library of verified algorithms, covering both Lean implementations and algorithms represented in other languages.
+- We plan on expanding the infrastructure for proving properties of Lean algorithms, including correctness, complexity, and other forms of analysis.
+- Reusable mathematical and semantic infrastructure should live elsewhere in CSLib when it is more general-purpose, so developments in this directory should integrate well with [Foundations](../Foundations), [Languages](../Languages), and [Logics](../Logics).

Cslib/Computability/Automata/DA/Prod.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Ching-Tsun Chou
+Authors: Fabrizio Montesi, Ching-Tsun Chou
 -/
 
 module

Cslib/Computability/Automata/DA/ToNA.lean

@@ -60,7 +60,7 @@ theorem toNAFinAcc_language_eq {a : DA.FinAcc State Symbol} :
   #adaptation_note
   /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
   constructor
-  · simp_all [mem_language a xs, Accepts, toNAFinAcc, toNA, FLTS.toLTS_mtr]
+  · simp [mem_language a xs, Accepts, toNAFinAcc, toNA, FLTS.toLTS_mtr]
   · intro _
     use a.start
     simp_all [Accepts, toNAFinAcc, toNA, FLTS.toLTS_mtr]
@@ -82,7 +82,7 @@ theorem toNABuchi_language_eq {a : DA.Buchi State Symbol} :
   ext xs; constructor
   #adaptation_note
   /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
-  · simp_all [Accepts, language, toNABuchi]
+  · simp [Accepts, language, toNABuchi]
   · intro h
     use (a.run xs)
     split_ands

Cslib/Computability/Automata/EpsilonNA/Basic.lean

@@ -46,9 +46,7 @@ namespace FinAcc
 that trace from the start state. -/
 @[scoped grind =]
 instance : Acceptor (FinAcc State Symbol) Symbol where
-  Accepts (a : FinAcc State Symbol) (xs : List Symbol) :=
-    ∃ s ∈ a.εClosure a.start, ∃ s' ∈ a.accept,
-    a.saturate.MTr s (xs.map (some ·)) s'
+  Accepts a xs := ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.SMTr s (xs.map some) s'
 
 end FinAcc
 

Cslib/Computability/Automata/EpsilonNA/ToNA.lean

@@ -7,32 +7,13 @@ Authors: Fabrizio Montesi
 module
 
 public import Cslib.Computability.Automata.EpsilonNA.Basic
+public import Cslib.Foundations.Semantics.LTS.MapLabel
 
 /-! # Translation of εNA into NA -/
 
 @[expose] public section
 
-namespace Cslib
-
-/-- Converts an `LTS` with Option labels into an `LTS` on the carried label type, by removing all
-ε-transitions. -/
-@[local grind =]
-def LTS.noε (lts : LTS State (Option Label)) : LTS State Label where
-  Tr s μ s' := lts.Tr s (some μ) s'
-
-@[local grind .]
-private lemma LTS.noε_saturate_tr
-  {lts : LTS State (Option Label)} {h : μ = some μ'} :
-  lts.saturate.Tr s μ s' ↔ lts.saturate.noε.Tr s μ' s' := by
-  grind
-
-@[scoped grind =]
-lemma LTS.noε_saturate_mTr {lts : LTS State (Option Label)} :
-  lts.saturate.MTr s (μs.map some) = lts.saturate.noε.MTr s μs := by
-  ext s'
-  induction μs generalizing s <;> grind [<= LTS.MTr.stepL]
-
-namespace Automata.εNA.FinAcc
+namespace Cslib.Automata.εNA.FinAcc
 
 variable {State Symbol : Type*}
 
@@ -41,21 +22,23 @@ variable {State Symbol : Type*}
 def toNAFinAcc (a : εNA.FinAcc State Symbol) : NA.FinAcc State Symbol where
   start := a.εClosure a.start
   accept := a.accept
-  Tr := a.saturate.noε.Tr
+  toLTS := a.saturate.mapLabel Option.some
 
 open Acceptor in
-open scoped NA.FinAcc in
+open scoped NA.FinAcc LTS LTS.MTr LTS.STr LTS.SMTr in
 /-- Correctness of `toNAFinAcc`. -/
-@[scoped grind _=_]
-theorem toNAFinAcc_language_eq {ena : εNA.FinAcc State Symbol} :
-    language ena.toNAFinAcc = language ena := by
+@[scoped grind =]
+theorem toNAFinAcc_language_eq {a : εNA.FinAcc State Symbol} :
+    language a.toNAFinAcc = language a := by
   ext xs
-  have : ∀ s s', ena.saturate.MTr s (xs.map some) s' = ena.saturate.noε.MTr s xs s' := by
-    simp [LTS.noε_saturate_mTr]
-  #adaptation_note
-  /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
-  grind [Accepts]
-
-end Automata.εNA.FinAcc
-
-end Cslib
+  constructor <;> intro ⟨s, hs, s', hs', h⟩
+  · have ⟨sStart, h_sStart, hs⟩ : ∃ i ∈ a.start, s ∈ a.saturate.image i HasTau.τ := by
+      simpa [toNAFinAcc, LTS.τClosure, LTS.setImage] using hs
+    use sStart, h_sStart, s', hs'
+    have h_start := (LTS.sTr_τSTr_iff a.toLTS).mp hs
+    exact LTS.SMTr.comp (LTS.sMTr_τSTr_iff.mp h_start) (by grind)
+  · cases xs with
+    | nil => cases h with | τ tau => exact ⟨s', LTS.tr_setImage hs tau, by grind⟩
+    | cons x xs => exact ⟨s, by grind [Set.mem_of_mem_of_subset]⟩
+
+end Cslib.Automata.εNA.FinAcc