Zulip Chat Archive

Stream: general

Topic: calculate with mod

Jeremy Avigad (Mar 20 2019 at 15:14):

What is the best way to prove (m * n) % n = 0 on nat? IIRC, the library used to have rules like these for calculating with mod, but now I can't find them. Am I missing something?

Chris Hughes (Mar 20 2019 at 15:21):


Chris Hughes (Mar 20 2019 at 15:23):

In general, the files, data.nat.modeq and data.zmod.basic might help with this stuff.

Jeremy Avigad (Mar 20 2019 at 15:25):


Scott Morrison (Mar 20 2019 at 21:34):

by library_search agrees: mul_mod_left m n :-)

I've actually run into some robustness problems (works on lots of examples, mysteriously fails in some cases, in every fix I try breaks something else...) but hopefully coming soon.

Patrick Massot (Mar 20 2019 at 21:42):

You are great at writing teasers!

Scott Morrison (Mar 20 2019 at 22:03):

Sorry.. life keeps intervening. :-)

Scott Morrison (Mar 20 2019 at 22:04):

It occurred to me on the bike ride in that I should split library_search into a few PRs. I should be able to do one that covers 95% of cases that is nice and simple. Then I can later add the full on "let's do backwards reasoning with clever choices of the search pattern", if I ever get that to be robust. :-)

Last updated: Dec 20 2023 at 11:08 UTC