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
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
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):
nnreal for the reals
Last updated: May 10 2021 at 17:39 UTC