Determining whether a definition is recursive

Stream: metaprogramming / tactics

[Jannis Limperg]

I'm trying to determine whether a name d refers to a recursive definition. My first idea was to check whether d occurs in its own value, but that doesn't work for well-founded and mutual recursion. E.g. the mutual block

mutual
  def f : Nat → Nat
    | 0 => 0
    | n + 1 => g n

  def g : Nat → Nat
    | 0 => 0
    | n + 1 => f n
end

compiles to f x = f._mutual ... x ... with f_mutual an application of WellFounded.fix and f nowhere in sight.

I think I can work around this for my actual application, but I'd still be curious whether there's a nice way to figure this out.

[Damiano Testa]

Does docs#Lean.isRec help?

[Mario Carneiro]

no, that tells you if a definition is an inductive recursor

[Mario Carneiro]

you could either look at the equation lemmas, or you could look at the compiled IR to find the self reference

[Mario Carneiro]

Although, f._mutual in the definition is also a clear indicator that the definition is recursive

[Alex J. Best]

You could also recursively search through definitions of constants occuring in the value (knowing that you can ignore declarations defined in some dependent module)

[Mario Carneiro]

@Alex J. Best that won't help, the kernel definition is in fact acyclic

[Mario Carneiro]

that's what the fix reduction is about

[Alex J. Best]

Oh right!

[Mario Carneiro]

I think you can use docs#Lean.Compiler.mkUnsafeRecName to get the name of the compiler's partial def corresponding to a recursive function, if it exists and/or is a mutualDefnDecl then I think you found a recursive function

[Mario Carneiro]

import Lean

mutual
  def f : Nat → Nat
    | 0 => 0
    | n + 1 => g n

  def g : Nat → Nat
    | 0 => 0
    | n + 1 => f n
end

mutual
  def f' : Nat → Nat
    | 0 => 0
    | n + 1 => g' n

  def g' : Nat → Nat
    | 0 => 0
    | n + 1 => g' n
end

open Lean

def isRecursive (env : Environment) (n : Name) : Bool := Id.run do
  env.contains (Lean.Compiler.mkUnsafeRecName n)

#eval show Elab.Command.CommandElabM _ from do
  println! isRecursive (← getEnv) ``f -- true
  println! isRecursive (← getEnv) ``g -- true
  println! isRecursive (← getEnv) ``Nat.add -- true
  println! isRecursive (← getEnv) ``Nat.succ -- false
  println! isRecursive (← getEnv) ``Nat -- false
  println! isRecursive (← getEnv) ``f' -- false
  println! isRecursive (← getEnv) ``g' -- true