sgl_power

import Definitions.Def_sgl_multiply

/-!
# Raising a run to a power

`c · (n + 1)^d` marks, from a run of `n`: multiply `d` times, ping-ponging
between two scratch tapes, then `c` more tallies into the final run.

The recursion is at the meta level — `d` is a number known when the machine is
built, so the machine for degree `d + 1` is the machine for degree `d` followed
by one multiplication.  No tape has to count to `d`.

Each multiplication reads the run built so far as its multiplier and lays down
one copy of the base per mark, so the run grows from `(n+1)^d` to
`(n+1)^d · (n+1)`.  The `+ 1` in the base is the reason the guide gets one
bump before the recursion starts: a multiplier of zero marks would stall the
loop, and `n + 1 ≥ 1` never does.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- One padding mark, then one tally per input cell: a run of `n + 1`. -/
def basePlusOne (src dst : Fin tapes) :=
  (putMark dst).andThen fun _ => copyTally src dst

set_option maxHeartbeats 1000000 in
/-- The base run: `n + 1` marks on a virgin tape. -/
theorem basePlusOne_spec (src dst : Fin tapes) (hsd : src ≠ dst)
    (x Ls Rs : List TapeSymbol) (T : Fin tapes → Tape)
    (hnb : ∀ c ∈ x, c ≠ TapeSymbol.blank)
    (hsrc : T src = cellsTape (TapeSymbol.blank :: Ls)
      (x ++ TapeSymbol.blank :: Rs))
    (hdst : T dst = cellsTape [] []) :
    ∃ cost : Nat,
      HaltsExactly (basePlusOne src dst)
        ((basePlusOne src dst).startCfg T) cost true ∧
      (((basePlusOne src dst).step^[cost])
        ((basePlusOne src dst).startCfg T)).tape =
        Function.update T dst
          (cellsTape (List.replicate (x.length + 1) (TapeSymbol.bit true)) []) := by
  classical
  obtain ⟨g1, s1⟩ := putMark_spec dst [] [] T hdst
  set T1 := Function.update T dst
    (cellsTape [TapeSymbol.bit true] ([] : List TapeSymbol).tail) with hT1
  have hT1src : T1 src = cellsTape (TapeSymbol.blank :: Ls)
      (x ++ TapeSymbol.blank :: Rs) := by
    rw [hT1, Function.update_of_ne hsd]
    exact hsrc
  have hT1dst : T1 dst = cellsTape [TapeSymbol.bit true] [] := by
    rw [hT1, Function.update_self]
    rfl
  obtain ⟨c2, g2, s2⟩ := copyTally_spec src dst hsd x Ls Rs
    [TapeSymbol.bit true] [] T1 hnb hT1src hT1dst
  have hch := chainStepC g1 s1 g2
  refine ⟨_, hch.1, ?_⟩
  have hfin : ((basePlusOne src dst).step^[_])
      ((basePlusOne src dst).startCfg T) = _ := hch.2
  rw [hfin]
  show (((copyTally src dst).step^[c2])
    ((copyTally src dst).startCfg T1)).tape = _
  rw [s2, hT1, Function.update_idem]
  congr 1
  show cellsTape (List.replicate x.length (TapeSymbol.bit true) ++
    [TapeSymbol.bit true]) (([] : List TapeSymbol).drop x.length) = _
  rw [show List.replicate x.length (TapeSymbol.bit true) ++
      [TapeSymbol.bit true] =
      List.replicate (x.length + 1) (TapeSymbol.bit true) from
    List.replicate_succ'.symm]
  cases hx : x.length with
  | zero => rfl
  | succ k => simp

set_option maxHeartbeats 1000000 in
/-- The base run, laid on top of an existing left context.  The seed tape
carries an origin marker, so this is the form the recursion actually uses. -/
theorem basePlusOne_at (src dst : Fin tapes) (hsd : src ≠ dst)
    (x Ls Rs Ld : List TapeSymbol) (T : Fin tapes → Tape)
    (hnb : ∀ c ∈ x, c ≠ TapeSymbol.blank)
    (hsrc : T src = cellsTape (TapeSymbol.blank :: Ls)
      (x ++ TapeSymbol.blank :: Rs))
    (hdst : T dst = cellsTape Ld []) :
    ∃ cost : Nat,
      HaltsExactly (basePlusOne src dst)
        ((basePlusOne src dst).startCfg T) cost true ∧
      (((basePlusOne src dst).step^[cost])
        ((basePlusOne src dst).startCfg T)).tape =
        Function.update T dst
          (cellsTape (List.replicate (x.length + 1) (TapeSymbol.bit true)
            ++ Ld) []) := by
  classical
  obtain ⟨g1, s1⟩ := putMark_spec dst Ld [] T hdst
  set T1 := Function.update T dst
    (cellsTape (TapeSymbol.bit true :: Ld) ([] : List TapeSymbol).tail)
    with hT1
  have hT1src : T1 src = cellsTape (TapeSymbol.blank :: Ls)
      (x ++ TapeSymbol.blank :: Rs) := by
    rw [hT1, Function.update_of_ne hsd]
    exact hsrc
  have hT1dst : T1 dst = cellsTape (TapeSymbol.bit true :: Ld) [] := by
    rw [hT1, Function.update_self]
    rfl
  obtain ⟨c2, g2, s2⟩ := copyTally_spec src dst hsd x Ls Rs
    (TapeSymbol.bit true :: Ld) [] T1 hnb hT1src hT1dst
  have hch := chainStepC g1 s1 g2
  refine ⟨_, hch.1, ?_⟩
  have hfin : ((basePlusOne src dst).step^[_])
      ((basePlusOne src dst).startCfg T) = _ := hch.2
  rw [hfin]
  show (((copyTally src dst).step^[c2])
    ((copyTally src dst).startCfg T1)).tape = _
  rw [s2, hT1, Function.update_idem]
  congr 1
  show cellsTape (List.replicate x.length (TapeSymbol.bit true) ++
    (TapeSymbol.bit true :: Ld)) (([] : List TapeSymbol).drop x.length) = _
  rw [show List.replicate x.length (TapeSymbol.bit true) ++
      (TapeSymbol.bit true :: Ld) =
      List.replicate (x.length + 1) (TapeSymbol.bit true) ++ Ld by
    rw [List.replicate_succ']
    simp]
  cases hx : x.length with
  | zero => rfl
  | succ k => simp

end SipserGacsLautemann