# How to prove the termination of Ackermann in Lean?

I'm trying to write the Ackermann function and prove it terminates in Lean 4

def Ackermann : Nat → Nat → Nat :=
fun x y =>
if x == 0 then y + 1 else
if y == 0 then Ackermann (x - 1) 1 else
Ackermann (x - 1) (Ackermann x (y - 1))
termination_by
Ackermann x y => (x, y)


but it rejects the termination proof. I don't know how to write lexicographic tuples, and I haven't found in the documentation I looked for. Thanks for your help.

Usually x-1 is harder to work with (but not impossible). Pattern matching is much easier from a type theoretic perspective. So (this is actually one of the test cases of Lean):

def ack : Nat → Nat → Nat
| 0,   y   => y+1
| x+1, 0   => ack x 1
| x+1, y+1 => ack x (ack (x+1) y)
termination_by _ a b => (a, b)

• Could you point us to a resource which explains the termination_by syntax? May 10 at 19:26

With dependent types and the awesome prelude of Lean 4, one can define the Ackermann function in any equivalent way as long as the definition is constructive. However, the more closely the definition for the Ackermann follows the definitions of its associated types (in this case, pattern matching on Nat like @Trebor's answer), the easier it is to reason about termination, preconditions, postconditions, etc.

For your definition, the goal is to prove these 3 lexicographic orderings given your termination_by measure:

1. Prod.Lex (· < ·) (· < ·) (x - 1, 1) (x, y) which suffices to prove x - 1 < x.
2. Prod.Lex (· < ·) (· < ·) (x, y - 1) (x, y) which suffices to prove y - 1 < y.
3. Prod.Lex (· < ·) (· < ·) (x - 1, Ackermann x (y - 1)) (x, y) which suffices to prove x - 1 < x.

First of all, we can use this lemma to simplify things:

theorem pos_sub_one_lt_self {n: Nat} (h: n ≠ 0): n - 1 < n :=
Nat.sub_lt (Nat.zero_lt_of_ne_zero h) .refl -- #check (Nat.le.refl: 0 < 1)


To package all the "decreasing" proofs in decreasing_by:

def Ackermann (x y: Nat): Nat :=
if hx: x = 0 then
y + 1
else if hy: y = 0 then
Ackermann (x - 1) 1
else
Ackermann (x - 1) (Ackermann x (y - 1))
termination_by _ => (x, y)
decreasing_by
simp_wf
try apply Prod.Lex.right
try exact pos_sub_one_lt_self hy
try apply Prod.Lex.left
try exact pos_sub_one_lt_self hx


To place "decreasing" proofs directly next to their usage, and let the decreasing_by pick them up automatically:

def Ackermann (x y: Nat): Nat :=
if hx: x = 0 then
y + 1
else if hy: y = 0 then
have: Prod.Lex (· < ·) (· < ·) (x - 1, 1) (x, y) :=
.left _ _ (pos_sub_one_lt_self hx)
Ackermann (x - 1) 1
else
have: Prod.Lex (· < ·) (· < ·) (x, y - 1) (x, y) :=
.right _ (pos_sub_one_lt_self hy)
have: Prod.Lex (· < ·) (· < ·) (x - 1, Ackermann x (y - 1)) (x, y) :=
.left _ _ (pos_sub_one_lt_self hx)
Ackermann (x - 1) (Ackermann x (y - 1))
termination_by _ => (x, y)


On my machine with leanprover/lean4:nightly-2023-03-09, the following snippet didn't work originally, but after solving the two variants above, the definition below magically started to work even in another project and even after restarting VSCode. Why?

def Ackermann (x y: Nat): Nat :=
if x = 0 then
y + 1
else if y = 0 then
Ackermann (x - 1) 1
else
Ackermann (x - 1) (Ackermann x (y - 1))
termination_by _ => (x, y)


Documentation and tutorial for custom well-founded recursions in Lean 4 is lacking. The way I figured it out is by implementing mod and div for my own ℕ by reading Nat.mod, Nat.div, and WF.lean in the prelude.

Here's a variant that doesn't require termination_by:

def ackAux (f : Nat → Nat) : Nat → Nat
| 0 => f 1
| y + 1 => f (ackAux f y)

def ack : Nat → Nat → Nat
| 0   => Nat.succ
| x+1 => ackAux (ack x)


In a more condensed form:

def ack : Nat → Nat → Nat
| 0   => Nat.succ
| x+1 =>
let f := ack x
let rec g : Nat → Nat
| 0 => f 1
| y+1 => f (g y)
g