Zulip Chat Archive

Stream: new members

Topic: reals


view this post on Zulip Alexandre Rademaker (Jul 02 2020 at 14:04):

I am trying to understand the outputs of:

#reduce 8.1    => 8
#eval 8.1         => 8
#check 8.1     => 81 / 10 : 
#eval (81 / 10) * 100 =>  800

Using Lean 'official' 3.4.2. I am trying to avoid having to reinstall everything. That is, removing the brew installation of Lean to install elan, mathlibtools and mathlib.

view this post on Zulip Reid Barton (Jul 02 2020 at 14:06):

Literals default to nat if there is no other type information available. Even fractional literals like 8.1. Yes, this is a bit silly.

view this post on Zulip Alexandre Rademaker (Jul 02 2020 at 14:08):

Let me give you more context. I am trying to see how far I can go in the translations of Haskell book examples to Lean. Reals appear in the cipher encoding example: https://gist.github.com/arademaker/73f5fb92601c0c129c95bea7fdbc7bf4

view this post on Zulip Reid Barton (Jul 02 2020 at 14:11):

In Haskell the translation of a fractional literal 8.1 is something like fromRational (81 % 10) where % is the division operator for Rational.

view this post on Zulip Reid Barton (Jul 02 2020 at 14:11):

If you just write a type annotation like #eval (8.1 : rat) then you'll get the expected result.

view this post on Zulip Alexandre Rademaker (Jul 02 2020 at 14:13):

Hi @Reid Barton , thank you. So I guess I will not be able to do it without the mathlib, right? It seems that rat type is not defined in the standard library of Lean.

view this post on Zulip Reid Barton (Jul 02 2020 at 14:14):

oh, I have no idea

view this post on Zulip Reid Barton (Jul 02 2020 at 14:14):

docs#rat

view this post on Zulip Reid Barton (Jul 02 2020 at 14:14):

I guess you're right.

view this post on Zulip Mario Carneiro (Jul 02 2020 at 14:17):

You can do it over an arbitrary field if you don't want to use mathlib

view this post on Zulip Mario Carneiro (Jul 02 2020 at 14:17):

although you will have to use 3.4.2 for that since fields have since been ripped out of core

view this post on Zulip Mario Carneiro (Jul 02 2020 at 14:20):

Here's a really silly rat-like type that works on 3.4.2:

def fraction :=  × 
instance : has_zero fraction := (0,1)
instance : has_one fraction := (1,1)
instance : has_add fraction := ⟨λ a b, (a.1 + b.1, a.2)
instance : has_div fraction := ⟨λ a b, (a.1, b.1)

#reduce (8.1 : fraction) -- (81, 10)

view this post on Zulip Alexandre Rademaker (Jul 02 2020 at 14:48):

Thank you so much @Mario Carneiro, but I didn't understand your remark about 3.4.2. You said that I could do it over a field but then you said 3.4.2 doesn't have field. Indeed, I didn't find in the Lean 3.4.2 core library the definition of field. Above it looks like you make a pair of natural numbers instances of four classes (I guess has_div can be seen as the inverse of has_mul) and this makes pair of nat numbers a field. Am I right?

view this post on Zulip Reid Barton (Jul 02 2020 at 14:50):

3.4.2 does have fields. https://github.com/leanprover/lean/blob/master/library/init/algebra/field.lean
They were removed from the core library in a more recent version.

view this post on Zulip Reid Barton (Jul 02 2020 at 14:51):

These definitions don't make ℕ × ℕ a field because, for one thing there is no instance of field given, and for another because they do not satisfy the field axioms.

view this post on Zulip Alexandre Rademaker (Jul 02 2020 at 14:51):

A more recent version of the Lean fork, right? The community version.

view this post on Zulip Reid Barton (Jul 02 2020 at 14:52):

If you want a field, the easiest way would be to install mathilb.

view this post on Zulip Reid Barton (Jul 02 2020 at 14:52):

Right.

view this post on Zulip Reid Barton (Jul 02 2020 at 14:52):

You can even use the lean-3.4.2 branch of mathlib if you really want to keep using Lean 3.4.2--it'll still be much better than not using mathlib at all.

view this post on Zulip Mario Carneiro (Jul 02 2020 at 14:54):

The given instances are only enough to be able to interpret m / n into the pair (m, n) (with which you can do what you like)

view this post on Zulip Alexandre Rademaker (Jul 02 2020 at 14:57):

Thank you all, now it is clear.


Last updated: May 06 2021 at 22:13 UTC