Zulip Chat Archive

Stream: new members

Topic: Proving properties about floating point arithmetic


view this post on Zulip Huỳnh Trần Khanh (Jan 04 2021 at 07:41):

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

view this post on Zulip Huỳnh Trần Khanh (Jan 04 2021 at 07:50):

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

view this post on Zulip Eric Wieser (Jan 04 2021 at 07:59):

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

view this post on Zulip Eric Wieser (Jan 04 2021 at 08:00):

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

view this post on Zulip Yakov Pechersky (Jan 04 2021 at 08:01):

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)

view this post on Zulip Yakov Pechersky (Jan 04 2021 at 08:02):

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

view this post on Zulip Eric Wieser (Jan 04 2021 at 08:04):

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

view this post on Zulip Eric Wieser (Jan 04 2021 at 08:06):

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

view this post on Zulip Huỳnh Trần Khanh (Jan 04 2021 at 08:12):

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

view this post on Zulip Eric Wieser (Jan 04 2021 at 08:13):

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

view this post on Zulip Yakov Pechersky (Jan 04 2021 at 08:15):

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.


Last updated: May 10 2021 at 18:22 UTC