4
$\begingroup$

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?

$\endgroup$

1 Answer 1

5
$\begingroup$

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
$\endgroup$
3
  • $\begingroup$ Thank you this is exactly what I was looking for :) $\endgroup$ Mar 8, 2023 at 14:10
  • $\begingroup$ Out of curiosity: how does this get elaborated in the kernel? To a mutual definition, or to a first-order fixpoint? $\endgroup$ Mar 9, 2023 at 10:14
  • 1
    $\begingroup$ @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. $\endgroup$
    – Jason Rute
    Mar 9, 2023 at 12:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.