sgl_casc_final

import Definitions.Def_sgl_casc_loop

/-!
# Reading the verdict

After the cascade, three votes sit under the live triple's heads.  The last
majority needs no tape at all: a test reads the three heads and reports
their majority as its verdict.  A leading test picks the live triple.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- The majority of three heads, as a test predicate. -/
def majAt (x1 x2 x3 : Fin tapes) :
    (Fin tapes → TapeSymbol) → Bool :=
  fun symbols =>
    majorityVoteConstruction (cellBool (symbols x1)) (cellBool (symbols x2))
      (cellBool (symbols x3))

/-- Read the verdict off whichever triple is live. -/
noncomputable def cascFinal (A1 A2 A3 B1 B2 B3 : Fin tapes) :=
  (TypedMachine.test (notBlankAt A1)).andThen fun v =>
    if v then TypedMachine.test (majAt A1 A2 A3)
    else TypedMachine.test (majAt B1 B2 B3)

set_option maxHeartbeats 1000000 in
/-- **The verdict is the majority of the three final votes.** -/
theorem cascFinal_spec (A1 A2 A3 B1 B2 B3 : Fin tapes)
    (p : Bool) (v1 v2 v3 : Bool) (T : Fin tapes → Tape)
    (L1 L2 L3 : List TapeSymbol)
    (h1 : T (if p then A1 else B1) = cellsTape L1
      (TapeSymbol.bit v1 :: TapeSymbol.blank :: []))
    (h2 : T (if p then A2 else B2) = cellsTape L2
      (TapeSymbol.bit v2 :: TapeSymbol.blank :: []))
    (h3 : T (if p then A3 else B3) = cellsTape L3
      (TapeSymbol.bit v3 :: TapeSymbol.blank :: []))
    (hA1blank : p = false → (T A1).head = TapeSymbol.blank) :
    HaltsExactly (cascFinal A1 A2 A3 B1 B2 B3)
      ((cascFinal A1 A2 A3 B1 B2 B3).startCfg T) 3
      (majorityVoteConstruction v1 v2 v3) := by
  classical
  have htestt : (((TypedMachine.test (notBlankAt A1)).step^[1])
      ((TypedMachine.test (notBlankAt A1)).startCfg T)).tape = T := by
    rw [Function.iterate_one]
    funext j
    simp [TypedMachine.step, TypedMachine.test, TypedMachine.startCfg,
      Tape.write_head_self, Tape.move]
  cases p with
  | true =>
      have h1' : T A1 = cellsTape L1
          (TapeSymbol.bit v1 :: TapeSymbol.blank :: []) := h1
      have h2' : T A2 = cellsTape L2
          (TapeSymbol.bit v2 :: TapeSymbol.blank :: []) := h2
      have h3' : T A3 = cellsTape L3
          (TapeSymbol.bit v3 :: TapeSymbol.blank :: []) := h3
      have htest := TypedMachine.test_spec (notBlankAt A1) T
      have hmark : (T A1).head ≠ TapeSymbol.blank := by
        rw [h1']
        show (TapeSymbol.bit v1 :: TapeSymbol.blank :: []).headD
          TapeSymbol.blank ≠ TapeSymbol.blank
        simp
      rw [notBlankAt_true A1 T hmark] at htest
      have hinner := TypedMachine.test_spec (majAt A1 A2 A3) T
      have hval : majAt A1 A2 A3 (fun i => (T i).head) =
          majorityVoteConstruction v1 v2 v3 := by
        show majorityVoteConstruction (cellBool (T A1).head)
          (cellBool (T A2).head) (cellBool (T A3).head) =
          majorityVoteConstruction v1 v2 v3
        rw [h1', h2', h3']
        rfl
      rw [hval] at hinner
      have hmain := chainStepD
        (M₂ := fun v =>
          if v then TypedMachine.test (majAt A1 A2 A3)
          else TypedMachine.test (majAt B1 B2 B3))
        htest htestt (by simpa using hinner)
      exact hmain.1
  | false =>
      have h1' : T B1 = cellsTape L1
          (TapeSymbol.bit v1 :: TapeSymbol.blank :: []) := h1
      have h2' : T B2 = cellsTape L2
          (TapeSymbol.bit v2 :: TapeSymbol.blank :: []) := h2
      have h3' : T B3 = cellsTape L3
          (TapeSymbol.bit v3 :: TapeSymbol.blank :: []) := h3
      have htest := TypedMachine.test_spec (notBlankAt A1) T
      rw [notBlankAt_false A1 T (hA1blank rfl)] at htest
      have hinner := TypedMachine.test_spec (majAt B1 B2 B3) T
      have hval : majAt B1 B2 B3 (fun i => (T i).head) =
          majorityVoteConstruction v1 v2 v3 := by
        show majorityVoteConstruction (cellBool (T B1).head)
          (cellBool (T B2).head) (cellBool (T B3).head) =
          majorityVoteConstruction v1 v2 v3
        rw [h1', h2', h3']
        rfl
      rw [hval] at hinner
      have hmain := chainStepD
        (M₂ := fun v =>
          if v then TypedMachine.test (majAt A1 A2 A3)
          else TypedMachine.test (majAt B1 B2 B3))
        htest htestt (by simpa using hinner)
      exact hmain.1

end SipserGacsLautemann