How does one show termination of a function that is structurally recursive over a type T with subterms of type List T?

Question

I've been having a bit of difficulty proving termination of a particular kind of function. I'm quite new to using Lean, so it's possible that what I'm missing is a language feature and not a technique, but here goes.

To show what I mean, consider the following type of trees.

inductive Tree (α : Type u) : Type u where
  | empty : Tree α
  | node : α → List (Tree α) → Tree α

Consider then some function that traverses a tree, like this one.

def Tree.number_of_nodes : Tree α → Nat
  | .empty => 0
  | .node _ ts => List.foldl (fun a e => a + number_of_nodes e) 1 ts

The function is not accepted because termination cannot be proved automatically. "Structural recursion cannot be used."

My question then: what is the best approach to prove termination of functions like these, where it feels like the answer to the question "why does this function terminate" is "structural recursion, of course", but where that's obscured to the checker by the fact that the recursion is on a subterm of an immediate subterm, and not on the immediate subterm itself?

This comes up a lot whenever a type is given a definition where some container (a List, in this case) is used to hold values of the same type being defined. For example, if the type were that of binary trees, where the "intermediate" type were Tree α × Tree α instead of List (Tree α), the same error message would arise.

So far, I've been unable to think of a well-founded relation to give to termination_by in these cases, so I end up writing decreasing_by admit, but I'd like to stop doing that for obvious reasons.

P.S. I'm using the latest Lean 4 through the Code extension.

P.P.S. Any resources about techniques for showing termination in other cases are welcome as well, even if not Lean specific, but that's really for another question.

Answer 1

For reference, in Coq, termination checking “just works” on this function:

Require Import List.

Inductive tree {A : Type} : Type :=
| empty : tree
| node (x : A) (ts : list tree) : tree.
Arguments tree A : clear implicits.

Fixpoint number_of_nodes {A} (t : tree A) : nat :=
  match t with
  | empty => 0
  | node x ts => fold_left (fun a e => a + number_of_nodes e) ts 1
  end.

This is a bit mysterious, so we should work out why this works in Coq but not Lean (or Agda or Idris, for that matter). To my understanding, the crucial component is the separation between the top-level definition fold_left and the checked fixpoint operator fix which provides its recursion.

Let us look at the definition of fold_left, and also the core term this definition elaborates to. The definition looks a bit strange because of this Section business, but this actually turns out to be crucial. In the core term, we can see that fold_left is of the form fun A B (f : A -> B -> A) => fix .... The arguments A, B, and f appear outside the fix construct because, in the source program, they were bound in the Section, outside the Fixpoint declaration.

Section Fold_Left_Recursor.
  Variables (A : Type) (B : Type).
  Variable f : A -> B -> A.

  Fixpoint fold_left (l:list B) (a0:A) : A :=
    match l with
      | nil => a0
      | cons b t => fold_left t (f a0 b)
    end.

  (* ... *)

End Fold_Left_Recursor.

Arguments fold_left [A B]%type_scope f%function_scope l%list_scope a0.

Print fold_left.

(*
fold_left =
fun (A B : Type) (f : A -> B -> A) =>
fix fold_left (l : list B) (a0 : A) {struct l} : A :=
  match l with
  | nil => a0
  | b :: t => fold_left t (f a0 b)
  end
     : forall A B : Type, (A -> B -> A) -> list B -> A -> A
 *)

Back in number_of_nodes, the termination checker sees the definition as follows. I have inlined the definition of fold_left, β-reduced away arguments A, B, and f, and β-reduced away the two arguments to f. The termination checker is happy to unfold definitions and do β-reductions, because these steps on their own are not recursive, and thus do not jeopardise the termination of the termination checking algorithm itself. However, we cannot do any unfolding of the fix construct, because it would become unclear when to stop. In Lean (I'm guessing), the equivalent of the fix construct appears immediately at the top of the function definition, stopping all of these β-reductions happening.

Fixpoint number_of_nodes {A} (t : tree A) : nat :=
  match t with
  | empty => 0
  | node x ts =>
    (fix fold_left (l : list (tree A)) (a0 : A) {struct l} : A :=
      match l with
      | nil => a0
      | e :: es => fold_left es (a0 + number_of_nodes e)
      end) ts 1
  end.

The important feature is that the occurrence of number_of_nodes is now applied to its argument (e), so we can ask whether e is structurally smaller than t. This seems plausible: ts is smaller than t because it's an argument to its constructor. Then, l is structurally decreasing in the fix-construct, so it is at most as big as ts in all calls. Finally, e is smaller than l, so by transitivity, we get what we wanted.

---

Thanks to Andrej for suggesting I write up this answer.

Answer 2

The part of Lean that tries to determine whether recursion is well-founded does not look inside definitions (it's dangerous to do so when one is dealing with recursive definitions). You can solve the problem by showing the definition of foldl down its throat.

inductive Tree (α : Type u) : Type u where
  | empty : Tree α
  | node : α → List (Tree α) → Tree α

def Tree.number_of_nodes : Tree α → Nat
  | .empty => 0
  | .node _ ts => foldl 1 ts
where
    foldl : Nat → List (Tree α) → Nat
      | n, [] => n
      | n, (t :: ts) => foldl (n + number_of_nodes t) ts

#eval Tree.number_of_nodes (.node 1 [.node 2 [], .node 3 [.node 5 []]])

It's not ideal, perhaps someone else knows a better way.