decimals in Lean

Stream: maths

[Kevin Buzzard]

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]

Somehow the definition of < on reals is leaking through.

[Kevin Buzzard]

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]

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

[Rob Lewis]

real.has_lt should probably be irreducible, no?

[Kevin Buzzard]

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]

[written before Rob's post]

[Kevin Buzzard]

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]

attribute [irreducible] real.has_lt

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

[Andrew Ashworth]

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

[Kevin Buzzard]

She said "in a few weeks"