RTM v4, in progress.

Cslib/Computability/Machines/RTM/Data.lean

@@ -0,0 +1,119 @@
+/-
+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.Init
+public import Mathlib.Data.Part
+
+/-!
+# Main internal data type for the rose tree machine (RTM)
+
+This file contains the main internal data structure for the RTM, `Data`, a rose tree.
+
+## Main definitions and notations
+
+- `Data` - the main data structure
+- `Data.size` - the size of a `Data` object when encoded using parentheses, complexity results
+  use this size as the main measure.
+- `Data.recL` - the main recursion principle for `Data`
+- `Data.inductionL` - the main induction principle for `Data`
+
+-/
+
+@[expose] public section
+
+namespace Turing
+
+namespace RoseTreeMachine
+
+/-- Rose-tree data structure, it allows us to encode most of Lean's data structures in a
+"natural" manner -/
+inductive Data where
+  | l : List Data → Data
+deriving Repr
+
+mutual
+  def Data.decEq : ∀ (a b : Data), Decidable (a = b)
+    | .l xs, .l ys =>
+      match Data.listDecEq xs ys with
+      | isTrue h => isTrue (congrArg Data.l h)
+      | isFalse h => isFalse fun heq => h (Data.l.inj heq)
+  def Data.listDecEq : ∀ (xs ys : List Data), Decidable (xs = ys)
+    | [], [] => isTrue rfl
+    | [], _ :: _ => isFalse (by simp)
+    | _ :: _, [] => isFalse (by simp)
+    | x :: xs, y :: ys =>
+      match Data.decEq x y, Data.listDecEq xs ys with
+      | isTrue hxy, isTrue hxys => isTrue (congrArg₂ List.cons hxy hxys)
+      | isFalse hxy, _ => isFalse fun h => hxy (List.cons.inj h).1
+      | _, isFalse hxys => isFalse fun h => hxys (List.cons.inj h).2
+end
+
+instance : DecidableEq Data := Data.decEq
+instance : BEq Data := inferInstance
+instance : LawfulBEq Data := inferInstance
+
+abbrev Data.empty := Data.l []
+
+
+@[scoped grind =]
+def Data.asList
+  | Data.l xs => xs
+
+@[simp]
+lemma Data.asList_empty : Data.empty.asList = [] := by rfl
+
+@[simp, scoped grind =]
+lemma Data.asList_l (d : Data) : Data.l d.asList = d := by simp [Data.asList]; grind
+
+@[simp, scoped grind =]
+lemma Data.l_asList (xs : List Data) : (Data.l xs).asList = xs := by simp [Data.asList]
+
+/-- The encoding length of `d`, relevant for complexity.
+This is the encoded size assuming an encoding into parenthesized expressions. -/
+def Data.size : Data → ℕ
+  | Data.l xs => 2 + (xs.map Data.size |>.sum)
+
+@[simp]
+lemma Data.size_le {d : Data} : 0 < d.size := by
+  obtain ⟨xs⟩ := d
+  grind [Data.size]
+
+@[simp, scoped grind =]
+lemma Data.size_empty : Data.empty.size = 2 := by simp [Data.empty, Data.size]
+
+@[simp, scoped grind =]
+lemma Data.cons_size {h : Data} {t : List Data} :
+    (Data.l (h :: t)).size = h.size + (Data.l t).size := by
+  simp [Data.size]
+  grind
+
+/-- Recursion principle for `Data`. -/
+@[elab_as_elim]
+def Data.recL {motive : Data → Sort*}
+    (nil : motive (Data.l []))
+    (cons : ∀ (x : Data) (xs : List Data),
+      motive x → motive (Data.l xs) → motive (Data.l (x :: xs))) :
+    ∀ d, motive d
+  | .l [] => nil
+  | .l (x :: xs) =>
+      cons x xs (Data.recL nil cons x) (Data.recL nil cons (.l xs))
+
+/-- Induction principle for `Data`, the `Prop`-valued companion to `Data.recL`. -/
+@[elab_as_elim]
+theorem Data.inductionL {motive : Data → Prop}
+    (nil : motive (Data.l []))
+    (cons : ∀ (x : Data) (xs : List Data),
+      motive x → motive (Data.l xs) → motive (Data.l (x :: xs)))
+    (d : Data) : motive d :=
+  Data.recL nil cons d
+
+abbrev TapeIndex := ℕ
+
+end RoseTreeMachine
+
+end Turing

Cslib/Computability/Machines/RTM/DataEncode.lean

@@ -0,0 +1,105 @@
+/-
+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.RTM.Data
+public import Mathlib.Data.Nat.Bits
+public import Mathlib.Data.List.Basic
+
+/-!
+# Encodings into `Data`
+
+This file defines the class that is used to encode arbitrary data structures into `Data`,
+so that RTMs (rose tree machines) can operate on them.
+
+Instances are provided for convenience for `Data` itself, `Bool`, `List α`, `Option α`, `α × β`,
+and `ℕ` (binary encoding via `List Bool`)
+
+-/
+
+@[expose] public section
+
+namespace Turing
+
+namespace RoseTreeMachine
+
+/-- Encoding of types into `Data`. -/
+class DataEncode (α : Type) where
+  encode : α → Data
+  h_inj : encode.Injective
+
+instance : DataEncode Data where
+  encode b := b
+  h_inj := by intros a b h_eq; grind
+
+@[simp, scoped grind =]
+lemma DataEncode_encode_data (d : Data) : DataEncode.encode d = d := rfl
+
+instance : DataEncode Bool where
+  encode b := if b then Data.l [ Data.l [] ] else Data.l []
+  h_inj := by intros a b h_eq; grind
+
+instance (α : Type) [DataEncode α] : DataEncode (List α) where
+  encode xs := Data.l (xs.map DataEncode.encode)
+  h_inj := by
+    intro a b h
+    exact List.map_injective_iff.mpr DataEncode.h_inj (Data.l.inj h)
+
+@[simp, scoped grind =]
+lemma DataEncode_list_nil {α : Type} [DataEncode α] :
+  DataEncode.encode ([] : List α) = Data.l [] := by
+  simp [DataEncode.encode]
+
+@[simp, scoped grind =]
+lemma DataEncode_list_eq_nil_iff_nil {α : Type} [DataEncode α] (xs : List α) :
+  DataEncode.encode xs = Data.empty ↔ xs = [] := by
+  simp [DataEncode.encode]
+
+@[simp, scoped grind =]
+lemma DataEncode_list_tail {α : Type} [DataEncode α] (xs : List α) :
+  (DataEncode.encode xs).asList.tail = (DataEncode.encode xs.tail).asList := by
+  simp [DataEncode.encode]
+
+instance (α : Type) [DataEncode α] : DataEncode (Option α) where
+  encode := fun
+    | none => Data.l []
+    | some x => Data.l [DataEncode.encode x]
+  h_inj := by
+    intro a b h
+    grind [DataEncode.h_inj]
+
+@[simp]
+lemma DataEncode_Option_empty {α : Type} [DataEncode α] (x : Option α) :
+  (DataEncode.encode x == Data.empty) = x.isNone := by
+  cases x <;> simp [DataEncode.encode, Data.empty]
+
+instance (α β : Type) [DataEncode α] [DataEncode β] : DataEncode (α × β) where
+  encode := fun (a, b) => Data.l [DataEncode.encode a, DataEncode.encode b]
+  h_inj := by
+    intro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h
+    grind [DataEncode.h_inj]
+
+lemma DataEncode_pair {α β : Type} [DataEncode α] [DataEncode β] (a : α) (b : β) :
+  DataEncode.encode (a, b) = Data.l [DataEncode.encode a, DataEncode.encode b] := by
+  simp [DataEncode.encode]
+
+instance : DataEncode ℕ where
+  encode x := DataEncode.encode (Nat.bits x)
+  h_inj := by
+    intro a b h
+    have hb : a.bits = b.bits := DataEncode.h_inj h
+    have hrec : ∀ n : ℕ, n.bits.foldr (fun b acc => Nat.bit b acc) 0 = n := by
+      intro n
+      induction n using Nat.binaryRec' with
+      | zero => simp
+      | bit b n hn ih => rw [Nat.bits_append_bit n b hn]; simp [ih]
+    have := congrArg (List.foldr (fun b acc => Nat.bit b acc) 0) hb
+    simpa [hrec] using this
+
+end RoseTreeMachine
+
+end Turing