Loop/06 tape transformers

.github/CODEOWNERS

@@ -1,5 +1,5 @@
 # For an overview of the governance model of cslib, please refer to /GOVERNANCE.md and /DECISION_MAKING.md
 
-* @fmontesi @chenson2018 @kim-em @arademaker @sorrachai
+* @fmontesi @chenson2018 @kim-em @arademaker @SamuelSchlesinger @sorrachai
 /.github/CODEOWNERS @fmontesi
 /DECISION_MAKING.md @fmontesi

.github/dependabot.yml

@@ -0,0 +1,25 @@
+version: 2
+updates:
+  # Keep action pins fresh. Grouped so that all bumps land in a single weekly PR,
+  # which bounds the number of full Lean CI builds this triggers.
+  - package-ecosystem: github-actions
+    directory: /
+    schedule:
+      interval: weekly
+    groups:
+      actions:
+        patterns: ["*"]
+    commit-message:
+      prefix: ci
+
+  # Python packages installed by workflows (see requirements.txt in this directory).
+  # Major bumps are left for a human to review.
+  - package-ecosystem: pip
+    directory: /.github
+    schedule:
+      interval: weekly
+    ignore:
+      - dependency-name: "*"
+        update-types: ["version-update:semver-major"]
+    commit-message:
+      prefix: ci

.github/requirements.txt

@@ -0,0 +1 @@
+zulip==0.9.1

.github/workflows/actionlint.yml

@@ -0,0 +1,31 @@
+name: actionlint
+
+on:
+  push:
+    branches:
+      - main
+    paths:
+      - '.github/workflows/**'
+  pull_request:
+    paths:
+      - '.github/workflows/**'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  actionlint:
+    name: Lint workflow files
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          sparse-checkout: |
+            .github/workflows
+
+      # Also runs shellcheck over every `run:` block and pyflakes over
+      # `shell: python` steps.
+      - uses: raven-actions/actionlint@3d39aea434753780c3b3d4a1a31c854b4dbf49d7 # v2.2.0
+        with:
+          version: 1.7.12

.github/workflows/bump_toolchain_nightly-testing.yml

@@ -45,7 +45,7 @@ jobs:
         GH_TOKEN: ${{ steps.app-token.outputs.token }}
       run: |
         # Extract date from RELEASE_TAG (format: nightly-YYYY-MM-DD)
-        DATE_PART=$(echo "$RELEASE_TAG" | sed 's/nightly-//')
+        DATE_PART="${RELEASE_TAG#nightly-}"
         NIGHTLY_TESTING_TAG="nightly-testing-${DATE_PART}"
         echo "NIGHTLY_TESTING_TAG=$NIGHTLY_TESTING_TAG" >> "${GITHUB_ENV}"
 

.github/workflows/lean_action_ci.yml

@@ -14,10 +14,6 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
-      - name: Set TEST_ARGS manually
-        run: |
-          echo "TEST_ARGS='--wfail --iofail'" >> $GITHUB_ENV
-        shell: bash
       - uses: leanprover/lean-action@v1
         with:
           build-args: "--wfail --iofail"

.github/workflows/report_failures_nightly-testing.yml

@@ -80,7 +80,7 @@ jobs:
     # Now post a success message to zulip, if the last message there is not a success message.
     # https://chat.openai.com/share/87656d2c-c804-4583-91aa-426d4f1537b3
     - name: Install Zulip API client
-      run: pip install zulip
+      run: pip install -r .github/requirements.txt
 
     - name: Check last message and post if necessary
       env:
@@ -268,17 +268,18 @@ jobs:
         BUMP_VERSION: ${{ steps.bump_version.outputs.result }}
         BUMP_BRANCH: ${{ steps.latest_bump_branch.outputs.result }}
         SHA: ${{ env.SHA }}
+        ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
       run: |
         echo "Installing zulip CLI..."
-        pip install zulip
+        pip install -r .github/requirements.txt
         echo "Configuring git identity for mathlib4-bot..."
         git config --global user.name "mathlib4-bot"
         git config --global user.email "github-mathlib4-bot@leanprover.zulipchat.com"
         echo "Setting up zulip credentials..."
         {
           echo "[api]"
           echo "email=github-mathlib4-bot@leanprover.zulipchat.com"
-          echo "key=${{ secrets.ZULIP_API_KEY }}"
+          echo "key=$ZULIP_API_KEY"
           echo "site=https://leanprover.zulipchat.com"
         } > ~/.zuliprc
         chmod 600 ~/.zuliprc

Cslib.lean

@@ -31,10 +31,23 @@ 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.Automata.TwoWayNA.Basic
+public import Cslib.Computability.Automata.TwoWayNA.ComplToNA
+public import Cslib.Computability.Automata.TwoWayNA.OfNA
 public import Cslib.Computability.Circuit.Basic
+public import Cslib.Computability.Circuit.Boolean.Basic
+public import Cslib.Computability.Circuit.Boolean.Counting
+public import Cslib.Computability.Circuit.Boolean.Lupanov
+public import Cslib.Computability.Circuit.Boolean.LupanovConstruction
+public import Cslib.Computability.Circuit.Boolean.Shannon
+public import Cslib.Computability.Circuit.Boolean.Synthesis
+public import Cslib.Computability.Circuit.Counting
+public import Cslib.Computability.Circuit.Finite
 public import Cslib.Computability.Circuit.Homomorphism
+public import Cslib.Computability.Circuit.Normalization
 public import Cslib.Computability.Circuit.Program
+public import Cslib.Computability.Circuit.Shannon
 public import Cslib.Computability.Circuit.Signature
+public import Cslib.Computability.Circuit.Synthesis
 public import Cslib.Computability.Circuit.Wire
 public import Cslib.Computability.Distributed.FLP.Algorithm
 public import Cslib.Computability.Distributed.FLP.CanReachVia
@@ -44,8 +57,9 @@ public import Cslib.Computability.Distributed.FLP.Impossibility
 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.Basic
 public import Cslib.Computability.Languages.Congruences.BuchiCongruence
-public import Cslib.Computability.Languages.Congruences.RightCongruence
+public import Cslib.Computability.Languages.Congruences.MyhillCongruence
 public import Cslib.Computability.Languages.ExampleEventuallyZero
 public import Cslib.Computability.Languages.Language
 public import Cslib.Computability.Languages.LanguageHom
@@ -54,10 +68,34 @@ public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
 public import Cslib.Computability.Languages.SafetyLiveness
+public import Cslib.Computability.Languages.SyntacticMonoid
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.AlmostConstant
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Comp
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Id
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Ite
+public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.Loop
+public import Cslib.Computability.Machines.Turing.MultiTape.ConfigBound
 public import Cslib.Computability.Machines.Turing.MultiTape.Configuration
 public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
 public import Cslib.Computability.Machines.Turing.MultiTape.DeterministicToNondeterministic
+public import Cslib.Computability.Machines.Turing.MultiTape.Encodings.Option
 public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic
+public import Cslib.Computability.Machines.Turing.MultiTape.NormalForms.Adapters
+public import Cslib.Computability.Machines.Turing.MultiTape.NormalForms.Instrument
+public import Cslib.Computability.Machines.Turing.MultiTape.NormalForms.Sweep
+public import Cslib.Computability.Machines.Turing.MultiTape.NormalForms.Tidy
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Branch
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Clear
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.EmitTape
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.ExtendTapes
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.InputFromTape
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.OutputToTape
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Repeat
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.RewindInput
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.RewindTape
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Sequential
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.StepLemmas
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TransformsTapes
 public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas
 public import Cslib.Computability.Machines.Turing.SingleTape.Defs
 public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
@@ -83,12 +121,16 @@ public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
 public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
 public import Cslib.Foundations.Control.Monad.Free.Fold
+public import Cslib.Foundations.Control.Monad.IsMonadHom
+public import Cslib.Foundations.Control.Monad.IsMonadHom.List
 public import Cslib.Foundations.Data.BiTape
 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.List.IsChainFromTo
+public import Cslib.Foundations.Data.Nat.Asymptotics
+public import Cslib.Foundations.Data.Nat.Factorial
 public import Cslib.Foundations.Data.Nat.Segment
 public import Cslib.Foundations.Data.OmegaSequence.Defs
 public import Cslib.Foundations.Data.OmegaSequence.Flatten

Cslib/Algorithms/CCS/VendingMachine.lean

@@ -48,27 +48,27 @@ inductive Constant
   | vm
 
 /-- The vending machine process. -/
-def vm : Process String Constant := const .vm
+def vm : Process String Constant := `(CCS| const .vm)
 
 /-! ## Deterministic vending machine -/
 
 /-- Constant definitions: vm = coin.(tea.VM + coffee.VM) -/
 @[local grind =]
 def vendingDefs : Constant → Option (Process String Constant)
-  | .vm => some <| pre Coin (choice (pre Tea (const .vm)) (pre Coffee (const .vm)))
+  | .vm => some <| `(CCS| Coin. ((Tea. const .vm) + (Coffee. const .vm)))
 
 /-- The LTS of CCS for the deterministic vending machine. -/
 abbrev ltsD := CCS.lts (defs := vendingDefs)
 
 /-- VM can perform a coin action. -/
-example : ltsD.Tr vm Coin (choice (pre Tea (const .vm)) (pre Coffee (const .vm))) :=
+example : ltsD.Tr vm Coin `(CCS| (Tea. (const .vm)) + (Coffee. (const .vm))) :=
   Tr.const rfl Tr.pre
 
 /-! ## Nondeterministic vending machine -/
 
 /-- vm = coin.tea.VM + coin.coffee.VM -/
 def vendingDefsND : Constant → Option (Process String Constant)
-  | .vm => some <| (choice (pre Coin (pre Tea (const .vm))) (pre Coin (pre Coffee (const .vm))))
+  | .vm => some <| `(CCS| (Coin. Tea. const .vm) + (Coin. Coffee. const .vm))
 
 /-- The LTS of CCS for the nondeterministic vending machine. -/
 abbrev ltsND := CCS.lts (defs := vendingDefsND)
@@ -78,8 +78,8 @@ open LTS LTS.IsBisimulation LTS.Bisimilarity
 /-- The deterministic and nondeterministic vending machines are not bisimilar. -/
 theorem vm_ltsD_ltsND_not_bisim : ¬(vm ~[ltsD, ltsND] vm) := by
   rintro ⟨r, hr, hbisim⟩
-  let p₁ := (choice (pre Tea (const Constant.vm)) (pre Coffee (const Constant.vm)))
-  let q₁ := (pre Tea (const Constant.vm))
+  let p₁ := `(CCS| (Tea. const Constant.vm) + (Coffee. const Constant.vm))
+  let q₁ := `(CCS| Tea. const Constant.vm)
   have ltsD_vm_deterministic : ltsD.DeterministicStateLabel vm Coin := by
     intro _ _ htr₁ htr₂
     grind [const_tr htr₁, const_tr htr₂]
@@ -90,7 +90,7 @@ theorem vm_ltsD_ltsND_not_bisim : ¬(vm ~[ltsD, ltsND] vm) := by
       (.const rfl .pre)
       (.const rfl (.choiceL .pre))
   have hp₁q₁ : p₁ ~[ltsD, ltsND] q₁ := by grind
-  have hp₁coffee : ltsD.Tr p₁ Coffee (const Constant.vm) := .choiceR .pre
+  have hp₁coffee : ltsD.Tr p₁ Coffee (.const .vm) := .choiceR .pre
   grind [hp₁q₁.follow_fst]
 
 end Cslib.Algorithms.CCS.VendingMachine

Cslib/Algorithms/Lean/MergeSort/MergeSort.lean

@@ -40,18 +40,14 @@ open List in
 @[simp, grind =]
 theorem ret_mergeM {T} [AddMonoid T] (xs ys : List α) (le : α → α → TimeM T Bool) :
     ⟪List.mergeM xs ys le⟫ = List.merge xs ys (fun x y => ⟪le x y⟫) := by
-  fun_induction merge with grind [mergeM, nil_merge, merge_right, cons_merge_cons]
+  simpa using Id.ext_iff.1 <| isMonadHom_pure_ret.map_listMergeM xs ys le
 
 open List in
 /-- `TimeM.ret` passes through `List.mergeSortM` into the comparator. -/
 @[simp]
 theorem ret_mergeSortM {T} [AddMonoid T] (xs : List α) (le : α → α → TimeM T Bool) :
     ⟪List.mergeSortM xs le⟫ = List.mergeSort xs (fun x y => ⟪le x y⟫) := by
-  fun_induction List.mergeSortM with
-  | case1 | case2 => simp
-  | case3 a b xs le iha ihb =>
-    simp only [ret_bind, ret_mergeM, mergeSort]
-    rw [iha, ihb]
+  simpa using Id.ext_iff.1 <| isMonadHom_pure_ret.map_listMergeSortM xs le
 
 variable [LinearOrder α]
 

Cslib/Algorithms/Lean/Sort/Insertion.lean

@@ -6,6 +6,7 @@ Authors: Jeremy Avigad, Eric Wieser
 module
 
 public import Mathlib.Data.List.Sort
+public import Cslib.Foundations.Control.Monad.IsMonadHom
 
 import Cslib.Init
 
@@ -18,18 +19,20 @@ algorithmic analysis.
 
 public section
 
+open Cslib (IsMonadHom)
+
 namespace List
 
-variable {m} [Monad m] (r : α → α → m Bool)
+variable {m n} [Monad m] [Monad n] (r : α → α → m Bool)
 
 /-- A monadic version of `List.orderedInsert`. -/
 def orderedInsertM (a : α) : List α → m (List α)
   | [] => return [a]
   | b :: l => do if ← r a b then return a :: b :: l else return b :: (← orderedInsertM a l)
 
-@[simp] theorem orderedInsertM_nil (a : α) : orderedInsertM r a [] = pure [a] := by
+@[simp, grind =] theorem orderedInsertM_nil (a : α) : orderedInsertM r a [] = pure [a] := by
   rfl
-@[simp] theorem orderedInsertM_cons (a b : α) (l : List α) :
+@[simp, grind =] theorem orderedInsertM_cons (a b : α) (l : List α) :
     orderedInsertM r a (b :: l) = do
       if ← r a b then return a :: b :: l else return b :: (← orderedInsertM r a l) := by
   rfl
@@ -45,6 +48,12 @@ theorem idRun_orderedInsertM (r : α → α → Id Bool) (a : α) (xs : List α)
     Id.run (orderedInsertM r a xs) = orderedInsert (fun x y => Id.run <| r x y) a xs :=
   orderedInsertM_pure _ _ _
 
+@[grind .]
+theorem _root_.Cslib.IsMonadHom.map_orderedInsertM {f : {β : Type} → m β → n β}
+    (hf : IsMonadHom m n f) (r : α → α → m Bool) (a : α) (xs : List α) :
+    f (orderedInsertM r a xs) = orderedInsertM (fun x y => f (r x y)) a xs := by
+  fun_induction orderedInsertM r a xs with grind
+
 /-- A monadic version of `List.insertionSort`. -/
 def insertionSortM : List α → m (List α)
   | [] => return []
@@ -66,4 +75,10 @@ theorem idRun_insertionSortM (xs : List α) (r : α → α → Id Bool) :
     Id.run (insertionSortM r xs) = insertionSort (fun x y => Id.run <| r x y) xs :=
   insertionSortM_pure _ _
 
+@[grind .]
+theorem _root_.Cslib.IsMonadHom.map_listInsertionSortM {f : {β : Type} → m β → n β}
+    (hf : IsMonadHom m n f) (r : α → α → m Bool) (xs : List α) :
+    f (insertionSortM r xs) = insertionSortM (fun x y => f (r x y)) xs := by
+  fun_induction insertionSortM r xs with simp [hf.map_pure, hf.map_bind, hf.map_orderedInsertM, *]
+
 end List

Cslib/Algorithms/Lean/Sort/Merge.lean

@@ -5,8 +5,9 @@ Authors: Kim Morrison, Eric Wieser
 -/
 module
 
-import all Init.Data.List.Sort.Basic
+public import Cslib.Foundations.Control.Monad.IsMonadHom
 
+import all Init.Data.List.Sort.Basic
 import Cslib.Init
 
 /-!
@@ -18,9 +19,11 @@ algorithmic analysis.
 
 public section
 
+open Cslib (IsMonadHom)
+
 namespace List
 
-variable {m} [Monad m]
+variable {m n} [Monad m] [Monad n]
 
 /-- A monadic version of `List.merge` -/
 def mergeM (xs ys : List α) (le : α → α → m Bool) : m (List α) := do
@@ -33,9 +36,11 @@ def mergeM (xs ys : List α) (le : α → α → m Bool) : m (List α) := do
     else
       return y :: (← mergeM (x :: xs) ys le)
 
-@[simp] theorem nil_mergeM (ys : List α) (le : α → α → m Bool) : mergeM [] ys le = pure ys := by
+@[simp, grind =]
+theorem nil_mergeM (ys : List α) (le : α → α → m Bool) : mergeM [] ys le = pure ys := by
   simp [mergeM]
-@[simp] theorem mergeM_right (xs : List α) (le : α → α → m Bool) : mergeM xs [] le = pure xs := by
+@[simp, grind =]
+theorem mergeM_right (xs : List α) (le : α → α → m Bool) : mergeM xs [] le = pure xs := by
   induction xs with
   | nil => simp
   | cons x xs ih => simp [mergeM]
@@ -57,6 +62,14 @@ theorem idRun_mergeM (xs ys : List α) (le : α → α → Id Bool) :
     Id.run (mergeM xs ys le) = merge xs ys (fun x y => Id.run <| le x y) :=
   mergeM_pure _ _ _
 
+@[grind .]
+theorem _root_.Cslib.IsMonadHom.map_listMergeM {f : {β : Type} → m β → n β}
+    (hf : IsMonadHom m n f) (xs ys : List α) (le : α → α → m Bool) :
+    f (mergeM xs ys le) = mergeM xs ys (fun x y => f (le x y)) := by
+  fun_induction mergeM xs ys le with
+  | case1 | case2 => grind
+  | case3 x xs y ys ihx ihy => simp [hf.map_bind, hf.map_pure, apply_ite f, ihx, ihy]
+
 /-- A monadic version of `List.mergeSortM` -/
 def mergeSortM (xs : List α) (le : α → α → m Bool) : m (List α) :=
   match xs with
@@ -88,4 +101,12 @@ theorem idRun_mergeSortM (xs : List α) (le : α → α → Id Bool) :
     Id.run (mergeSortM xs le) = mergeSort xs (fun x y => Id.run <| le x y) :=
   mergeSortM_pure _ _
 
+@[grind .]
+theorem _root_.Cslib.IsMonadHom.map_listMergeSortM {f : {β : Type} → m β → n β}
+    (hf : IsMonadHom m n f) (xs : List α) (le : α → α → m Bool) :
+    f (mergeSortM xs le) = mergeSortM xs (fun x y => f (le x y)) := by
+  fun_induction mergeSortM xs le with
+  | case1 | case2 => simp [hf.map_pure]
+  | case3 a b xs le ih1 ih2 => simp only [mergeSortM, hf.map_bind, ih1, ih2, hf.map_listMergeM, le]
+
 end List