Difference between structural and well-founded recursion

Stream: new members

[Vivek Rajesh Joshi]

While reading TPIL chapter 8 (Induction and recursion), I came across this example of well-founded recursion:

open Nat

theorem div_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
  fun h => sub_lt (Nat.lt_of_lt_of_le h.left h.right) h.left

def div.F (x : Nat) (f : (x₁ : Nat) → x₁ < x → Nat → Nat) (y : Nat) : Nat :=
  if h : 0 < y ∧ y ≤ x then
    f (x - y) (div_lemma h) y + 1
  else
    zero

noncomputable def div := WellFounded.fix (measure id).wf div.F

Although it's a bit hard for me to figure out what is going on here, I can see that div is a well-founded recursive function, since it is defined in terms of the arguments for WellFounded.fix . However, in the next definition, I don't understand the role that well-foundedness of < plays:

def div (x y : Nat) : Nat :=
  if h : 0 < y ∧ y ≤ x then
    have : x - y < x := Nat.sub_lt (Nat.lt_of_lt_of_le h.1 h.2) h.1
    div (x - y) y + 1
  else
    0

This definition seems to be the same as a structurally recursive definition. What is the difference between the two? Why does Lean not use structural recursion to compile this definition?

[Henrik Böving]

In structural recursion the proof of termination works out as follows: We can see that for some argument, each time that we make a recursive call, there is at least one constructor of that argument removed. This allows Lean to do a translation to a more basic concept called recursors. Recursors is how the kernel actually thinks about recursive pattern matching function, it doesn't have a built in notion of matches and stuff like that.

Then with well founded recursion you can basically do whatever you want with an argument as long as some function on your arguments decreases by some well founded relation (sometimes you even have to tell lean yourself which one that is). This makes a translation to recursors much harder because they very closely represent the idea of structural recursion and only that. So now you need some way to tell the underlying type theory about what you are doing and that way is WellFounded.fix

Now if you look at the definition of div. From the POV of the thing that handles pattern matching it cannot really tell that x - y makes the 1st argument structurally smaller. Sure we know that since y > 0 it must do that (and that x cannot be 0 due to the additiobal condition in the if) because we know about how - works but that is not something that this part of the system can figure out on its own.