Zulip Chat Archive
Stream: new members
Topic: reals
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.
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.
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
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.
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.
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.
Reid Barton (Jul 02 2020 at 14:14):
oh, I have no idea
Reid Barton (Jul 02 2020 at 14:14):
Reid Barton (Jul 02 2020 at 14:14):
I guess you're right.
Mario Carneiro (Jul 02 2020 at 14:17):
You can do it over an arbitrary field if you don't want to use mathlib
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
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)
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?
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.
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.
Alexandre Rademaker (Jul 02 2020 at 14:51):
A more recent version of the Lean fork, right? The community version.
Reid Barton (Jul 02 2020 at 14:52):
If you want a field, the easiest way would be to install mathilb.
Reid Barton (Jul 02 2020 at 14:52):
Right.
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.
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)
Alexandre Rademaker (Jul 02 2020 at 14:57):
Thank you all, now it is clear.
Last updated: Dec 20 2023 at 11:08 UTC