Nat.recON for defining a computation function

Stream: lean4

[Mukesh Tiwari]

Hi everyone, why does the function succ_nat below fail to compute?

More context on why I am writing the function like this: my partner is learning Lean and currently she is trying to understand induction on natural numbers. She has a good understanding of dependent function so I tried to challenge her a bit by asking her to write a non-dependent function that takes a natural number n and return n + 1. We were able to write the code but we could not compute with it (see the error).

open Nat


theorem succ_nat (n : Nat) : Nat :=
  Nat.recOn (motive := fun _ => Nat) n
  1 (fun _ ih => ih + 1)


#eval succ_nat 3

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'succ_nat', and it does not have executable code

I wrote the code in Coq and it computes fine.

Section Nat.


  Definition succ_nat (n : nat) : nat :=
    nat_rect (fun _ => nat) 1
    (fun _ ih => ih + 1) n.

  Eval compute in (succ_nat 4).

  Check nat_rect.
   (* Type signature of nat_rect (just in case)
nat_rect : forall P : nat -> Type, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n *)

End Nat.

[Richard Copley]

When I try with the current toolchain, your first example gives the error type of theorem 'succ_nat' is not a proposition, and the example below gives the error code generator does not support recursor 'Nat.recOn' yet, consider using 'match ... with' and/or structural recursion. Hopefully that clears things up? Seems like you're not doing anything wrong but you have encountered a limitation.

def succ_nat (n : Nat) : Nat :=
  Nat.recOn (motive := fun _ => Nat) n
  1 (fun _ ih => ih + 1)

[Henrik Böving]

Recursors are not supported by the Lean compiler for a couple of reasons. You can still run #reduce which instead of performing efficient computation with compiled code will symbolically evaluate your expression by using reduction rules from lambda calculus. These rules do of course support the recursor.

[Mukesh Tiwari]

How do update Lean? Currently I am using

mukesh.tiwari@Mukeshs-MBP-2 ~ % lean --version
Lean (version 4.7.0, aarch64-apple-darwin, commit 6fce8f7d5cd1, Release)

So how I can update it to the latest stable version?

[Henrik Böving]

Usually your lean projects will contain a lean-toolchain file in which you can put your specific lean version, that way you can have multiple lean versions for different projects on the same machine

[Mukesh Tiwari]

Thanks you very much @Henrik Böving @Richard Copley !

[Yaël Dillies]

I at least see one glaringly obvious error: succ_nat should not be a theorem but a def I failed to see this was already mentioned