Collatz.lean

Collatz.lean

import Mathlib

/--
Do one collatz iteration
-/
def collatz (n : Nat) := 
  if n % 2 == 0 then n / 2 else 3 * n + 1

/-
Algorithmic collatz termination

Takes a number `n` and an amount of "fuel" and returns the boolean
true iff `n` terminates within `fuel` iterations of collatz.
-/
def collatzTerm (n fuel : Nat) : Bool :=
  match fuel with
  | 0 => false
  | x + 1 => if n == 1 then true else collatzTerm (collatz n) x

/-- 
Definitional collatz termination

Takes a number `n` and holds if `n` eventually terminates under collatz.
-/
inductive collatz_term : (n : Nat) → Prop where
  | base : collatz_term 1 
  | step {n : Nat} : collatz_term (collatz n) → collatz_term n 

/--
Verify the soundness of the checker

If a number algorithmically terminates for some fuel, then it definitionally terminates.
-/
lemma checker_sound {n fuel : ℕ} (h : collatzTerm n fuel = true) : collatz_term n := by 
  unfold collatzTerm at h
  match fuel with
  | 0 => simp only [Bool.false_eq_true] at h
  | f + 1 => 
    simp only [beq_iff_eq, Bool.if_true_left, Bool.or_eq_true, decide_eq_true_eq] at h; 
    match h with
    | .inl x => rw [x]; exact .base
    | .inr x => exact .step (checker_sound x)

/--
Use the algorithmic checker via native_decide
-/
theorem twenty_seven_terminates : collatz_term 27 := checker_sound (fuel := 112) (by native_decide)

/--
info: 'twenty_seven_terminates' depends on axioms: [propext, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound]
-/
#guard_msgs in
#print axioms twenty_seven_terminates