sgl_mul_loop

import Definitions.Def_sgl_mark_times
import Definitions.Def_sgl_walk_costs
import Definitions.Def_sgl_left_loop
import Definitions.Def_sgl_clog_loop

/-!
# Multiplying two tallies

One tally pass per mark of the multiplier: the multiplicand's marks are laid
down again and again onto the accumulator, which therefore grows by the
product.  The tally pass restores its source, so nothing has to be rewound
between rounds.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- One round: consume a multiplier mark, add the multiplicand's count. -/
noncomputable def mulBody (a b c : Fin tapes) := leftBody a (tallyOnto b c)

/-- The multiplication loop. -/
noncomputable def mulLoop (a b c : Fin tapes) :=
  (mulBody a b c).repeatUntilFalse

/-- The loop invariant: `j` multiplier marks left, the multiplicand rewound,
`w` marks on the accumulator. -/
def MulInv (a b c : Fin tapes) (j n w : Nat)
    (La Ra Lb Lc : List TapeSymbol) (T : Fin tapes → Tape) : Prop :=
  T a = cellsTape
    (List.replicate j (TapeSymbol.bit true) ++ TapeSymbol.blank :: La) Ra ∧
  T b = cellsTape (TapeSymbol.blank :: Lb)
    (List.replicate n (TapeSymbol.bit true) ++ TapeSymbol.blank :: []) ∧
  T c = cellsTape (List.replicate w (TapeSymbol.bit true) ++ Lc) []

set_option maxHeartbeats 1000000 in
/-- **One multiplication round.** -/
theorem mulRound (a b c : Fin tapes) (hab : a ≠ b) (hac : a ≠ c)
    (hbc : b ≠ c) (j n w : Nat) (La Ra Lb Lc : List TapeSymbol)
    (T : Fin tapes → Tape)
    (hInv : MulInv a b c (j + 1) n w La Ra Lb Lc T) :
    ∃ cost : Nat,
      cost ≤ 9 * n + 15 ∧
      HaltsExactly (mulBody a b c) ((mulBody a b c).startCfg T) cost true ∧
      MulInv a b c j n (n + w) La
        (TapeSymbol.bit true :: (Ra.headD TapeSymbol.blank :: Ra.tail))
        Lb Lc
        ((((mulBody a b c).step^[cost])
          ((mulBody a b c).startCfg T)).tape) ∧
      (∀ k, k ≠ a → k ≠ c →
        (((mulBody a b c).step^[cost])
          ((mulBody a b c).startCfg T)).tape k = T k) := by
  classical
  obtain ⟨ha, hb, hc⟩ := hInv
  set T1 := Function.update T a (moveDir HeadMove.left (T a)) with hT1
  have hT1a : T1 a = cellsTape
      (List.replicate j (TapeSymbol.bit true) ++ TapeSymbol.blank :: La)
      (TapeSymbol.bit true :: (Ra.headD TapeSymbol.blank :: Ra.tail)) := by
    rw [hT1, Function.update_self, ha,
      show List.replicate (j + 1) (TapeSymbol.bit true) =
        TapeSymbol.bit true :: List.replicate j (TapeSymbol.bit true)
        from rfl, cellsTape_moveLeft_headD]
    rfl
  have hmark : (T1 a).head ≠ TapeSymbol.blank := by
    rw [hT1a]
    show (TapeSymbol.bit true ::
      (Ra.headD TapeSymbol.blank :: Ra.tail)).headD TapeSymbol.blank ≠
      TapeSymbol.blank
    simp
  obtain ⟨ct, hct, gt, tt⟩ := tallyOnto_specB b c hbc
    (List.replicate n (TapeSymbol.bit true)) Lb []
    (List.replicate w (TapeSymbol.bit true) ++ Lc) [] T1
    (replicate_marks_nonblank n)
    (by rw [hT1, Function.update_of_ne hab.symm, hb])
    (by rw [hT1, Function.update_of_ne hac.symm, hc])
  rw [List.length_replicate] at hct tt
  obtain ⟨gbody, tbody⟩ := leftBody_mark a (tallyOnto b c) T
    (Function.update T1 c
      (cellsTape (List.replicate n (TapeSymbol.bit true) ++
        (List.replicate w (TapeSymbol.bit true) ++ Lc))
        (List.drop n []))) ct hmark (by rw [← hT1]; exact gt)
    (by rw [← hT1]; exact tt)
  refine ⟨_, by omega, gbody, ⟨?_, ?_, ?_⟩, ?_⟩
  · unfold mulBody
    rw [tbody, Function.update_of_ne hac, hT1a]
  · unfold mulBody
    rw [tbody, Function.update_of_ne hbc, hT1,
      Function.update_of_ne hab.symm, hb]
  · unfold mulBody
    rw [tbody, Function.update_self, List.drop_nil,
      show List.replicate n (TapeSymbol.bit true) ++
        (List.replicate w (TapeSymbol.bit true) ++ Lc) =
        List.replicate (n + w) (TapeSymbol.bit true) ++ Lc by
        rw [List.replicate_add, List.append_assoc]]
  · intro k hka hkc
    unfold mulBody
    rw [tbody, Function.update_of_ne hkc, hT1, Function.update_of_ne hka]

set_option maxHeartbeats 4000000 in
/-- **The product.**  One pass per multiplier mark leaves `j * n + w` marks
on the accumulator. -/
theorem mulLoop_run (a b c : Fin tapes) (hab : a ≠ b) (hac : a ≠ c)
    (hbc : b ≠ c) :
    ∀ (j n w : Nat) (La Ra Lb Lc : List TapeSymbol) (T : Fin tapes → Tape),
      MulInv a b c j n w La Ra Lb Lc T →
      ∃ cost : Nat,
        cost ≤ j * (9 * n + 16) + 5 ∧
        HaltsExactly (mulLoop a b c) ((mulLoop a b c).startCfg T) cost
          false ∧
        (((mulLoop a b c).step^[cost])
          ((mulLoop a b c).startCfg T)).tape c =
          cellsTape (List.replicate (j * n + w) (TapeSymbol.bit true) ++ Lc)
            [] ∧
        (((mulLoop a b c).step^[cost])
          ((mulLoop a b c).startCfg T)).tape a =
          cellsTape La (TapeSymbol.blank ::
            (List.replicate j (TapeSymbol.bit true) ++
              (Ra.headD TapeSymbol.blank :: Ra.tail))) ∧
        (∀ k, k ≠ a → k ≠ c →
          (((mulLoop a b c).step^[cost])
            ((mulLoop a b c).startCfg T)).tape k = T k) := by
  intro j
  induction j with
  | zero =>
      intro n w La Ra Lb Lc T hInv
      obtain ⟨ha, hb, hc⟩ := hInv
      have hblank : ((Function.update T a
          (moveDir HeadMove.left (T a)) a)).head = TapeSymbol.blank := by
        rw [Function.update_self, ha]
        show (moveDir HeadMove.left
          (cellsTape (TapeSymbol.blank :: La) Ra)).head = _
        rw [cellsTape_moveLeft_headD]
        rfl
      obtain ⟨gexit, texit⟩ := leftBody_blank a (tallyOnto b c) T hblank
      have htape : (((mulLoop a b c).step^[
          1 + 1 + (1 + 1 + (0 + 1 + 0))])
          ((mulLoop a b c).startCfg T)).tape =
          Function.update T a (moveDir HeadMove.left (T a)) := by
        show (((leftBody a (tallyOnto b c)).repeatUntilFalse.step^[
          1 + 1 + (1 + 1 + (0 + 1 + 0))])
          ((leftBody a (tallyOnto b c)).startCfg T)).tape = _
        rw [TypedMachine.repeatUntilFalse_iterate_fresh _ _ _ gexit.fresh]
        exact texit
      refine ⟨1 + 1 + (1 + 1 + (0 + 1 + 0)), by omega, ?_, ?_, ?_, ?_⟩
      · constructor
        · show (mulLoop a b c).result
            (((leftBody a (tallyOnto b c)).repeatUntilFalse.step^[
              1 + 1 + (1 + 1 + (0 + 1 + 0))])
              ((leftBody a (tallyOnto b c)).startCfg T)).state = some false
          exact (leftBody a (tallyOnto b c)).repeatUntilFalse_exit _ _ gexit
        · intro s hs
          show (mulLoop a b c).result
            (((leftBody a (tallyOnto b c)).repeatUntilFalse.step^[s])
              ((leftBody a (tallyOnto b c)).startCfg T)).state = none
          exact TypedMachine.repeatUntilFalse_pre_fresh _ _ _ _ gexit s hs
      · rw [htape, Function.update_of_ne hac.symm, hc, Nat.zero_mul,
          Nat.zero_add]
      · rw [htape, Function.update_self, ha,
          show List.replicate 0 (TapeSymbol.bit true) ++
            TapeSymbol.blank :: La = TapeSymbol.blank :: La from rfl,
          cellsTape_moveLeft_headD]
        rfl
      · intro k hka hkc
        rw [htape, Function.update_of_ne hka]
  | succ j ih =>
      intro n w La Ra Lb Lc T hInv
      obtain ⟨cb, hcb, ground, hInv', hroth⟩ := mulRound a b c hab hac hbc
        j n w La Ra Lb Lc T hInv
      obtain ⟨cost', hcost', hrest, hcfin, hafin, hoth⟩ := ih n (n + w) La
        (TapeSymbol.bit true :: (Ra.headD TapeSymbol.blank :: Ra.tail))
        Lb Lc
        ((((mulBody a b c).step^[cb])
          ((mulBody a b c).startCfg T)).tape) hInv'
      have hsh : (((mulLoop a b c).step^[cb + 1 + cost'])
          ((mulLoop a b c).startCfg T)) =
          (((mulLoop a b c).step^[cost'])
            ((mulLoop a b c).startCfg
              ((((mulBody a b c).step^[cb])
                ((mulBody a b c).startCfg T)).tape))) :=
        repeatUntilFalse_shift_tape (mulBody a b c)
          ((mulLoop a b c).startCfg T) cb cost' ground
      refine ⟨cb + 1 + cost', ?_, ?_, ?_, ?_, ?_⟩
      · have hexp : (j + 1) * (9 * n + 16) = j * (9 * n + 16) + (9 * n + 16) := by
          ring
        omega
      · exact repeatUntilFalse_shift (mulBody a b c)
          ((mulLoop a b c).startCfg T) cb cost' false ground hrest
      · rw [hsh, hcfin,
          show j * n + (n + w) = (j + 1) * n + w by ring]
      · rw [hsh, hafin]
        show cellsTape La (TapeSymbol.blank ::
          (List.replicate j (TapeSymbol.bit true) ++
            (TapeSymbol.bit true ::
              (Ra.headD TapeSymbol.blank :: Ra.tail)))) = _
        rw [show List.replicate j (TapeSymbol.bit true) ++
            (TapeSymbol.bit true ::
              (Ra.headD TapeSymbol.blank :: Ra.tail)) =
            List.replicate (j + 1) (TapeSymbol.bit true) ++
              (Ra.headD TapeSymbol.blank :: Ra.tail) by
          rw [List.replicate_succ', List.append_assoc]
          rfl]
      · intro k hka hkc
        rw [hsh, hoth k hka hkc]
        exact hroth k hka hkc

end SipserGacsLautemann