## Stream: general

### Topic: native.float equality is inconsistent

#### Mario Carneiro (Dec 26 2020 at 21:19):

I just noticed that float equality is exposed as an implementation of decidable_eq. This is not correct:

def test_eq {α} [decidable_eq α] (x : α) := to_bool (x = x)

theorem test_eq_tt {α} [decidable_eq α] (x : α) : test_eq x = tt :=
(to_bool_iff _).2 rfl

#eval test_eq native.float.qNaN -- ff


#### Mario Carneiro (Dec 26 2020 at 21:24):

We could just implement has_equiv or some other notation instead of = (which means something specific in lean and does not permit funny things like IEEE float equality)

#### Mario Carneiro (Dec 26 2020 at 21:26):

Since there is no to_bits function on native.float, it would also be possible to implement a decidable_eq instance that makes any two NaNs equal, i.e. x = y <-> x.eq y \/ (is_nan x /\ is_nan y)

#### Jacques Carette (Dec 26 2020 at 21:30):

Note that you also run into trouble with +-infinity -- if they both invert to unsigned 0, things get weird again. But +-0 are supposed to be equal (in IEEE's highly non-mathematical notion of equal).

#### Mario Carneiro (Dec 26 2020 at 21:30):

ah, that's true, my proposed alternative would have to check for signed zero

#### Mario Carneiro (Dec 26 2020 at 21:31):

probably the easiest implementation of a conforming = is just x.to_bits = y.to_bits

#### Marc Huisinga (Dec 26 2020 at 21:31):

yup, +0 = -0 but 1/+0 = +inf != -inf = 1/-0

#### Mario Carneiro (Dec 26 2020 at 21:34):

def test_congr {α} [decidable_eq α] (x y : α) (f : α → α) := to_bool (x = y → f x = f y)

theorem test_congr_tt {α} [decidable_eq α] (x y : α) (f) : test_congr x y f = tt :=
(to_bool_iff _).2 (λ x, by rw x)

#eval test_congr (0:native.float) (-0) (λ x, 1 / x) -- ff


#### Eric Wieser (Dec 26 2020 at 21:34):

I'm guessing not even a quot can represent the irreflexivity of nan equality?

#### Mario Carneiro (Dec 26 2020 at 21:34):

no, that would help with the congr example just given but not irreflexivity

#### Mario Carneiro (Dec 26 2020 at 21:37):

But I think any quotient that identifies 0 and -0 and is closed under congr would have to identify +inf and -inf; is it possible to prove this also identifies all finite numbers?

#### Mario Carneiro (Dec 26 2020 at 21:37):

oh lol there is -nan too

#### Marc Huisinga (Dec 26 2020 at 21:40):

Mario Carneiro said:

is it possible to prove this also identifies all finite numbers?

-inf <= x <= +inf?

#### Mario Carneiro (Dec 26 2020 at 21:40):

uh oh: tanh inf = 1, tanh -inf = -1

#### Mario Carneiro (Dec 26 2020 at 21:41):

Are you assuming le_antisymm there @Marc Huisinga ?

#### Mario Carneiro (Dec 26 2020 at 21:41):

I'm just assuming that the equality is closed under congruence

#### Marc Huisinga (Dec 26 2020 at 21:42):

i haven't actually looked up how stuff is specified in lean 3, just guessing

#### Mario Carneiro (Dec 26 2020 at 21:43):

There is no specification, they are mostly uninterpreted functions

#### Mario Carneiro (Dec 26 2020 at 21:43):

which is mostly fine, except that this still assumes they are "functions", i.e. respect equality

#### Mario Carneiro (Dec 26 2020 at 21:44):

and so implementing decidable_eq is a strong statement since two things that are equal can't be distinguished by later function application

#### Mario Carneiro (Dec 26 2020 at 21:45):

I'm not even sure it's totally safe to assume they are functions in this sense in lean 4 since the compilation works by generating C code and gcc can do funny things like increasing the precision on intermediate computations

#### Mario Carneiro (Dec 26 2020 at 21:46):

so determinism goes out the window

#### Leonardo de Moura (Dec 27 2020 at 01:22):

@Marc Huisinga There is no float type in Lean 3. It seems someone added them to the Lean 3 community branch.

#### Bryan Gin-ge Chen (Dec 27 2020 at 01:39):

float was added to community Lean 3 by @Edward Ayers in lean#2.

#### Jason Rute (Dec 27 2020 at 14:02):

When you say "inconsistent", do you mean you can prove false or just that it is weird behavior in the meta world? I tried to turn your example into a proof of tt = ff, but even though #eval test_eq native.float.qNaN comes out asff, I can't find a way to prove test_eq native.float.qNaN = ff. Does the fact that float is meta protect the consistency of Lean (3 community version)?

#### Jason Rute (Dec 27 2020 at 14:25):

This won't even check:

example : decidable_eq native.float := native.float.dec_eq


So even though native.float.dec_eq looks like an inconsistent axiom, is not usable in proofs it seems. (Maybe this is all obvious, but I got confused with the "inconsistent" terminology.)

#### Jason Rute (Dec 28 2020 at 13:17):

Again this is probably obvious to everyone else, but I convinced myself by "inconsistent" here we just mean that if we prove something about = we should try to make make our meta definitions behave as if they are functions which respect Lean's equality rule, which float currently does not.

#### Jason Rute (Dec 28 2020 at 13:17):

Other than that there is nothing logically inconsistent since meta definitions don't have to obey Lean theorems about functions and equality. Here is an example I coded up reproducing the problems with float but just using a meta type I coded in Lean:

meta def paradox : unit -> false

meta def cheat (p : Prop) : p := false.elim (paradox ())

| pos : ℕ → bad_int  -- has +0
| neg : ℕ → bad_int  -- has -0

| (pos 0) (neg 0) := tt
| nan nan := ff
| (pos i) (pos j) := i = j
| (neg i) (neg j) := i = j
| _ _ := ff

| (pos n) := pos 1
| (neg n) := neg 1
| nan := nan

meta def dec_eq_rel (i j : bad_int) : decidable (i = j) :=
decidable.is_true (cheat (i = j))
else
decidable.is_false (cheat (i ≠ j))

meta def dec_eq : decidable_eq bad_int := dec_eq_rel
attribute [instance] dec_eq

def test_eq {α} [decidable_eq α] (x : α) := to_bool (x = x)

theorem test_eq_tt {α} [decidable_eq α] (x : α) : test_eq x = tt :=
(to_bool_iff _).2 rfl

#eval test_eq nan -- ff

def test_congr {α} [decidable_eq α] (x y : α) (f : α → α) := to_bool (x = y → f x = f y)

theorem test_congr_tt {α} [decidable_eq α] (x y : α) (f) : test_congr x y f = tt :=
(to_bool_iff _).2 (λ x, by rw x)

#eval test_congr (pos 0) (neg 0) bad_sign -- ff



#### Mario Carneiro (Dec 28 2020 at 17:08):

Yes, you can argue in this way. However, keep in mind that bad meta definitions also compromise the correctness of lean's compiler, which matters even for meta code because this is what gives them meaning. That is, to the extent that meta code is like code you would find in C or Haskell, this kind of thing can cause miscompilation because lean makes some assumptions about pure code being pure

#### Mario Carneiro (Dec 28 2020 at 17:12):

We're doing a similar thing right now to cover up another inconsistency in level I found a long time ago:

open level
meta example : max zero zero ≠ zero := λ h, level.no_confusion h
#eval to_bool (max zero zero = zero) -- tt


#### Kevin Buzzard (Dec 28 2020 at 17:18):

If it's not a proof of false, it's not an inconsistency, surely

#### Chris Hughes (Dec 28 2020 at 17:20):

It's still a problem if it means your unsafe code is even less safe than you expected.

#### Mario Carneiro (Dec 28 2020 at 18:19):

I will note that a proof of false was in fact used in Jason's example

#### Mario Carneiro (Dec 28 2020 at 18:21):

meta code allows you to bypass restrictions, it's not "safe". But that doesn't mean we shouldn't make every effort to not be wrong

#### Kevin Lacker (Dec 28 2020 at 18:23):

i think the right thing to do for floating point equality is to check x.to_bits = y.to_bits and if you need the abomination that is ieee equality to call it ieee_eq or something

#### Kevin Lacker (Dec 28 2020 at 18:24):

in general you rarely want to be checking ieee equality for floating point numbers anyway, only if you're doing something like verifying that a serialization->deserialization worked where you'd want bitwise equality

#### Patrick Massot (Dec 28 2020 at 18:25):

This will be even more important in Lean 4 where we'll have more power to create custom commands. For instance it should be pretty easy to create a major_theorem command which acts like theorem excepts it replaces whatever statement you type with 0 = 0 before asking for a proof. Of course the Lean kernel will see a statement and proof of 0 = 0 but a human reading the Lean file will see any statement you want.

#### Mario Carneiro (Dec 28 2020 at 18:33):

Kevin Lacker said:

i think the right thing to do for floating point equality is to check x.to_bits = y.to_bits and if you need the abomination that is ieee equality to call it ieee_eq or something

I agree with this. Using = or == is a bad habit inherited from other programming languages that don't have such a strong stance on formal correctness. Rust uses PartialEq instead of Eq essentially only because floats exist, but I would much rather compromise on notational convenience of float ops because it's important to recognize the float weirdness happening in each operation.

#### Mario Carneiro (Dec 28 2020 at 18:34):

Patrick Massot said:

This will be even more important in Lean 4 where we'll have more power to create custom commands. For instance it should be pretty easy to create a major_theorem command which acts like theorem excepts it replaces whatever statement you type with 0 = 0 before asking for a proof. Of course the Lean kernel will see a statement and proof of 0 = 0 but a human reading the Lean file will see any statement you want.

I think it's possible to override theorem to do that, actually

#### Johan Commelin (Dec 28 2020 at 18:35):

wait, and you are telling us now...

#### Patrick Massot (Dec 28 2020 at 18:35):

It may be possible in Lean 3 already, but I wanted to point out it will probably be easy in Lean 4.

#### Johan Commelin (Dec 28 2020 at 18:35):

all these months we've been sweating to prove our theorems... and we were just one override and a rfl away from proving them

#### Mario Carneiro (Dec 28 2020 at 18:36):

Yes, this is a major concern of mine regarding the tremendous syntax flexibility of lean 4. You basically can't trust anything you see

#### Johan Commelin (Dec 28 2020 at 18:38):

"trusted syntax is an editor feature" -- anonymous

#### Leonardo de Moura (Dec 28 2020 at 19:30):

I think it is important to clarify a few points and avoid misinformation being spread.

1- Most users assume "inconsistent" means "being able to prove false". This is not the case here.

2- The bug is in the native implementation (in C++) of float equality. The bug is in the Lean 3 community branch only.

3- The bug only affects people using the Lean 3 community branch as a programming language.
One may claim it also affects users writing tactics. As far as I know, nobody uses float for writing tactics.
However, even if someone wrote a tactic using them, it would be just another buggy tactic. Incorrect proofs produced by buggy tactics are caught by the kernel.

4- A less alarmist way to describe the bug is: "The native implementation of float equality is incorrect. It doesn't correctly implement the type it claims to implement. This bug affects people using the Lean 3 community branch, float, and Lean as a programming language".

5- No "proof of false" has ever been reported to a Lean developer. If a "proof of false" is one day found, we would tag it as a high priority and would fix it.

6- In Lean, users can inspect, and export objects constructed using the system. This allows users to scrutinize any result proved using Lean. In Lean 4, users have access to not only the Kernel terms but all built-in data structures representing parsers, elaborators, instances, classes, etc.

7- One doesn't need "tremendous syntax flexibility" to tricky naive users to believe they proved something they didn't. Example:

notation false := true

theorem unsound : false :=
trivial


One can easily obfuscate the example above and make the exploit less obvious. However, the previous point remains, we provide tools for users to scrutinize and export their results.

8- Users can write their own independent type checkers and visualizers for Lean developments. A few independent type checkers have already been implemented. I know that 2 of them are efficient enough for checking real/big Lean developments.

#### Mario Carneiro (Dec 28 2020 at 19:36):

I'm not laying any blame at lean 4 here. My original post was about lean 3 community edition. Some of the follow on comments apply to lean 4, but this particular issue has already been fixed

#### Mario Carneiro (Dec 28 2020 at 19:39):

Re: 7, I agree that it's easy to write things that don't mean what they say in lean 3 (and even easier in lean 4). This doesn't make me any less concerned. Ideally we would have something like the export format with trusted syntax, but where you can actually read it. This does not currently exist.

#### Mario Carneiro (Dec 28 2020 at 19:43):

Re: 1, I don't have a good term for this. Is "miscompilation" better? "Inconsistent with reality"? The code doesn't do what it says. Regarding "can't prove false", of course in meta code you very much can, but that's obviously not what people are talking about. native.float is a meta feature, it lacks whatever sense of correctness you can meaningfully apply to meta things.

#### Mario Carneiro (Dec 28 2020 at 19:51):

Mario Carneiro said:

Yes, this is a major concern of mine regarding the tremendous syntax flexibility of lean 4. You basically can't trust anything you see

I admit this is hyperbolic. Of course in practice this isn't likely to be a major issue. But from a formal perspective, I really don't know if I can tighten this claim up very much; you more or less have to read the entirety of the lean code and parser infrastructure before you can make any sure claims about the lack of tricky parser mechanisms in use. Maybe we need a "Lean Zero" for verified syntax? :)

#### Patrick Massot (Dec 28 2020 at 19:57):

Leo, I don't know how much of your message is directed towards my two messages in this thread, but I'd like to clarify that I'm not worried at all, and I'm super excited to get access to Lean 4 flexibility in the future. My message was a comment on Mario's "meta code allows you to bypass restrictions, it's not "safe". But that doesn't mean we shouldn't make every effort to not be wrong". As you point out yourself, there are ways to write deceiving Lean code, but this wasn't meant as a critique, only reinforcing the claim that we should make every effort to write good meta code.

#### Mario Carneiro (Dec 28 2020 at 20:04):

Jason Rute said:

When you say "inconsistent", do you mean you can prove false or just that it is weird behavior in the meta world? I tried to turn your example into a proof of tt = ff, but even though #eval test_eq native.float.qNaN comes out asff, I can't find a way to prove test_eq native.float.qNaN = ff. Does the fact that float is meta protect the consistency of Lean (3 community version)?

Leo already said this, but just to be clear: This is just weird behavior in meta world. The kernel doesn't see any declarations marked meta, so logical soundness of the lean kernel is not compromised.

#### Leonardo de Moura (Dec 28 2020 at 20:09):

@Mario Carneiro This is not the first message I see from you that has a very "alarmist tone".
The main point is the bug does not affect the soundness of results proved using Lean.
The key issue here for me is: Should we trust results proved using Lean?

Regarding "can't prove false", of course in meta code you very much can, but that's obviously not what people are talking about.

I disagree. It was not obvious to Jason Rute. He wrote

When you say "inconsistent", do you mean you can prove false or just that it is weird behavior in the meta world?

He is clearly concerned about the soundness of the system.

Re: 1, I don't have a good term for this. Is "miscompilation" better?

You could have simply said: "this bug does not affect the soundness of results proved using Lean"
You could have just answered "no, you cannot prove false" to Jason. He was clearly asking whether the bug affects the soundness of the system or not.

Ideally we would have something like the export format with trusted syntax, but where you can actually read it. This does not currently exist.

We don't need an export format in Lean 4 anymore. Users can traverse all data structures and export whatever they want using the format they want.
As far as I know, Gabriel's external type checker can pretty-print the results it checked.

Maybe we need a "Lean Zero" for verified syntax? :smile: