refactor(Encoding): hoist the pair projections out of the Cobham internals

Complexitylib/Classes/P/Cobham/Internal/BlockScan.lean

@@ -10,11 +10,12 @@ public import Complexitylib.Classes.P.Cobham.Internal.Vec
 /-!
 # What the block scanners compute — proof internals
 
-The two total parsers of a self-delimiting block — `Cobham.fstBlock` decodes the
-leading block's payload, `Cobham.sndBlock` returns the suffix after it — and the
-control states their scanners share. `Complexity.pairSplitCoreTM` handles only
-valid pair inputs, so the total decoders need machines of their own; those are
-`Internal.SndBlock`, `Internal.FstBlock` and `Internal.Cat`, one per machine.
+The two total parsers of a self-delimiting block — `pairFst` decodes the
+leading block's payload, `pairSnd` returns the suffix after it (both defined in
+`Complexitylib.Encoding.Pairing`) — and the control states their scanners
+share. `Complexity.pairSplitCoreTM` handles only valid pair inputs, so the total
+decoders need machines of their own; those are `Internal.SndBlock`,
+`Internal.FstBlock` and `Internal.Cat`, one per machine.
 -/
 
 
@@ -24,43 +25,18 @@ namespace Complexity
 
 namespace Cobham
 
-/-- Decode the payload of the leading self-delimiting block: read doubled bits
-until the `[false, true]` separator. On a valid pair `pair x y` this
-returns `x` (see `fstBlock_pair`); on malformed input it returns the bits decoded
-so far. This total, incremental form is what the `fstBlockTM` scanner computes. -/
-def fstBlock : List Bool → List Bool
-  | false :: false :: z => false :: fstBlock z
-  | true :: true :: z => true :: fstBlock z
-  | _ => []
-
-/-- Take the suffix after the leading self-delimiting block (the second `unpair?`
-component), or `[]` if the input is not a valid block. On `encodeVec` of a
-nonempty vector this returns the head component `v 0`. -/
-def sndBlock (z : List Bool) : List Bool :=
-  match unpair? z with
-  | some (_, s) => s
-  | none => []
-
-@[simp] theorem fstBlock_pair (x y : List Bool) : fstBlock (pair x y) = x := by
-  induction x with
-  | nil => rfl
-  | cons b x ih => cases b <;> (rw [pair_cons_eq]; simp [fstBlock, ih])
-
-@[simp] theorem sndBlock_pair (x y : List Bool) : sndBlock (pair x y) = y := by
-  simp [sndBlock]
-
 /-- Stripping the head component of an encoded vector yields the encoded tail.
 (Not a `simp` lemma: `simp` already reaches this via `encodeVec_succ` and
-`fstBlock_pair`.) -/
+`pairFst_pair`.) -/
 theorem fstBlock_encodeVec_succ {n : ℕ} (v : Fin (n + 1) → List Bool) :
-    fstBlock (encodeVec v) = encodeVec (Fin.tail v) := by
+    pairFst (encodeVec v) = encodeVec (Fin.tail v) := by
   simp
 
 /-- The suffix of an encoded vector is its head component.
 (Not a `simp` lemma: `simp` already reaches this via `encodeVec_succ` and
-`sndBlock_pair`.) -/
+`pairSnd_pair`.) -/
 theorem sndBlock_encodeVec_succ {n : ℕ} (v : Fin (n + 1) → List Bool) :
-    sndBlock (encodeVec v) = v 0 := by
+    pairSnd (encodeVec v) = v 0 := by
   simp
 
 /-- Control states of the block-decoding scanners. -/

Complexitylib/Classes/P/Cobham/Internal/Cat.lean

@@ -33,7 +33,7 @@ open Complexity.TM
 
 /-! ### Concatenation
 
-`catBlocks` is `fstBlock` and `sndBlock` fused: decode the leading block's
+`catBlocks` is `pairFst` and `pairSnd` fused: decode the leading block's
 payload *and* keep the suffix, so on a genuine pair it is concatenation. Its
 machine is `sndBlockTM` with the scan also emitting each decoded bit — the one
 `FP` primitive that lets two computed strings be joined. -/

Complexitylib/Classes/P/Cobham/Internal/FstBlock.lean

@@ -32,7 +32,7 @@ open Complexity.TM
 
 /-- The payload decoder: scan doubled payload bits, emitting each decoded bit to
 the output, until the `[false, true]` separator or end of input. Computes
-`fstBlock`. -/
+`pairFst`. -/
 def fstBlockTM : TM 0 where
   Q := ScanPhase
   qstart := .skip
@@ -94,14 +94,14 @@ def fstBlockTM : TM 0 where
     | .done => exact rightOfStart_allIdle iHead wHeads oHead
 
 /-- The scan of `fstBlockTM`: from `scanA` on input `w` with output holding `acc`,
-the machine emits the decoded payload of `w`, halting with `acc ++ fstBlock w`. -/
+the machine emits the decoded payload of `w`, halting with `acc ++ pairFst w`. -/
 private theorem fstBlockTM_scan_loop :
     ∀ (fuel : ℕ) (w acc : List Bool), w.length ≤ fuel → ∀ (c : Cfg 0 fstBlockTM.Q),
       c.state = ScanPhase.scanA →
       c.input.HasBinarySuffix w →
       c.output.HasBinaryPrefix acc →
       ∃ c' t, t ≤ 2 * w.length + 2 ∧ fstBlockTM.reachesIn t c c' ∧ fstBlockTM.halted c' ∧
-        c'.output.HasBinaryPrefix (acc ++ fstBlock w) := by
+        c'.output.HasBinaryPrefix (acc ++ pairFst w) := by
   intro fuel
   induction fuel with
   | zero =>
@@ -119,7 +119,7 @@ private theorem fstBlockTM_scan_loop :
         .step (by simp [TM.step, hstate, fstBlockTM, hread]) .zero, rfl, ?_⟩
       rw [show c.output.writeAndMove (readBackWrite c.output.read) (idleDir c.output.read)
           = c.output from Tape.writeAndMove_readBack_idle_of_ne_start _ houtne]
-      simpa [fstBlock] using hpre
+      simpa [pairFst] using hpre
   | succ fuel ih =>
       intro w acc hw c hstate hsuf hpre
       have houtne : c.output.read ≠ Γ.start := by rw [hpre.read_blank]; decide
@@ -135,7 +135,7 @@ private theorem fstBlockTM_scan_loop :
             .step (by simp [TM.step, hstate, fstBlockTM, hread]) .zero, rfl, ?_⟩
           rw [show c.output.writeAndMove (readBackWrite c.output.read) (idleDir c.output.read)
               = c.output from Tape.writeAndMove_readBack_idle_of_ne_start _ houtne]
-          simpa [fstBlock] using hpre
+          simpa [pairFst] using hpre
       | [false] =>
           have hread : c.input.read = Γ.ofBool false := hsuf.read_cons
           let c1 : Cfg 0 fstBlockTM.Q :=
@@ -163,7 +163,7 @@ private theorem fstBlockTM_scan_loop :
             .step hstep (.step (by simp [TM.step, fstBlockTM, hread1, c1]) .zero), rfl, ?_⟩
           rw [show c1.output.writeAndMove (readBackWrite c1.output.read) (idleDir c1.output.read)
               = c1.output from Tape.writeAndMove_readBack_idle_of_ne_start _ houtne1]
-          simpa [fstBlock] using hpre1
+          simpa [pairFst] using hpre1
       | [true] =>
           have hread : c.input.read = Γ.ofBool true := hsuf.read_cons
           let c1 : Cfg 0 fstBlockTM.Q :=
@@ -191,7 +191,7 @@ private theorem fstBlockTM_scan_loop :
             .step hstep (.step (by simp [TM.step, fstBlockTM, hread1, c1]) .zero), rfl, ?_⟩
           rw [show c1.output.writeAndMove (readBackWrite c1.output.read) (idleDir c1.output.read)
               = c1.output from Tape.writeAndMove_readBack_idle_of_ne_start _ houtne1]
-          simpa [fstBlock] using hpre1
+          simpa [pairFst] using hpre1
       | false :: true :: y =>
           have hreadA : c.input.read = Γ.ofBool false := hsuf.read_cons
           let c1 : Cfg 0 fstBlockTM.Q :=
@@ -220,7 +220,7 @@ private theorem fstBlockTM_scan_loop :
             rfl, ?_⟩
           rw [show c1.output.writeAndMove (readBackWrite c1.output.read) (idleDir c1.output.read)
               = c1.output from Tape.writeAndMove_readBack_idle_of_ne_start _ houtne1]
-          simpa [fstBlock] using hpre1
+          simpa [pairFst] using hpre1
       | true :: false :: rest =>
           have hreadA : c.input.read = Γ.ofBool true := hsuf.read_cons
           let c1 : Cfg 0 fstBlockTM.Q :=
@@ -249,7 +249,7 @@ private theorem fstBlockTM_scan_loop :
             rfl, ?_⟩
           rw [show c1.output.writeAndMove (readBackWrite c1.output.read) (idleDir c1.output.read)
               = c1.output from Tape.writeAndMove_readBack_idle_of_ne_start _ houtne1]
-          simpa [fstBlock] using hpre1
+          simpa [pairFst] using hpre1
       | false :: false :: z =>
           have hreadA : c.input.read = Γ.ofBool false := hsuf.read_cons
           let c1 : Cfg 0 fstBlockTM.Q :=
@@ -286,7 +286,7 @@ private theorem fstBlockTM_scan_loop :
             ih z (acc ++ [false]) hzfuel c2 rfl hsuf2 hpre2
           refine ⟨c', t + 1 + 1, by simp only [List.length_cons]; omega,
             .step hstepA (.step hstepB hreach), hhalt, ?_⟩
-          have hfb : fstBlock (false :: false :: z) = false :: fstBlock z := rfl
+          have hfb : pairFst (false :: false :: z) = false :: pairFst z := rfl
           rw [hfb, List.append_assoc, List.cons_append, List.nil_append] at *
           exact hcout
       | true :: true :: z =>
@@ -325,12 +325,12 @@ private theorem fstBlockTM_scan_loop :
             ih z (acc ++ [true]) hzfuel c2 rfl hsuf2 hpre2
           refine ⟨c', t + 1 + 1, by simp only [List.length_cons]; omega,
             .step hstepA (.step hstepB hreach), hhalt, ?_⟩
-          have hfb : fstBlock (true :: true :: z) = true :: fstBlock z := rfl
+          have hfb : pairFst (true :: true :: z) = true :: pairFst z := rfl
           rw [hfb, List.append_assoc, List.cons_append, List.nil_append] at *
           exact hcout
 
-/-- `fstBlock` is polynomial-time, via the `fstBlockTM` scanner. -/
-theorem fstBlock_mem_FP : fstBlock ∈ FP := by
+/-- `pairFst` is polynomial-time, via the `fstBlockTM` scanner. -/
+theorem fstBlock_mem_FP : pairFst ∈ FP := by
   refine ⟨1, 0, fstBlockTM, (fun m => 2 * m + 3), ?_, ?_⟩
   · intro z
     let c1 : Cfg 0 fstBlockTM.Q :=

Complexitylib/Classes/P/Cobham/Internal/Reorder.lean

@@ -33,23 +33,23 @@ open Complexity.TM
 
 /-- Drop the third component of a right-nested triple. Copy doubled payload bits
 verbatim until the `[false, true]` separator, then decode the *next* block's
-payload (`fstBlock`). On a valid triple this satisfies
+payload (`pairFst`). On a valid triple this satisfies
 `reorder (pair A (pair B C)) = pair A B` (`reorder_pair_pair`). The incremental
 recursion (writing before knowing validity) is what the `reorderTM` scanner
 computes; it is total and needs no sub-machines. -/
 def reorder : List Bool → List Bool
   | false :: false :: z => false :: false :: reorder z
   | true :: true :: z => true :: true :: reorder z
-  | false :: true :: z => false :: true :: fstBlock z
+  | false :: true :: z => false :: true :: pairFst z
   | c :: _ => [c]
   | [] => []
 
 theorem reorder_pair_pair (A B C : List Bool) :
     reorder (pair A (pair B C)) = pair A B := by
   induction A with
   | nil =>
-      show false :: true :: fstBlock (pair B C) = false :: true :: B
-      rw [fstBlock_pair]
+      show false :: true :: pairFst (pair B C) = false :: true :: B
+      rw [pairFst_pair]
   | cons a A ih =>
       rw [pair_cons_eq]
       cases a
@@ -176,15 +176,15 @@ def reorderTM : TM 0 where
     | .rdone => exact rightOfStart_allIdle iHead wHeads oHead
 
 /-- Phase 2 of `reorderTM`: from `rdecA` on input `w` with output holding `acc`,
-decode and emit `fstBlock w`, halting with `acc ++ fstBlock w`. Identical in shape
+decode and emit `pairFst w`, halting with `acc ++ pairFst w`. Identical in shape
 to `fstBlockTM_scan_loop`. -/
 private theorem reorderTM_dec_loop :
     ∀ (fuel : ℕ) (w acc : List Bool), w.length ≤ fuel → ∀ (c : Cfg 0 reorderTM.Q),
       c.state = ReorderPhase.rdecA →
       c.input.HasBinarySuffix w →
       c.output.HasBinaryPrefix acc →
       ∃ c' t, t ≤ 2 * w.length + 2 ∧ reorderTM.reachesIn t c c' ∧ reorderTM.halted c' ∧
-        c'.output.HasBinaryPrefix (acc ++ fstBlock w) := by
+        c'.output.HasBinaryPrefix (acc ++ pairFst w) := by
   intro fuel
   induction fuel with
   | zero =>
@@ -202,7 +202,7 @@ private theorem reorderTM_dec_loop :
         .step (by simp [TM.step, hstate, reorderTM, hread]) .zero, rfl, ?_⟩
       rw [show c.output.writeAndMove (readBackWrite c.output.read) (idleDir c.output.read)
           = c.output from Tape.writeAndMove_readBack_idle_of_ne_start _ houtne]
-      simpa [fstBlock] using hpre
+      simpa [pairFst] using hpre
   | succ fuel ih =>
       intro w acc hw c hstate hsuf hpre
       have houtne : c.output.read ≠ Γ.start := by rw [hpre.read_blank]; decide
@@ -218,7 +218,7 @@ private theorem reorderTM_dec_loop :
             .step (by simp [TM.step, hstate, reorderTM, hread]) .zero, rfl, ?_⟩
           rw [show c.output.writeAndMove (readBackWrite c.output.read) (idleDir c.output.read)
               = c.output from Tape.writeAndMove_readBack_idle_of_ne_start _ houtne]
-          simpa [fstBlock] using hpre
+          simpa [pairFst] using hpre
       | [false] =>
           have hread : c.input.read = Γ.ofBool false := hsuf.read_cons
           let c1 : Cfg 0 reorderTM.Q :=
@@ -246,7 +246,7 @@ private theorem reorderTM_dec_loop :
             .step hstep (.step (by simp [TM.step, reorderTM, hread1, c1]) .zero), rfl, ?_⟩
           rw [show c1.output.writeAndMove (readBackWrite c1.output.read) (idleDir c1.output.read)
               = c1.output from Tape.writeAndMove_readBack_idle_of_ne_start _ houtne1]
-          simpa [fstBlock] using hpre1
+          simpa [pairFst] using hpre1
       | [true] =>
           have hread : c.input.read = Γ.ofBool true := hsuf.read_cons
           let c1 : Cfg 0 reorderTM.Q :=
@@ -274,7 +274,7 @@ private theorem reorderTM_dec_loop :
             .step hstep (.step (by simp [TM.step, reorderTM, hread1, c1]) .zero), rfl, ?_⟩
           rw [show c1.output.writeAndMove (readBackWrite c1.output.read) (idleDir c1.output.read)
               = c1.output from Tape.writeAndMove_readBack_idle_of_ne_start _ houtne1]
-          simpa [fstBlock] using hpre1
+          simpa [pairFst] using hpre1
       | false :: true :: y =>
           have hreadA : c.input.read = Γ.ofBool false := hsuf.read_cons
           let c1 : Cfg 0 reorderTM.Q :=
@@ -303,7 +303,7 @@ private theorem reorderTM_dec_loop :
             rfl, ?_⟩
           rw [show c1.output.writeAndMove (readBackWrite c1.output.read) (idleDir c1.output.read)
               = c1.output from Tape.writeAndMove_readBack_idle_of_ne_start _ houtne1]
-          simpa [fstBlock] using hpre1
+          simpa [pairFst] using hpre1
       | true :: false :: rest =>
           have hreadA : c.input.read = Γ.ofBool true := hsuf.read_cons
           let c1 : Cfg 0 reorderTM.Q :=
@@ -332,7 +332,7 @@ private theorem reorderTM_dec_loop :
             rfl, ?_⟩
           rw [show c1.output.writeAndMove (readBackWrite c1.output.read) (idleDir c1.output.read)
               = c1.output from Tape.writeAndMove_readBack_idle_of_ne_start _ houtne1]
-          simpa [fstBlock] using hpre1
+          simpa [pairFst] using hpre1
       | false :: false :: z =>
           have hreadA : c.input.read = Γ.ofBool false := hsuf.read_cons
           let c1 : Cfg 0 reorderTM.Q :=
@@ -369,7 +369,7 @@ private theorem reorderTM_dec_loop :
             ih z (acc ++ [false]) hzfuel c2 rfl hsuf2 hpre2
           refine ⟨c', t + 1 + 1, by simp only [List.length_cons]; omega,
             .step hstepA (.step hstepB hreach), hhalt, ?_⟩
-          have hfb : fstBlock (false :: false :: z) = false :: fstBlock z := rfl
+          have hfb : pairFst (false :: false :: z) = false :: pairFst z := rfl
           rw [hfb, List.append_assoc, List.cons_append, List.nil_append] at *
           exact hcout
       | true :: true :: z =>
@@ -408,7 +408,7 @@ private theorem reorderTM_dec_loop :
             ih z (acc ++ [true]) hzfuel c2 rfl hsuf2 hpre2
           refine ⟨c', t + 1 + 1, by simp only [List.length_cons]; omega,
             .step hstepA (.step hstepB hreach), hhalt, ?_⟩
-          have hfb : fstBlock (true :: true :: z) = true :: fstBlock z := rfl
+          have hfb : pairFst (true :: true :: z) = true :: pairFst z := rfl
           rw [hfb, List.append_assoc, List.cons_append, List.nil_append] at *
           exact hcout
 
@@ -557,7 +557,7 @@ private theorem reorderTM_copy_loop :
             reorderTM_dec_loop fuel y (acc ++ [false, true]) hyfuel c2 rfl hsuf2 hpre2
           refine ⟨c', t + 1 + 1, by simp only [List.length_cons]; omega,
             .step hstepA (.step hstepB hreach), hhalt, ?_⟩
-          have hr : reorder (false :: true :: y) = false :: true :: fstBlock y := rfl
+          have hr : reorder (false :: true :: y) = false :: true :: pairFst y := rfl
           rw [hr]
           rwa [List.append_assoc] at hcout
       | false :: false :: z =>