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!