sgl_power_step

import Definitions.Def_sgl_power

/-!
# What one multiplication does to every tape

`multiply_spec` reports the product tape; a chain of multiplications needs the
rest — the multiplier consumed in a known shape, the source restored, and
everything else untouched.  All three read off the same iterate, so they are
stated over it once and evaluated per tape.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- The full final tape of a multiplication. -/
theorem multiply_run (mult src dst : Fin tapes)
    (hsd : src ≠ dst) (hdm : dst ≠ mult) (hsm : src ≠ mult)
    (x Ls Rs 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))
    (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 =
        ((markedStep mult (tallyEffect src dst x.length))^[m]) T := 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
  exact 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

/-- Tapes other than the multiplier and the product are untouched. -/
theorem multiply_other (mult src dst : Fin tapes) (n : Nat) :
    ∀ (r : Nat) (T : Fin tapes → Tape) (j : Fin tapes), j ≠ mult → j ≠ dst →
      (((markedStep mult (tallyEffect src dst n))^[r]) T) j = T j := by
  intro r
  induction r with
  | zero => intro T j _ _; rfl
  | succ r ih =>
      intro T j hjm hjd
      rw [Function.iterate_succ_apply', markedStep,
        Function.update_of_ne hjm, tallyEffect, Function.update_of_ne hjd]
      exact ih T j hjm hjd

/-- The multiplier ends consumed: marks in its left context, head on blank. -/
theorem multiply_mult (mult src dst : Fin tapes)
    (hsd : src ≠ dst) (hdm : dst ≠ mult) (hsm : src ≠ mult)
    (x Ls Rs Lg Rg : List TapeSymbol) (m : Nat)
    (T : Fin tapes → Tape)
    (hsrc : T src = cellsTape (TapeSymbol.blank :: Ls)
      (x ++ TapeSymbol.blank :: Rs))
    (hmult : T mult = cellsTape Lg
      (List.replicate m (TapeSymbol.bit true) ++ TapeSymbol.blank :: Rg)) :
    (((markedStep mult (tallyEffect src dst x.length))^[m]) T) mult =
      cellsTape (List.replicate m (TapeSymbol.bit true) ++ Lg)
        (TapeSymbol.blank :: Rg) := by
  classical
  have hpres : ∀ U, (fun U => U src = cellsTape (TapeSymbol.blank :: Ls)
      (x ++ TapeSymbol.blank :: Rs)) U →
      (fun U => U src = cellsTape (TapeSymbol.blank :: Ls)
        (x ++ TapeSymbol.blank :: Rs))
        (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
  have hfg : ∀ U, (fun U => U src = cellsTape (TapeSymbol.blank :: Ls)
      (x ++ TapeSymbol.blank :: Rs)) U →
      (tallyEffect src dst x.length U) mult = U mult := by
    intro U _
    rw [tallyEffect, Function.update_of_ne (Ne.symm hdm)]
  have := markedStep_guide_inv mult
    (fun U => U src = cellsTape (TapeSymbol.blank :: Ls)
      (x ++ TapeSymbol.blank :: Rs))
    (tallyEffect src dst x.length) hpres hfg m Lg Rg T hsrc hmult m
    (le_refl m)
  rw [this]
  simp

end SipserGacsLautemann