recursively defined function with more than one variable

Stream: new members

[rzeta0]

I'm continuing to explore recursively defined functions, this time introducing an extra variable:

$f(n)=\begin{cases} \:c & \;\text{if }n=0\\ \:2n-1+f(n-1) & \;\text{otherwise} \end{cases}$

I have tried and failed to write this in Lean. I'd welcome guidance.

Here is one failed attempt:

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

Another failed attempt:

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

Perhaps I should be thinking about $f(c, n)$ instead?

$f(c, n)=\begin{cases} \:c & \;\text{if }n=0\\ \:2n-1+f(c, n-1) & \;\text{otherwise} \end{cases}$

For now I don't plan on using c to be anything other than a free constant subject only to the constraint that it is a natural number - f n would be preferable to f c n.

[Damiano Testa]

Are you sure that the issue is not simply that the notation for Nat is not in scope?

[Damiano Testa]

Adding import Mathlib makes your code compile.

[rzeta0]

here's an MWE that fails:

import Mathlib.Tactic

def f : ℕ → ℕ
  | 0 => (c : ℕ) -- < -- red line under c
  | n + 1 => 2 * n + 1 + f  n

this MWE works:

import Mathlib.Tactic

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

Is it possible to change this one so that calls to f are f n and not f c n?

I want to have c as an algebraic object but not use it as a parameter passed to f, just a constant inside the definition.

[Damiano Testa]

The value of the function does depend on c, so Lean needs to have access to c one way or another.

[Damiano Testa]

Depending on what you want to do with f, you can try to "hide" the fact that c is an input to your function, but what solution is appropriate, depends on the goal.

[Damiano Testa]

Here are ways of "hiding" the dependence on c, but each one comes with its shortcomings:

import Mathlib.Tactic

namespace A
opaque c : Nat

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

end A

namespace B
axiom c : Nat

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

end B

namespace C
abbrev c := 42

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

end C

[Edward van de Meent]

if you only want to hide the recursion on c in the definition, the following works:

def f (c : ℕ) : ℕ → ℕ := go where
  go
  | 0 => c
  | n + 1 => 2 * n + 1 + go n

[Ilmārs Cīrulis]

Do you mean smth like this?

import Mathlib

def c := 123

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

#check f

[Kyle Miller]

@Damiano Testa No neeed for opaque/axiom/abbrev. You can make these be actual parameters to the function using variable.

variable (c : ℕ)

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

#check (f)
-- f : ℕ → ℕ → ℕ

[Kyle Miller]

Best to wrap that in section ... end to limit the scope of variable.

You also can see this in the wild:

variable (c : Nat) in
def f : Nat → Nat
  | 0 => c
  | n + 1 => 2 * n + 1 + f n

[Damiano Testa]

Sure, that also works, but I was aiming to get the signature of f to not have c.

[Damiano Testa]

If f is allowed to be a function of 2 variables, then I agree that all of my suggestions have some form of flaw.

[Kyle Miller]

The opaque/axiom/abbrev solutions should come with a big proviso that they are global constants and are completely unchangeable after the definition of f, not constants in the "parameters that tend to take fixed values" sense that you can find in informal mathematics.

[Kyle Miller]

Is it possible to change this one so that calls to f are f n and not f c n?

You did answer this question for "call f like f n for all time", and my answer is just "call f like f n from within the definition of f, but after that it is f c n".

[Dan Velleman]

@rzeta0 : I'm not sure why you called this a failed attempt:

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

It works fine for me. Is the issue that you wanted a function of one variable, n, not two variables, c and n? Actually, you do have a function of the one variable n here. Let me explain.

People often think of the function f above as a function of two variables, but that's not quite accurate. f has type ℕ → ℕ → ℕ, which means ℕ → (ℕ → ℕ). So it is a function of one variable, and when you apply that function to a natural number c, the result has type ℕ → ℕ; in other words, if c is a natural number, then f c has type ℕ → ℕ, so it is a function from ℕ to ℕ. You can then apply that function to a natural number n by writing f c n, and the result is a natural number. The point is that you can write f c, and that's a meaningful expression, and it denotes the function that I think you are interested in. (People sometimes call this a partial application of the function f.) For example, f 3 is the function given by the following definition:

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

This is not that different from ordinary mathematical notation. For example, you might have wanted to indicate the fact that your function $f$ depends on $c$ by calling it $f_c$ instead of $f$. Well, f c is Lean notation for $f_c$.