Polymorphic definitions

Stream: new members

[Saif Ghobash]

Is there any way I can have two definitions with the same name, for example, I would prefer having one definition of convergence of a sequence, convergence to 0 and to non-zero values. So here is an example

def converges (f : ℕ → ℝ) (a : ℝ):=
∀ ε : ℝ, 0 < ε → ∃ N : ℕ , ∀ n : ℕ, n > N  → abs (f n - a) < ε

def converges (f : ℕ → ℝ) :=
∀ ε : ℝ, 0 < ε → ∃ N : ℕ , ∀ n : ℕ, n > N  → abs (f n) < ε

Its a simple example, and it probably just makes sense to have the first definition and simply use 0 as the proposed limit, however would it be possible to have lean infer the proper definition depending on the context?

[Ryan Lahfa]

It is possible to mark variables as implicit, e.g. {a: \R}

[Ryan Lahfa]

Lean will try to provide a value based on the context

[Ryan Lahfa]

Though, it will not fix your problem, I'm not sure what sense it is to say converges f without specifying any limit, except: there is a limit l such that converges_limit f l for example.

[Saif Ghobash]

@Ryan Lahfa It doesn't make that much sense, but it was just an example to see if it is possible.

[Ryan Lahfa]

I'm not aware of polymorphic definitions in this sense, in Lean, and it's non-obvious to me to find the closest natural usecase for your idea @Saif Ghobash

[Saif Ghobash]

@Ryan Lahfa It may not be very useful in math, however it is used in programming languages (Java etc) as an abstraction mechanism so it would have use cases in that sense.

[Saif Ghobash]

since lean is also a programming language.

[Ryan Lahfa]

@Saif Ghobash In that case, you just want to generalize over the arguments types, right? In those languages, e.g. Java, Rust, etc. they use generics, generics are quite first class in Lean.

Rather if your question is whether is it possible to specialize a generic function, I guess you can just pattern match your arguments and provide inductive definitions? But maybe there is a better way to do it.

[Alex J. Best]

One way is to use a "notational" typeclass, e.g. like we do use the symbol + to mean addition of naturals, addition of reals etc. I'm not sure how to do this in a way to have variable number of arguments but maybe

import data.nat.basic
import data.real.basic
class has_converges (α : Type) := (converges : α → Prop)
open has_converges
instance :has_converges ((ℕ → ℝ) × ℝ):= ⟨λ ⟨f, a⟩,
∀ ε : ℝ, 0 < ε → ∃ N : ℕ , ∀ n : ℕ, n > N  → abs (f n - a) < ε⟩
#check converges (λ n : ℕ, 1/ (n:ℝ), (0:ℝ))

instance : has_converges (ℕ → ℝ) := ⟨λ f,
∀ ε : ℝ, 0 < ε → ∃ N : ℕ , ∀ n : ℕ, n > N  → abs (f n) < ε⟩

#check converges (λ n : ℕ, 1/ (n:ℝ))

is close to what you want?

[Alex J. Best]

For your original example you can also use default arguments, but it sounds like thats not really what your question was

import data.nat.basic
import data.real.basic
def converges (f : ℕ → ℝ) (a : ℝ := 0):=
∀ ε : ℝ, 0 < ε → ∃ N : ℕ , ∀ n : ℕ, n > N  → abs (f n - a) < ε

#check converges (λ n, n)
#check converges (λ n, n) 1

[Saif Ghobash]

@Alex J. Best Yeah my original example could've used defaults, but the first piece of code you gave is what I needed, thank you!
And thank you @Ryan Lahfa .

[Reid Barton]

You can also just use two names in different namespaces.

[Reid Barton]

It might help if you gave a non-artificial example of what you want to do.