refactor(Encodings): generate structure encodings with enc_structure

Complexity.lean

@@ -2029,6 +2029,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pi
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.StepMachine
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.StepMachineComp
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.StreamFold
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Sum
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Tape
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary

Complexity/Computability/Complexity/Classes/Space/TQBF/Membership.lean

@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Complexity.Classes.Space
 public import Complexity.Computability.Complexity.Classes.Space.TQBF.Evaluation
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCountedIteration
 import Complexity.Computability.Machines.Turing.MultiTape.Combinators.IterateWhile
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatPower
@@ -66,103 +67,20 @@ open Cslib.Logic.PL Turing.MultiTapeTM
 
 /-! ### Encodings -/
 
-/-- The fields of a frame. -/
-def Frame.fields (f : Frame) : (QBF.Kind × ℕ) × Option Bool × List (QBF.Kind × ℕ) :=
-  (f.token, f.first, f.rest)
-
-/-- The encoding of the fields of a frame. -/
-abbrev encFrameFields : (QBF.Kind × ℕ) × Option Bool × List (QBF.Kind × ℕ) ↪ List Bool :=
-  encPair encToken (encPair (encOption encBool) (encList encToken))
-
 /-- Frames encoded by their fields. -/
-def encFrame : Frame ↪ List Bool :=
-  ⟨fun f => encFrameFields f.fields, fun f g h => by
-    obtain ⟨⟩ := f
-    obtain ⟨⟩ := g
-    simpa [Frame.fields] using encFrameFields.injective h⟩
-
-/-- The fields of a state. -/
-def State.fields (s : State) : List (QBF.Kind × ℕ) × List Frame × Option Bool × Bool :=
-  (s.input, s.stack, s.value, s.ok)
-
-/-- The encoding of the fields of a state. -/
-abbrev encStateFields : List (QBF.Kind × ℕ) × List Frame × Option Bool × Bool ↪ List Bool :=
-  encPair (encList encToken) (encPair (encList encFrame) (encPair (encOption encBool) encBool))
+enc_structure encFrame : Frame where
+  token : encToken, first : (encOption encBool), rest : (encList encToken)
 
 /-- States encoded by their fields. -/
-def encState : State ↪ List Bool :=
-  ⟨fun s => encStateFields s.fields, fun s t h => by
-    obtain ⟨⟩ := s
-    obtain ⟨⟩ := t
-    simpa [State.fields] using encStateFields.injective h⟩
+enc_structure encState : State where
+  input : (encList encToken), stack : (encList encFrame), value : (encOption encBool), ok : encBool
 
 /-! ### The step in polynomial time -/
 
 section Step
 
 open ComputableInPolyTime
 
-/-- The fields of a state, the identity on encoded values. -/
-@[local fun_prop] private lemma fields_pt :
-    ComputableInPolyTime State.fields encState encStateFields :=
-  of_eq fun _ => rfl
-
-/-- A state from its fields, the identity on encoded values. -/
-@[local fun_prop] private lemma stateMk_pt :
-    ComputableInPolyTime
-      (fun p : List (QBF.Kind × ℕ) × List Frame × Option Bool × Bool =>
-        State.mk p.1 p.2.1 p.2.2.1 p.2.2.2) encStateFields encState :=
-  of_eq fun _ => rfl
-
-/-- The fields of a frame, the identity on encoded values. -/
-@[local fun_prop] private lemma frameFields_pt :
-    ComputableInPolyTime Frame.fields encFrame encFrameFields :=
-  of_eq fun _ => rfl
-
-/-- A frame from its fields, the identity on encoded values. -/
-@[local fun_prop] private lemma frameMk_pt :
-    ComputableInPolyTime
-      (fun p : (QBF.Kind × ℕ) × Option Bool × List (QBF.Kind × ℕ) => Frame.mk p.1 p.2.1 p.2.2)
-      encFrameFields encFrame :=
-  of_eq fun _ => rfl
-
-@[local fun_prop] private lemma stateMk_comp_pt {α : Type} {encIn : α ↪ List Bool}
-    {f₁ : α → List (QBF.Kind × ℕ)} {f₂ : α → List Frame}
-    {f₃ : α → Option Bool} {f₄ : α → Bool}
-    (h₁ : ComputableInPolyTime f₁ encIn (encList encToken))
-    (h₂ : ComputableInPolyTime f₂ encIn (encList encFrame))
-    (h₃ : ComputableInPolyTime f₃ encIn (encOption encBool))
-    (h₄ : ComputableInPolyTime f₄ encIn encBool) :
-    ComputableInPolyTime (fun a => State.mk (f₁ a) (f₂ a) (f₃ a) (f₄ a)) encIn encState :=
-  stateMk_pt.comp (h₁.prod (h₂.prod (h₃.prod h₄)))
-
-@[local fun_prop] private lemma input_pt :
-    ComputableInPolyTime State.input encState (encList encToken) :=
-  (fst _ _).comp fields_pt
-
-@[local fun_prop] private lemma stack_pt :
-    ComputableInPolyTime State.stack encState (encList encFrame) :=
-  ((fst _ _).comp (snd _ _)).comp fields_pt
-
-@[local fun_prop] private lemma value_pt :
-    ComputableInPolyTime State.value encState (encOption encBool) :=
-  ((fst _ _).comp ((snd _ _).comp (snd _ _))).comp fields_pt
-
-@[local fun_prop] private lemma ok_pt : ComputableInPolyTime State.ok encState encBool :=
-  ((snd _ _).comp ((snd _ _).comp (snd _ _))).comp fields_pt
-
-@[local fun_prop] private lemma token_pt :
-    ComputableInPolyTime Frame.token encFrame encToken :=
-  (fst _ _).comp frameFields_pt
-
-@[local fun_prop] private lemma first_pt :
-    ComputableInPolyTime Frame.first encFrame (encOption encBool) :=
-  ((fst _ _).comp (snd _ _)).comp frameFields_pt
-
-@[local fun_prop] private lemma rest_pt :
-    ComputableInPolyTime Frame.rest encFrame (encList encToken) :=
-  ((snd _ _).comp (snd _ _)).comp frameFields_pt
-
 /-- The next token, or `(top, 0)` when the input is empty. -/
 private def State.head (s : State) : QBF.Kind × ℕ := s.input.headD (.top, 0)
 
@@ -251,7 +169,7 @@ private theorem assignment_eq (stack : List Frame) (v : ℕ) :
   have h : ComputableInPolyTime (fun p : State × Frame => Frame.binds p.1.head.2 p.2)
       (encPair encState encFrame) encBool :=
     binds_pt.comp (g := fun p : State × Frame => (p.1.head.2, p.2)) (by fun_prop)
-  exact optionIsSome (findWithInput stack_pt h)
+  exact optionIsSome (findWithInput (encState_stack_polyTime id') h)
 
 /-- The value of the next variable, by a search of the stack. -/
 @[local fun_prop] private lemma assignment_pt :
@@ -260,7 +178,8 @@ private theorem assignment_eq (stack : List Frame) (v : ℕ) :
   have h : ComputableInPolyTime (fun p : State × Frame => Frame.binds p.1.head.2 p.2)
       (encPair encState encFrame) encBool :=
     binds_pt.comp (g := fun p : State × Frame => (p.1.head.2, p.2)) (by fun_prop)
-  exact optionElimWithInput (findWithInput stack_pt h) (const false) (by fun_prop)
+  exact optionElimWithInput (findWithInput (encState_stack_polyTime id') h) (const false)
+    (by fun_prop)
 
 /-- A step reading a token is polynomial-time. -/
 private lemma readStep_pt (k : QBF.Kind) :
@@ -275,7 +194,7 @@ private lemma retStep_pt (k : QBF.Kind) (second : Bool) :
 /-- **A step of the evaluator is polynomial-time** in the encoded state. -/
 theorem computableInPolyTime_step : ComputableInPolyTime step encState encState := by
   rw [show step = _ from funext step_eq]
-  refine ite (optionIsSome value_pt) (ite (by fun_prop) id' ?_)
+  refine ite (optionIsSome (encState_value_polyTime id')) (ite (by fun_prop) id' ?_)
     (ite (by fun_prop) (by fun_prop) ?_)
   · exact finite_cases (tagEncoding := encPair encKind encBool)
       (tag := fun s => (s.top.token.1, s.top.first.isSome))
@@ -311,9 +230,8 @@ private theorem length_encFrame_le {φ : QBF ℕ} {f : Frame} (h : f.token :: f.
     (encFrame f).length ≤ (encQBF φ).length + 5 := by
   have hs := length_encList_le_of_suffix h
   have hfirst : (encOption encBool f.first).length ≤ 2 := by cases f.first <;> simp [encOption]
-  change (encFrameFields f.fields).length ≤ _
   rw [encQBF_apply]
-  simp only [Frame.fields, length_encPair, encList_cons, List.length_append, length_frame] at hs ⊢
+  simp only [encFrame_apply, length_encPair, encList_cons, List.length_append, length_frame] at hs ⊢
   omega
 
 /-- **The states of a run are of quadratic size**: a state satisfying the invariant on `φ` has an
@@ -329,8 +247,7 @@ theorem length_encState_le {φ : QBF ℕ} {s : State} (h : Good φ s) :
     h.length_stack_le.trans (by have := three_mul_length_tokens_le φ; omega)
   have hval : (encOption encBool s.value).length ≤ 2 := by cases s.value <;> simp [encOption]
   have hmul := Nat.mul_le_mul_right (2 * ((encQBF φ).length + 5) + 1) hdepth
-  change (encStateFields s.fields).length ≤ _
-  simp only [State.fields, length_encPair, encBool_apply, List.length_singleton]
+  simp only [encState_apply, length_encPair, encBool_apply, List.length_singleton]
   nlinarith
 
 /-! ### The evaluator in polynomial space -/

Complexity/Computability/GenericRAM/Simulation/Turing.lean

@@ -12,6 +12,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Internal.Equali
 public import Complexity.Computability.GenericRAM.Simulation.Finite
 public import Complexity.Computability.GenericRAM.SparseMemory.Turing
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Pi
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 
 /-!
 # Native implementation of fixed-program finite RAM steps
@@ -68,22 +69,11 @@ open NativeCertificate
 variable {M : Model.{0, 0, 0, 0}} {r : ℕ}
 
 /-- Encode all finite state components, including the default and distinct stored bindings. -/
-def encoding (enc : M.Encoding) : FiniteState M r ↪ List Bool :=
-  ⟨fun s => encPair encNat (encPair (encPi enc.value)
-      (encPair enc.value (SparseMemory.encoding enc.address enc.value)))
-      (s.pc, s.regs, s.default, s.memory), by
-    intro s t h
-    have hp := (encPair encNat (encPair (encPi enc.value)
-      (encPair enc.value (SparseMemory.encoding enc.address enc.value)))).injective h
-    cases s
-    cases t
-    cases hp
-    rfl⟩
-
-@[simp] theorem encoding_apply (enc : M.Encoding) (s : FiniteState M r) :
-    encoding enc s = encPair encNat (encPair (encPi enc.value)
-      (encPair enc.value (SparseMemory.encoding enc.address enc.value)))
-      (s.pc, s.regs, s.default, s.memory) := rfl
+enc_structure encoding (enc : M.Encoding) : FiniteState M r where
+  pc : encNat, regs : (encPi (Index := Fin r) enc.value), default : enc.value,
+  memory : (SparseMemory.encoding enc.address enc.value)
+
+attribute [simp] encoding_apply
 
 /-- Configuration is a runtime input, alongside the complete finite state. -/
 abbrev inputEncoding (enc : M.Encoding) :

Complexity/Computability/Kolmogorov/MINKT.lean

@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Complexity.Classes.NP.Witness
 public import Complexity.Computability.Complexity.Classes.Promise.Basic
 public import Complexity.Computability.Kolmogorov.TimeBounded
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
@@ -111,16 +112,9 @@ namespace MINKT
 
 /-- Standard encoding of `MINKT.Instance`: the string `x`, followed by `1^time` and `1^size` in
 unary ([Ko][Ko1991]; [Hirahara, Definition 9][Hirahara2018]). -/
-def enc : Instance ↪ List Bool :=
-  (⟨fun i => (i.string, (i.time, i.size)), fun i j h => by
-    cases i; cases j; simpa using h⟩ : Instance ↪ List Bool × (ℕ × ℕ)).trans
-    (encPair encBits (encPair encUnary encUnary))
+enc_structure enc : Instance where string : encBits, time : encUnary, size : encUnary
 
-/-- Applying `MINKT.enc` encodes `(i.string, (i.time, i.size))` via `encPair`. -/
-@[simp]
-theorem enc_apply (i : Instance) :
-    enc i = encPair encBits (encPair encUnary encUnary) (i.string, (i.time, i.size)) :=
-  rfl
+attribute [simp] enc_apply
 
 /-- The unary size parameter `i.size` is at most the encoded instance length `(enc i).length`. -/
 theorem size_le_length_enc (i : Instance) : i.size ≤ (enc i).length := by

Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/InductiveCounting/Machine.lean

@@ -11,6 +11,7 @@ public import Complexity.Algorithms.Reachability.InductiveCounting.Bounds
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.InductiveCounting.Encoding
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.InductiveCounting.Graph
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.NondeterministicQueryMachine
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 
 /-!
 # The input-scanning query machine for inductive counting
@@ -70,16 +71,8 @@ structure Runtime where
   counting : Option Cslib.InductiveCounting.State
 
 /-- The state encoding omits the input and every proof-level choice history. -/
-def encRuntime : Runtime ↪ List Bool :=
-  ⟨fun s => encPair encNat (encPair encNat (encPair encBool (encOption encState)))
-      (s.length, s.radix, s.checked, s.counting), by
-    intro s t h
-    have h' := (encPair encNat (encPair encNat (encPair encBool (encOption encState)))).injective h
-    cases s
-    cases t
-    simp only [Prod.mk.injEq] at h'
-    obtain ⟨rfl, rfl, rfl, rfl⟩ := h'
-    rfl⟩
+enc_structure encRuntime : Runtime where
+  length : encNat, radix : encNat, checked : encBool, counting : (encOption encState)
 
 variable {k : ℕ} {State : Type} [Fintype State] (ntm : MultiTapeNTM k Bool State)
 

Complexity/Computability/Machines/Turing/MultiTape/Complexity/Space/Reachability.lean

@@ -7,6 +7,7 @@ Authors: Bolton Bailey, Samuel Schlesinger
 module
 -- upstream: candidate
 
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Structure
 public import Complexity.Algorithms.Reachability.Savitch
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
@@ -94,20 +95,9 @@ namespace Savitch
 
 /-! ### Encodings -/
 
-/-- The fields of a frame. -/
-def Frame.fields (f : Frame) : ℕ × List Bool × List Bool × List Bool × Bool :=
-  (f.level, f.src, f.dst, f.mid, f.phase)
-
-/-- The encoding of the fields of a frame: the level in unary, the words as themselves. -/
-abbrev encFrameFields : ℕ × List Bool × List Bool × List Bool × Bool ↪ List Bool :=
-  encPair encUnary (encPair encBits (encPair encBits (encPair encBits encBool)))
-
-/-- Frames encoded by their fields. -/
-def encFrame : Frame ↪ List Bool :=
-  ⟨fun f => encFrameFields f.fields, fun f g h => by
-    obtain ⟨⟩ := f
-    obtain ⟨⟩ := g
-    simpa [Frame.fields] using encFrameFields.injective h⟩
+/-- Frames encoded by their fields: the level in unary, the words as themselves. -/
+enc_structure encFrame : Frame where
+  level : encUnary, src : encBits, dst : encBits, mid : encBits, phase : encBool
 
 /-- The register as a pending call, if any, and the returned value, `false` during a call. -/
 def Reg.toPair : Reg → Option (ℕ × List Bool × List Bool) × Bool
@@ -124,11 +114,7 @@ def encReg : Reg ↪ List Bool :=
     cases r <;> cases r' <;> simp_all [Reg.toPair]⟩
 
 /-- States encoded as the list of their frames followed by their register. -/
-def encState : State ↪ List Bool :=
-  ⟨fun s => encPair (encList encFrame) encReg (s.stack, s.reg), fun s s' h => by
-    obtain ⟨⟩ := s
-    obtain ⟨⟩ := s'
-    simpa using (encPair (encList encFrame) encReg).injective h⟩
+enc_structure encState : State where stack : (encList encFrame), reg : encReg
 
 /-! ### The step in linear time, apart from the edge test -/
 
@@ -220,19 +206,20 @@ attribute [local fun_prop] ComputableTidilyInDegree.increment
 /-- The stack of a state. -/
 @[local fun_prop] private lemma stack_deg :
     ComputableTidilyInDegree State.stack encState (encList encFrame) 1 1 :=
-  of_linear (.of_unframe fun s => by simp [encState])
+  of_linear (.of_unframe fun s => by simp [encState_apply])
 
 /-- The register of a state. -/
 @[local fun_prop] private lemma reg_deg : ComputableTidilyInDegree State.reg encState encReg 1 1 :=
-  of_linear (.of_dropFrame fun s => by simp [encState])
+  of_linear (.of_dropFrame fun s => by simp [encState_apply])
 
 /-- The register as a pair, the identity on encoded values. -/
 @[local fun_prop] private lemma toPair_deg :
     ComputableTidilyInDegree Reg.toPair encReg (encPair (encOption encCall) encBool) 1 1 :=
   of_eq fun _ => rfl
 
 /-- The fields of a frame, the identity on encoded values. -/
-private lemma fields_deg : ComputableTidilyInDegree Frame.fields encFrame encFrameFields 1 1 :=
+private lemma fields_deg : ComputableTidilyInDegree
+    (fun f : Frame => (f.level, f.src, f.dst, f.mid, f.phase)) encFrame encFrameFields 1 1 :=
   of_eq fun _ => rfl
 
 /-- The level of a frame. -/
@@ -355,8 +342,7 @@ private theorem step_eq (edge : List Bool → List Bool → Bool) (w : ℕ) (s :
 theorem length_encFrame (f : Frame) :
     (encFrame f).length =
       2 * f.level + 2 * f.src.length + 2 * f.dst.length + 2 * f.mid.length + 5 := by
-  change (encFrameFields f.fields).length = _
-  simp only [Frame.fields, length_encPair, encUnary_apply, encBits_apply, encBool_apply,
+  simp only [encFrame_apply, length_encPair, encUnary_apply, encBits_apply, encBool_apply,
     List.length_replicate, List.length_singleton]
   omega
 
@@ -374,7 +360,7 @@ theorem length_encReg_ret (b : Bool) : (encReg (.ret b)).length = 2 := rfl
 /-- The length of an encoded state. -/
 theorem length_encState (s : State) :
     (encState s).length = 2 * (encList encFrame s.stack).length + 1 + (encReg s.reg).length := by
-  simp [encState]
+  simp [encState_apply]
 
 /-! ### A step carrying the parameter of the edge test -/