Making a type

Stream: new members

[Iocta]

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]

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]

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]

(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]

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]

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]

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

[Iocta]

Is there a positive reals type?

[Alex J. Best]

There is nnreal for the reals \ge 0