RFC: Recursive functions mutual with (pointwise) proofs

It is often required to define a recursive function together with properties of that recursive function:

• When using nested recursion, often one needs to know something about the result of the function (e.g. smaller than the argument).
• When using functions with proof arguments (e.g. xs[i]), a similar question arises.

Usually, when this comes up, the best we can do is to change the result type of the function to a subtype, to make the properties available to the otherwise opaque recursive calls.

But this is tedious: it makes the code more verbose and technical, and generated artifacts (equational theorems, functional induction theorems) are not in the expected form and may need to be redefined.

It would be more natural if one could just write

mutual
def f : (x : X) → Y := …
theorem P_f : (x : X) → P (f x) := …
end

and Lean would do the transformation to

mutual
def f_P_f : (x : X) → {y : Y // P y} := …
end
def f (x : X) : Y := (f_P_f x).1
def P_f (x : X) : P (f x) := (f_P_f x).2

automatically under the hood.

Right now, this is a non-starter, because already the declaration heads in a mutual group must not mention each other. We’d have to somehow relax this requirement, and then recognize the supported patterns (and give good error messages otherwise).

Once we get past this, the rest seems to be “just engineering”, actually quite similar to what we already do to allow mutual structural recursion.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

This RFC names no files, tests, or entry points. Start by examining the implementation of mutual structural recursion and the restriction that mutual declaration heads must not mention each other. Done means supporting the described recursive-function and pointwise-proof pattern while preserving expected generated theorems and producing useful errors for unsupported patterns.