## Stream: new members

### Topic: fail to show termination for comparison of recursive struct

#### awalterschulze (Nov 20 2022 at 14:24):

A relatively minimal example, which has a recursive structure on which we are trying to do lexicographical comparison efficiently, by first comparing with a pre-calculated hash before traversing the recursive structure.

inductive Desc where
| intro
(name : String)
(hash : UInt64)
(params : List Desc)
: Desc
deriving Repr

-- Returns the lexicographical comparison of two lists
def lexLists (c: α -> α -> Ordering): List α -> List α -> Ordering
| x::xs, y::ys =>
let r := c x y
if r != Ordering.eq
then r
else lexLists c xs ys
| _, _ => Ordering.eq

def cmp (x y: Desc): Ordering :=
match x with
| ⟨xname, xhash, xparams⟩ =>
match y with
| ⟨yname, yhash, yparams⟩ =>
let chash := compare xhash yhash
if chash != Ordering.eq
then chash
else
let cname := compare xname yname
if cname != Ordering.eq
then cname
else lexLists cmp xparams yparams


This gives the following error:

fail to show termination for
cmp
with errors
structural recursion cannot be used

failed to prove termination, use termination_by to specify a well-founded relation


I have had a similar problem in Coq, which we solved with a inline fix, see

https://github.com/katydid/proofs/blob/old-coq/src/Symbolic/Ast/CmpSmartFunc.v#L29

From what I read Lean4 had a smarter termination checker, but I guess this is still a tough one to crack.
Is there a way to declare an inline recursive function in Lean4 and would that possibly help the termination checker?

#### awalterschulze (Apr 25 2023 at 10:12):

Found a solution on stack exchange https://proofassistants.stackexchange.com/questions/2035/is-there-a-way-in-leanprover-to-declare-an-inline-recursive-function-like-fix-i

#### Kevin Buzzard (Apr 25 2023 at 10:50):

That's cool that the SE site is helpful.

Last updated: Dec 20 2023 at 11:08 UTC