FormalConjecturesForMathlib.Computability.TuringMachine.BusyBeavers

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import FormalConjecturesForMathlib.Computability.TuringMachine.PostTuringMachine
public import Mathlib.Computability.TuringMachine.StackTuringMachine
public import Mathlib.Data.ENat.Lattice

@[expose] public section

Turing Machines, Busy Beaver version.

A variant on the definition of the TM0 model in Mathlib: while the statements the TM can make in the usual TM0 are split into two categories (either write at the current position or move left/right), we want to combine the two to stick to the BB convention: first write at the current position and then move left/right.

Note that this Turing Machine model also works with states of type Option Γ. This is because in the busy beaver context, the turing machines also have an addition "halting" state

See also https://git.sr.ht/~vigoux/busybeaver for a different approach to formalising these objects.

namespace Turingopen Mathlibopen Relation StateTransitionopen Natnamespace BusyBeaver

-- type of tape symbols
variable (Γ : Type*)

-- type of "labels" or TM states
variable (Λ : Type*)

A Turing machine "statement" is just a command to write a symbol on the tape (at the current position) and then move left or right.

structure Stmt where write ::
  symbol : Γ
  dir : Dir
deriving Inhabited

A Post-Turing machine with symbol type Γ and label type Λ is a function which, given the current state q : Λ and the tape head a : Γ, either halts (returns none) or returns a new state q' : Option Λ and a Stmt describing what to do: a command to write a symbol and move left or right. Notice that there are two ways of halting at a given (state, head) pair: either the machine halts immediately (i.e. the function returns none), or the machine moves to the "halting state", i.e. none : Option Λ and performs one last action.

Typically, both Λ and Γ are required to be inhabited; the default value for Γ is the "blank" tape value, and the default value of Λ is the initial state.

@[nolint unusedArguments]
def Machine [Inhabited Λ] :=
  Λ → Γ → Option (Option Λ × Stmt Γ)

instance Machine.inhabited [Inhabited Λ] : Inhabited (Machine Γ Λ) := byΓ:Type u_1Λ:Type u_2inst✝:Inhabited Λ⊢ Inhabited (Machine Γ Λ)
  unfold MachineΓ:Type u_1Λ:Type u_2inst✝:Inhabited Λ⊢ Inhabited (Λ → Γ → Option (Option Λ × Stmt Γ)); infer_instanceAll goals completed! 🐙

The configuration state of a Turing machine during operation consists of a label (machine state), and a tape. The tape is represented in the form (a, L, R), meaning the tape looks like L.rev ++ [a] ++ R with the machine currently reading the a. The lists are automatically extended with blanks as the machine moves around.

@[ext]
structure Cfg [Inhabited Γ] where

The current machine state.

q : Option Λ

The current state of the tape: current symbol, left and right parts.

tape : Tape Γvariable {Γ Λ}variable [Inhabited Λ]variable [Inhabited Γ]instance Cfg.inhabited : Inhabited (Cfg Γ Λ) := ⟨⟨default, default⟩⟩namespace Machine

Execution semantics of the Turing machine.

def step (M : Machine Γ Λ) : Cfg Γ Λ → Option (Cfg Γ Λ)
| ⟨none, _⟩ => none
| ⟨some q, T⟩ => (M q T.1).map
    fun ⟨q', a⟩ ↦ ⟨q', match a with
    | Stmt.write a d => (T.write a).move d⟩

The statement Reaches M s₁ s₂ means that s₂ is obtained starting from s₁ after a finite number of steps from s₂.

def Reaches (M : Machine Γ Λ) : Cfg Γ Λ → Cfg Γ Λ → Prop := ReflTransGen fun a b ↦ b ∈ step M a

The initial configuration.

def init (l : List Γ) : Cfg Γ Λ := ⟨some default, Tape.mk₁ l⟩

Evaluate a Turing machine on initial input to a final state, if it terminates.

def eval (M : Machine Γ Λ) (l : List Γ) : Part (ListBlank Γ) :=
  (StateTransition.eval (step M) (init l)).map fun c ↦ c.tape.right₀

def multiStep (M : Machine Γ Λ) (config : Cfg Γ Λ) (n : ℕ) : Option (Cfg Γ Λ) :=
    (Option.bind · (step M))^[n] config

@[simp]
lemma multiStep_zero (M : Machine Γ Λ) (config : Cfg Γ Λ) : M.multiStep config 0 = some config :=
  rfl

@[simp]
lemma multiStep_one (M : Machine Γ Λ) (config : Cfg Γ Λ) : M.multiStep config 1 = M.step config :=
  rfl



@[simp]
lemma multiStep_succ (M : Machine Γ Λ) (config : Cfg Γ Λ) (n : ℕ) :
    M.multiStep config (n + 1) = Option.bind (M.multiStep config n) M.step := byΓ:Type u_1Λ:Type u_2inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λconfig:Cfg Γ Λn:ℕ⊢ M.multiStep config (n + 1) = (M.multiStep config n).bind M.step
  rw [multiStep,Γ:Type u_1Λ:Type u_2inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λconfig:Cfg Γ Λn:ℕ⊢ (fun x ↦ x.bind M.step)^[n + 1] (some config) = (M.multiStep config n).bind M.stepAll goals completed! 🐙 Function.iterate_succ',Γ:Type u_1Λ:Type u_2inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λconfig:Cfg Γ Λn:ℕ⊢ ((fun x ↦ x.bind M.step) ∘ (fun x ↦ x.bind M.step)^[n]) (some config) = (M.multiStep config n).bind M.stepAll goals completed! 🐙 Function.comp_apply,Γ:Type u_1Λ:Type u_2inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λconfig:Cfg Γ Λn:ℕ⊢ ((fun x ↦ x.bind M.step)^[n] (some config)).bind M.step = (M.multiStep config n).bind M.stepAll goals completed! 🐙 multiStepΓ:Type u_1Λ:Type u_2inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λconfig:Cfg Γ Λn:ℕ⊢ ((fun x ↦ x.bind M.step)^[n] (some config)).bind M.step = ((fun x ↦ x.bind M.step)^[n] (some config)).bind M.stepAll goals completed! 🐙]All goals completed! 🐙



@[simp]
lemma multiStep_eq_none_mono {M : Machine Γ Λ} {config : Cfg Γ Λ} {m n : ℕ}
    (H : M.multiStep config n = none) (hnm : n ≤ m) :
    M.multiStep config m = none := byΓ:Type u_1Λ:Type u_2inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λconfig:Cfg Γ Λm:ℕn:ℕH:M.multiStep config n = nonehnm:n ≤ m⊢ M.multiStep config m = none
  induction hnm with
  | refl =>reflΓ:Type u_1Λ:Type u_2inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λconfig:Cfg Γ Λm:ℕn:ℕH:M.multiStep config n = none⊢ M.multiStep config n = none exact HAll goals completed! 🐙
  | @step m hnm H =>stepΓ:Type u_1Λ:Type u_2inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λconfig:Cfg Γ Λm✝:ℕn:ℕH✝:M.multiStep config n = nonem:ℕhnm:n.le mH:M.multiStep config m = none⊢ M.multiStep config m.succ = none
    rw [multiStep_succ,stepΓ:Type u_1Λ:Type u_2inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λconfig:Cfg Γ Λm✝:ℕn:ℕH✝:M.multiStep config n = nonem:ℕhnm:n.le mH:M.multiStep config m = none⊢ (M.multiStep config m).bind M.step = nonestepΓ:Type u_1Λ:Type u_2inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λconfig:Cfg Γ Λm✝:ℕn:ℕH✝:M.multiStep config n = nonem:ℕhnm:n.le mH:M.multiStep config m = none⊢ none.bind M.step = none HstepΓ:Type u_1Λ:Type u_2inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λconfig:Cfg Γ Λm✝:ℕn:ℕH✝:M.multiStep config n = nonem:ℕhnm:n.le mH:M.multiStep config m = none⊢ none.bind M.step = nonestepΓ:Type u_1Λ:Type u_2inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λconfig:Cfg Γ Λm✝:ℕn:ℕH✝:M.multiStep config n = nonem:ℕhnm:n.le mH:M.multiStep config m = none⊢ none.bind M.step = none]stepΓ:Type u_1Λ:Type u_2inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λconfig:Cfg Γ Λm✝:ℕn:ℕH✝:M.multiStep config n = nonem:ℕhnm:n.le mH:M.multiStep config m = none⊢ none.bind M.step = none
    rflAll goals completed! 🐙

variable {Γ Λ : Type*} [Inhabited Λ] [Inhabited Γ]variable (M : Machine Γ Λ)

M.IsHaltingInput l is the predicate that M is a halting configuration for M.

def IsHaltingInput (l : List Γ) : Prop := (eval M l).Dom

M.HaltsAtConfiguration s is the predicate that M is a halting configuration for M.

def IsHaltingConfiguration (s : Cfg Γ Λ) : Prop := (step M s).isNone

The property that a Turing Machine M eventually halts when starting from an empty tape

class IsHalting : Prop where
  halts : M.IsHaltingInput []

The predicate that a machine starting at configuration s stops after at most n steps, i.e. reaches a configuration from which there are no defined transitions.

def HaltsAfter (s : Cfg Γ Λ) (n : ℕ) : Prop :=
  M.multiStep s (n+1) = none



lemma haltsAfter_zero_iff (s : Cfg Γ Λ) :
    HaltsAfter M s 0 ↔ step M s = none := byΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λ⊢ M.HaltsAfter s 0 ↔ M.step s = none
  rw [HaltsAfter,Γ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λ⊢ M.multiStep s (0 + 1) = none ↔ M.step s = noneAll goals completed! 🐙 multiStep,Γ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λ⊢ (fun x ↦ x.bind M.step)^[0 + 1] (some s) = none ↔ M.step s = noneAll goals completed! 🐙 Function.iterate_one,Γ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λ⊢ (some s).bind M.step = none ↔ M.step s = noneAll goals completed! 🐙 Option.bind_someΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λ⊢ M.step s = none ↔ M.step s = noneAll goals completed! 🐙]All goals completed! 🐙

lemma isHalting_iff_exists_haltsAt : IsHalting M ↔ ∃ n, M.HaltsAfter (init []) n :=
  ⟨fun _ ↦ eval_dom_iff.mpr IsHalting.halts, fun H ↦ ⟨eval_dom_iff.mp H⟩⟩



lemma exists_of_not_haltsAfter (s : Cfg Γ Λ) (n : ℕ) (H : ¬M.HaltsAfter s n) :
    ∃ (a : Λ) (b : Tape Γ), M.multiStep s n = some ⟨a, b⟩ := byΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:¬M.HaltsAfter s n⊢ ∃ a b, M.multiStep s n = some { q := some a, tape := b }
  contrapose! HΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }⊢ M.HaltsAfter s n
  rw [HaltsAfter,Γ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }⊢ M.multiStep s (n + 1) = noneΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }⊢ (M.multiStep s n).bind M.step = none multiStep_succΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }⊢ (M.multiStep s n).bind M.step = noneΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }⊢ (M.multiStep s n).bind M.step = none]Γ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }⊢ (M.multiStep s n).bind M.step = none
  obtain H | ⟨⟨u, u'⟩, hu⟩ := (Option.eq_none_or_eq_some (M.multiStep s n))inlΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH✝:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }H:M.multiStep s n = none⊢ (M.multiStep s n).bind M.step = noneinrΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }⊢ (M.multiStep s n).bind M.step = none
  ·inlΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH✝:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }H:M.multiStep s n = none⊢ (M.multiStep s n).bind M.step = none simp [H]All goals completed! 🐙
  ·inrΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }⊢ (M.multiStep s n).bind M.step = none suffices u = none byΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }this:u = none⊢ (M.multiStep s n).bind M.step = noneinrΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }⊢ u = none rw [hu,Γ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }this:u = none⊢ (some { q := u, tape := u' }).bind M.step = noneΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }this:u = none⊢ (some { q := none, tape := u' }).bind M.step = noneinrΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }⊢ u = none thisΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }this:u = none⊢ (some { q := none, tape := u' }).bind M.step = noneΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }this:u = none⊢ (some { q := none, tape := u' }).bind M.step = noneinrΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }⊢ u = none]Γ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }this:u = none⊢ (some { q := none, tape := u' }).bind M.step = noneinrΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }⊢ u = none ; rflinrΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }⊢ u = noneinrΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }⊢ u = none
    rw [Option.eq_none_iff_forall_ne_someinrΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }⊢ ∀ (a : Λ), u ≠ some ainrΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }⊢ ∀ (a : Λ), u ≠ some a]inrΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }⊢ ∀ (a : Λ), u ≠ some a
    intro a hcinrΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u:Option Λu':Tape Γhu:M.multiStep s n = some { q := u, tape := u' }a:Λhc:u = some a⊢ False
    subst hcinrΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λs:Cfg Γ Λn:ℕH:∀ (a : Λ) (b : Tape Γ), M.multiStep s n ≠ some { q := some a, tape := b }u':Tape Γa:Λhu:M.multiStep s n = some { q := some a, tape := u' }⊢ False
    simp [hu] at H ⊢All goals completed! 🐙

lemma not_isHalting_iff_forall_isSome_multiStep :
    ¬ IsHalting M ↔ ∀ n, M.multiStep (init []) (n + 1) |>.isSome := byΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λ⊢ ¬M.IsHalting ↔ ∀ (n : ℕ), (M.multiStep (init []) (n + 1)).isSome = true
  simp_rw [Γ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λ⊢ ¬M.IsHalting ↔ ∀ (n : ℕ), (M.multiStep (init []) (n + 1)).isSome = trueisHalting_iff_exists_haltsAt,Γ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λ⊢ (¬∃ n, M.HaltsAfter (init []) n) ↔ ∀ (n : ℕ), (M.multiStep (init []) (n + 1)).isSome = true HaltsAfter,Γ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λ⊢ (¬∃ n, M.multiStep (init []) (n + 1) = none) ↔ ∀ (n : ℕ), (M.multiStep (init []) (n + 1)).isSome = true Option.isSome_iff_ne_noneΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λ⊢ (¬∃ n, M.multiStep (init []) (n + 1) = none) ↔ ∀ (n : ℕ), M.multiStep (init []) (n + 1) ≠ none]
  push NotΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λ⊢ (∀ (n : ℕ), M.multiStep (init []) (n + 1) ≠ none) ↔ ∀ (n : ℕ), M.multiStep (init []) (n + 1) ≠ none
  rflAll goals completed! 🐙



lemma not_isHalting_of_forall_isSome (H : ∀ l s, ∃ a b, M l s = some (some a, b)) :
    ¬IsHalting M := byΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)⊢ ¬M.IsHalting
  rw [not_isHalting_iff_forall_isSome_multiStepΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)⊢ ∀ (n : ℕ), (M.multiStep (init []) (n + 1)).isSome = trueΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)⊢ ∀ (n : ℕ), (M.multiStep (init []) (n + 1)).isSome = true]Γ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)⊢ ∀ (n : ℕ), (M.multiStep (init []) (n + 1)).isSome = true
  intro nΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)n:ℕ⊢ (M.multiStep (init []) (n + 1)).isSome = true
  induction n with
  | zero =>zeroΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)⊢ (M.multiStep (init []) (0 + 1)).isSome = true
    obtain ⟨a, b, H⟩ := H default (Tape.mk₁ []).headzeroΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH✝:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)a:Λb:Stmt ΓH:M default (Tape.mk₁ []).head = some (some a, b)⊢ (M.multiStep (init []) (0 + 1)).isSome = true
    simp [init, step, H]All goals completed! 🐙
  | succ n ih =>succΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)n:ℕih:(M.multiStep (init []) (n + 1)).isSome = true⊢ (M.multiStep (init []) (n + 1 + 1)).isSome = true
    obtain ⟨a, b, hab⟩ := exists_of_not_haltsAfter _ _ _ (byΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)n:ℕih:(M.multiStep (init []) (n + 1)).isSome = true⊢ ¬HaltsAfter ?m.64 ?m.65 ?m.66succΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)n:ℕih:(M.multiStep (init []) (n + 1)).isSome = truea:Λb:Tape Γhab:M.multiStep (init []) n = some { q := some a, tape := b }⊢ (M.multiStep (init []) (n + 1 + 1)).isSome = true rwa [Option.isSome_iff_ne_noneΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)n:ℕih✝:(M.multiStep (init []) (n + 1)).isSome = trueih:M.multiStep (init []) (n + 1) ≠ none⊢ ¬HaltsAfter ?m.64 ?m.65 ?m.66succΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)n:ℕih:(M.multiStep (init []) (n + 1)).isSome = truea:Λb:Tape Γhab:M.multiStep (init []) n = some { q := some a, tape := b }⊢ (M.multiStep (init []) (n + 1 + 1)).isSome = true]Γ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)n:ℕih✝:(M.multiStep (init []) (n + 1)).isSome = trueih:M.multiStep (init []) (n + 1) ≠ none⊢ ¬HaltsAfter ?m.64 ?m.65 ?m.66succΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)n:ℕih:(M.multiStep (init []) (n + 1)).isSome = truea:Λb:Tape Γhab:M.multiStep (init []) n = some { q := some a, tape := b }⊢ (M.multiStep (init []) (n + 1 + 1)).isSome = true at ih)succΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)n:ℕih:(M.multiStep (init []) (n + 1)).isSome = truea:Λb:Tape Γhab:M.multiStep (init []) n = some { q := some a, tape := b }⊢ (M.multiStep (init []) (n + 1 + 1)).isSome = true
    obtain ⟨c, d, hcd⟩ := H a b.headsuccΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)n:ℕih:(M.multiStep (init []) (n + 1)).isSome = truea:Λb:Tape Γhab:M.multiStep (init []) n = some { q := some a, tape := b }c:Λd:Stmt Γhcd:M a b.head = some (some c, d)⊢ (M.multiStep (init []) (n + 1 + 1)).isSome = true
    obtain ⟨e, f, hef⟩ := H c (Tape.move d.dir (Tape.write d.symbol b)).headsuccΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ ΛH:∀ (l : Λ) (s : Γ), ∃ a b, M l s = some (some a, b)n:ℕih:(M.multiStep (init []) (n + 1)).isSome = truea:Λb:Tape Γhab:M.multiStep (init []) n = some { q := some a, tape := b }c:Λd:Stmt Γhcd:M a b.head = some (some c, d)e:Λf:Stmt Γhef:M c (Tape.move d.dir (Tape.write d.symbol b)).head = some (some e, f)⊢ (M.multiStep (init []) (n + 1 + 1)).isSome = true
    simp [multiStep_succ, multiStep_succ, hab, step, hcd, hef]All goals completed! 🐙

noncomputable def haltingNumber : ENat :=
  -- The smallest `n` such that `M` halts after `n` steps when starting from an empty tape.
  -- If no such `n` exists then this is equal to `⊤`.
  sInf {(n : ENat) |  (n : ℕ) (_ : HaltsAfter M (init []) n) }

theorem haltingNumber_def (n : ℕ) (hn : ∃ a, M.multiStep (init []) n = some a)
    (ha' : M.multiStep (init []) (n + 1) = none) :
    M.haltingNumber = n := byΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λn:ℕhn:∃ a, M.multiStep (init []) n = some aha':M.multiStep (init []) (n + 1) = none⊢ M.haltingNumber = ↑n
  refine IsGLB.sInf_eq (IsLeast.isGLB ⟨⟨n, byΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λn:ℕhn:∃ a, M.multiStep (init []) n = some aha':M.multiStep (init []) (n + 1) = none⊢ M.HaltsAfter (init []) n rwa [HaltsAfterΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λn:ℕhn:∃ a, M.multiStep (init []) n = some aha':M.multiStep (init []) (n + 1) = none⊢ M.multiStep (init []) (n + 1) = none]Γ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λn:ℕhn:∃ a, M.multiStep (init []) n = some aha':M.multiStep (init []) (n + 1) = none⊢ M.multiStep (init []) (n + 1) = none, rfl⟩, fun m ⟨k, _, _⟩ ↦ ?_⟩)
  cases mtopΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λn:ℕhn:∃ a, M.multiStep (init []) n = some aha':M.multiStep (init []) (n + 1) = nonek:ℕw✝:M.HaltsAfter (init []) kx✝:⊤ ∈ {x | ∃ n, ∃ (_ : M.HaltsAfter (init []) n), ↑n = x}h✝:↑k = ⊤⊢ ↑n ≤ ⊤coeΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λn:ℕhn:∃ a, M.multiStep (init []) n = some aha':M.multiStep (init []) (n + 1) = nonek:ℕw✝:M.HaltsAfter (init []) ka✝:ℕx✝:↑a✝ ∈ {x | ∃ n, ∃ (_ : M.HaltsAfter (init []) n), ↑n = x}h✝:↑k = ↑a✝⊢ ↑n ≤ ↑a✝
  ·topΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λn:ℕhn:∃ a, M.multiStep (init []) n = some aha':M.multiStep (init []) (n + 1) = nonek:ℕw✝:M.HaltsAfter (init []) kx✝:⊤ ∈ {x | ∃ n, ∃ (_ : M.HaltsAfter (init []) n), ↑n = x}h✝:↑k = ⊤⊢ ↑n ≤ ⊤ exact le_topAll goals completed! 🐙
  ·coeΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λn:ℕhn:∃ a, M.multiStep (init []) n = some aha':M.multiStep (init []) (n + 1) = nonek:ℕw✝:M.HaltsAfter (init []) ka✝:ℕx✝:↑a✝ ∈ {x | ∃ n, ∃ (_ : M.HaltsAfter (init []) n), ↑n = x}h✝:↑k = ↑a✝⊢ ↑n ≤ ↑a✝ by_contra! hccoeΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λn:ℕhn:∃ a, M.multiStep (init []) n = some aha':M.multiStep (init []) (n + 1) = nonek:ℕw✝:M.HaltsAfter (init []) ka✝:ℕx✝:↑a✝ ∈ {x | ∃ n, ∃ (_ : M.HaltsAfter (init []) n), ↑n = x}h✝:↑k = ↑a✝hc:↑a✝ < ↑n⊢ False
    simp_all [multiStep_eq_none_mono ‹_› (show k + 1 ≤ n byΓ:Type u_3Λ:Type u_4inst✝¹:Inhabited Λinst✝:Inhabited ΓM:Machine Γ Λn:ℕhn:∃ a, M.multiStep (init []) n = some aha':M.multiStep (init []) (n + 1) = none⊢ M.haltingNumber = ↑n aesopAll goals completed! 🐙)]

end Machineend BusyBeaverend Turing