## Stream: new members

### Topic: Making a type

#### Iocta (Jun 28 2020 at 00:50):

I want to create a new type that should act exactly like real. I will later add some subtype predicates to it but for now I just want it to behave like real. How do I do that? I tried def myreal : Type := real but afaict that doesn't have has_mul.

#### Shing Tak Lam (Jun 28 2020 at 01:04):

I guess this might be what you want? I think this has all the properties (typeclasses) that real does? But in general you can just use variables and put whatever typeclasses you want the type of have.

import algebra.ordered_field

variables (myreal : Type) [discrete_linear_ordered_field myreal]


#### Alex J. Best (Jun 28 2020 at 01:05):

I'm not sure exactly what you want to achieve (it would help if you explained a little more what your actual goal is perhaps).
But you can do this:

@[derive has_mul]
def myreal := real


to add whatever instances you like automatically my transferring them from real, finding a list of all the possible instances on real wouldn't be recommended though.
You could also do

@[reducible]
def myreal := real


If you are going to make it a subtype of real later why not make it one now, but a trivial condition if you cant yet define the condition you want so that the type behaves like a subtype.

#### Iocta (Jun 28 2020 at 01:10):

(it would help if you explained a little more what your actual goal is perhaps).

Sure. I want to try proving some theorems from elementary probability as an exercise. I figured it would be easier to start by just saying "a probability is a real" and replace the definitions later, than to start from measure theory ... though I could be wrong

#### Iocta (Jun 28 2020 at 01:13):

import data.real.basic
import data.nat.basic
import data.complex.exponential

-- XXX For now ℝ denotes a probability, and real denotes a real.
-- This should be changed to an actual probability type.

def binomial_coefficient (n k : nat) : int :=
(nat.fact n) / ((nat.fact (n - k)) * (nat.fact k))

def binomial_pmf (n: nat) (p : ℝ) (k : nat) : ℝ  :=
(binomial_coefficient n k) * (p ^ k) * (1 - p) ^ (n - k)

def Poisson_pmf (lambda: real) (k: nat) : ℝ :=
(lambda ^ k) / ( (nat.fact k) * (real.exp lambda) )


I immediately run into definition 'Poisson_pmf' is noncomputable, it depends on 'real.division_ring', not sure what to do with that.

#### Alex J. Best (Jun 28 2020 at 01:14):

I'd recommend doing what @Shing Tak Lam says then, maybe not starting from discrete_linear_ordered_field but just has_mul or comm_semiring as variables, assumptions on what your type satisfies, then later if you actually construct the type with these properties all the theorems will apply.

#### Alex J. Best (Jun 28 2020 at 01:15):

you can add noncomputable theory at the top of the file (under imports)

#### Iocta (Jun 28 2020 at 02:33):

Is there a positive reals type?

#### Alex J. Best (Jun 28 2020 at 03:19):

There is nnreal for the reals \ge 0

Last updated: May 10 2021 at 17:39 UTC