Termination of mutual recursive definition

Stream: new members

[bruno cuconato]

Hi, I've been toying with an implementation in Lean 4 (commit ded7216a12cb) of primitive recursive functions, following this Agda version. When implementing the evaluator (whose termination Agda seems to be able to prove), Lean says structural recursion does not handle mutually recursive functions, and that I should use termination_by to show it terminates.

inductive PRF : Nat → Type where
  | zero    : PRF 0
  | succ    : PRF 1
  | proj    : {n : Nat} → Fin n → PRF n -- projection
  | comp    : {m k : Nat} → PRF m → (Fin m → PRF k) → PRF k -- composition
  | primrec : {n : Nat} → PRF n → PRF (n + 2) → PRF (n + 1) -- primitive recursion

def evaluate (f : PRF a) (arg : Fin a → Nat) : Nat :=
  match f with
  | PRF.zero => 0
  | PRF.succ => arg 0 + 1
  | PRF.proj i => arg i
  | PRF.comp g hs => evaluate g (λ i => evaluate (hs i) arg)
  | PRF.primrec g h =>
    let rec primrec : Nat → Nat
    | 0 =>
      evaluate
        g
        (λ {val := i, isLt := i_lt_n} =>
          arg {val := i + 1, isLt := Nat.succ_le_succ i_lt_n})
    | n + 1 =>
      evaluate
        h
        (λ fini =>
          match fini with
          | {val := 0, isLt := _} => primrec n
          | {val := 1, isLt := _} => n
          | {val := i + 2, isLt} => arg {val := i + 1, isLt := Nat.pred_le_pred isLt})
    primrec (arg 0)

1. Are there any plans for Lean 4 to support the automatic termination check of mutually recursive function by structural recursion?
2. How do I prove this terminates? I have tried looking for examples using termination_by or decreasing_by on Lean std library, but nothing seems very enlightening to me…

[Mario Carneiro]

The easiest way is to make the inner function not mutually recursive with the outer one, by extracting evaluate g and evaluate h out of the inner function:

def evaluate (f : PRF a) (arg : Fin a → Nat) : Nat :=
  match f with
  | PRF.zero => 0
  | PRF.succ => arg 0 + 1
  | PRF.proj i => arg i
  | PRF.comp g hs => evaluate g fun i => evaluate (hs i) arg
  | PRF.primrec g h =>
    let IHg := evaluate g
    let IHh := evaluate h
    let rec primrec : Nat → Nat
    | 0 => IHg fun ⟨i, i_lt_n⟩ => arg ⟨i + 1, Nat.succ_le_succ i_lt_n⟩
    | n + 1 => IHh fun
      | ⟨0, _⟩ => primrec n
      | ⟨1, _⟩ => n
      | ⟨i + 2, isLt⟩ => arg ⟨i + 1, Nat.pred_le_pred isLt⟩
    primrec (arg 0)

[bruno cuconato]

That was simpler than I thought I'd be, thank you @Mario Carneiro !