How to know if a function is recursive?

Stream: lean4

[Abdalrhman M Mohamed]

Is there a utility in Lean that tells if a function is recursive, mutually recursive, or not recursive?

-- recursive
def Nat.add' : Nat → Nat → Nat
  | 0     , b => b
  | succ a, b => succ (add' a b)

-- not recursive
def Nat.double x := Nat.add' x x

mutual
-- mutually recursive
def Nat.odd : Nat → Bool
  | 0     => false
  | n + 1 => ¬(even n)

-- mutually recursive
def Nat.even : Nat → Bool
  | 0     => true
  | n + 1 => ¬(odd n)
end

[Leonardo de Moura]

We currently don't have an API for directly answering this question, but we can add it.
How are you planning to use it? I am assuming this is for the CVC 5 <-> Lean interface :)
So, I am assuming you also want to know whether a function is tagged as partial or not.
If it is mutually recursive, I am assuming you also want to retrieve all functions in the mutual block, correct?
We have all this information internally, but we need to figure out how to provide it in a convenient way.

[Arthur Paulino]

Leonardo de Moura said:

all functions in the mutual block

Is this currently available? I know we have it for inductives. But for definitions we're computing it in a more involved way. If we have it as an attribute of DefinitionVal that would be great :pray:
CC: @Hanting Zhang @John Burnham

[Leonardo de Moura]

@Arthur Paulino I will add an API for retrieving this information.

[Wojciech Nawrocki]

Fwiw, the two places I went looking for this were FunInfo and DefinitionVal. Either one seems fairly natural/convenient.

[Arthur Paulino]

For us, having it available in DefinitionVal would be ideal because we're building on top of Lean.Environment. I don't recall seeing FunInfo :thinking:

[Abdalrhman M Mohamed]

How are you planning to use it? I am assuming this is for the CVC 5 <-> Lean interface :)

Yes. You're right!

If it is mutually recursive, I am assuming you also want to retrieve all functions in the mutual block, correct?

That would be awesome!!! It would be nice to have something similar for mutual datatypes

[Leonardo de Moura]

We now have

def ConstantInfo.all : ConstantInfo → List Name

The name is not great, but it is consistent with InductiveVal.all.
The test suite has an example: https://github.com/leanprover/lean4/blob/98c775da3472401c03f7688b4292e6ee3a25bba3/tests/lean/allFieldForConstants.lean
Recall that Lean breaks a mutual block into strongly connected components. Example:

mutual
  partial def f (x : Nat) : Nat :=
    if x < 10 then g x + 1 else 0
  partial def g (x : Nat) : Nat :=
    f (x * 3 / 2)
  partial def h (x : Nat) : Nat :=
    f x
end

#eval printMutualBlock ``f -- [f, g]
#eval printMutualBlock ``g -- [f, g]
-- Recall that Lean breaks a mutual block into strongly connected components
#eval printMutualBlock ``h -- [h]

[Leonardo de Moura]

The new data is ignored by the Lean kernel.

[Arthur Paulino]

Thanks!!

[Guilherme Reis]

Hey guys, how can I do this VClosure type?

inductive Value where
  | VInt (value : Int)
  | VClosure (context : Std.HashMap String Value)

the error that I'm getting: (kernel) arg #1 of 'Value.VClosure' contains a non-valid occurrence of the datatypes being declared

[Arthur Paulino]

@Guilherme Reis I'd recommend asking this question in a dedicated thread :+1:

[Mario Carneiro]

One interesting consequence of the SCC algorithm used in mutual compilation is that you can use mutual definitions to declare non-mutual definitions out of order:

mutual
  def f (x : Nat) : Nat := g x
  def g (x : Nat) : Nat := x
end

As far as I can tell there is no difference between these functions and:

def g (x : Nat) : Nat := x
def f (x : Nat) : Nat := g x

So this might be useful for writing functions out of order for presentation purposes or something.