Polymorphic Round Function

Stream: new members

[Colin Jones ⚛️]

I understand the round function in mathlib requires a LinearOrderedField to work, but is there a way to make it polymorphic.

def rp (x : α) [HSub α α α] := x - round x

Specifically, is there a way to make this evaluate using Float.round when alpha is a Float, but still keep the flexibility of polymorphism?

[Derek Rhodes]

Hi, I not an expert in this, but, I wanted to see where things start breaking down.

import Mathlib

variable (α : Type) [LinearOrderedRing α] [FloorRing α]

def rp (x : α) := x - round x

instance : AddMonoid Float where
  add := (· + ·)
  add_assoc a b c := by
    -- IEEE 754 floats are not associative
    sorry

-- the CS stack exchange has a workable example of non-associativity
-- https://cs.stackexchange.com/a/169153

def x : Float := -1e9
def y : Float := 1e9
def z : Float := 1e-9

#eval (x + y) + z  -- result: 1e-09, Lean doesn't show enough precision to see
#eval x + (y + z)  -- result: 0.0

#eval (x + y) + z == x + (y + z)  -- false
#eval (x + y) + z = x + (y + z)   -- failed to synthesize Decidable

Here's a nice paragraph from the Lean language reference

Lean exposes the underlying platform's floating-point values for use in
programming, but they are not encoded in Lean's logic. They are represented
by an opaque type. This means that the kernel is not capable of computing
with or reasoning about floating-point values without additional axioms. A
consequence of this is that equality of floating-point numbers is not
decidable...

I've seen other discussion here on zulip regarding algebra and proofs on IEEE Floats, and they were not heartening.

However, I think it would be really cool to see what people could prove about them. For instance: bounds on error accumulation with sequences of machine instructions. I would imagine that capability would be appreciated in robotics, aerospace, missile defense, machine learning, etc. So, maybe there's already work done? As I said, I'm not an expert but am also interested in the answer to your question.

[Eric Wieser]

Regarding docs#Int.floor` etc, I think it would be reasonable to split the data-only parts of docs#FloorRing into a new base typeclass

[Colin Jones ⚛️]

Figured it out:

class HasRound (α : Type) where
  pround : α → α

instance : HasRound Float where
  pround := Float.round

instance [LinearOrderedField α] [FloorRing α] : HasRound α where
  pround := (fun (x : α) => round x)

I didn't want to prove anything on floats; I know they are wacky. I just wanted a function that could do both round functions