RFC: Mutual structural recursion to support non-matching functions

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Mutually recursive functions cannot use structural recursion when one of the functions does not match on the inductive type.

Steps to Reproduce

mutual

def foo : Nat → Nat
  | 0 => 0
  | n + 1 => bar n
  termination_by structural n => n

def bar (n : Nat) : Nat :=
  foo n + 1

end

Expected behavior: Code succeeds with no errors.

Actual behavior: The following error:

error: failed to infer structural recursion:
Cannot use parameters #1 of foo and n of bar:
  failed to eliminate recursive application
    foo n

Versions

Lean 4.19.0-rc2

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal mutual-recursion example from the issue against the stated Lean 4.19.0-rc2 version and confirm the structural-recursion error. Investigate the structural recursion handling for mutually recursive definitions; done means the example compiles successfully without the reported error.