Results about finite space and regular languages

.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

CONTRIBUTING.md

@@ -126,7 +126,7 @@ 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.
+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,23 @@ 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.Consensus
+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 +36,12 @@ 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.ConfigBound
+public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+public import Cslib.Computability.Machines.Turing.MultiTape.Regular
+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
@@ -64,13 +73,19 @@ 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 +96,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 +132,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 +144,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,8 +157,10 @@ 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

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/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/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