## Stream: new members

### Topic: Polymorphic definitions

#### Saif Ghobash (Jan 30 2021 at 21:50):

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 (Jan 30 2021 at 21:58):

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

#### Ryan Lahfa (Jan 30 2021 at 21:58):

Lean will try to provide a value based on the context

#### Ryan Lahfa (Jan 30 2021 at 21:59):

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 (Jan 30 2021 at 22:03):

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

#### Ryan Lahfa (Jan 30 2021 at 22:04):

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 (Jan 30 2021 at 22:10):

@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 (Jan 30 2021 at 22:10):

since lean is also a programming language.

#### Ryan Lahfa (Jan 30 2021 at 22:12):

@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 (Jan 30 2021 at 22:21):

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 (Jan 30 2021 at 22:22):

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 (Jan 30 2021 at 22:23):

@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 (Jan 30 2021 at 22:24):

You can also just use two names in different namespaces.

#### Reid Barton (Jan 30 2021 at 22:24):

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

Last updated: Dec 20 2023 at 11:08 UTC