TapeZipper.lean

/-
The two-stack zipper for an ordinary single-head Turing machine tape.

A tape is held as `left` (the cells strictly left of the head, nearest first),
`cur` (the scanned cell), and `right` (the cells strictly right of the head,
nearest first).  `left` and `right` are *finite* lists; a position beyond
either list reads as the blank symbol.  This is the distinction the packet
requires: an empty stack is not a blank cell, it is the absence of any
recorded cell, and reading there yields blank.

`get` gives the cell at an offset from the head, so the four shift equations
for each move say exactly that a move slides the window by one and writes the
outgoing symbol into the cell the head is leaving.
-/

import FPRDTransfer.StackMachine

namespace FPRD

/-- Head motion for one tape in one transition. -/
inductive Move where
  | left : Move
  | right : Move
  | stay : Move

/-- A tape as a zipper: two finite lists and the scanned symbol. -/
structure Tape (T : Type) where
  left : List T
  cur : T
  right : List T

namespace Tape

variable {T : Type}

/-- The cell at a signed offset from the head.  Offsets beyond the recorded
lists read as the blank symbol `b`. -/
def get (t : Tape T) (b : T) : Int → T
  | Int.ofNat 0 => t.cur
  | Int.ofNat (n + 1) => t.right.getD n b
  | Int.negSucc n => t.left.getD n b

/-- Write `a` under the head and move right.  One `push` on `left`, one `pop`
on `right`; the new scanned symbol is the old top of `right`, or blank. -/
def moveRight (t : Tape T) (a b : T) : Tape T where
  left := a :: t.left
  cur := t.right.headD b
  right := t.right.tail

/-- Write `a` under the head and move left. -/
def moveLeft (t : Tape T) (a b : T) : Tape T where
  left := t.left.tail
  cur := t.left.headD b
  right := a :: t.right

/-- Write `a` under the head and stay.  Both stacks are kept. -/
def stay (t : Tape T) (a : T) : Tape T where
  left := t.left
  cur := a
  right := t.right

/-! ### The window really shifts

Each group of equations pins `get` on the whole of `Int`, so together they say
the zipper behaves as a bi-infinite blank-padded tape.  These equations are
model-interface checks.  The operational transfer proof below uses the
projection lemmas `apply_left`, `apply_right`, and `apply_cur`; the final
machine-to-scaffold theorem separately proves equality through `Tape.get`. -/

@[simp] theorem stay_get_zero (t : Tape T) (a b : T) : (t.stay a).get b 0 = a := rfl

@[simp] theorem stay_get_pos (t : Tape T) (a b : T) (n : Nat) :
    (t.stay a).get b (Int.ofNat (n + 1)) = t.right.getD n b := rfl

@[simp] theorem stay_get_neg (t : Tape T) (a b : T) (n : Nat) :
    (t.stay a).get b (Int.negSucc n) = t.left.getD n b := rfl

theorem moveRight_get_zero (t : Tape T) (a b : T) :
    (t.moveRight a b).get b 0 = t.right.getD 0 b := by
  obtain ⟨L, c, R⟩ := t
  cases R <;> rfl

theorem moveRight_get_pos (t : Tape T) (a b : T) (n : Nat) :
    (t.moveRight a b).get b (Int.ofNat (n + 1)) = t.right.getD (n + 1) b := by
  obtain ⟨L, c, R⟩ := t
  cases R <;> rfl

theorem moveRight_get_neg_zero (t : Tape T) (a b : T) :
    (t.moveRight a b).get b (Int.negSucc 0) = a := rfl

theorem moveRight_get_neg_succ (t : Tape T) (a b : T) (n : Nat) :
    (t.moveRight a b).get b (Int.negSucc (n + 1)) = t.left.getD n b := rfl

theorem moveLeft_get_zero (t : Tape T) (a b : T) :
    (t.moveLeft a b).get b 0 = t.left.getD 0 b := by
  obtain ⟨L, c, R⟩ := t
  cases L <;> rfl

theorem moveLeft_get_pos_zero (t : Tape T) (a b : T) :
    (t.moveLeft a b).get b (Int.ofNat 1) = a := rfl

theorem moveLeft_get_pos_succ (t : Tape T) (a b : T) (n : Nat) :
    (t.moveLeft a b).get b (Int.ofNat (n + 2)) = t.right.getD n b := rfl

theorem moveLeft_get_neg (t : Tape T) (a b : T) (n : Nat) :
    (t.moveLeft a b).get b (Int.negSucc n) = t.left.getD (n + 1) b := by
  obtain ⟨L, c, R⟩ := t
  cases L <;> rfl

/-! ### The zipper's stack actions

Each move is at most one action per stack, which is what lets one appended
scaffold node carry a whole multitape transition. -/

/-- The action on the `left` stack. -/
def leftOp (a : T) : Move → StackOp T
  | .right => .push a
  | .left => .pop
  | .stay => .keep

/-- The action on the `right` stack. -/
def rightOp (a : T) : Move → StackOp T
  | .right => .pop
  | .left => .push a
  | .stay => .keep

/-- The new scanned symbol after writing `a` and moving. -/
def nextCur (t : Tape T) (a b : T) : Move → T
  | .right => t.right.headD b
  | .left => t.left.headD b
  | .stay => a

/-- Applying the move to the zipper. -/
def apply (t : Tape T) (a b : T) : Move → Tape T
  | .right => t.moveRight a b
  | .left => t.moveLeft a b
  | .stay => t.stay a

/-- The zipper's `left` list is exactly what `leftOp` does to it. -/
theorem apply_left (t : Tape T) (a b : T) (mv : Move) :
    (t.apply a b mv).left = (leftOp a mv).apply t.left := by
  cases mv <;> rfl

/-- The zipper's `right` list is exactly what `rightOp` does to it. -/
theorem apply_right (t : Tape T) (a b : T) (mv : Move) :
    (t.apply a b mv).right = (rightOp a mv).apply t.right := by
  cases mv <;> rfl

/-- The new scanned symbol is a function of the finite control plus the two
stack tops, so it can live in the control. -/
theorem apply_cur (t : Tape T) (a b : T) (mv : Move) :
    (t.apply a b mv).cur = nextCur t a b mv := by
  cases mv <;> rfl

theorem headD_eq_head? (l : List T) (b : T) :
    l.headD b = (l.head?).getD b := by
  cases l <;> rfl

/-- `nextCur` depends on the tapes only through the two stack tops. -/
theorem nextCur_of_tops (t : Tape T) (a b : T) (mv : Move) :
    nextCur t a b mv =
      match mv with
      | .right => (t.right.head?).getD b
      | .left => (t.left.head?).getD b
      | .stay => a := by
  cases mv
  · simp only [nextCur]; exact headD_eq_head? t.left b
  · simp only [nextCur]; exact headD_eq_head? t.right b
  · rfl

end Tape

end FPRD