Proving nan != nan

Stream: Is there code for X?

[Leni Aniva]

Is there a way to prove this?

def nan := 0.0 / 0.0
#eval nan != nan
example : nan != nan := by
  decide

Evaluating nan != nan directly gives a boolean answer

[Mario Carneiro]

no

[Mario Carneiro]

well, you can use native_decide

[Mario Carneiro]

but the float functions are otherwise opaque

[Leni Aniva]

Mario Carneiro said:

well, you can use native_decide

How does this thing work? When I use #print I only see an _auxLemma

[Mario Carneiro]

it runs eval and trusts the result

[Notification Bot]

Leni Aniva has marked this topic as resolved.

[Mario Carneiro]

the underlying mechanism is docs#Lean.reduceBool, which is an opaque function which, when reduced in the kernel, will run the interpreter on the argument, plus an axiom saying that it is the identity function (and hence the eval result is consistent with the actual definition of the function)

[Brando Miranda]

Apologies for unresolving the topic.

I'm trying to understand if it is ok to use == in my theorems. An example theorem:

example:2.0==2.0:=bysafe_tactic_please

But the description of native_decide sounds scary:

native_decide is a synonym for decide +native. It will attempt to prove a goal of type p by synthesizing an instance of Decidable p and then evaluating it to isTrue ... Unlike decide, this uses #eval to evaluate the decidability instance.

This should be used with care because it adds the entire lean compiler to the trusted part, and the axiom Lean.ofReduceBool will show up in #print axioms for theorems using this method or anything that transitively depends on them. Nevertheless, because it is compiled, this can be significantly more efficient than using decide, and for very large computations this is one way to run external programs and trust the result.

example : (List.range 1000).length = 1000 := by native_decide

is it really safe to use native_decide?

[Brando Miranda]

if I want to make a universal theorem about floats, is the approach to do:

For all floats except nan, some property f holds?

eg pseudo Lean4

theorem uni : \forall x : Float, f x == 0.0, f x <= 1.0, 0.0 <= f x := by
-- 1 native_decide
-- 2, 3 more tactics that work

PS: How do I say, except Nan? Or make theorems about floats?

[Kyle Miller]

Floats are tricky to prove anything about, since they're opaque and have no axioms. Using native_decide pulls in the runtime characteristics of Float to prove things.

Something you might consider instead is to work with some abstract type that has the axioms you need (maybe a docs#LinearOrderedRing ?), then you can pretend that Float satisfies these axioms at evaluation time. It's not 100% correct to do this though, since it's an approximation (for example, with floats a + b = a does not imply b = 0). I think @Tomas Skrivan has experience with this in SciLean.

[Brando Miranda]

Not ideal, but I think I'm ok for now to use runtime characteristics to do proofs (or at least theorems). What I'm confused is that I can't seem to identify the pattern of when to use = vs ==. Eg

#eval 2.0
example : 2.0 = 2.0 := by rfl
-- example : 2.0 = 2.0 := by native_decide -- FAILS

#eval 2.0
-- example : 2.0 == 2.0 := by rfl -- FAILS
example : 2.0 == 2.0 := by native_decide

[Brando Miranda]

Ok so from my above "experiment" I think == and by native_decide seems to always work while rfl does not always work.

[Brando Miranda]

Ok I think == with by naitve_decide seems to satisfy the English specs I said ("I'm ok with run time evals")

[Brando Miranda]

Since decidable equality with floats doesn't exist so I think = and rfl doesn't always work? (though idk of an example).

[Kyle Miller]

rfl can prove 2.0 = 2.0 since the LHS and RHS are identical, so Eq.refl can apply.

You're correct that there's no DecidableEq instance for Float, so it's not possible to synthesize an algorithm to calculate whether or not 2.0 = 2.0.

The reason 2.0 == 2.0 can be evaluated is that == is Bool-valued, so there's no need to synthesize an algorithm (== is already an algorithm, and it uses the runtime == for Float)

[Brando Miranda]

Ignoring the nan issue (ie nan != nan), which is a big issue I think for my goals (doing universal theorems about floats). Can universal theorems about floats be made with ==?

E.g.

def truncateNumber (x : Float) : Float :=
  x - Float.floor x

theorem truncateNumber_correct (x : Float) :
  truncateNumber x = x - Float.floor x ∧ 0 ≤ truncateNumber x ∧ truncateNumber x < 1 := sorry

Is = or == the right thing to do?

PS: I know it's a little silly, but I'm just trying to figure out how to make universal theorems about floats that are sensible (even if not perfect). If possible.

[Kyle Miller]

I'd think this isn't possible

[Brando Miranda]

Kyle Miller said:

I'd think this isn't possible

what about this hack?

def nan := 0.0 / 0.0

theorem truncateNumber_correct (x : Float) :
  x ≠ nan → truncateNumber x = x - Float.floor x ∧ 0 ≤ truncateNumber x ∧ truncateNumber x < 1 := sorry

since rfl works on floats per your comment, it seems the above is an ok candidate?

[Kyle Miller]

(Potentially one could admit a decision procedure as an extra axiom that checks your theorem for all possible x; there are at most 2^64 values, which is theoretically possible to exhaust, but practically you might not want to wait that long.)

[Brando Miranda]

ah I see, so the issue is that evaluate needs an actual float to work.

[Kyle Miller]

In truncateNumber_correct, you can prove truncateNumber x = x - Float.floor x using rfl (that's true by definition of truncateNumber), but you can't get the inequalities without additional Float axioms.

[Kyle Miller]

You could add Float axioms yourself though. Maybe it's worth doing? You'll have to be very careful since these won't be machine-verified; though with some effort you could do some testing to see they aren't immediately refuted.

[Brando Miranda]

I don't know if I have time to do that (or if I'm the right person). Let me think about it. I think I'm ok at least with a sorry proof that uses the correct version of = or == for now.

[Brando Miranda]

as a ugly hack I could do an existential quantifier and use == for the first one, but it wouldn't fix the inequalities issues (since the rest of the infrastructure for floats doesn't exist)

[Brando Miranda]

actually even an existential might work for inequalities:

-- 1) Basic test case: 3.5 → 0.5
#eval truncateNumber 3.5
example : truncateNumber 3.5 == 0.5 := by native_decide

-- 2) Small decimal part: 1.33 → 0.33
#eval truncateNumber 1.33
example : Float.abs (truncateNumber 1.33 - 0.33) < 1e-6 := by native_decide

but it's very hacky

[Brando Miranda]

I think

theorem truncateNumber_correct (x : Float) :
  ¬ Float.isNaN x ∧ ¬ Float.isInf x →
  truncateNumber x = x - Float.floor x ∧ 0 ≤ truncateNumber x ∧ truncateNumber x < 1 := sorry

is ok? (after I hypothetically make the Floats library properly some day)

[Brando Miranda]

does floats exist in Isabelle or Coq perhaps to help me?

[Brando Miranda]

or a close language to Lean 4

[Mario Carneiro]

coq has a nice float library called flocq

[Aaron Liu]

Just curious, why do you need theorems about Floats?

[Brando Miranda]

as far as I know, Real numbers don't exist in real programs used in practice and I wanted to formalize programs more similar to real programs used in practice in Lean 4 (I admit I'd likely start with very toy examples)

[Brando Miranda]

Mario Carneiro said:

coq has a nice float library called flocq

amazing! thank you Mario!

[Chris Wong]

Skimming the flocq docs, it looks like it builds a model of floating point from scratch, without referencing the native type.

[Yury G. Kudryashov]

You can try to write axioms about Float that implement some official specifications.

[Yury G. Kudryashov]

Or you can write a type class LawfulFloat and assume it whenever you prove something about floats.

[Yury G. Kudryashov]

Then one can verify your axioms for a specific system (hardware, OS, compiler) by checking all possible values (probably, takes a lot of time).

[Jz Pan]

What about writing an IEEE754 float implementation in Lean? Just like software float library in C/C++ which uses int64 to simulate double.

[Yury G. Kudryashov]

AFAIU, you can do it but it won't use the hardware/OS/compiler-provided float, so it will be slower.

[Yury G. Kudryashov]

Possibly, you can have both, but I don't know how to do it.

[Edward van de Meent]

I seem to recall someone actually working on a verified implementation of float?

[Edward van de Meent]

Right, discord user rob_23oba mentioned working on IEEE-754 compliant floats

[Markus Himmel]

If at some point there is a successful community library that exposes a typeclass like IsIEEECompliantFloat, provides an instance of this class using a pure Lean implementation of IEEE-754 floats (docs#FP.Float ?) and proves useful theorems about floats, then the FRO will be very interested in exploring ways of modifying Lean's native Float type so that it is possible to instantiate IsIEEECompliantFloat Float.

[Jz Pan]

Markus Himmel said:

IsIEEECompliantFloat Float

I don't think this makes sense, as it's not the type Float being IEEE-754 compliant, but the functions on Float are IEEE-754 compliant: add, subtract, etc., and sin, cos, ...

[Jz Pan]

Is this declaration ABI correct?

@[unbox]
structure MyFloat : Type where
  ofRaw :: toRaw : UInt64

[Mario Carneiro]

no, it would need to be wrapping a Float

[Mario Carneiro]

float and double are different from uintN_t in the C ABI

[Mario Carneiro]

e.g on intel floats are passed in the float registers in the calling convention

[Joseph Myers]

If your structure wraps an integer, that would also imply that you're formalizing at IEEE specification level 4, where the choices of NaN payloads are significant (and those often differ between implementations - and even between different instructions on the same architecture, e.g. x87 and SSE floating point have different rules for choosing the payload resulting from an operation between two NaNs). IEEE specification level 3, where most (not all) things are fully specified in IEEE 754, is probably a better option for formalization for most purposes.

[Robin Arnez]

Jz Pan schrieb:

Markus Himmel said:

IsIEEECompliantFloat Float

I don't think this makes sense, as it's not the type Float being IEEE-754 compliant, but the functions on Float are IEEE-754 compliant: add, subtract, etc., and sin, cos, ...

I'd think that IsIEEECompliantFloat α would be a type class like this:

class IsIEEECompliantFloat (α : Type u) (fmt : BinaryFloatFormat) extends Add α, Sub α, Neg α, Mul α, Div α, LE α, LT α, BEq α, α ≃ BinaryFloat fmt where
  sqrt (x : α) : α
  apply_add (x y : α) : toFun (x + y) = toFun x + toFun y
  apply_sub (x y : α) : toFun (x - y) = toFun x - toFun y
  -- ...
  apply_sqrt (x : α) : toFun (sqrt x) = (toFun x).sqrt

And then you could make an instance of it with all of Floats normal functions/instances and there you have your assertion that the Float functions work.
(note that sin, cos, pow, etc. are weird cases because the standard doesn't define them and they are usually defined from the other existing functions, so we don't put those here)

[Robin Arnez]

Jz Pan schrieb:

Is this declaration ABI correct?

@[unbox]
structure MyFloat : Type where
  ofRaw :: toRaw : UInt64

Lean already makes a special case for Floats, UInts, etc. so while this is not correct as an ABI, the compiler will take care of that (if your type would be called Float, that is). Like Joseph said, this would imply multiple NaNs which can get in the way of proofs (e.g. proving x + nan = nan would be impossible because it actually isn't true on some platforms where the left hand side would turn out to be a different NaN than the right hand side). I thought of an approach that might solve this though: separate Float into a NativeFloat with multiple NaNs which has a similar definition as yours and then the normal Float which is merely a quotient on NativeFloat that makes all NaNs equal. The advantage of this approach is that we can treat Float and NativeFloat as normal types and use match and everything like usual, similar to how Array works. A definition as an inductive would make this more difficult because then you'd need to emit code that checks isNaN, isInf, etc. and decode everything.

[Mario Carneiro]

Lean's functions on Float already check for nans and ensure that you can't get at payload bits using e.g. toBits, which would otherwise result in nondeterminism in opaque functions and hence UB (because lean logical functions must be deterministic)

[Mario Carneiro]

The inductive type which is isomorphic to Float is the one where there is exactly one nan value

[Mario Carneiro]

I would encourage anyone wanting to improve the state of lean floats to PR something to Batteries

[Joseph Myers]

Robin Arnez said:

(note that sin, cos, pow, etc. are weird cases because the standard doesn't define them and they are usually defined from the other existing functions, so we don't put those here)

The standard does define them, as recommended operations (see subclause 9.2). I don't think the difference between recommended and required operations is very important for formalization, except that IEEE 754 is a complicated enough standard that there are many more important operations that would be higher priority. (And if you wanted computable definitions rather than just relying on tactics for computation, computable versions of those functions would be a lot more complicated to write than either noncomputable versions or computable versions of the required operations.)

[Jz Pan]

I think the IEEE754 standard permits different NaNs, at least there are sNaN and qNaN, both of them can have payloads, see https://en.wikipedia.org/wiki/Double-precision_floating-point_format and https://en.wikipedia.org/wiki/NaN

[Robin Arnez]

Joseph Myers schrieb:

The standard does define them, as recommended operations

Yes but pretty much no implementation of floating point will actually give you the exact result, they will all be incorrect by 1 ulp in a few places. So writing a definition of sin that e.g. works as rounding Real.sin would be probably correct per specification but will still differ from the implementations that are provided by math libraries. This makes it pretty difficult to formalize, since you'd somehow have to write a definition that allows for rounding errors in the actual implementation. Besides, Real.sin is not in core lean, so you'd have to still write some of it yourself.

[Robin Arnez]

Jz Pan schrieb:

I think the IEEE754 standard permits different NaNs, at least there are sNaN and qNaN, both of them can have payloads, see https://en.wikipedia.org/wiki/Double-precision_floating-point_format and https://en.wikipedia.org/wiki/NaN

Yes, but multiple NaNs get in the way of proofs because different implementations handle them differently, so nan:0x403124 + nan:0x341003 might be nan:0x403124 or nan:0x741003 or -nan:0x400000 or whatever. You can't really prove useful things about NaN with such a definition.

[Jz Pan]

Robin Arnez said:

Jz Pan schrieb:

I think the IEEE754 standard permits different NaNs, at least there are sNaN and qNaN, both of them can have payloads, see https://en.wikipedia.org/wiki/Double-precision_floating-point_format and https://en.wikipedia.org/wiki/NaN

Yes, but multiple NaNs get in the way of proofs because different implementations handle them differently, so nan:0x403124 + nan:0x341003 might be nan:0x403124 or nan:0x741003 or -nan:0x400000 or whatever. You can't really prove useful things about NaN with such a definition.

You can only prove things for a specific software IEEE-754 float implementation. But not the hardware Float.

[Jz Pan]

Optionally, native_decide can add axiom that software float is coincide with hardware float when there are no NaNs.

[Jz Pan]

... and that could probably prove False easily.

[Notification Bot]

Yury G. Kudryashov has marked this topic as unresolved.

[Yury G. Kudryashov]

Instead of adding an axiom, you can add a typeclass [LawfulFloat Float] as outlined above. Then your theorems will be conditional to Float being lawful.

[Mario Carneiro]

Robin Arnez said:

Yes but pretty much no implementation of floating point will actually give you the exact result, they will all be incorrect by 1 ulp in a few places.

IIRC Float.sin is off by much more than 1 ulp on intel because they got pi wrong in the argument reduction step. I think this is in the spec now(!)

[Ruben Van de Velde]

Is that like the Indiana pi bill?

[Robin Arnez]

Mario Carneiro schrieb:

I would encourage anyone wanting to improve the state of lean floats to PR something to Batteries

I'd be happy to PR something to Batteries! However, I tried defining a type similar to flocq and ran into issues writing the proof required for the finite constructor (I ended up using Mathlib.Algebra.Order.Ring.Rat and such). The scope for something in batteries would probably rather be an axiomatic definition of the common operations with some lemmas about 0, inf and nan and perhaps some simprocs for reducing the float operations. This would probably mean that there'd be some code duplication for Float vs Float32 though...
For the implementation I'm thinking:

/-- Returns whether `x` is a NaN bit pattern, that is `Float.ofBits x = Float.nan` -/
def Float.isNaNBits (x : UInt64) : Bool := (x >>> 52) &&& 0x7FF = 0x7FF ∧ x &&& 0x000F_FFFF_FFFF_FFFF ≠ 0

axiom Float.ofBits_toBits (x : Float) : ofBits x.toBits = x
axiom Float.toBits_ofBits_of_not_isNaNBits (x : UInt64) (h : isNaNBits x = false) : (ofBits x).toBits = x
axiom Float.toBits_ofBits_of_isNaNBits (x : UInt64) (h : isNaNBits x) : (ofBits x).toBits = 0x7FF8_0000_0000_0000

This would still leave it open how we actually define Float (as an inductive, a wrapper around Quot (fun x y => Float.isNaNBits x ∧ Float.isNaNBits y) or as quotient around a float with multiple NaNs or whatever).
Then everything else can be defined using toBits and ofBits.

[Robin Arnez]

I've now put my first wip draft with the simplest definitions (ofBits, toBits, isNaN, isFinite, isInf and neg) as batteries#1141 and will probably continue adding definitions and theorems. @Mario Carneiro, if you're interested, I encourage you to take a look.

[Robin Arnez]

I've now proven nan != nan within my PR lol

[Mario Carneiro]

You should probably merge what you have with FP.Basic in mathlib first

[Mario Carneiro]

because that's basically a port of the first few definitions in flocq

[Robin Arnez]

I rewrote FP.Basic but I needed Mathlib.Algebra.Order.Ring.Rat. You can probably do it without but it felt too complicated otherwise.

[Robin Arnez]

You know, the current definition is full of unsafes

[Mario Carneiro]

the unsafes are just because someone was lazy and didn't want to prove some proof obligations

[Mario Carneiro]

it's a sorry that gets past the mathlib linter

[Robin Arnez]

Basic.lean
if you're interested, the proofs aren't particularly nice though

[Robin Arnez]

Maybe you have some ideas how this could be ported to batteries / have a nicer proof.

[Mario Carneiro]

hm, it might be better to PR to mathlib first then, if the maintainers are alright with it. I would like to separate out the part about upstreaming bits of rat ring theorems

[Mario Carneiro]

it might also be that this is just too annoying without an algebraic hierarchy, in which case it will have to stay in mathlib for the time being

[Robin Arnez]

I feel like the most important things for Float are its relationships with Rat or Real and Rat doesn't have a proof framework on batteries, only on mathlib.

[Mario Carneiro]

The basic theorems about rat should be upstreamed

[Mario Carneiro]

that won't be enough if you need to use ring and linarith, but you can at least do manual proofs using the ring axioms that way

[Robin Arnez]

Yeah that would probably be enough for most of what I was doing here (I mean it was mostly a manual proof)

[Robin Arnez]

What do you think should happen with the batteries draft PR then? Should I rather put this into a PR to mathlib?

[Mario Carneiro]

I think so

[Robin Arnez]

Oh, there is also one more thing: I used Nat.divFloat in my definition (for convenience) but not your definition (which was wrong for subnormals and used e.g. scaleB and div through inf and nan which are things we wanted to define). Should I then just make a duplicate Nat.divFloat' in the mathlib pr?

[Mario Carneiro]

I'm not sure I follow

[Robin Arnez]

Well, you know Nat.divFloat from Batteries.Lean.Float (this one). I defined my own version of it that is (hopefully) correct and works with toBits and ofBits only. However, these two definitions would conflict.

[Mario Carneiro]

I don't think the definition should use Float at all

[Mario Carneiro]

everything should be about the ordinary non-opaque type FP.Float

[Robin Arnez]

I mean the axiomatic redefinition.

[Robin Arnez]

Or should I just not care about that right now?

[Mario Carneiro]

the first task is to have a good theory of floats completely independent of lean's Float type

[Mario Carneiro]

once we have that we can look into what we would need to do to retrofit the theory onto Float via some refactoring and shuffling of theorems between repos

[Robin Arnez]

oh, okay, yeah we can do that

[Mario Carneiro]

so basically we just want a definition with the right mathematical properties to be a putative alternative definition of Float

[Mario Carneiro]

ignoring issues about data representation of inductive types in the compiler

[Robin Arnez]

Also, there was an idea I had, which is, instead of defining float (FP.Float) operations through natural number division, define them through an auxiliary PositiveBinaryRealApprox (I have not come up with a better name lol) which is

structure PositiveBinaryRealApprox where
  log2 : Int
  approx (x : Int) : Nat × Bool
  approx_correct (x : Int) : (approx (x - 1)).1 = (approx x).1 / 2
  approx_exact_iff (x : Int) :
    (approx x).2 ↔ ∀ y > x, (approx y).1 = (approx x).1 <<< (y - x).toNat
  log2_correct (x : Int) : (approx x).1 = 0 ↔ x + log2 < 0

The reason for it being computability and having a simple connection to Real and making it easier to have one rounding function def FP.Float.round (x : PositiveBinaryRealApprox) (rm : RoundingMode) : FP.Float. Do you think this is a good idea?

[Mario Carneiro]

couldn't you use Rat in place of PositiveBinaryRealApprox for a much simpler spec?

[Mario Carneiro]

it also sounds kind of like you are reinventing computable reals

[Robin Arnez]

There's sqrt though

[Robin Arnez]

And yes, the intention is basically computable reals but this particular version makes rounding simplest I think:

def FP.Float.round (sign : Bool) (x : PositiveBinaryRealApprox) (rm : RoundingMode) : FP.Float fmt :=
  if hinf : fmt.maxExp ≤ x.log2 then .inf sign else

  let exp := max (x.log2 + 1 - fmt.precision) fmt.minExp
  let rounded :=
    match rm with
    | .zero => (x.approx exp).1
    | .ceil => (x.approx exp).1 + (!sign && (x.approx exp).2).toNat
    | .floor => (x.approx exp).1 + (sign && (x.approx exp).2).toNat
    | .nearest_inf => ((x.approx (exp + 1)).1 + 1) / 2
    | .nearest_even =>
      let (val, exact) := x.approx (exp + 1)
      if val % 4 = 1 ∧ exact then val / 2 else (val + 1) / 2
  if h2 : rounded ≥ 2 ^ fmt.precision then -- overflow
    sorry
  else
    .finite sign exp rounded sorry

[Robin Arnez]

The intention is obviously that we treat PositiveBinaryRealApprox like { x : Real // 0 < x } in proofs while having a computable definition.

[Robin Arnez]

Robin Arnez schrieb:

There's sqrt though

While sin, cos probably won't be supported through a computable definition, sqrt is still one of the operations that is supported exactly on pretty much all platforms (iirc) and we should have a definition for it.

[Robin Arnez]

Also rounding reals in general would also be nice

[Mario Carneiro]

so round reals then

[Mario Carneiro]

no need to use computable reals here

[Robin Arnez]

I guess you're right, we don't have any obligations to make this computable, this just needs to exist for specification and proof purposes. I just feel like it is weird to have everything marked noncomputable when you can compute it in theory. But you're probably right that the spec should probably be just a noncomputable definition and then you can do @[csimp] and whatever for computable definitions later.