sgl_multiply

import Definitions.Def_sgl_marked_loop_inv
import Definitions.Def_sgl_tally2

/-!
# Multiplying in unary

A run of `m` marks times a run of `n` marks is `m` copies of the second run,
laid end to end.  `copyTally` appends one copy and restores its source, and
`markedLoop` repeats a subroutine once per mark — so the product is the two
composed, with nothing new to prove about either.

The one thing that has to be said afresh is the tally's *exact* cost.  Its
published specification hides the cost behind an existential, which is fine for
a single call and useless inside a loop, where every round must cost the same
known amount.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}


/-! ## The product -/

/-- The tally's effect on the tapes. -/
def tallyEffect (src dst : Fin tapes) (n : Nat) (T : Fin tapes → Tape) :
    Fin tapes → Tape :=
  Function.update T dst
    (cellsTape (List.replicate n (TapeSymbol.bit true) ++ (T dst).left)
      (((T dst).head :: (T dst).right).drop n))

theorem cellsTape_drop_blank (L : List TapeSymbol) (n : Nat) :
    cellsTape L (([TapeSymbol.blank] : List TapeSymbol).drop n) =
      cellsTape L [] := by
  cases n with
  | zero => rfl
  | succ n => simp

/-- **The product accumulates.**  After `r` rounds the target holds `r · n`
marks. -/
theorem tallyEffect_iterate (mult src dst : Fin tapes) (hdm : dst ≠ mult)
    (n : Nat) (Ldst : List TapeSymbol) :
    ∀ (r : Nat) (T : Fin tapes → Tape), T dst = cellsTape Ldst [] →
      (((markedStep mult (tallyEffect src dst n))^[r]) T) dst =
        cellsTape (List.replicate (r * n) (TapeSymbol.bit true) ++ Ldst) [] := by
  intro r
  induction r with
  | zero => intro T hT; simpa using hT
  | succ r ih =>
      intro T hT
      rw [Function.iterate_succ_apply']
      have hprev := ih T hT
      show (markedStep mult (tallyEffect src dst n)
        (((markedStep mult (tallyEffect src dst n))^[r]) T)) dst = _
      rw [markedStep, Function.update_of_ne hdm, tallyEffect,
        Function.update_self, hprev]
      show cellsTape (List.replicate n (TapeSymbol.bit true) ++
        (List.replicate (r * n) (TapeSymbol.bit true) ++ Ldst))
        (([TapeSymbol.blank] : List TapeSymbol).drop n) = _
      rw [cellsTape_drop_blank, ← List.append_assoc, ← List.replicate_add]
      congr 2
      ring

/-- Lay down one copy of `src`'s run for each mark of `mult`. -/
def multiply (mult src dst : Fin tapes) := markedLoop mult (copyTally src dst)

set_option maxHeartbeats 4000000 in
/-- **Unary multiplication.**  The target gains `m · |x|` marks. -/
theorem multiply_spec (mult src dst : Fin tapes)
    (hsd : src ≠ dst) (hdm : dst ≠ mult) (hsm : src ≠ mult)
    (x Ls Rs Ldst Lg Rg : List TapeSymbol) (m : Nat) (hm : 1 ≤ m)
    (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 Ldst [])
    (hmult : T mult = cellsTape Lg
      (List.replicate m (TapeSymbol.bit true) ++ TapeSymbol.blank :: Rg)) :
    HaltsExactly (multiply mult src dst)
        ((multiply mult src dst).startCfg T)
        ((m - 1) * (x.length * 5 + 4 + 1 + (x.length * 4 + 3 + 1 + 1)
            + 1 + (1 + 1 + 1) + 1)
          + (x.length * 5 + 4 + 1 + (x.length * 4 + 3 + 1 + 1)
            + 1 + (1 + 1 + 1))) false ∧
      (((multiply mult src dst).step^[
          (m - 1) * (x.length * 5 + 4 + 1 + (x.length * 4 + 3 + 1 + 1)
              + 1 + (1 + 1 + 1) + 1)
            + (x.length * 5 + 4 + 1 + (x.length * 4 + 3 + 1 + 1)
              + 1 + (1 + 1 + 1))])
        ((multiply mult src dst).startCfg T)).tape dst =
        cellsTape (List.replicate (m * x.length) (TapeSymbol.bit true)
          ++ Ldst) [] := by
  classical
  set Inv : (Fin tapes → Tape) → Prop :=
    fun U => U src = cellsTape (TapeSymbol.blank :: Ls)
      (x ++ TapeSymbol.blank :: Rs) with hInvDef
  have hbody : ∀ U, Inv U →
      HaltsExactly (copyTally src dst) ((copyTally src dst).startCfg U)
        (x.length * 5 + 4 + 1 + (x.length * 4 + 3 + 1 + 1)) true ∧
      (((copyTally src dst).step^[
          x.length * 5 + 4 + 1 + (x.length * 4 + 3 + 1 + 1)])
        ((copyTally src dst).startCfg U)).tape =
        tallyEffect src dst x.length U := by
    intro U hU
    exact copyTally_exact src dst hsd x Ls Rs (U dst).left
      ((U dst).head :: (U dst).right) U hnb hU rfl
  have hfg : ∀ U, Inv U → (tallyEffect src dst x.length U) mult = U mult := by
    intro U _
    rw [tallyEffect, Function.update_of_ne (Ne.symm hdm)]
  have hpres : ∀ U, Inv U →
      Inv (markedStep mult (tallyEffect src dst x.length) U) := by
    intro U hU
    show (markedStep mult (tallyEffect src dst x.length) U) src = _
    rw [markedStep, Function.update_of_ne hsm, tallyEffect,
      Function.update_of_ne hsd]
    exact hU
  obtain ⟨hhalt, htape⟩ := markedLoop_spec_inv mult (copyTally src dst) Inv
    (tallyEffect src dst x.length)
    (x.length * 5 + 4 + 1 + (x.length * 4 + 3 + 1 + 1))
    hbody hpres hfg m hm T hsrc Lg Rg hmult
  refine ⟨hhalt, ?_⟩
  have hfin : (((multiply mult src dst).step^[
      (m - 1) * (x.length * 5 + 4 + 1 + (x.length * 4 + 3 + 1 + 1)
          + 1 + (1 + 1 + 1) + 1)
        + (x.length * 5 + 4 + 1 + (x.length * 4 + 3 + 1 + 1)
          + 1 + (1 + 1 + 1))])
      ((multiply mult src dst).startCfg T)).tape =
      ((markedStep mult (tallyEffect src dst x.length))^[m]) T := htape
  rw [hfin]
  exact tallyEffect_iterate mult src dst hdm x.length Ldst m T hdst

end SipserGacsLautemann