Termination Checker Question

Stream: lean4

[Aaron Eline]

Ran into an unexpected (to me) failure of the termination checker, I was curious for more information about how the checker worked.

Here's a simple lean file that fails to compile:

import Std.Data.Nat
import Std.Data.List


inductive Expr where
    | lit : Nat -> Expr
    | add : Expr -> Expr -> Expr
    | mult : List Expr -> Expr


def sum (ns : List Nat) : Nat :=
    match ns with
    | [] => 0
    | n :: ns => n + (sum ns)

def sum_of_lits (e : Expr) : Nat :=
    match e with
    | .lit n => n
    | .add e1 e2 => (sum_of_lits e1) + (sum_of_lits e2)
    | .mult es => sum (List.map sum_of_lits es)

It fails to being unable to prove termination of the recursive call to sum_of_lits as an argument to List.map.

In Coq, the equivalent file:

Require Import Coq.Lists.List.
Open Scope list_scope.
Import ListNotations.

Inductive expr : Type :=
    | Num : nat -> expr
    | Add : expr -> expr -> expr
    | Mult : list expr -> expr.

Fixpoint sum (ns : list nat) : nat :=
    match ns with
    | [] => 0
    | (x::xs) => x + (sum xs)
    end.

Fixpoint sum_all_literals (e : expr) : nat :=
    match e with
    | Num n => n
    | Add e1 e2 => (sum_all_literals e1) + (sum_all_literals e2)
    | Mult es => sum (map sum_all_literals es)
    end.

Which compiles fine. I was curious about the differences in the termination checkers, is this a fundamental limitation of a lean design decision?

[Henrik Böving]

The difference between how termination is checked in lean and coq is quite drastical. The specific case that you have at hand is a nested inductive type which is not currently supported very well when it comes to automation sadly.

[Joachim Breitner]

That said, this is (one way) to make it work:

import Std.Data.Nat
import Std.Data.List


inductive Expr where
    | lit : Nat -> Expr
    | add : Expr -> Expr -> Expr
    | mult : List Expr -> Expr


def sum (ns : List Nat) : Nat :=
    match ns with
    | [] => 0
    | n :: ns => n + (sum ns)

def sum_of_lits (e : Expr) : Nat :=
    match e with
    | .lit n => n
    | .add e1 e2 => (sum_of_lits e1) + (sum_of_lits e2)
    | .mult es => sum (List.map (fun ⟨e, _⟩ => sum_of_lits e) (List.attach es))

[Aaron Eline]

Joachim Breitner said:

That said, this is (one way) to make it work:

Could you explain the List.attach?

[Henrik Böving]

It turns some list xs of as into a list of as that have a proof that they are a member of xs. This proof is enough to let the automation see that there is a well founded recursion going on.

[Aaron Eline]

Henrik Böving said:

It turns some list xs of as into a list of as that have a proof that they are a member of xs. This proof is enough to let the automation see that there is a well founded recursion going on.

Ah cool, thanks a bunch

[Joachim Breitner]

Also see https://lean-lang.org/blog/2024-1-11-recursive-definitions-in-lean/, section on nested recursion