Commit 2026-04-21 05:56 597460a8

View on Github →

refactor(Computability): split Halting.lean into separate files (#38138) This PR splits the monolithic Mathlib/Computability/Halting.lean into three separate files to improve modularity and prepare the ground for future additions to RE sets theory. Changes:

  • Extracted the Nat.Partrec' vector basis into Mathlib/Computability/PartrecBasis.lean.
  • Extracted the foundational theory (ComputablePred, REPred, Post's theorem) into Mathlib/Computability/RE.lean.
  • Halting.lean now strictly contains undecidability results (Halting problem, Rice's theorem).
  • Fixed downstream imports in TuringMachine/Config.lean.

Estimated changes

deleted theorem Computable.computablePred
deleted theorem Computable.find
deleted theorem ComputablePred.ite
deleted theorem ComputablePred.of_eq
deleted theorem ComputablePred.to_re
deleted def ComputablePred
deleted def Nat.Partrec'.Vec
deleted theorem Nat.Partrec'.comp'
deleted theorem Nat.Partrec'.comp₁
deleted theorem Nat.Partrec'.head
deleted theorem Nat.Partrec'.idv
deleted theorem Nat.Partrec'.of_eq
deleted theorem Nat.Partrec'.of_part
deleted theorem Nat.Partrec'.of_prim
deleted theorem Nat.Partrec'.part_iff
deleted theorem Nat.Partrec'.part_iff₁
deleted theorem Nat.Partrec'.part_iff₂
deleted theorem Nat.Partrec'.rfindOpt
deleted theorem Nat.Partrec'.tail
deleted theorem Nat.Partrec'.to_part
deleted theorem Nat.Partrec'.vec_iff
deleted inductive Nat.Partrec'
deleted theorem Nat.Partrec.merge'
deleted theorem Partrec.cond
deleted theorem Partrec.dom_re
deleted theorem Partrec.merge'
deleted theorem Partrec.merge
deleted theorem REPred.of_eq
deleted def REPred
added def Nat.Partrec'.Vec
added theorem Nat.Partrec'.comp'
added theorem Nat.Partrec'.comp₁
added theorem Nat.Partrec'.head
added theorem Nat.Partrec'.idv
added theorem Nat.Partrec'.of_eq
added theorem Nat.Partrec'.of_part
added theorem Nat.Partrec'.of_prim
added theorem Nat.Partrec'.part_iff
added theorem Nat.Partrec'.rfindOpt
added theorem Nat.Partrec'.tail
added theorem Nat.Partrec'.to_part
added theorem Nat.Partrec'.vec_iff
added inductive Nat.Partrec'
added theorem Computable.find
added theorem ComputablePred.ite
added theorem ComputablePred.of_eq
added theorem ComputablePred.to_re
added def ComputablePred
added theorem Nat.Partrec.merge'
added theorem Partrec.cond
added theorem Partrec.dom_re
added theorem Partrec.merge'
added theorem Partrec.merge
added theorem REPred.of_eq
added def REPred