Complexity theory using combinators based on fold and some other prim…

Cslib/Computability/Machines/Turing/MultiTape/Complexity.lean

@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Data
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Encoding
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Defs
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Bounds
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Primitives
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.BoundsAttr
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.BoundsTactic
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Fold
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.While
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.DepthRec
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.Cnf
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.Reach
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.ListIndex
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.ListMap
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.ListUpdate
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.NatMul
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.Lookup
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.LookupTable
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.MachineDesc
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.Tape
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.Synthesis
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.TapeView
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.TapeStep
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.SimConfig
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.SimSpace
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.InputCursor
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.SpaceBound
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.Universal
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Examples.NatArith
+
+/-!
+# Complexity of multi-tape Turing machines (draft)
+
+**STATUS: draft.** Not listed in `Cslib.lean`, because 18 statements are `sorry`-ed. They fall
+into exactly two groups:
+
+* **Machine constructions** (17). The `Bounds.computes` field of every primitive in
+  `Primitives.lean`, of `Bounds.fold` and of `Bounds.while`, together with
+  `ComputableUpTo.comp` and `foldl_computableUpTo`. No concrete multi-tape Turing machine is built
+  anywhere in this development, so every one of these is assumed.
+* **`ComputableUpTo.absorb`** (1), routine `Nat.pow` arithmetic (proof sketch in its docstring).
+
+Everything else is proved, and the split is checkable with `#print axioms`: the correctness of
+every example's fold, all of the size bookkeeping, and the whole simulation stack come out free of
+`sorryAx`.
+
+## The main results
+
+* `foldl_computableUpTo` / `Bounds.fold` — the cost of a `List.foldl`, from the cost of its parts.
+* `Bounds.while` — the same for unbounded iteration; note the time bound carries the trip count
+  and the space bound does not, because iterations reuse tapes.
+* `Simulation.simulates` — a finite, *encodable* configuration reproduces a genuine
+  `Turing.MultiTapeTM` run, for every number of tapes, alphabet size and state count. `Cfg` itself
+  is not encodable: its `workTapes` field is a family of functions `ℤ → Option Symbol`.
+* `Simulation.zipper_length_le_spaceUsed` — that simulation's storage is bounded by the simulated
+  machine's `spaceUsedByTape`, *not* by its running time.
+* `Cnf.formulaSat_polyTimeLinSpace` — **verifying a CNF assignment is polynomial time and linear
+  space**, the `SAT ∈ NP` verifier. It takes no hypotheses: the certificate chain behind it rests
+  only on the assumed primitives above. Seven of its ten certificates are synthesised by the
+  `bounds` tactic; the three that are not are exactly the folds, whose accumulator bounds a tactic
+  cannot invent.
+* The `bounds` tactic (`Complexity/BoundsTactic.lean`) — synthesises a `Bounds` certificate for a
+  Lean function by recursing on its definition, using `@[bounds]`-tagged certificates as leaves.
+
+## Layout
+
+| file | contents |
+| --- | --- |
+| `Complexity/Data.lean` | the rose-tree type, its size measure and bit encoding |
+| `Complexity/Encoding.lean` | `DataEncode` and the encoded-size lemmas |
+| `Complexity/Defs.lean` | `DataComputableInTimeAndSpace`, `ComputableUpTo`, `PolyTimeLinSpace` |
+| `Complexity/Bounds.lean` | `Bounds`, the resource certificate, and its coarse views |
+| `Complexity/Primitives.lean` | the elementary building blocks (machines assumed) |
+| `Complexity/Fold.lean` | `foldl_computableUpTo` and `Bounds.fold` |
+| `Complexity/While.lean` | `Bounds.while`, unbounded iteration |
+| `Complexity/DepthRec.lean` | `Bounds.depthRec`, recursion whose depth depends on the input |
+| `Complexity/BoundsAttr.lean`, `BoundsTactic.lean` | `@[bounds]` and the `bounds` tactic |
+
+Worked examples of the fold theorem:
+
+| file | contents |
+| --- | --- |
+| `Examples/ListIndex.lean`, `ListMap.lean`, `ListUpdate.lean` | indexing, `map`, update |
+| `Examples/NatArith.lean`, `NatMul.lean` | `succ`, `add`, `mul` on binary numerals |
+| `Examples/Lookup.lean`, `LookupTable.lean` | association-list lookup and its faithfulness |
+
+The simulation stack, culminating in a result about `Turing.MultiTapeTM` itself:
+
+| file | contents |
+| --- | --- |
+| `Examples/Tape.lean`, `TapeView.lean` | tapes as zippers; `tapeFun`; `Extent` |
+| `Examples/TapeStep.lean` | one work-tape action vs `step`'s tape update |
+| `Examples/InputCursor.lean` | the input head, including `moveInputPos`'s clamping |
+| `Examples/SpaceBound.lean` | discrete IVT; head span ≤ `spaceUsedByTape` |
+| `Examples/MachineDesc.lean` | untyped machine descriptions, for any `k`/alphabet/states |
+| `Examples/SimConfig.lean` | `SimCfg`, `Represents`, and the step commutation |
+| `Examples/SimSpace.lean` | the simulation's storage, bounded by simulated space |
+| `Examples/Universal.lean` | a universal machine over encoded transition tables |
+
+## References
+
+* [issue #611, *Plan for complexity theory*](https://github.com/leanprover/cslib/issues/611)
+* [issue #590, *Framework for encoding arbitrary types on Turing machines*](https://github.com/leanprover/cslib/issues/590)
+-/

Cslib/Computability/Machines/Turing/MultiTape/Complexity/Bounds.lean

@@ -0,0 +1,148 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Complexity.Defs
+public meta import Cslib.Computability.Machines.Turing.MultiTape.Complexity.BoundsAttr
+
+/-!
+# Resource certificates
+
+`Bounds f` bundles everything a combinator needs to know about `f`: a time bound, a work-tape
+space bound, a bound on the size of its output, the monotonicity of all three, and the proofs that
+they hold. Combinators then become *definitions that compute bounds* rather than theorems that
+restate them, and their monotonicity side conditions discharge themselves.
+
+## Design
+
+* **Indexed by the function.** `Bounds f`, not a structure with an `fn` field, so that one can
+  state `Bounds Nat.succ` and keep the function visible in the type.
+* **Built on `DataComputableInTimeAndSpace`, not `ComputableUpTo`.** The coarse view discards
+  polynomial factors in time and constant factors in space *at the point of statement*; an algebra
+  built on top of it could never recover them. `Bounds.polyTimeLinSpace` takes the coarse view at
+  the very end instead.
+* **`outSize` is a field of its own.** It is not derivable from `space`: the output tape is
+  write-only and is not charged for space, so a machine may emit far more than its work-tape
+  space. (`outSize ≤ time` is always available — at most one symbol is emitted per step — but it is
+  usually far too weak.)
+* `Bounds` is `Type`-valued: it is a witness, not a property. Use `ComputableUpTo` when a `Prop` is
+  wanted.
+-/
+
+@[expose] public section
+
+namespace Turing
+
+namespace MultiTapeTM
+
+open RoseTreeMachine
+
+variable {α β : Type} [DataEncode α] [DataEncode β]
+
+/-- A resource certificate for `f`: bounds on its running time, its work-tape space and the size
+of its output, all as functions of the encoded input size, together with their monotonicity and
+the proofs that they hold. -/
+structure Bounds (f : α → β) where
+  /-- Bound on the number of steps, in the encoded input size. -/
+  time : ℕ → ℕ
+  /-- Bound on the number of work-tape cells visited, in the encoded input size. -/
+  space : ℕ → ℕ
+  /-- Bound on the encoded size of the output, in the encoded input size. -/
+  outSize : ℕ → ℕ
+  /-- Combinators evaluate `time` at an over-approximation of the true input size. -/
+  time_mono : Monotone time
+  /-- Combinators evaluate `space` at an over-approximation of the true input size. -/
+  space_mono : Monotone space
+  /-- Combinators evaluate `outSize` at an over-approximation of the true input size. -/
+  outSize_mono : Monotone outSize
+  /-- Some multi-tape Turing machine computes `f` within `time` and `space`. -/
+  computes : DataComputableInTimeAndSpace f time space
+  /-- The output really is no bigger than `outSize` says. -/
+  out_le : ∀ a, (DataEncode.encode (f a)).size ≤ outSize (DataEncode.encode a).size
+
+namespace Bounds
+
+/-- Transport a certificate along an equality of functions. Used to turn a certificate for the
+literal shape a combinator produces into one for the function actually of interest. -/
+def congr {f g : α → β} (b : Bounds f) (h : f = g := by rfl) : Bounds g where
+  time := b.time
+  space := b.space
+  outSize := b.outSize
+  time_mono := b.time_mono
+  space_mono := b.space_mono
+  outSize_mono := b.outSize_mono
+  computes := h ▸ b.computes
+  out_le := h ▸ b.out_le
+
+/-- Transport leaves the time bound alone.
+
+`congr` copies the resource fields *verbatim* and confines `Eq.rec` to the `Prop` fields, so this
+and its siblings hold by `rfl` and a transported certificate's bounds stay definitionally readable
+through any chain of retargets. Transporting the whole structure instead would leave them stuck
+behind `Eq.rec`, silently disabling `Bounds.polyTimeLinSpace` for every derived certificate. -/
+@[simp, boundsDefs] lemma congr_time {f g : α → β} (b : Bounds f) (h : f = g) :
+    (b.congr h).time = b.time := rfl
+
+/-- Transport leaves the space bound alone. -/
+@[simp, boundsDefs] lemma congr_space {f g : α → β} (b : Bounds f) (h : f = g) :
+    (b.congr h).space = b.space := rfl
+
+/-- Transport leaves the output-size bound alone. -/
+@[simp, boundsDefs] lemma congr_outSize {f g : α → β} (b : Bounds f) (h : f = g) :
+    (b.congr h).outSize = b.outSize := rfl
+
+
+/-- Weaken all three bounds at once. Composition produces one specific closed form; this is how
+one restates it more readably. -/
+def weaken {f : α → β} (b : Bounds f) (t s o : ℕ → ℕ)
+    (ht_mono : Monotone t) (hs_mono : Monotone s) (ho_mono : Monotone o)
+    (ht : ∀ n, b.time n ≤ t n) (hs : ∀ n, b.space n ≤ s n) (ho : ∀ n, b.outSize n ≤ o n) :
+    Bounds f where
+  time := t
+  space := s
+  outSize := o
+  time_mono := ht_mono
+  space_mono := hs_mono
+  outSize_mono := ho_mono
+  computes := b.computes.mono ht hs
+  out_le a := le_trans (b.out_le a) (ho _)
+
+section Weaken
+variable {f : α → β} (b : Bounds f) (t s o : ℕ → ℕ) (ht_mono : Monotone t) (hs_mono : Monotone s)
+  (ho_mono : Monotone o) (ht : ∀ n, b.time n ≤ t n) (hs : ∀ n, b.space n ≤ s n)
+  (ho : ∀ n, b.outSize n ≤ o n)
+
+@[simp, boundsDefs] lemma weaken_time :
+    (b.weaken t s o ht_mono hs_mono ho_mono ht hs ho).time = t := rfl
+
+@[simp, boundsDefs] lemma weaken_space :
+    (b.weaken t s o ht_mono hs_mono ho_mono ht hs ho).space = s := rfl
+
+@[simp, boundsDefs] lemma weaken_outSize :
+    (b.weaken t s o ht_mono hs_mono ho_mono ht hs ho).outSize = o := rfl
+
+end Weaken
+
+/-- Every certificate yields the coarse `ComputableUpTo` statement with the same bounds. -/
+theorem toComputableUpTo {f : α → β} (b : Bounds f) : ComputableUpTo f b.time b.space :=
+  ⟨1, b.computes.mono
+    (fun n => by simp only [pow_one, one_mul]; omega)
+    (fun n => by simp only [one_mul]; omega)⟩
+
+/-- Read "polynomial time, linear space" off a certificate. This is the intended last step of an
+example: build the certificate with exact bounds, then take the coarse view once. -/
+theorem polyTimeLinSpace {f : α → β} (b : Bounds f) (d k e : ℕ)
+    (ht : ∀ n, b.time n ≤ d * (n + n + 2) ^ k)
+    (hs : ∀ n, b.space n ≤ e * (n + 1)) :
+    PolyTimeLinSpace f :=
+  b.toComputableUpTo.absorb d k e ht hs
+
+end Bounds
+
+end MultiTapeTM
+
+end Turing

Cslib/Computability/Machines/Turing/MultiTape/Complexity/BoundsAttr.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Lean
+
+/-!
+# The `@[bounds]` attribute
+
+Registers a `Bounds` certificate as a *leaf* for the `bounds` tactic. Anything already proved —
+a primitive, a hand-built certificate, or the result of `Bounds.fold` / `Bounds.while` — can be
+registered, and the tactic will stop its recursion there.
+
+This is the intended way to handle loops and recursion. `Bounds.fold` and `Bounds.while` take
+arguments a tactic cannot invent (the accumulator bound `A`, the trip count `N`), so they are
+deliberately *not* given tactic support; instead the human proves the certificate once and
+registers it.
+
+The extension lives in its own module because Lean forbids using an `initialize` declaration in
+the module that declares it.
+-/
+
+open Lean
+
+public section
+
+/-- Certificates registered as leaves for the `bounds` tactic. -/
+initialize boundsExt : SimplePersistentEnvExtension Name (Array Name) ←
+  registerSimplePersistentEnvExtension
+    { addEntryFn := Array.push
+      addImportedFn := fun as => as.foldl (· ++ ·) #[] }
+
+/-- Simp set unfolding every `Bounds` combinator, so a synthesised certificate's bounds can be
+read off. Populated in `BoundsTactic.lean`, where the combinators are in scope. -/
+register_simp_attr boundsDefs
+
+initialize registerBuiltinAttribute {
+    name := `bounds
+    descr := "register a `Bounds` certificate as a leaf for the `bounds` tactic"
+    add := fun decl _ _ => modifyEnv fun env => boundsExt.addEntry env decl
+  }
+
+end