sgl_xor_bridge

import Definitions.Def_sgl_capped_adv

/-!
# What the xor walk computes, in the decode's terms

The machine reads cells and pads with blanks; the decode reads Booleans and
pads with `false`.  `cellBool` was chosen to make these agree, and this is the
lemma that says so: the walk's output over a window of the encoded tape is
exactly the zip of the query against the decoded segment, bit for bit,
including the positions past the encoding's end.
-/

namespace SipserGacsLautemann

/-- Reading a dropped mapped list's head, as the underlying `getD`. -/
theorem cellBool_headD_drop (enc : List Bool) :
    ∀ s : Nat,
      cellBool (((enc.map TapeSymbol.bit).drop s).headD TapeSymbol.blank) =
        enc.getD s false := by
  induction enc with
  | nil => intro s; cases s <;> rfl
  | cons b bs ih =>
      intro s
      cases s with
      | zero => rfl
      | succ s => exact ih s

/-- Dropping one more. -/
theorem tail_drop_map (l : List TapeSymbol) (s : Nat) :
    (l.drop s).tail = l.drop (s + 1) := by
  induction l generalizing s with
  | nil => cases s <;> rfl
  | cons c cs ih =>
      cases s with
      | zero => rfl
      | succ s => exact ih s

/-- The padded segment, as a list. -/
def segList (enc : List Bool) (s n : Nat) : List Bool :=
  List.ofFn fun j : Fin n => enc.getD (s + j.val) false

theorem segList_succ (enc : List Bool) (s n : Nat) :
    segList enc s (n + 1) =
      enc.getD s false :: segList enc (s + 1) n := by
  rw [segList, segList, List.ofFn_succ]
  refine congrArg₂ List.cons ?_ ?_
  · simp
  · refine congrArg List.ofFn (funext fun i => ?_)
    have harith : s + (i.val + 1) = s + 1 + i.val := by omega
    show List.getD enc (s + (i.val + 1)) false =
      List.getD enc (s + 1 + i.val) false
    rw [harith]

/-- **The walk computes the zip against the decoded segment.** -/
theorem xorCells_query (ys : List Bool) :
    ∀ (enc : List Bool) (s : Nat),
      xorCells (ys.map TapeSymbol.bit) ((enc.map TapeSymbol.bit).drop s) =
        (List.zipWith (· != ·) ys (segList enc s ys.length)).map
          TapeSymbol.bit := by
  induction ys with
  | nil => intro enc s; rfl
  | cons y ys ih =>
      intro enc s
      rw [show (y :: ys).length = ys.length + 1 from rfl, segList_succ]
      show TapeSymbol.bit (cellBool (TapeSymbol.bit y) !=
          cellBool (((enc.map TapeSymbol.bit).drop s).headD
            TapeSymbol.blank)) ::
          xorCells (ys.map TapeSymbol.bit)
            ((enc.map TapeSymbol.bit).drop s).tail = _
      rw [cellBool_headD_drop, tail_drop_map, ih enc (s + 1)]
      rfl

end SipserGacsLautemann