Termination Proofs

1-- This wouldn't be safe:
2-- def bad (n : Nat) : Nat := bad n  -- Infinite loop!
3
4-- Lean rejects functions that might not terminate
5-- Every recursive call must make "progress"

1-- Lean often proves termination automatically
2def factorial : Nat → Nat
3  | 0 => 1
4  | n + 1 => (n + 1) * factorial n
5-- ✓ Lean sees: n < n + 1
6
7def length : List α → Nat
8  | [] => 0
9  | _ :: xs => 1 + length xs
10-- ✓ Lean sees: xs is structurally smaller
11
12def fib : Nat → Nat
13  | 0 => 0
14  | 1 => 1
15  | n + 2 => fib (n + 1) + fib n
16-- ✓ Both recursive calls decrease

1-- Lean's primary termination checker uses structural recursion
2-- Arguments must decrease according to a well-founded order
3
4def sum : List Nat → Nat
5  | [] => 0
6  | x :: xs => x + sum xs  -- xs is a subterm of x :: xs
7
8def treeSize : Tree α → Nat
9  | .leaf => 0
10  | .node left _ right => 1 + treeSize left + treeSize right
11  -- left and right are subterms of node

1-- When Lean can't infer termination, specify what decreases
2def gcd (a b : Nat) : Nat :=
3  if b = 0 then a
4  else gcd b (a % b)
5termination_by b  -- b decreases each call
6
7-- For multiple arguments, use a tuple or expression
8def ack : Nat → Nat → Nat
9  | 0, n => n + 1
10  | m + 1, 0 => ack m 1
11  | m + 1, n + 1 => ack m (ack (m + 1) n)
12termination_by m n => (m, n)  -- Lexicographic order

1-- When termination isn't obvious, provide a proof
2def div (n m : Nat) (h : m > 0) : Nat :=
3  if n < m then 0
4  else 1 + div (n - m) m h
5termination_by n
6decreasing_by
7  simp_wf  -- Simplify well-founded goal
8  omega    -- Prove n - m < n when m > 0 and n ≥ m

1-- Add a "fuel" parameter that decreases
2def search (fuel : Nat) (f : Nat → Bool) (n : Nat) : Option Nat :=
3  match fuel with
4  | 0 => none  -- Out of fuel
5  | fuel + 1 =>
6    if f n then some n
7    else search fuel f (n + 1)
8termination_by fuel

1mutual
2  def isEven : Nat → Bool
3    | 0 => true
4    | n + 1 => isOdd n
5
6  def isOdd : Nat → Bool
7    | 0 => false
8    | n + 1 => isEven n
9end
10-- Termination: n decreases in both directions

1def f91 (n : Nat) : Nat :=
2  if n > 100 then n - 10
3  else f91 (f91 (n + 11))
4-- Requires sophisticated termination proof!
5-- This is McCarthy's famous f91 function

1-- When you can't prove termination, use partial
2partial def infiniteLoop : Nat → Nat
3  | n => infiniteLoop (n + 1)  -- No termination proof needed
4
5-- partial functions can't be used in proofs!
6-- They may not terminate, breaking soundness

1def binarySearch (arr : Array Int) (target : Int) (lo hi : Nat) : Option Nat :=
2  if lo ≥ hi then none
3  else
4    let mid := (lo + hi) / 2
5    if arr[mid]! < target then binarySearch arr target (mid + 1) hi
6    else if arr[mid]! > target then binarySearch arr target lo mid
7    else some mid
8termination_by hi - lo
9decreasing_by all_goals simp_wf; omega

1def quickSort : List Nat → List Nat
2  | [] => []
3  | pivot :: rest =>
4    let smaller := rest.filter (· < pivot)
5    let larger := rest.filter (· ≥ pivot)
6    quickSort smaller ++ [pivot] ++ quickSort larger
7termination_by xs => xs.length
8-- smaller and larger have length < rest.length + 1