Zulip Chat Archive

Stream: maths

Topic: decimals in Lean


view this post on Zulip 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?

view this post on Zulip Chris Hughes (Nov 23 2019 at 14:50):

Somehow the definition of < on reals is leaking through.

view this post on Zulip 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.

view this post on Zulip 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
}

view this post on Zulip Rob Lewis (Nov 23 2019 at 14:57):

real.has_lt should probably be irreducible, no?

view this post on Zulip 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 :-)

view this post on Zulip Kevin Buzzard (Nov 23 2019 at 14:58):

[written before Rob's post]

view this post on Zulip 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

view this post on Zulip 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
}

view this post on Zulip Andrew Ashworth (Nov 23 2019 at 16:29):

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

view this post on Zulip Kevin Buzzard (Nov 23 2019 at 16:59):

She said "in a few weeks"


Last updated: May 18 2021 at 07:19 UTC