Stream: new members
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?
Huỳnh Trần Khanh (Jan 04 2021 at 07:50):
Apologies if I sound stupid, I am pretty much a noob.
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
Eric Wieser (Jan 04 2021 at 08:00):
Mathlib has a start at that in docs#fp.float
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)
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
Eric Wieser (Jan 04 2021 at 08:04):
A better link than @Huỳnh Trần Khanh's: non-raw github
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
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.
Eric Wieser (Jan 04 2021 at 08:13):
https://github.com/kth-competitive-programming/kactl/issues/185 for the bad assumption
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