How to prove termination of mutually recursive functions if only some decrease their arguments?

Question

I need to prove termination of mutually recursive functions. However, only some of those functions actually (structurally) decrease their arguments, other functions do some other calculations and pass the value on, unchanged. Here's a distilled example:

mutual
def foo (n: Nat) :=
  match n with
  | Nat.zero => trivial
  | Nat.succ pred => bar pred

def bar (n: Nat): True := foo n
end

This simple example actually compiles, because Lean figures out a workable measure on its own. However, in my actual code, I need to have explicit termination_by clauses, because some of my recursive functions do need a more complex termination measure that Lean cannot figure out on its own, (and mutually recursive functions are required to all have termination_by clauses if at least one does). termination_by sizeOf n does not work, because bar does not decrease the argument when calling foo.

Question: How may I prove termination of the above with explicitly defined termination measures?

Answer 1

The trick is to "order" the functions themselves by using a product as the measure. Here's a working example:

mutual
def foo (n: Nat) :=
  match n with
  | Nat.zero => trivial
  | Nat.succ pred => bar pred
termination_by (sizeOf n, 0)

def bar (n: Nat): True := foo n
termination_by (sizeOf n, 1)
end

This is easily discoverable by using termination_by? as the termination clause – with this construct (described eg. here), Lean will zeroth attempt to derive a working termination measure, and then suggest the measure to the user. A little confusingly, however, it only works after it is added to all the functions.