Is there a way in LeanProver to declare an inline recursive function, like fix in Coq?

Question

Is there a way to declare an inline recursive function, like fix in Coq?

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. I also had the same question about Coq.

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?

Answer 1

You can use let rec or where to introduce a helper function mutually recursive with cmp and Lean will automatically prove (well-founded) termination.

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' xparams yparams
where lexLists'
  | x::xs, y::ys =>
    let r := cmp x y
    if r != Ordering.eq
    then r
    else lexLists' xs ys
  | _, _ => Ordering.eq