Is there a Float.pi

Stream: maths

[Colin Jones ⚛️]

Is there in Mathlib a Float.Pi like Real.Pi that is defined as a floating point number and is computable?

[Walter Moreira]

The file Init/Data/Float.lean in Lean's source code contains the basic definitions for Float. There doesn't seem to have constants for Pi or e.

You could potentially define your own with:

def fPi : Float := Float.atan2 0 (-1)
/--
info: 3.141593
-/
#guard_msgs in
#eval fPi

[Colin Jones ⚛️]

I'm looking at the documentation and Float.atan2 and other functions are defined as "opaque". What does opaque mean?

[Eric Wieser]

That you can't use its definition in a proof

[Colin Jones ⚛️]

Is it possible to do something like this:

def Pi {α : Type} :=
  if α = ℝ then
    π
  else
    Float.atan2 0 (-1)

[Aaron Liu]

Colin Jones ⚛️ said:

Is it possible to do something like this:

def Pi {α : Type} :=
  if α = ℝ then
    π
  else
    Float.atan2 0 (-1)

Yes, but it will have to be noncomputable

[Colin Jones ⚛️]

So pointless if I wanted to use it as a Float?

[Aaron Liu]

You can do something similar with typeclasses that does compute.

[Aaron Liu]

for example purposes

import Mathlib

class HasPi (α : Type*) where
  pi : α

notation "π" => HasPi.pi

noncomputable instance : HasPi ℝ where
  pi := Real.pi

instance : HasPi Float where
  pi := Float.atan2 0 (-1)

#eval (π : Float)

theorem Real.pi_eq_pi : π = Real.pi := rfl

[Colin Jones ⚛️]

Thank you!

[Jason Rute]

I was just thinking about this. Why isn’t there a Float.pi? If Float is 64 bit, we know the closest binary value to pi (https://stackoverflow.com/questions/72365104/the-most-accurate-approximation-of-pi-in-ieee-754-float64). If Lean just uses the current C version of floats, then can’t we just use that, or is this not part of the C standard?

[Jason Rute]

(Also, I see this isn’t the best stream for this discussion as this is the #maths stream.)

[Jason Rute]

Ok, it seems c doesn’t have a standard for pi (https://langdev.stackexchange.com/questions/2075/what-obstacles-prevented-c-and-c-from-standardizing-π), but still most languages support it, and I think there is an ieee standard for what it should be.

[Jason Rute]

I just checked and the atan2 0 (-1)and 0x1.921fb54442d18p1 definitions are the same (at least on https://live.lean-lang.org/ server).

-- trig def
def Float.pi0 : Float := Float.atan2 0 (-1)

-- 64-bit precision: 0x1.921fb54442d18p1 = 56593902016227520 x 2^(-54)
def Float.pi1 : Float:= Float.ofBinaryScientific 56593902016227520 (-54)

-- higher precision: 0x3.243f6a8885a308d313198a2e03707344ap0L = 68417829380157871863019543882359730131240 x 2^(-134)
def Float.pi2 : Float:= Float.ofBinaryScientific 68417829380157871863019543882359730131240 (-134)

#eval Float.pi0  -- 3.141593
#eval Float.pi1  -- 3.141593
#eval Float.pi2  -- 3.141593

-- check if bits are the same
#eval Float.pi0.toBits  -- 4614256656552045848
#eval Float.pi1.toBits  -- 4614256656552045848
#eval Float.pi2.toBits  -- 4614256656552045848

[Jason Rute]

Same with Float32.