rule for recursive part of recursive function

Stream: new members

[rzeta0]

The following is a simple example of a recursively defined function:

def f : ℕ → ℕ
  | 0 => 0
  | n + 1 => 2 * n + 1 + f n

Initially I thought the recursive part | n + 1 => 2 * n + 1 + f n was required to map from n + 1. I thought this because that is what induction proofs must do in the inductive step.

I was wrong, confirmed when I saw in MoP that some functions mapped from n + 2.

So the question I ask myself is, what are the constraints on a recursively defined function.

The only one I can guess at is that if n is a natural number, then no part of the definition can use subtraction.

I assume Lean doesn't check for contradictory branches of the definition, eg:

def f : ℕ → ℕ
  | 0 => 0
  | 0 => 1 -- < -- contradicts
  | n + 1 => 2 * n + 1 + f n

or gaps, eg the follow doesn't define f 3

def f : ℕ → ℕ
  | 0 => 0
  | 1 => 0
  | n + 5 => 2 * n + 1 + f n

Am I right?

[Eric Wieser]

Did you try just typing those into Lean and seeing what happens?

[Eric Wieser]

e.g. the first one you can test with #eval f 0

[rzeta0]

Both give an error when I try it - which is re-assuring.

These are just my guesses at scenarios which are not allowed and checked for by Lean.

There may be others?

[Kevin Buzzard]

You can just experiment yourself here, right?

[nrs]

you will get a clearer idea of the lower-level definition here by replacing the pattern-matching with a Nat.casesOn (the definition must first produce a successful translation of the match into Nat.casesOn before recursion is elaborated)

[nrs]

to study this you may use whatsnew in over functions you are used to. the Nat.brecOn part of the resulting output arises after recursion is elaborated. the match statement contained within (within the Nat.brecOn function, in the whatsnew in output) is the statement as it is before recursion elaboration