Termination of mutual recursion

Stream: new members

[Harun Khan]

Hi! I'm having trouble proving the termination of two mutually recursive functions in Lean 4. The first one calls the second one and then decreases in the second one and the second one already decreases.

mutual
def foo : Nat → Nat → Bool
  | 0, j => false
  | i, 0 => false
  | i, j+1 => foo i j ∧ goo i (j+1)

def goo : Nat → Nat → Bool
  | 0, j => false
  | i, 0 => false
  | i+1, j+1 => foo i j ∧ goo i (j+1)
end
termination_by
  foo i j => i + j
  goo i j => i + j

How do I show termination?

[Arthur Adjedj]

This works:

mutual
def foo : Nat → Nat → Bool
  | 0, _ => false
  | _, 0 => false
  | i, j+1 => foo i j ∧ goo i (j+1)

def goo : Nat → Nat → Bool
  | 0, _ => false
  | _, 0 => false
  | i+1, j+1 => foo i j ∧ goo i (j+1)
end
termination_by
  foo i j => i + j + 1
  goo i j => i + j