Assisting Agda's termination checker to make a recursive function

Question

Suppose we wish to define a function for some types A₀ ⋯ Aₙ and B

f : A₀ ⋯ Aₙ → B
f x₀ ⋯ xₙ = ... recursive call to f ...

Assume that this definition is not structurally recursive.

Assume also that I have definitions for the following:

1. a function g : A₀ ⋯ Aₙ → ℕ which takes some subset of the arguments of f to a natural number;

2. for every case of f: a proof that g of the arguments passed to the recursive call is strictly smaller than g of the incoming arguments (using the built-in _<_ or _<′_ relation on natural numbers).

How would I put these parts together to make a recursive function, using the Induction modules from the Agda "standard" library?

---

This question is a follow-up to this question on the same subject, to which very complete answers have been given. However, I feel that the example function's type was unfortunately chosen as ℕ → ℕ, which makes it hard for me to see how this extends to the general case.

Also, note that I'm not expecting a large answer with explanation on the workings behind well-founded induction and its implementation in Agda, as @Vitus as kindly provided quite an elaborate answer for this.

Answer 1

If you have a function A → B and you know that B has a well-founded relation, you can construct a well-founded relation on A:

_<_ : B → B → Set
f   : A → B

_≺_ : A → A → Set
x ≺ y = f x < f y
-- or more concisely
_≺_ = _<_ on f -- 'on' come from Function module

Proving that _≺_ is also well-founded isn't that hard, but it's already in standard library so we'll just use that:

open Inverse-image
  {A = A}     -- new type
  {_<_ = _≺_} -- new relation
  f
  renaming (well-founded to <⇒≺-well-founded)

The Inverse-image exports well-founded value as the proof. We can then use this value to get the actual function that does recursion for us:

≺-well-founded = <⇒≺-well-founded <-well-founded

open All (≺-well-founded)
  renaming (wfRec to ≺-rec)

And that's it, ≺-rec can now be used to implement recursive functions with A as an argument type.

---

The ≺-rec is then used roughly as:

g : A → C
g = ≺-rec
  _  {- level paremeter -}
  _  {- A → Set; return type in case Agda cannot figure out the dependency -}
  go {- helper function -}
  where
  go : ∀ x → (∀ y → y ≺ x → C) → C
  go x rec = ... (rec arg proof) ...

arg is the argument to the recursive occurence and proof is a proof that the argument is actually smaller.

When the return type depends on the arguments, the helper function looks roughly like this:

go : ∀ x → (∀ y → y ≺ x → C y) → C x

---

When dealing with functions with multiple arguments, you will need to bunch those into a single type so that the relation can talk about all of them. This usually means pairs or, in case there's a dependency between arguments, dependent pairs.