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

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?

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

• Thank you this is exactly what I was looking for :) Mar 8, 2023 at 14:10
• Out of curiosity: how does this get elaborated in the kernel? To a mutual definition, or to a first-order fixpoint? Mar 9, 2023 at 10:14
• @Mevenlennon-Bertrand I don’t know the terminology well enough, but it creates a mutual definition that both functions call and that definition uses Wellfounded.fix (I assume to show the definition is well founded). You can easily see the details with #print if you have lean 4 installed or use the online editor. Mar 9, 2023 at 12:00