sgl_first_halt

import Definitions.Def_sgl_loop_answer

/-!
# From "halts within" to "halts exactly"

A machine's correctness is stated as *halting within* a time bound: at that
time the result is `some v`.  A round instead needs the first time the result
is anything at all, together with the fact that nothing happened before it.
The two agree because a halted configuration is a fixed point of `step`, so the
result never changes once set.
-/

namespace SipserGacsLautemann

variable {tapes states : Nat}

/-- A halted configuration is a fixed point. -/
theorem Machine.step_halted (M : Machine tapes states)
    (cfg : Configuration tapes states) (v : Bool)
    (h : M.result cfg.state = some v) : M.step cfg = cfg := by
  rw [Machine.step, h]

/-- Once the result is set it stays set. -/
theorem Machine.result_stable (M : Machine tapes states)
    (cfg : Configuration tapes states) (v : Bool) (t : Nat) :
    ∀ k : Nat, M.result ((M.step^[t]) cfg).state = some v →
      M.result ((M.step^[t + k]) cfg).state = some v := by
  intro k
  induction k with
  | zero => intro h; simpa using h
  | succ k ih =>
      intro h
      have hik := ih h
      rw [show t + (k + 1) = (t + k) + 1 from rfl, Function.iterate_succ_apply',
        Machine.step_halted M _ v hik]
      exact hik

/-- **The first halting time.** -/
theorem Machine.firstHalt (M : Machine tapes states)
    (cfg : Configuration tapes states) (T : Nat) (v : Bool)
    (h : M.result ((M.step^[T]) cfg).state = some v) :
    ∃ Tm : Nat, Tm ≤ T ∧
      (∀ s, s < Tm → M.result ((M.step^[s]) cfg).state = none) ∧
      M.result ((M.step^[Tm]) cfg).state = some v := by
  classical
  have hexT : M.result ((M.step^[T]) cfg).state ≠ none := by rw [h]; simp
  have hex : ∃ t, M.result ((M.step^[t]) cfg).state ≠ none := ⟨T, hexT⟩
  have hle : Nat.find hex ≤ T := Nat.find_le hexT
  refine ⟨Nat.find hex, hle, ?_, ?_⟩
  · intro s hs
    have := Nat.find_min hex hs
    simpa using this
  · have hne := Nat.find_spec hex
    cases hc : M.result ((M.step^[Nat.find hex]) cfg).state with
    | none => exact absurd hc hne
    | some w =>
        obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_le hle
        have := Machine.result_stable M cfg w (Nat.find hex) k hc
        rw [← hk, h] at this
        exact this.symm

end SipserGacsLautemann