Zulip Chat Archive

Stream: new members

Topic: Making a type


view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Alex J. Best (Jun 28 2020 at 01:15):

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

view this post on Zulip Iocta (Jun 28 2020 at 02:33):

Is there a positive reals type?

view this post on Zulip 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