Proofs about floats and verifiable software

Stream: new members

[Dylan Le]

Hi all, new to using lean4. I am interested in using it for verification of a simple controller (think mountain car type controller) for research and have a few questions.

In Dafny, you could add floats and reason about what their values would be (as I have been told), can you do the same in lean4? For example see these two proofs, how would you go about showing them correct?

example : 1.0 + 1.0 = 2.0 := by
  sorry

variable (x:Float)
axiom zero_add_float :
  x + 0.0 = x
example : x + 0.0 = x := by
  sorry

The second example could just be a rewrite rule rw [zero_add_float], but is there something builtin for lean that I can use instead of having to define the zero_add_float axiom?

Another question I had was about the verification of algorithms or data structures, in Adacore Spark you can write the pre and post conditions for any function and verify it meets the requirements. Is there any way I could do something like that in lean4 for functional programming or am I thinking about this the wrong way.

[Ruben Van de Velde]

Is the axiom even true? :)

[Dylan Le]

Ruben Van de Velde said:

Is the axiom even true? :)

I was actually thinking about this yesterday. I am unfamiliar with how float works in lean4, but I assume inf + 0.0 = inf and -inf + 0.0 = -inf and all other cases should be correct?

Unless you are talking about roundoff issues, where I give x a value that has no precise floating point representation... That I am unsure if it makes sense.

[Ruben Van de Velde]

The main thing I recall from a class that covered (idealized) floats is that anything that claims equality of floats is probably wrong, but maybe you found the exception

[Dylan Le]

In general I am not looking at the equality of floats, that I understand can be perilous. Usually I am interested in questions like will x + y >= z always hold given some floating point values. But for these examples I feel like there is nothing wrong.

[Dylan Le]

The main reason I am interested in floats in this case is that readings from a sensor will have some floating point representation. I want to be able to reason about floats to stick to that domain.

[Tyler Josephson ⚛️]

You may be interested in interval arithmetic. Check out this thread!

[Tyler Josephson ⚛️]

Alternatively, if you want to write proofs about functions on idealized real numbers, and then perform computations on floating point numbers, there are a number of approaches discussed on Zulip here. For example, this one, or this one.

@John Velkey ⚛️ and @Tomas Skrivan have used polymorphic types for this, so a function with real-typed arguments can be used for proofs, and the same function with float-typed arguments can be used in computations.

[Tyler Josephson ⚛️]

But I have this question - why won't Lean let me use equality here?

#eval 0.1 + 0.2 < 0.3 -- false
#eval 0.1 + 0.2 > 0.3 -- true (my favorite example of floating-point arithmetic)
#eval 1.0 + 1.0 < 2.0 -- false
#eval 1.0 + 1.0 > 2.0 -- false
#eval 1.0 + 1.0 = 2.0 -- failed to synthesize, Decidable (1.0 + 1.0 = 2.0)

[Tomas Skrivan]

Because (NaN == NaN) == false in C therefore having instance of decidable equality on Float would be inconsistent.

[Tomas Skrivan]

I think there is also the issue that +0.0 = -0.0 but 1.0/(+0.0) != 1.0/(-0.0) which breaks function extensionality.

[Richard Copley]

Lean uses BEq for the native floating-point equality:

#eval 1.0 + 1.0 == 2.0 -- true
#eval 0.0 / 0.0 == 0.0 / 0.0 -- false

[Dylan Le]

Richard Copley said:

Lean uses BEq for the native floating-point equality:

#eval 1.0 + 1.0 == 2.0 -- true
#eval 0.0 / 0.0 == 0.0 / 0.0 -- false

Would you be able to use this then for proving the first example?

[Dylan Le]

Tyler Josephson ⚛️ said:

You may be interested in interval arithmetic. Check out this thread!

I don't believe this link is working it looks empty.

[Dylan Le]

Tomas Skrivan said:

Because (NaN == NaN) == false in C therefore having instance of decidable equality on Float would be inconsistent.

So is there any subset of reasoning for floats given certain constraints? For example only positive floating point representation of numbers is allowed. I agree the "axiom" I put forth will have some problems with NaN and signs.

[Richard Copley]

Dylan Le said:

Richard Copley said:

Lean uses BEq for the native floating-point equality:

#eval 1.0 + 1.0 == 2.0 -- true
#eval 0.0 / 0.0 == 0.0 / 0.0 -- false

Would you be able to use this then for proving the first example?

You can prove that they're BEq.beq:

example : (1.0 + 1.0 == 2.0) = true := by
  native_decide

[Dylan Le]

Richard Copley said:

Dylan Le said:

Richard Copley said:

Lean uses BEq for the native floating-point equality:

#eval 1.0 + 1.0 == 2.0 -- true
#eval 0.0 / 0.0 == 0.0 / 0.0 -- false

Would you be able to use this then for proving the first example?

You can prove that they're BEq.beq:

example : (1.0 + 1.0 == 2.0) = true := by
  native_decide

If I am understanding this correctly, it is calling under the hood evaluating 1.0 + 1.0 == 2.0 in lean? Is that correct? Any way to do this manually without using native_decide, out of curiosity?

[Richard Copley]

I guess so. In C++, one might even say. I'm not sure of the details.
Try these:

example : (1.0 + 1.0 == 2.0) = true := by
  show_term native_decide

theorem xxx : (1.0 + 1.0 == 2.0) = true := by
  native_decide

#print xxx

[Dylan Le]

Using show_term

Try this: exact of_decide_eq_true (Lean.ofReduceBool _example._nativeDecide_1 true (Eq.refl true))

Here's the message, trying to understand it but looks like just trying to decide true = true?

theorem xxx : (1.0 + 1.0 == 2.0) = true :=
of_decide_eq_true (Lean.ofReduceBool xxx._nativeDecide_1 true (Eq.refl true))

Same here.

[Dylan Le]

Which I guess is pretty makes sense by what my example is trying to show :sweat_smile:

[Richard Copley]

I don't know. One can have a look around:

whatsnew in
theorem xxx : (1.0 + 1.0 == 2.0) = true := by
  native_decide

#print xxx -- of_decide_eq_true (Lean.ofReduceBool xxx._nativeDecide_1 true (Eq.refl true))
#print xxx._nativeDecide_1 -- Bool := decide ((1.0 + 1.0 == 2.0) = true)
#eval xxx._nativeDecide_1 -- true
#check decide ((1.0 + 1.0 == 2.0) = true) -- Prop
#eval decide ((1.0 + 1.0 == 2.0) = true) -- true
#check Lean.ofReduceBool -- ∀ (a b : Bool), Lean.reduceBool a = b → a = b
#check of_decide_eq_true -- of_decide_eq_true {p : Prop} [inst : Decidable p] (a : decide p = true) : p

It seems to boil down to the fact that xxx._nativeDecide_1 evaluates to (true : Bool) which is true by magic (meaning that I don't know how to dig any deeper).

[Eric Rodriguez]

native_decide basically says 'I trust whatever the virtual machine says'; the eval xxx._native_decide_1 is pretty much exactly what it's doing

[Mario Carneiro]

Tomas Skrivan said:

Because (NaN == NaN) == false in C therefore having instance of decidable equality on Float would be inconsistent.

This isn't strictly true; what it really means is that it is not possible to have a LawfulBEq instance, nor to have x == y <-> x = y, but x = y "true equality" is decidable for IEEE floats, it's just a bit disappointing: All NaNs are equal, -0 and +0 are not equal, otherwise it matches ==

[Mario Carneiro]

I think it is sensible for lean not to provide a DecidableEq Float instance though because then it will open up the possibility of mistakenly using x = y instead of x == y or vice versa

[Mario Carneiro]

Here's a proof that the zeroes are not equal using native_decide:

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