## Stream: maths

### Topic: decimals in Lean

#### Kevin Buzzard (Nov 23 2019 at 14:43):

I've never used these before. I was just playing around with them and ran into this (Lean knows 0.5=1/2 by the way :D ) :

import data.real.basic

noncomputable def x : ℝ := 0.5

#print x -- 1 / 2
set_option pp.numerals false
#print x -- has_one.one ℝ / bit0 (has_one.one ℝ)
set_option pp.numerals true

example : ∃ x : ℝ, x < 1 := ⟨0.5, by norm_num⟩

class less_than_one :=
(x : ℝ)
(thm : x < 1)

-- Lean assures me it's computable
instance foo : less_than_one :=
{ x := 0,
thm := by norm_num -- works fine
}

noncomputable instance bar : less_than_one :=
{ x := 0.5,
thm := by norm_num -- fails
}

/-
norm_num failed to simplify
state:
⊢ quotient.lift_on₂ (algebra.div 1 2) 1 has_lt.lt real.has_lt._proof_1
-/


Where did quotient.lift_on₂ come from?

#### Chris Hughes (Nov 23 2019 at 14:50):

Somehow the definition of < on reals is leaking through.

#### Kevin Buzzard (Nov 23 2019 at 14:54):

Oh! I was thinking it was some crazy internal construction of the class! I'm such a fool :D

def XXX : has_lt ℝ := by apply_instance
#print XXX -- real.has_lt (duh)
#print real.has_lt
/-
@[instance]
protected def real.has_lt : has_lt ℝ :=
{lt := λ (x y : ℝ), quotient.lift_on₂ x y has_lt.lt real.has_lt._proof_1}
-/


And there it is.

#### Kevin Buzzard (Nov 23 2019 at 14:55):

noncomputable instance bar : less_than_one :=
{ x := 0.5,
thm := show (0.5 : ℝ) < 1, by norm_num -- works
}


#### Rob Lewis (Nov 23 2019 at 14:57):

real.has_lt should probably be irreducible, no?

#### Kevin Buzzard (Nov 23 2019 at 14:57):

attribute [irreducible] real.has_lt

noncomputable instance bar : less_than_one :=
{ x := 0.5,
thm := by norm_num -- still fails
}

/-
norm_num failed to simplify
state:
⊢ algebra.div 1 2 < 1
-/


Oh I thought I was such a pro :-)

#### Kevin Buzzard (Nov 23 2019 at 14:58):

[written before Rob's post]

#### Kevin Buzzard (Nov 23 2019 at 15:01):

So of course this all comes from trying to do, shock horror, an example of something. I was talking with @Athina about her forthcoming paper about using Lean with 1st years and she said that one thing she had noticed was that Lean users tended to try examples less and just get on with the proofs. I can see why :D

#### Kevin Buzzard (Nov 23 2019 at 15:03):

attribute [irreducible] real.has_lt

noncomputable instance bar : less_than_one :=
{ x := 0.5,
thm := by unfold algebra.div; norm_num
}


#### Andrew Ashworth (Nov 23 2019 at 16:29):

Will the paper be out soon? Seems interesting and worth a read.

#### Kevin Buzzard (Nov 23 2019 at 16:59):

She said "in a few weeks"

Last updated: May 18 2021 at 07:19 UTC