fail to show termination for comparison of recursive struct

Stream: new members

[awalterschulze]

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]

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]

That's cool that the SE site is helpful.