We can’t prove anything about Float right?

Stream: Program verification

[Jason Rute]

I recently told someone that we can’t prove (or disprove) something as simple as

theorem float_lt_transitive (a b c : Float) : a < b -> b < c -> a < c := sorry

in Lean because Float is opaque. I want to (1) confirm this is correct and (2) check that there are no plans to change this soon.

[Markus Himmel]

1. Yes, this is correct.
2. See my message at #Is there code for X? > Proving nan != nan @ 💬

[Cody Roux]

As a side note: It is my unconsidered opinion that one could proceed by building polymorphic code that depends on common type classes between Real and Float, e.g. Add,Mul, etc and OfScientific, and prove things about the Real instance. But of course, that says nothing about the floating point errors of the Float version.

Anything more, I think, would require porting a large portion of https://flocq.gitlabpages.inria.fr/

[Bas Spitters]

One could consider exposing Rocq as an external prover (in the sense of lean-smt), and prove the properties using Flocq...

[Matteo Cipollina]

Fyi some discussion here: #Machine Learning for Theorem Proving > Artificial Algorithms
A very early stage port of (the easy part of) Flocq is here (@GasStationManager made further developments ):
https://github.com/mkaratarakis/HopfieldNet/blob/master/HopfieldNet/floats/Flocqv2.lean

[Bas Spitters]

@Matteo Cipollina That's pretty cool! Could you summarize your experience doing the transpilation. What tools/prompts did you use, what worked and what is still hard?

[Bas Spitters]

If we could only translate the statements from Rocq to Lean, that would already be great progress.

[Matteo Cipollina]

Bas Spitters ha scritto:

Matteo Cipollina That's pretty cool! Could you summarize your experience doing the transpilation. What tools/prompts did you use, what worked and what is still hard?

Thank you :) Indeed I'd dare claim that it is already possible to semi-automate the porting of Flocq to Lean (a thankless job otherwise), and potentially, with supervision, the porting of Rocq code to Lean. What I did - after getting familiar with Flocq - and think about various alternative designs, was to create curated API distillate of relevant API in Flocq (and from Flocq's paper and relevant literature, while studying them) and relevant Mathlib API a good port should build on and that I did not want to reduplicate, have these as .md files and then use them as context wherever I needed help to check for myself or for CoPilot to help in the proofs and, most importantly, to provide context to AI helping me regularly, brutally review the code against criteria like accuracy vs Flocq math, 'optimal level of generality', integration with mathlib, insight against Flocq original. With a good blueprint, this orchestration, some care in choosing words, simple short prompts, and some judgment/taste, a lot can be done quite quickly. Always zero or one-shot. What is hard is to keep up with the theory to decide the correct assumptions for the definitions and theorems statements at each new step, in the subsequent parts. One reason I've stopped is that I wanted study more and also try to think of a reimplementation rather than porting (to allow a compatible license to mathlib). But actually, I just had no time to continue it in the last months, but I will try to develop it more with @Michail Karatarakis and @GasStationManager, trying to share some more lessons for these general-purpose low-gratification porting :)

[Cody Roux]

I'd say this kind of stuff seems like an ethical use of LLMs...