Proving properties about floating point arithmetic

Stream: new members

[Huỳnh Trần Khanh]

Can I prove that something like this is correct in Lean 4? Or is Lean 4 not capable enough?

[Huỳnh Trần Khanh]

Apologies if I sound stupid, I am pretty much a noob.

[Eric Wieser]

I'm sure you could do it in lean 3 too, but in both cases you'll have to start by telling lean the rules of floating point numbers

[Eric Wieser]

Mathlib has a start at that in docs#fp.float

[Yakov Pechersky]

There are also docs#unsigned integers, but I haven't seen anything about how conversion of the bit patterns from unsigned to signed is the modulo operation (for some fixed bit width, here I think you use 64)

[Yakov Pechersky]

The definition at https://github.com/kth-competitive-programming/kactl/blob/master/doc/modmul-proof.md has an M and a c, and I can't tell which is the typo

[Eric Wieser]

A better link than @Huỳnh Trần Khanh's: non-raw github

[Eric Wieser]

Note that the proof @Yakov Pechersky links to starts with a false assumption about the precision of long double, which is platform-dependent, most notably equal to double on windows

[Huỳnh Trần Khanh]

I'd assume M is the typo because the rest of the proof uses c. Maybe I should file an issue against the repo.

[Eric Wieser]

https://github.com/kth-competitive-programming/kactl/issues/185 for the bad assumption

[Yakov Pechersky]

The proof sketch is doable (although some things seemed to be hand-waved) if you have the right definitions and API around them. You could try to make this statement about ints and rats first.