Zulip Chat Archive

Stream: new members

Topic: modular arithmetic


view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:32):

does mathlib or lean have a system for doing modular arithmetic, or the related theorems like fermat's little theorem? i can't find anything on the mathlib docs search, but i feel like i might be searching for the wrong thing

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:33):

The equivalence relation on N/Z of being congruent mod n is called nat.modeq/int.modeq, and the quotient ring is called Zmod n.

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:33):

What happens if you search there for Fermat?

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:34):

it kicks me to a google search, fermat site:https://leanprover-community.github.io/mathlib_docs

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:34):

and then the links on that google search are broken

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:35):

or at least the one mentioning number theory is

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:35):

lol I wanted Fermat and got format

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:35):

was there formerly a page in the docs named field_theory/finite.html ?

view this post on Zulip Alex J. Best (Sep 30 2020 at 15:36):

We have docs#zmod and docs#int.modeq, with fermat being docs#zmod.pow_card and similar results in https://github.com/leanprover-community/mathlib/blob/master/src/field_theory/finite/basic.lean#L282

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:36):

eew that's pretty nasty. Yes I think there was.

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:36):

@Rob Lewis presumably we can't do much about google returning out of date links?

view this post on Zulip Bryan Gin-ge Chen (Sep 30 2020 at 15:36):

GitHub search is sometimes better than the site-specific Google search (which seems to be always out-of-date): https://github.com/leanprover-community/mathlib/search?q=fermat

view this post on Zulip Heather Macbeth (Sep 30 2020 at 15:37):

And there was a discussion a few days ago with some other forms of Fermat:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/p.20divides.20x-x.5Ep

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:37):

ah ok - src/field_theory/finite/basic.lean is the file i was looking for

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:38):

@Kevin Buzzard is there a sitemap? usually those prevent out of date links

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:39):

Bryan will I'm sure know. I'm not involved with the website.

view this post on Zulip Bryan Gin-ge Chen (Sep 30 2020 at 15:39):

The docs are generated by the code in the doc-gen repo. I don't think we're generating a site map yet.

view this post on Zulip Rob Lewis (Sep 30 2020 at 15:39):

Kevin Buzzard said:

Rob Lewis presumably we can't do much about google returning out of date links?

No, AFAIK there's nothing we can do. There is a sitemap. This change happened a couple days ago.

view this post on Zulip Rob Lewis (Sep 30 2020 at 15:40):

https://leanprover-community.github.io/mathlib_docs/sitemap.txt

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:41):

is there a robots.txt pointing to the sitemap? i dont see one

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:41):

https://leanprover-community.github.io/robots.txt not found

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:41):

so google might not know to pick up the sitemap?

view this post on Zulip Rob Lewis (Sep 30 2020 at 15:42):

It's registered in the Google search console.

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:42):

So is it worth adding a "github search" option to the docs search?

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:42):

On this occasion it fared better than google.

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:43):

~~what with the quanta article coming out tomorrow morning¬¬

view this post on Zulip Rob Lewis (Sep 30 2020 at 15:43):

The builtin docs search doesn't use Google anymore either, it's strictly based on declaration names.

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:43):

Right, which was why we couldn't use it to find Fermat's Little Theorem

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:44):

the search on https://leanprover-community.github.io/mathlib_docs/ sent me to a google search

view this post on Zulip Rob Lewis (Sep 30 2020 at 15:45):

Oh, that's sneaky. Actually clicking the search button has a different effect than hitting enter...

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:45):

with currently broken links

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:45):

hitting enter did nothing, so i clicked the search button

view this post on Zulip Bryan Gin-ge Chen (Sep 30 2020 at 15:45):

We definitely want both since I think the declaration name search doesn't see docstrings / comments.

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:46):

The point is that currently neither option works when searching for "Fermat"

view this post on Zulip Rob Lewis (Sep 30 2020 at 15:46):

I think this is very far from an ideal user interface, but yeah, it should be easy enough to redirect the button to GitHub.

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:46):

whereas github search does work

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:46):

Hitting enter takes you to format because no Fermat is in any name in mathlib

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:47):

probably if you just do nothing and wait, google will fix up the links before too long

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:47):

presumably you aren't changing the URLs around all that frequently

view this post on Zulip Bryan Gin-ge Chen (Sep 30 2020 at 15:47):

Unfortunately, we are...

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:47):

ha

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:48):

we move fast and break things

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:49):

what does the docs search do when I hit enter - does it just send me to the #1 result?

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:49):

for example, i'm searching now for "totient" - i'm trying to figure out if the theorem that phi(ab) = phi(a)*phi(b) is anywhere

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:50):

but if i type "totient" and hit enter, the search just takes me right to the page for nat.totient, which is like just one of the many places that do things with totients

view this post on Zulip Adam Topaz (Sep 30 2020 at 15:51):

This file has a bunch of stuff:
https://github.com/leanprover-community/mathlib/blob/master/src/field_theory/finite/basic.lean

view this post on Zulip Adam Topaz (Sep 30 2020 at 15:51):

But I don't see the fact that φ\varphi is multiplicative.

view this post on Zulip Rob Lewis (Sep 30 2020 at 15:52):

Neither Google nor GitHub is obviously better. Google is a good fuzzy search that keeps you in the doc pages but can be outdated. GitHub is up to date but it's a stricter search and you can't easily get from GitHub back to the docs.

view this post on Zulip Rob Lewis (Sep 30 2020 at 15:53):

"Awesome doc search" was supposed to be a bachelor thesis project this spring but, uh, world events got in the way. It's still in the pipeline.

view this post on Zulip Adam Topaz (Sep 30 2020 at 15:53):

But digging through the imports, there's this too:
https://github.com/leanprover-community/mathlib/blob/master/src/data/nat/totient.lean

view this post on Zulip Adam Topaz (Sep 30 2020 at 15:54):

You can also do a git grep for totient

view this post on Zulip Adam Topaz (Sep 30 2020 at 15:54):

That will tell you all the files where it appears.

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:55):

kind of an unrelated question - can you guys actually read code like: (λ m hm, have hm : m < n / d ∧ gcd (n / d) m = 1, by simpa using hm,
mem_filter.2 ⟨mem_range.2 $ nat.mul_div_cancel' hd ▸
(mul_lt_mul_left hd0).2 hm.1,
by rw [← nat.mul_div_cancel' hd, gcd_mul_left, hm.2, mul_one]⟩)

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:55):

@Kevin Lacker there's a cemetary at the bottom of https://leanprover-community.github.io/lean_projects.html, a web page which I can never find the link to.

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:55):

because you remember what everything like mem_filter, mem_range, gcd_mul_left, you know what those are

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:56):

or is it more like, this stuff is write-once, read-never

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:56):

the compiler accepts it, therefore it's a success

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:56):

i'm just trying to figure out what standards to hold myself to here

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:56):

Do you understand how to use the infoview?

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:56):

Here's an interesting exercise.

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:56):

well i'm on github so there's no infoview

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:57):

You don't read code on github

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:57):

that's crazy

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:57):

okay I am starting to understand your culture better

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:57):

that's like watching a movie with the sound off

view this post on Zulip Bryan Gin-ge Chen (Sep 30 2020 at 15:57):

#4312 defines multiplicative functions, though at a first glance it doesn't have the totient.

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:57):

you download the project and you read the code with the help of the infoview

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:58):

You put your cursor just after the := and you can then just keep hitting the right arrow key and you can see everything that's going on

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:58):

you can see the state of the machine at that point

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:59):

isn't that like saying, we don't read code, we just step through it in the debugger

view this post on Zulip Kevin Lacker (Sep 30 2020 at 15:59):

so basically yes, the code is unreadable

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:59):

I can read that code

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 15:59):

can you post it again but using triple backticks so it gets highlighted correctly?

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 16:00):

and I'll read it to you

view this post on Zulip Kevin Lacker (Sep 30 2020 at 16:01):

can you just explain this part of the code: coprime_div_gcd_div_gcd

view this post on Zulip Kevin Lacker (Sep 30 2020 at 16:01):

do you know what that does offhand, or no

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 16:01):

if you were running this code on your computer you could just hover your mouse over that and something would pop up telling you what that meant precisely

view this post on Zulip Kevin Lacker (Sep 30 2020 at 16:02):

        b / d, mem_filter.2 mem_range.2 ((mul_lt_mul_left (show 0 < d, from hb.2  hb.2.symm  hd0)).1
            (by rw [ hb.2, nat.mul_div_cancel' (gcd_dvd_left _ _),
              nat.mul_div_cancel' (gcd_dvd_right _ _)]; exact hb.1)),
                hb.2  coprime_div_gcd_div_gcd (hb.2.symm  hd0)⟩,
          hb.2  nat.mul_div_cancel' (gcd_dvd_right _ _)⟩))```

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 16:02):

but because I can "speak a bit of Lean" I can guess what that means

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 16:02):

it is an assertion that two numbers are coprime, and one number is being called "div_gcd" and the other is also called "div_gcd"

view this post on Zulip Kevin Lacker (Sep 30 2020 at 16:03):

i literally laughed out loud. not sure why

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 16:03):

and so I would conjecure that this was the statement that if a and b were numbers in some suitable system which had a notion of gcd

view this post on Zulip Bryan Gin-ge Chen (Sep 30 2020 at 16:03):

(I think Kevin L said that he uses emacs, so instead of hovering he might have to hit some ctrl- ctrl- keybind.)

view this post on Zulip Kevin Lacker (Sep 30 2020 at 16:03):

it's not clear to me which buffer is the "info view" in emacs-world

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 16:03):

then it's the assertion that a/gcd(a,b) and b/gcd(a,b) were coprime

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 16:04):

the lean infoview is a more convenient version of any of the emacs buffers, for beginners at least

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 16:05):

unless it's now possible to have the infoview in emacs, which it might be knowing this lot

view this post on Zulip Adam Topaz (Sep 30 2020 at 16:05):

One thing that's maybe not so clear is the notation , and the infoview would tell you precisely what this means.

view this post on Zulip Kevin Lacker (Sep 30 2020 at 16:05):

the emacs docs and vscode docs don't seem to use any of the same terminology, so i can't quite tell how they compare

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 16:06):

If you're a beginner and are reading a lot of code, then having it running locally is essential because then every question you have about the code can be answered.

view this post on Zulip Kevin Lacker (Sep 30 2020 at 16:06):

but basically I am getting it. the code is not readable in the traditional software engineering sense that people just look at some code and know what it does. the standard practice is to be analyzing everything with the editor tooling, and also in practice to write code once and never change it

view this post on Zulip Mario Carneiro (Sep 30 2020 at 16:06):

It is a bit unfortunate but I think that unreadability without the goal view is always a side effect of tactic based proofs

view this post on Zulip Mario Carneiro (Sep 30 2020 at 16:07):

I think what we really need is a viewer that provides this information in a static document format

view this post on Zulip Mario Carneiro (Sep 30 2020 at 16:07):

Metamath proofs are basically that

view this post on Zulip Kevin Lacker (Sep 30 2020 at 16:07):

it makes sense, though, you never have a proof that you want to just alter its behavior a little bit. once a proof is valid, you're done, you never need to change it

view this post on Zulip Adam Topaz (Sep 30 2020 at 16:07):

I don't know about that... I've tried to read some agda proofs before, and found it more difficult than reading tactic blocks

view this post on Zulip Mario Carneiro (Sep 30 2020 at 16:07):

Oh term mode proofs as well

view this post on Zulip Mario Carneiro (Sep 30 2020 at 16:08):

I didn't mean to make a contrast against term mode there

view this post on Zulip Adam Topaz (Sep 30 2020 at 16:08):

Ah ok.

view this post on Zulip Mario Carneiro (Sep 30 2020 at 16:08):

If you look at a giant lambda calculus term without the types it's bewildering

view this post on Zulip Mario Carneiro (Sep 30 2020 at 16:08):

That's the basic motivation behind #explode

view this post on Zulip Mario Carneiro (Sep 30 2020 at 16:09):

the real explanation is the sequence of types that appear, the proof term is just a serialization mechanism for the inference rules being applied

view this post on Zulip Johan Commelin (Sep 30 2020 at 16:09):

I guess we can try to run lean-formatter against the entire repo. Not sure how many CPUs it will burn though.

view this post on Zulip Mario Carneiro (Sep 30 2020 at 16:10):

If we can get lean running on the web this could be done dynamically on a per-proof basis

view this post on Zulip Mario Carneiro (Sep 30 2020 at 16:10):

although some engineering would be needed to make it snappy without having to work from scratch every time

view this post on Zulip Mario Carneiro (Sep 30 2020 at 16:12):

ideally you could just load up the oleans and be ready to step through the text

view this post on Zulip Rob Lewis (Sep 30 2020 at 16:33):

Kevin Buzzard said:

Kevin Lacker there's a cemetary at the bottom of https://leanprover-community.github.io/lean_projects.html, a web page which I can never find the link to.

@Kevin Buzzard now linked at the bottom of https://leanprover-community.github.io/ and in the "Community" memu.

view this post on Zulip Patrick Massot (Sep 30 2020 at 16:36):

Kevin Lacker said:

it makes sense, though, you never have a proof that you want to just alter its behavior a little bit. once a proof is valid, you're done, you never need to change it

Of course we change proofs very often when we generalize stuff or alter definitions slightly. There is no problem at all.

view this post on Zulip Scott Morrison (Oct 01 2020 at 02:21):

I think a good rule of thumb for deciding when inscrutable proofs are okay is the following:

  • if it is the sort of fact that, if you started explaining it to a mathematician, they would stare at you blankly and not understand that there was even anything to explain, you can make the Lean proof as terse and inscrutable as you like
  • if anyone could reasonably be expected to have to stop and think about a step, ideally it is possible to reconstruct that step from looking at the proof (admittedly, perhaps with the goal view)
  • if you'd actually say it in a research paper or textbook, it deserves a human-readable comment (even if just a doc-string re-explaining the type of the def or lemma)

Last updated: May 12 2021 at 04:19 UTC