# Non-trivial recursive function: how to prove recursion is well-founded?

I am trying to formalize the Church-Rosser theorem for the untyped-lambda calculus. There are actually multiple such theorems, depending on whether one is considering only beta-reduction, or beta- and eta-reduction, or something more exotic. I would like my implementation to be parameterized so that I can reuse it across different reduction modalities.

I am following Selinger’s lecture notes, which explains the classic proof due to Tait and Martin-Löf. The step on page 35 is to implement the maximal one-step parallel reduction operation.

This operation can be explained as follows: if the term under examination is amenable to the reduction(s) being considered (eta, beta, both, …) then first recurse on the subterms, and then perform a reduction on the result. Otherwise, immediately recurse on the subterms.

Implementing this in such a way that the reduction is pluggable requires passing a callback to the reduction function. Here is a sketch implementation for beta reduction:

``````(* Perform beta reduction, and call the continuation on the resulting subterms.*)
Definition subst (cont: Term -> Term) (t: Term): option Term :=
match t with
| (\t1) \$\$ t2 => Some(subst (cont t1) (cont t2))
| _ => None
end.

Section reduction.
Hypothesis op: (Term -> Term) -> Term -> option Term.

Definition maximal_parallel_reduction: Term -> Term :=
fix f (t: Term) :=
match op f t with
| Some t' => t'
| None =>
match t with
| Var n => Var n
| t1 \$\$ t2 => (f t1) \$\$ (f t2)
| \t' => \(f t')
end
end.
End reduction.
``````

Now Coq’s checks for well-founded recursion don’t agree with the call `op f t`. I’ve never had to deal with non-trivial recursion in Coq. Is my best guess to work with `well_founded`?

Recursive occurrences of a `fix`point must be applied to a subterm of its decreasing argument. Here in `op f t`, `f` is not applied to anything.

This would probably be accepted if you replace the `op` parameter with `subst` , because it unfolds to applications of `cont` (that is `f`) to subterms of `t`.

It is also common to have to rephrase “pen and paper” definitions so they’re easier to formalize in Coq. The definition you gave translates to three somewhat overlapping `match` expressions. You can do it with a single match, at the cost of a little more verbose definition in English.

``````  fix f t :=
match t with
| Var n => Var n
| (\ t1) \$\$ t2 => subst (f t1) (f t2)
| t1 \$\$ t2 => f t1 \$\$ f t2
| \t' => \(f t')
end.
``````