closing Float `-0 = 0`

Stream: lean4

[Arien Malec]

In my Complex Number Game in Lean 4, for a proof I'm down to

r: Float
⊢ -0 = 0

which seems like it should close trivally via rfl or simp but doesn't -- I've looked through the builtin Lean 4 definitions and Std4/Mathlib4 stuff but probably I'm missing something obvious. (I'm aware of floating point representation issues but that shouldn't be an issue here...).

[Arien Malec]

example: -(0: Float) = 0 := sorry is the #mwe I'd guess

[Kevin Buzzard]

He who lives by the float, dies by the float. Is there a reason you're not using some axiomatised real?

[Arien Malec]

#lean4
Kevin Buzzard said:

Is there a reason you're not using some axiomatised real?

#lean4

Is there a reason I'm using Lean 4 rather than Lean 3? Seemed like fun at the time....

[Alex J. Best]

You can make axioms for the real numbers in Lean 4, even without actually setting up a type that fulfils them though. Its "just" the 20 or so axioms of docs#conditionally_complete_linear_ordered_field. Probably its best to define field and ordered field etc along the way.

[Arien Malec]

Perhaps for a followup. In the interim I closed with an IEEE 744 numerically valid but ontologically dubious axiom.

[Alex J. Best]

native_decide?

[Arien Malec]

not Decidable

[Alex J. Best]

I'm confused sorry, are you using the native_decide tactic / axiom (which just checks your equality in the VM basically) or adding an axiom positing your equality?

[Alex J. Best]

Hmm I'm now confused, native decide shows that -0 \le 0 and 0 \le -0 but not equality indeed

[Henrik Böving]

That is because we only have decidable equality over floats implemented with BEq and not an actual DecidableEq instance...and now we are back at BEq vs Eq again

[Arien Malec]

For clarity, I solved this brute force by
@[simp] axiom Float.neg_zero: -(0: Float) = 0

the IEEE754 language here is "Comparisons shall ignore the sign of zero (so +0 = −0)" but they behave differently WRT to producing +/-NaN and +/-∞

Floating point oddities will plague humanity until the heat death of the universe.

[Mario Carneiro]

FYI, -0 ≠ 0 is provable using native_decide

[Mario Carneiro]

so that "ontologically dubious" axiom is in fact false

[Mario Carneiro]

example : (-0 : Float) ≠ 0 := by
  apply mt (congrArg (fun x => (1 / x > 0 : Bool)))
  native_decide

[Mario Carneiro]

It is very deliberate that the float BEq is not a DecidableEq instance

[Mario Carneiro]

the only reasonable DecidableEq instance on float is bit-equality, and this makes -0 and 0 not equal

[Mario Carneiro]

@Arien Malec

[Arien Malec]

Again, IEEE754 says that comparisons ignore the sign of zero, so if we are using IEEE754 comparisons, the axiom is correct; it's ontologically dubious because they don't behave the same in corner cases and bit differ in the sign bit.

[Mario Carneiro]

One property of equality is that x = y -> f x = f y, for all f. That is, if any operation in the language distinguishes x and y then they are not equal. This is a really strong claim, and it is falsified by -0 vs 0 because if you apply the 1/x function you get distinct values (namely $-\infty$ and $+\infty$ respectively).

[Mario Carneiro]

it's not sufficient for some comparison function to say they are equal. We already have that, this is -0 == 0 and that is true

[Mario Carneiro]

but == does not imply = in this case

[Arien Malec]

In any case, the solution to my particular problem is to have Reals

[Mario Carneiro]

yes, the answer to "how do I reason about Floats" is usually "don't"

[Kevin Buzzard]

For clarity, I solved this brute force by (adding an axiom)

Which is why I'm suggesting you use axiomatic reals, because adding axioms to existing types involvea a risk that Mario will come along and break your game with a proof of false. On the other hand using axiomatic reals will be fine because you know you could build them if you had to, and the ring tactic will work (which it provably won't do for floats). In Patrick's natural number game he uses axiomatic naturals not Nat.

[Arien Malec]

hmm. For my self-teaching purposes would this be something like

inductive MyReal (f: Float) where
| zero
| one
| number : (a: Float) → MyReal f

?

[Arien Malec]

I mean I'm obviously not deriving the reals from cauchy sequences...

inductive MyReal where
| zero
| one
| number

is also a trivial possibility, yeah?

[Johan Commelin]

No, it would be more like

variables (R : Type) [ConditionallyCompleteLinearOrderedField R]

[Johan Commelin]

But you would still have to define CondCompLinOrdFld, because it hasn't yet been ported from mathlib3 to mathlib4.

[Kevin Buzzard]

You can just #print it or even look at the lean 3 docs to see the fields of the structure you want. Why do you want a map from float? If you want to prove theorems you shouldn't be going near float. You've already been bitten once.

[Arien Malec]

the, uh, programmer in me wants complex numbers to have numbers in 'em.

[Kevin Buzzard]

The real numbers are numbers.

[Kevin Buzzard]

Every number you can write down and which in your mental model is a float, in my mental model is a real.

[Kevin Buzzard]

And Gauss and Euler agree with me, they've never heard of floats but they've certainly heard of real numbers.

[Kevin Buzzard]

docs#conditionally_complete_linear_ordered_field

[Kevin Buzzard]

There's your axioms, although a bunch of them are junk and can be removed as far as you're concerned. you can remove: nsmul, nsmul_zero', nsmul_succ', sub, sub_eq_add_neg, zsmul, zsmul_zero', zsmul_succ', zsmul_neg', int_cast, nat_cast, nat_cast_zero, nat_cast_succ, int_cast_of_nat, int_cast_neg_succ_of_nat, npow, npow_zero', npow_succ', decidable_le, decidable_eq, decidable_lt, max_def, min_def, div, div_eq_mul_inv, zpow, zpow_zero', zpow_succ', zpow_neg', rat_cast, rat_cast_mk, qsmul, and qsmul_eq_mul'. Those are just implementation details. Then make the field instance and you can prove -0=0 with ring.

[Kevin Buzzard]

In fact I wonder if you can just get away with assuming it's a totally ordered field. Will you ever assume completeness?

[Arien Malec]

For a programmer, numbers are for computing stuff, not proving stuff, which is the mental barrier I keep tripping over. Yeah, was looking at the surface area there, and concluding that I can do away with most of that.

[Kevin Buzzard]

So let me just check: the goal of the exercise here _is_ to prove things, right?

[Kevin Buzzard]

The problem with float is that almost none of the remaining axioms are actually true for floats. For example a+(b+c)=(a+b)+c is not always true, because of rounding issues. This result is true for reals. On the other hand reals are not computable at all -- if you want to do any computations then this is when floats start to shine.

[Kevin Buzzard]

In the Lean 3 complex number game I just prove theorems and don't do any calculations at all.

[Arien Malec]

Something I understand intellectually then the programmer brain keeps piping up.

[Arien Malec]

I think WRT your complex number game, all I need are the basic field axioms.

[Kevin Buzzard]

For the complex number game I'm pretty sure I could have got away with just assuming that the reals were a field! I'm not even sure I needed that 1+1+1+1+... was never zero :-)

[Kevin Buzzard]

I might have divded by 2 occasionally but I'm not sure I ever divided by anything else, so indeed you might just be able to get away with assuming the axioms of a field. I don't even know if I used < on the reals, because < doesn't extend to the complexes in any mathematically satisfying way.

[Arien Malec]

I might ignore trying to prove the complex numbers are an algebraically closed field, because I don't think the machinery is there.

[Kevin Buzzard]

yeah that's just a joke level. An undergraduate at Imperial had just formalised the proof he'd been taught in class, so I mentioned it.

[Kevin Buzzard]

The proof is complicated (and here you would certainly need all those extra axioms).

[Arien Malec]

Need exponentiation to do the norm -- that's it, really.

[James Gallicchio]

Could the rationals be an option? Computable and proof friendly!

[Kevin Buzzard]

You only need squaring and that's just an abbreviation for multiplication x*x so that works in any field

[Anne Baanen]

Kevin Buzzard said:

On the other hand reals are not computable at all -- if you want to do any computations then this is when floats start to shine.

Nitpick: addition, subtraction, multiplication, exp, sqrt, etc are all perfectly computable on (every decent model of) the reals. You only get into trouble when the function is discontinuous.

[Anne Baanen]

On the other hand, division (at least the way mathlib implements it) and boolean equality are discontinuous. On the gripping hand, equality of floats is also rather problematic.

[Damiano Testa]

To highlight Anne's point about division, this recent question was exactly about noncomputability of division for the (mathlib) reals.

[Gabriel Ebner]

One notable example of such a discontinuous function on the reals is toString. Which sounds a bit like a popular science philosophical question: if I can't see the output of a function, is it still computable?

[Mario Carneiro]

Which reminds me of some of the curious properties of mathlib's "computable" definition of the reals as quotients of cauchy sequences. Since those sequences are essentially Nat -> Rat functions they are in principle computable, but you can't actually observe any of the values since there isn't anything you can do which is both observable in some nice discrete type like Bool and also respects the quotient.

[Mario Carneiro]

So preserving computability of operations on the reals like max or sqrt really does have no advantage other than giving you a warm fuzzy feeling

[Arien Malec]

The underlying philosophical issue is the issue of things that are "in principle" computable but only by assuming infinite time and space with no physical limitations. Given the constraints of finite space and time, you get really terrible things like Float.

[Mario Carneiro]

That's not true, Rat is also usable in finite space and time and has much better theoretical properties

[Mario Carneiro]

There are also other ways to do computable reals which you can actually observe the properties of, by having a modulus of convergence

[Mario Carneiro]

If you care about approximating numbers to finite precision, interval arithmetic is another approach which is theoretically sensible and computable in finite space and time. Float is just... not that

[Mario Carneiro]

Float is a way to do operations that do something with some bits that vaguely hint at having something to do with real numbers while providing almost no guarantees, or rather providing lots of almost-guarantees that can be stressed to the breaking point without trying too hard

[Arien Malec]

One could certainly imagine basing computation on Rat but there are still issues of finite representation over infinite sequences, and it's still useful to represent numbers via ToStringor equivalent where some of the same issues arise. What I'm saying (and then I'll drop it), is that fp numbers might be a particularly problematic solution but issues of finite representation are always going to arise. But this is all now far from my little project of a toy representation of Real so I can get on with toy proofs of Complex.

[Mario Carneiro]

if you actually want "calculator numbers" then Rat is fine. Any number you can type is rational

[Mario Carneiro]

As far as I can tell you don't really even need infinite sequences. There are a few tasks that require properly irrational numbers but they are pretty rare IME - normally you can get by by fixing approximations to numbers like pi if you need them. (Note that this is entirely about doing actual calculations on reals; for mathematics of course you actually need the full structure of the reals but you also don't need to be a calculator very much in that case.)

[Kevin Buzzard]

To be honest @Arien Malec I wonder whether rat would be a perfect solution for you. It will have all the structure you need for the complex number game other than the silly last level which was not really supposed to be taken seriously anyway

[Arien Malec]

I don't think Mathlib4 has Rat? Maybe I need to switch to the Rational Number Game and prove all the goodness there first.

[Adam Topaz]

docs4#Rat

[Adam Topaz]

And for your purposes: docs4#instDecidableEqRat

[Adam Topaz]

(It's in Std4, which is a dependency of Mathlib4)

[Arien Malec]

Ah, in Std4!

[Arien Malec]

Rat seems to be broken ATM

Or rather Std.Nat.Lemmas

[Arien Malec]

And all working again! On with the show without the detour.

[Arien Malec]

Live by Lean4, die by Lean4

unknown constant Rat.mul_zero

[Kevin Buzzard]

If it's a ring you can use the ring tactic to prove everything ringy. In lean 3 there certainly wasn't a rat- specific lemma for every theorem about rings..mul_zero was in the root namespace and applied to any ring. I don't know how it's set up in Lean 4 though

[Mario Carneiro]

The ring theorems for Rat haven't been proved yet, only the definition. PR's welcome!

[Mario Carneiro]

@Kevin Buzzard While true, I'm fairly sure that mul_zero would have been filled in for Rat specifically in the ring instance, so Rat.mul_zero would presumably exist

[Mario Carneiro]

BTW the lemmas for Rat and fields generally are one of the final pieces remaining to restore ring to its former glory, so it's a prime opportunity for people who want to play the Rational Number Game for real

[Kevin Buzzard]

mul_zero isn't an axiom for rings so I don't see why Rat would be expected to have its own one

[Arien Malec]

Mario Carneiro said:

The ring theorems for Rat haven't been proved yet, only the definition. PR's welcome!

On it. Slowly, but on it.

[Scott Morrison]

@Arien Malec, note that there are two ways to go about this:

1. porting in an ad-hoc way the theorems about Rat that you want
2. working our way through the import hierarchy of mathlib, doing everything file at a time.

Method 1. may get you there faster, but almost certainly all work will be subsequently thrown out and replaced by the work coming from Method 2. On the other hand, pursuing Method 1 is a great learning experience, to get you up to speed!

[Mario Carneiro]

Not necessarily (in this case), because std4 cannot and will not inherit the entirety of that import graph you posted

[Mario Carneiro]

which is to say, I expect the outward interface of Data.Rat.Basic to stay basically the same as in mathlib but not the proofs. The proofs should be mostly the same however once we prove theorems that simplify the complicated current definition of things like Rat.add by proving theorems like a /. b + c /. d = (a * d + b * c) /. c * d and using that to get all the ring theorems