## Stream: new members

### Topic: Kevin Wilson: Introduction (+ a question on small examples)

#### Kevin Wilson (Jan 24 2022 at 17:36):

Hi there,

My name is Kevin Wilson. Currently I run the data science group at The Policy Lab at Brown University and generally think about organizing and utilizing administrative data nowadays, but in a former life I got a Ph.D. in number theory. A friend of mine and I were discussing his work in theorem provers the other day, and he mentioned how much the lean and mathlib communities had grown, so I figured I'd check it out!

First off, thank you for all the wonderful resources. Lean and mathlib installed exactly as advertised in the docs, and both the tutorial and the natural number game were excellent introductions.

So I thought I'd try to prove something on my own from my own branch of math: The number of squarefree integers less than X is ~ X/zeta(2). That seemed a good deal to bite off, so I figured I'd try an example:

The set of squarefree integers at most 9 is {1, 2, 3, 5, 6, 7}.

I quickly found myself lost in the thickets of the documentation of finset and so I wondered if I could prove the set of squarefree integers at most 1 has size 1. I got to here:

import algebra.squarefree
import tactic

noncomputable theory
open_locale classical

def set_squarefree_le_x (N : ℕ): finset ℕ := finset.filter squarefree (finset.range (N + 1))

lemma sq_1_eq_1 : finset.card (set_squarefree_le_x 1) = 1 :=
begin
unfold set_squarefree_le_x,
rw finset.card_eq_succ,
use 1,
use ∅,
split,
simp,
split,
rw finset.eq_singleton_iff_unique_mem,
--- etc
end


At this point I got this in the interactive pane:

rewrite tactic failed, did not find instance of the pattern in the target expression
?m_2 = {?m_3}
state:
2 goals
⊢ {1} = finset.filter squarefree (finset.range (1 + 1))

⊢ ∅.card = 0


I stared at this for a long while (and eventually came up with a much longer proof to get around this), but I realized I must be approaching this the wrong way.

I was curious if there's some advice on approaching these sort of small, concrete examples, especially about subsets of the integers or subgroups of specific finite groups?

Thanks in advance for any help here, and thank you for the great work on this library!

Kevin

#### Riccardo Brasca (Jan 24 2022 at 17:44):

I would do this saying that finset.filter squarefree (finset.range (N + 1)) is a subset of finset.range (N + 1), so the cardinality is smaller.

#### Riccardo Brasca (Jan 24 2022 at 17:46):

The cardinality of finset.range is surely in mathlib, so you have that the cardinality is at most 2.

#### Yaël Dillies (Jan 24 2022 at 17:46):

Hey! Welcome. Small concrete calculations are usually the worst, so I'm not sure what to answer.

#### Yaël Dillies (Jan 24 2022 at 17:47):

We have docs#nat.squarefree.decidable_pred, so in such a small case the calculation can actually be done automatically.

#### Johan Commelin (Jan 24 2022 at 17:47):

@Kevin Wilson Welcome! There is something called decidable_pred. It basically means that there is an algorithm that you can run to find out the truth of a certain predicate/proposition. If you are lucky, someone has already shown that squarefree is a decidable predicate on the natural numbers. If so, your lemma should be provable in one line: dec_trivial.
But this proof method will probably become unbearably slow for N ≥ 10. Maybe even earlier.

#### Riccardo Brasca (Jan 24 2022 at 17:48):

But I agree with Yael, the rest is annoying, you have to prove that 0 is not in the filter, so it is actually a subset of erase and blah blah

#### Yaël Dillies (Jan 24 2022 at 17:51):

Johan Commelin said:

But this proof method will probably become unbearably slow for N ≥ 10. Maybe even earlier.

Erhm...

#### Yaël Dillies (Jan 24 2022 at 17:52):

import algebra.squarefree

#eval (list.range 50000).filter squarefree


#### Yaël Dillies (Jan 24 2022 at 17:53):

list.length of that yields 30401.

#### Kevin Wilson (Jan 24 2022 at 17:53):

(Sorry, not used to Zulip so sent this before I saw the later messages! Please give me a moment while I read them!)

@Riccardo Brasca I did think about that, but eventually you have to show that it's ≤ 1, so you'll eventually need to enumerate finset.range (1 + 1) and check each element. Hence I figured I'd just show in this case, it was equal to {1}. :-)

@Yaël Dillies Sadness. If there are examples, though, I'd be happy to take a look, even if they're the worst!

#### Yaël Dillies (Jan 24 2022 at 17:55):

In that case, your pain also came from using docs#finset.range rather than docs#list.range. Finsets are unordered, so they lack an easy induction treatment, as opposed to lists. For small calculations, lists are usually better.

#### Yaël Dillies (Jan 24 2022 at 17:56):

If you're interested, here's a PR that does precisely this: small calculations in a smart way using lists. #10645

#### Kevin Wilson (Jan 24 2022 at 17:58):

@Johan Commelin Yeah I was confused by the decideable_pred because it was clearly already in the algebra.squarefree packages as @Yaël Dillies points out. It was unclear if I needed to hint that somehow to the rewriter and even how to do such things.

@Yaël Dillies this makes sense. I was drawn to docs#finset.range because, well, it seemed like what I was going for. I'll take a look at this small Roth number computation and see if I can make this work! Thanks!

#### Johan Commelin (Jan 24 2022 at 17:59):

@Yaël Dillies This doesn't work, do you know why?

lemma sq_1_eq_1 : finset.card (set_squarefree_le_x 1) = 1 :=
begin
delta set_squarefree_le_x,
dec_trivial,
end


#### Yaël Dillies (Jan 24 2022 at 17:59):

Because it's a finset, Johan. Replace that with a list and it will work out.

#### Johan Commelin (Jan 24 2022 at 18:00):

Why the heck is that a problem? Lean should be able to compute with finset.range 2.

#### Yaël Dillies (Jan 24 2022 at 18:01):

Hmm, maybe I said bullshit. This doesn't work either

import algebra.squarefree

example : ((list.range 2).filter squarefree).length = 1 := rfl


#### Yaël Dillies (Jan 24 2022 at 18:01):

Is it that #eval can do stuff that rfl or dec_trivial can't?

#### Rob Lewis (Jan 24 2022 at 18:02):

Hi @Kevin Wilson ! I'm also at Brown, new this year to the CS department, and taught a course using Lean this fall. Nice to see someone else nearby getting into it!

#### Yaël Dillies (Jan 24 2022 at 18:04):

But it's a problem with squarefree, because example : ((list.range 2).filter ⊤).length = 2 := rfl works

#### Yaël Dillies (Jan 24 2022 at 18:05):

Ahah! Is it some reducibility setting maybe?

#### Kevin Wilson (Jan 24 2022 at 18:07):

Nice to meet you, @Rob Lewis ! I'll definitely take a look at this course. I might bug you for a coffee at some point as well!

#### Eric Rodriguez (Jan 24 2022 at 18:25):

how do you trace dec_trivial calls? this is something I've wanted to know for a while and never found an answer sadly

#### Eric Rodriguez (Jan 24 2022 at 18:25):

something is very weird in that example...

#### Yakov Pechersky (Jan 24 2022 at 19:07):

Finsets have an induction on them, what do you mean Yael that they don't have an easy one?

#### Yaël Dillies (Jan 24 2022 at 19:07):

I think I got confused by the error.

#### Heather Macbeth (Jan 24 2022 at 20:36):

Hi @Kevin Wilson, nice to see you here!

#### Kevin Wilson (Jan 24 2022 at 22:29):

Hi @Heather Macbeth ! Long time no see!!

#### Heather Macbeth (Jan 24 2022 at 22:31):

Indeed! Well, if we get you addicted here, it may be short time much see!

#### Kyle Miller (Jan 24 2022 at 22:51):

Yaël Dillies said:

Ahah! Is it some reducibility setting maybe?

This is a sort of error I asked about a couple weeks ago, and Mario was saying it's something to do with which axioms appear in the definition, and some of them make it get "stuck."

Some examples to show some behavior (but not explaining what's wrong with squarefree):

import algebra.squarefree

example : ¬ squarefree 0 := dec_trivial -- ok
example : ¬ squarefree 1 := dec_trivial -- fails
example : squarefree 2 := dec_trivial -- fails

instance : decidable (squarefree 2) :=
is_true begin
rw nat.squarefree_iff_nodup_factors (dec_trivial : 2 ≠ 0),
norm_num
end

example : squarefree 2 := dec_trivial -- ok


#### Kyle Miller (Jan 24 2022 at 22:52):

I suspect the problem is that n.factors.nodup gets stuck on n.factors, which involves division, so well-founded recursion. (But I don't really know.)

#### Kyle Miller (Jan 24 2022 at 22:53):

New guess: it's that factors itself depends on well-founded recursion. Those don't seem to work with dec_trivial...

def factors : ℕ → list ℕ
| 0 := []
| 1 := []
| n@(k+2) :=
let m := min_fac n in have n / m < n := factors_lemma,
m :: factors (n / m)


#### Kyle Miller (Jan 24 2022 at 23:04):

It looks like it's possible to get it to work with an auxiliary algorithm for squarefree. I wrote a terrible one that does trial division with a naive upper bound:

def squarefree'_aux (n : ℕ) : ℕ → bool
| 0 := tt
| 1 := tt
| t'@(t+1) := if n % (t'*t') = 0 then ff else squarefree'_aux t

def squarefree' : ℕ → bool
| 0 := ff
| 1 := ff
| n := squarefree'_aux n n

lemma squarefree_iff_squarefree' (n : ℕ) :
squarefree n ↔ squarefree' n := sorry

instance foo {n : ℕ} : decidable (squarefree n) :=
begin
refine if hs : squarefree' n then _ else _,
apply is_true, rw squarefree_iff_squarefree', assumption,
apply is_false, rw squarefree_iff_squarefree', assumption,
end

example : ¬ squarefree 1 := dec_trivial -- works
example : squarefree 37 := dec_trivial -- works


#### Yaël Dillies (Jan 24 2022 at 23:08):

Can't you use docs#decidable_of_iff' to shorten foo?

#### Kyle Miller (Jan 24 2022 at 23:15):

I thought when I'd tried that the examples got stuck, but I guess that works too. (I wrote it in a way where I could be sure it definitely wouldn't get stuck, since this isn't so fun to debug :smile:). Replaced in code block

#### Yaël Dillies (Jan 24 2022 at 23:18):

I think decidable_of_iff and decidable_of_iff' were explicitly designed not to get stuck.

#### Kyle Miller (Jan 24 2022 at 23:31):

I wonder how you can write factors to be similarly efficient but still not get stuck. Maybe you can have an auxiliary function that you give "gas" (i.e., the number of recursive steps it will ever apply), and you can estimate how much gas you'll ever need? For example, factors won't ever give more factors than n, so that can serve as the gas to power the recursion. (And of course nat.min_fac uses well-founded recursion, too...)

#### Kevin Wilson (Jan 25 2022 at 18:37):

I'd be curious if there is, because by attempts at proving this squarefree number asymptotic seems to keep getting stymied at dec_trivials that seemingly get stuck on things like squarefree and factors and divisors.

#### Alex J. Best (Jan 25 2022 at 18:43):

If you are trying to prove an asymptotic dec_trivial likely won't be too helpful anyway, its just a way of forcing lean to evaluate closed expressions. So its useful to do small calculations when a problem is inherently finite, but will not be able to really prove much more than that. Where are you stuck exactly?

#### Kevin Wilson (Jan 25 2022 at 18:52):

There's a lot of induction lying around in proving some rearrangement equals some other rearrangement. So the base cases end up looking like needing to prove f 1 = 1. I can type #eval f 1 and it shows me 1. Writing it out by hand is, well, quite nightmarish!

#### Yaël Dillies (Jan 25 2022 at 18:54):

Also I must tell you that you probably didn't pick the easiest problem to start with!

#### Kevin Wilson (Jan 25 2022 at 18:54):

Gotta challenge yourself! :-)

#### Yaël Dillies (Jan 25 2022 at 18:55):

(we don't even have the Zeta function)

#### Kevin Wilson (Jan 25 2022 at 18:55):

But I'm definitely realizing that!

#### Kevin Wilson (Jan 25 2022 at 18:56):

Conveniently, the standard proof doesn't directly use the zeta function. But it does involve proving things like $\sum_{d^2 \mid n} \mu(d) = 1$ if and only if $n$ is squarefree.

#### Kevin Wilson (Jan 25 2022 at 18:58):

And that proof essentially goes: a) prove that function is multiplicative; b) prove it for prime powers. I saw there were arithmetic_functions, moebius, and even the notion of a multiplicative arithmetic function, so I figured at least the foundation is there!

#### Alex J. Best (Jan 25 2022 at 19:00):

Ok dec_trivial could be helpful but maybe another good way when the definitions are a bit more complicated is to coax tactic#norm_num into unfolding the right things and evaluating them (normally this involves passing it extra function names / lemmas, like for simp, so that it rewrites the right things until it gets to a point it can actually do the calculation)

#### Kyle Miller (Jan 25 2022 at 19:01):

@Kevin Wilson Did you finish the proof in your first post? I took a stab at it and got through mostly with simp, ext, norm_num, and interval_cases.

import algebra.squarefree
import tactic

noncomputable theory
open_locale classical

def set_squarefree_le_x (N : ℕ): finset ℕ := finset.filter squarefree (finset.range (N + 1))

lemma sq_1_eq_1 : finset.card (set_squarefree_le_x 1) = 1 :=
begin
unfold set_squarefree_le_x,
rw finset.card_eq_succ,
use 1,
use ∅,
split,
simp,
simp,
ext,
simp,
split,
rintro rfl,
simp,
rintro ⟨ha, hsf⟩,
norm_num at ha,
interval_cases a,
simpa using hsf,
end


#### Kyle Miller (Jan 25 2022 at 19:04):

With a somewhat cleaned-up proof (I squeeze_simped to fix non-terminal simps, and I added braces for goals):

lemma sq_1_eq_1 : finset.card (set_squarefree_le_x 1) = 1 :=
begin
unfold set_squarefree_le_x,
rw finset.card_eq_succ,
use [1, ∅],
simp only [true_and, finset.not_mem_empty, insert_emptyc_eq, finset.card_empty, and_true,
eq_self_iff_true, not_false_iff],
ext a,
simp only [finset.mem_singleton, finset.mem_filter, finset.mem_range],
split,
{ rintro rfl,
simp, },
{ rintro ⟨ha, hsf⟩,
norm_num at ha,
interval_cases a,
simpa using hsf, },
end


#### Johan Commelin (Jan 25 2022 at 19:05):

(Aside @Kevin Wilson: on zulip you can write latex/math using double dollars: $a^2 + b^2 \in \mathbb R$ yields $a^2 + b^2 \in \mathbb R$.)

#### Johan Commelin (Jan 25 2022 at 19:07):

Alex J. Best said:

Ok dec_trivial could be helpful but maybe another good way when the definitions are a bit more complicated is to coax tactic#norm_num into unfolding the right things and evaluating them (normally this involves passing it extra function names / lemmas, like for simp, so that it rewrites the right things until it gets to a point it can actually do the calculation)

I guess norm_num doesn't know what to do with square_free as of today, right?

#### Kevin Wilson (Jan 25 2022 at 19:07):

That is correct :-)

#### Kevin Wilson (Jan 25 2022 at 19:08):

@Kyle Miller I did finish a proof, but it was quite a bit longer. I hadn't come across the ext tactic, which does make this a lot easier! I ended up with several auxiliary lemmas whose purpose was essentially to get me ext

#### Alex J. Best (Jan 25 2022 at 19:25):

Here's a slightly different version, but still annoyingly long to be honest

lemma sq_1_eq_1 : finset.card (set_squarefree_le_x 1) = 1 :=
begin
unfold set_squarefree_le_x,
have : finset.filter squarefree (finset.range (1 + 1)) = {1},
{ ext a,
norm_num,
split,
{ rintros ⟨h, hh⟩,
interval_cases a, -- reorders goals?
simpa using hh, },
{ simp {contextual := tt}, } },
rw this,
apply finset.card_singleton,
end


#### Alex J. Best (Jan 25 2022 at 23:24):

And for a bit of fun I wrote a different decidable instance for squarefree, its also trial division I suppose, I just approach the setup a bit differently

import algebra.squarefree

instance nat.decidable_is_unit : decidable_pred (@is_unit ℕ _) :=
begin
intro x,
exact decidable_of_iff _ nat.is_unit_iff.symm,
end

instance nat_sq : decidable_pred (λ x : ℕ, squarefree x) :=
begin
intro n,
by_cases hz : n = 0,
{ simp only [hz, not_squarefree_zero],
exact decidable.false, },
have : squarefree n ↔ (∀ x, x ≤ n → x * x ∣ n → is_unit x),
{ rw squarefree,
apply forall_congr,
intro x,
split; intros hx,
{ intro h,
exact hx, },
intro h,
apply hx _ h,
have hl : x * x ≤ n,
exact nat.le_of_dvd (zero_lt_iff.mpr hz) h,
have : 1 ≤ x,
{ by_contra hn,
simp only [not_le, nat.lt_one_iff] at hn,
apply hz,
simpa [hn] using h, },
have h' : x * 1 ≤ x * x,
refine mul_le_mul' (le_refl x) this,
rw [mul_one] at h',
exact h'.trans hl, },
exact decidable_of_iff _ this.symm,
end

example : squarefree 130 := dec_trivial


#### Mario Carneiro (Jan 25 2022 at 23:48):

Johan Commelin said:

I guess norm_num doesn't know what to do with square_free as of today, right?

#### Kevin Wilson (Jan 26 2022 at 02:37):

This is very cool! Thank you for the intro to all the internals as well!

#11666

#### Mario Carneiro (Jan 26 2022 at 03:18):

And here's an application to use norm_num to sum up all the squarefrees up to a bound:

import algebra.squarefree

example : ((list.range 50).map squarefree).count true = 31 :=
by norm_num [list.range, list.range_core]


I had to write it in a slightly funny way because this is just relying on simp to simplify the list stuff, there isn't any custom evaluation code for it. It also doesn't seem be be able to handle very large numbers; there are much better algorithms for calculating the sum of squarefrees up to a bound than just expanding out the list and simplifying.

#### Mario Carneiro (Jan 26 2022 at 03:20):

The actual underlying algorithm seems to be able to handle pretty large numbers so I guess it is the surrounding simp stuff that is expensive

example : squarefree 99302206 := by norm_num


#### Kevin Wilson (Mar 13 2022 at 14:09):

So I finished my goal: the "usual" proof on the asymptotics of squarefree numbers. https://github.com/khwilson/squarefree_asymptotics

It turned out to be quite long, but I'd love to record my experiences somewhere at least as a tutorial for others. And I'd love any comments on how this could have been done better. Indeed, I think my biggest conundrum was that it was hard to find good examples of "how to approach an integral problem" or "how to prove that two functions differ on a set of measure 0."

Thanks again for all the early help!

#### Yaël Dillies (Mar 13 2022 at 14:18):

Wow, that's amazing!

cc @Bhavik Mehta

#### Yaël Dillies (Mar 13 2022 at 14:19):

(we were originally a bit sorry for you that you had chosen such a hard item)

#### Kevin Wilson (Mar 13 2022 at 14:30):

Never underestimate the power of "doing things while watching Downton Abbey [or your preferred mindless television show]" :-)

#### Riccardo Brasca (Mar 13 2022 at 14:31):

Congratulations!! A good way to get feedback is to try to PR what you proved.

You can start with some preliminary lemmas (try to open several short PRs rather than a big one).

#### Sebastien Gouezel (Mar 13 2022 at 15:54):

I was having a look at the readme on your page, and I see there that you are asking if there is a good way of formalising the notion of "for sufficiently large parameters, ...". The answer is that we are already using this a lot, and this is called filters. You can grep the library for ∀ᶠ.*in at_top to see how it is used.

#### Kevin Wilson (Mar 13 2022 at 20:27):

@Riccardo Brasca great idea! Do you have a recommendation for a PR that was good in your opinion? Especially for PRs that depend on each other? (Always a problem in software!)

@Sebastien Gouezel Yeah with the filters, I spent a lot of time in the code and in the docs trying to find good examples and I couldn’t quite figure out how to put it altogether, at least in an elegant way. Hence the notes at the bottom that I couldn’t quite grok them or how to prove that two sets differ on a set of measure 0 😅

If you have a favorite example, I’d love a pointer!

Thanks again!

#### Riccardo Brasca (Mar 14 2022 at 08:26):

You can just open one or two PR with the basic material (mentioning what the final goal is), and once they are accepted you can remove the result from your repository. There is no need to PR everything at the same time, especially if this means a lot of dependent PR.

#### Kyle Miller (Mar 14 2022 at 08:41):

I briefly looked at general.lean to see if there were a lemma or two that could be a small PR, but I got sidetracked with one_le_of_ne_zero, since it seemed like it just had to be in mathlib already in some form. If you do

lemma one_le_of_ne_zero {m : ℕ} : 1 ≤ m ↔ m ≠ 0 := by library_search


it gives nat.one_le_iff_ne_zero. Similarly, the lemma two_le_prime is nat.prime.two_le. I couldn't find prime_squarefree immediately by the same tactic, but searching for "prime squarefree" in the online docs turned up docs#prime.squarefree

These seem to be new:

lemma sqrt_one_eq_one : 1 = sqrt 1 := by { rw eq_sqrt, simp, linarith, }

lemma one_le_sqrt {n : ℕ} (hn : 1 ≤ n) : 1 ≤ sqrt n :=
begin
rw sqrt_one_eq_one,
exact sqrt_le_sqrt hn,
end


#### Damiano Testa (Mar 14 2022 at 08:47):

Btw, lemma sqrt_one_eq_one is probably more mathlib-like formulated with the equality in the opposite way:

lemma sqrt_one_eq_one : sqrt 1 = 1


The guiding principle being that the RHS should be "simpler" than the LHS.

#### Damiano Testa (Mar 14 2022 at 08:52):

Also, convert nat.sqrt_eq 1 might simplify the proof, leaving only a mul_one (untested).
docs#nat.sqrt_eq

#### Yaël Dillies (Mar 14 2022 at 08:58):

I swear sqrt 1 = 1 has to be rfl (if we're talking about docs#nat.sqrt)

#### Kevin Buzzard (Mar 14 2022 at 09:08):

well you would be wrong

#### Kevin Wilson (Mar 14 2022 at 12:46):

Thank you for the comments. I'll take a stab at migrating some of those!

One thing that was confusing to me throughout was when the naming convention called for "object notation" (e.g., prime.two_le) versus [not sure what it should be called but the opposite] notation, (e.g., two_le_prime). Never quite figured out the patter!

#### Riccardo Brasca (Mar 14 2022 at 12:51):

You can look on zulip for "not dot notation", there are quite a lot of threads, but the idea is that we like it and we try to use it.

Take for example docs#polynomial.monic.pow: it says that the power of a monic polynomial is monic, so it has as an assumption hp : p.monic. The idea of dot notation is that we can use it writing hp.pow n instead of monic.pow hp n.

#### Riccardo Brasca (Mar 14 2022 at 12:52):

But at beginning don't worry too much about this, it will be part of the review process

"not notation"

dot notation :-)

#### Kevin Wilson (Mar 14 2022 at 12:56):

Made @Kyle Miller 's changes (love small change requests that reduce code!) https://github.com/khwilson/squarefree_asymptotics/pull/1

#### Kevin Wilson (Mar 14 2022 at 13:02):

Also, I think I found prime.squarfree but everything fails to unify if you use that. I think because N isn't a monoid according to Lean? (I hit this sort of thing several times.)

#### Kevin Wilson (Mar 14 2022 at 13:02):

lemma prime_squarfree {p : ℕ} (hp : nat.prime p) : squarefree p :=
begin
exact prime.squarefree hp,
end


#### Kevin Buzzard (Mar 14 2022 at 13:03):

Surely N is a monoid?

#### Kevin Wilson (Mar 14 2022 at 13:03):

type mismatch at application
prime.squarefree hp
term
hp
has type
prime p
but is expected to have type
@prime ℕ (@cancel_comm_monoid_with_zero.to_comm_monoid_with_zero ℕ nat.cancel_comm_monoid_with_zero) p
state:
p : ℕ,
hp : prime p
⊢ squarefree p


#### Kevin Buzzard (Mar 14 2022 at 13:03):

The issue there I suspect is that there is more than one notion of prime in play.

#### Alex J. Best (Mar 14 2022 at 13:04):

We have a bit of description of how nice dot notation can be at the end of the section https://leanprover-community.github.io/tips_and_tricks.html#avoiding-many-nested-parentheses-with- of the tips and tricks page

#### Kevin Wilson (Mar 14 2022 at 13:05):

Also, I definitely agree the dot notation is nice! I just couldn't quite grok when to use dot notation instead of the _of_ notation (and especially when to search with the dot notation instead of the _of_ notation :-) )

#### Riccardo Brasca (Mar 14 2022 at 13:05):

Yes, docs#nat.prime is not the same as docs#prime

#### Riccardo Brasca (Mar 14 2022 at 13:05):

But we surely know somewhere that they are equivalent

#### Kevin Buzzard (Mar 14 2022 at 13:05):

Can you post fully working code? I can't reproduce your error.

import data.nat.prime
import algebra.squarefree

lemma prime_squarfree {p : ℕ} (hp : nat.prime p) : squarefree p :=
begin
exact prime.squarefree hp,
end


gives the problem I'm flagging -- nat.prime isn't the same as prime (but my error is much more sensible than yours)

#### Kevin Wilson (Mar 14 2022 at 13:06):

And @Kevin Buzzard yes, you're correct. Reading that error it definitely seems that N is a monoid! But perhaps there's some Lean magic to get it to work

#### Riccardo Brasca (Mar 14 2022 at 13:06):

docs#nat.prime_iff

#### Kevin Wilson (Mar 14 2022 at 13:07):

import algebra.squarefree

noncomputable theory
open nat
open_locale classical

lemma prime_squarfree {p : ℕ} (hp : nat.prime p) : squarefree p :=
begin
exact prime.squarefree hp,
end


#### Kevin Wilson (Mar 14 2022 at 13:07):

@Kevin Buzzard ^^^

#### Kevin Buzzard (Mar 14 2022 at 13:07):

Oh you have open nat, yeah that makes the same error look a lot more exotic :-)

#### Kevin Wilson (Mar 14 2022 at 13:08):

Hah still not exactly sure what counts as "minimum" and how to debug :-)

#### Kevin Buzzard (Mar 14 2022 at 13:08):

lemma prime_squarfree {p : ℕ} (hp : nat.prime p) : squarefree p :=
begin
rw nat.prime_iff at hp,
exact prime.squarefree hp,
end


as Riccardo said. There are two primes here, and with open nat they're both called prime.

#### Kevin Wilson (Mar 14 2022 at 13:09):

Ah well that would explain that. I'm guessing nat.prime has special features that prime doesn't have?

#### Kevin Buzzard (Mar 14 2022 at 13:09):

By the way I would recommend you avoid open_locale classical, it was a "hammer" approach to decidability problems popular a few years ago; we now have far more precise tools to deal with these issues.

#### Kevin Buzzard (Mar 14 2022 at 13:09):

nat.prime and prime are simply two different things.

#### Kevin Wilson (Mar 14 2022 at 13:10):

Oh I just meant that why don't you just define nat.prime via nat.prime_iff ?

#### Kevin Buzzard (Mar 14 2022 at 13:10):

nat.prime is about naturals, prime is a far more general algebraic concept which works for commutative rings and has a different definition. This is why you need nat.prime_iff to glue the two concepts together.

#### Kevin Buzzard (Mar 14 2022 at 13:11):

It's not for me to say why definitions are as they are. Perhaps historical? nat.prime was defined by the computer scientists before we mathematicians came along telling them that there was a far more general concept of primality?

#### Kevin Wilson (Mar 14 2022 at 13:11):

Hah! "Path dependence" is almost always the answer

#### Kevin Buzzard (Mar 14 2022 at 13:11):

Yeah, it might also be that :-)

#### Eric Rodriguez (Mar 14 2022 at 13:12):

yeah, that's what happened

#### Riccardo Brasca (Mar 14 2022 at 13:12):

We changed the definition recently, didn't we? Using irreducible.

#### Riccardo Brasca (Mar 14 2022 at 13:12):

But I may be wrong

#### Kevin Buzzard (Mar 14 2022 at 13:12):

Indeed it seems that nat.prime was refactored 3 months ago in #11031

#### Ruben Van de Velde (Mar 14 2022 at 13:13):

Yeah, but it takes > 500 lines to prove that irreducible implies prime for nat

...by Ruben :-)

#### Ruben Van de Velde (Mar 14 2022 at 13:13):

We could probably turn it around, but that was more work than I wanted to take on at that point

#### Eric Rodriguez (Mar 14 2022 at 13:13):

https://github.com/leanprover-community/mathlib/blob/81a31ca4a8c0287bf0b0ce40f1a0df16543b7abe/src/data/nat/prime.lean this is the old version, which also isn't prime

#### Eric Rodriguez (Mar 14 2022 at 13:14):

there's like a zillion things in the library that are specialised for nat just so we can get the rest of the theory going, which is annoying but I guess how it has to be

#### Kevin Wilson (Mar 14 2022 at 13:17):

Gotta start somewhere :-)

#### Kevin Wilson (Mar 14 2022 at 13:20):

It would be "neat" (and very probably terrible) if there was some sort of shim overtop "CS nat" that obviated this for folks like me, but I guess if mathlib is C in this analogy, this would be asking for Python [or your even higher level language of choice]

#### Kevin Wilson (Mar 14 2022 at 13:39):

Anyway, @Kevin Buzzard removed the open_locale classical's. They showed up early due to an auxiliary function.

#### Kevin Wilson (Mar 14 2022 at 13:39):

https://github.com/khwilson/squarefree_asymptotics/pull/2

#### Kevin Wilson (Mar 14 2022 at 13:42):

Before disappearing to the day job, the contributing notice for mathlib notes that I'm supposed to "ask for write access to non-master branches of the mathlib repository." Where do I ask this question? (If it is here, I'm khwilson on github. :-) )

#### Riccardo Brasca (Mar 14 2022 at 13:48):

Let me see if I am able to do it with my phone

#### Riccardo Brasca (Mar 14 2022 at 13:51):

You should have an invitation

#### Kevin Buzzard (Mar 14 2022 at 13:53):

Kevin Wilson said:

Anyway, Kevin Buzzard removed the open_locale classical's. They showed up early due to an auxiliary function.

If you need classical assumptions (e.g. decidability) in the statement of a theorem or definition, put them in explicltly; if you just need them in a proof, use the classical tactic beforehand. That's the (simplified version of the) modern mantra.

#### Kevin Wilson (Mar 14 2022 at 13:55):

Makes a lot of sense. As you can see from the start of this thread, decidability was a lot to grok early on! ("Why is this red squiggly appearing just because I wrote ite ?!?! )

#### Ruben Van de Velde (Mar 14 2022 at 14:25):

It seems like redefining nat.prime := prime might be workable after all - I'll see if I have time to work it out thus week

#### Mauricio Collares (Mar 14 2022 at 14:37):

I'd argue that nat.prime and prime are different definitions in mathematics too, as reflected in almost any number theory book (e.g., Apostol). That is, if you say "the definition of nat.prime is is really the definition for irreducible in a more general context", I think this will ring a bell for most mathematicians.

#### Riccardo Brasca (Mar 14 2022 at 14:48):

It's unfortunate that what we call a prime number in primary school is actually an irreducible element in N. But that's life I guess

#### Eric Rodriguez (Mar 14 2022 at 14:52):

Mauricio Collares said:

I'd argue that nat.prime and prime are different definitions in mathematics too, as reflected in almost any number theory book (e.g., Apostol). That is, if you say "the definition of nat.prime is is really the definition for irreducible in a more general context", I think this will ring a bell for most mathematicians.

sure, but they're equivalent, and considering we have prime.irreducible things work out pretty nicely in the general case

#### Mario Carneiro (Mar 14 2022 at 19:29):

@Kevin Buzzard said:

nat.prime is about naturals, prime is a far more general algebraic concept which works for commutative rings and has a different definition. This is why you need nat.prime_iff to glue the two concepts together.

It's not for me to say why definitions are as they are. Perhaps historical? nat.prime was defined by the computer scientists before we mathematicians came along telling them that there was a far more general concept of primality?

I very much doubt "computer science" motivations are at play here. Most likely this is something like Jeremy Avigad wanting simple proofs about primality like exists_infinite_primes to actually be comprehensible as an introductory example to first-year students. This tends not to last long before being refactored away in current mathlib, though.

#### Kevin Wilson (Mar 16 2022 at 04:54):

OK, I have started migrating various lemmas over to mathlib with some success (two PRs in!). But in the process I figured I'd try to generalize and simplify various things. Then I hit a weird issue I'm not sure how to debug. Specifically, I need the following lemma:

import order.filter
import topology.basic
import data.real.basic
import topology.instances.real
import order

noncomputable theory
open filter
open_locale topological_space

lemma real_tendsto_implies_nat_tendsto
{a : ℝ} {f : ℝ → ℝ}
(hf : filter.tendsto f at_top (𝓝 a)) :
filter.tendsto (λ (n : ℕ), f ↑n) filter.at_top (𝓝 a) :=
begin
rw filter.tendsto_at_top',
intros s hs,
rw filter.tendsto_at_top' at hf,
specialize hf s hs,
cases hf with a ha,
use ⌈a⌉₊,
intros b,
specialize ha ↑b,
intros hb,
have : ⌈a⌉₊ ≤ b, exact hb,
have : a ≤ ↑b,
calc a ≤ ↑⌈a⌉₊ : nat.le_ceil a
... ≤ ↑b : nat.cast_le.mpr this,
exact ha this,
end


Of course, this should be true for basically anything where all the elements are defined, so I attempted to do the following:

import order.filter
import topology.basic
import data.real.basic
import topology.instances.real
import order

noncomputable theory
open filter
open_locale topological_space

lemma real_tendsto_implies_nat_tendsto'
{α β : Type*}
[nonempty α] [semilattice_sup α] [linear_ordered_semiring α]
[topological_space β] [preorder β] [order_closed_topology β]
{a : β} {f : α → β} (hf : tendsto f at_top (𝓝 a)) :
tendsto (λ (n : ℕ), f ↑n) filter.at_top (𝓝 a) :=
begin
rw filter.tendsto_at_top',
intros s hs,
-- Fails
rw filter.tendsto_at_top' at hf,
sorry,
end


This seemed odd, so I did some experimentation and it seems to be failing with a bit of a strange (to me!) error:

import order.filter
import topology.basic
import data.real.basic
import topology.instances.real
import order

noncomputable theory
open filter
open_locale topological_space

lemma real_tendsto_implies_nat_tendsto''
{α β : Type*}
[aa : nonempty α] [bb : semilattice_sup α] [linear_ordered_semiring α]
[topological_space β] [preorder β] [order_closed_topology β]
{a : β} {f : α → β} (hf : tendsto f at_top (𝓝 a)) :
tendsto (λ (n : ℕ), f ↑n) filter.at_top (𝓝 a) :=
begin
rw filter.tendsto_at_top',
intros s hs,
-- Fails with detailed error
-- type mismatch at application
--   tendsto_at_top'.mp hf
-- term
--   hf
-- has type
--   @tendsto α β f
--     (@at_top α
--       (@partial_order.to_preorder α
--                 (@linear_ordered_semiring.to_ordered_semiring α _inst_1)))))
--     (𝓝 a)
-- but is expected to have type
--   @tendsto α β f (@at_top α (@partial_order.to_preorder α (@semilattice_sup.to_partial_order α bb))) (𝓝 a)
let foo := (@filter.tendsto_at_top' α β aa bb f (𝓝 a)).mp hf,
sorry,
end


Which I interpret as an issue that the preorder can arise either from the explicit semilattice_sup or the implicit linear_ordercoming from a linear_ordered_ring. This works fine for α = ℝ because ℝ's semilattice_sup structure explicitly comes from its linear_order structure https://leanprover-community.github.io/mathlib_docs/data/real/basic.html#real.semilattice_sup

So my question is: what's the right way to specify, "I mean things where the semilattice_sup structure comes from the linear_order structure?"

Thanks again!

#### Heather Macbeth (Mar 16 2022 at 05:41):

@Kevin Wilson To jump immediately to your original motivation:

#### Heather Macbeth (Mar 16 2022 at 05:48):

And to answer the question you asked: linear_order implies semilattice_sup, so you can assume just the former and the latter will be silently inferred where needed.

example {α : Type*} [linear_order α] : semilattice_sup α := by apply_instance


#### Kevin Wilson (Mar 16 2022 at 13:52):

example is the keyword! Very cool :-)

As for the spoiler proof, that's amazing. Half the battle is searching for the right lemma :-)

Though, notably, the lemma I wrote supposes a linear_ordered_semiring, whereas archimedean (an assumption of tendsto_coe_nat_at_top_at_top) implies floor_ring(https://leanprover-community.github.io/mathlib_docs/algebra/order/archimedean.html#archimedean.floor_ring).

#### Heather Macbeth (Mar 16 2022 at 16:35):

@Kevin Wilson I think it's the other way, right? floor_ring implies archimedean. And the lemma tendsto_coe_nat_at_top_at_top is stated for archimedean, the weaker one, so it applies for (eg) the nonnegative reals, too.

import data.real.nnreal
import order.filter.archimedean

open_locale nnreal
open filter

example : tendsto (λ n : ℕ, (n:ℝ≥0)) at_top at_top := tendsto_coe_nat_at_top_at_top


#### Yaël Dillies (Mar 16 2022 at 16:42):

No, Heather. archimedean also noncomputably imply floor_ring.

#### Kevin Buzzard (Mar 16 2022 at 16:52):

I suspect that you can make $\mathbb{R}[X]$ into a linear ordered ring by demanding that $0<|X|$ but that $|X|<\epsilon$ for all positive $\epsilon$, and then following your nose (I didn't check this but I think I've checked it in the past). This might well be a floor_ring which is not archimedean -- something for the counterexamples folder? (there might be simpler examples)

#### Kevin Buzzard (Mar 16 2022 at 16:55):

Ridiculously, the reason I was thinking about this a few years ago was working with @Calle Sönne on decimal expansions! He started off wanting to define them for the reals, but I pointed out that it should work for the rationals, and then we started wondering exactly which rings decimal expansions should work for, and we thought that floor_rings were an excellent choice! And then realised that perhaps the decimal expansion of a number might not sum back up to the number again because of examples like this :-)

#### Adam Topaz (Mar 16 2022 at 16:59):

Kevin Buzzard said:

I suspect that you can make $\mathbb{R}[X]$ into a linear ordered ring by demanding that $0<|X|$ but that $|X|<\epsilon$ for all positive $\epsilon$, and then following your nose (I didn't check this but I think I've checked it in the past). This might well be a floor_ring which is not archimedean -- something for the counterexamples folder? (there might be simpler examples)

This would be a fun counterexample to try to construct using what we have in mathlib for model theory! Take an ultrapower of $\mathbb{R}$ w.r.t. a nonprincipal ultrafilter on $\mathbb{N}$, and let $\epsilon = (1/n)_n$ be an infinitesimal element in this ultrapower. Now prove that $\epsilon$ is transcendental over $\mathbb{R}$, etc.

#### Reid Barton (Mar 16 2022 at 20:10):

Wait I'm confused now--I think there are multiple notions of archimedean here (I mean besides the p-adic related one).

docs#archimedean

#### Reid Barton (Mar 16 2022 at 20:10):

I would argue this isn't the definition that most people would guess

#### Reid Barton (Mar 16 2022 at 20:10):

but it doesn't matter for fields

#### Kevin Wilson (Mar 16 2022 at 20:52):

To @Kevin Buzzard , I think that is correct. All sorts of weird orderings on polynomial rings that Groebner bases make use of! See theorem 2.5 here and then take the floor to be the floor of the constant coefficient.

#### Kevin Wilson (Mar 16 2022 at 23:25):

Speaking of, @Heather Macbeth everything in the file with tendsto_coe_nat_at_top_at_top seems to be implied by the lemma exists_nat_ge. Now this lemma is _also_ true in a floor_semiring (just take the ceil of an element and use the Galois connection).

I don't actually use this lemma at this level of generality, but I'm happy while I'm here to swap out the lemmas in the file to use this (slightly) more general lemma. However, as @Yaël Dillies pointed out, archimedean rings are only _noncomputably_ floor_rings. I honestly do not know the implications of this for the library, so I'm also happy _not_ to do this and just use Heather's trick for my purposes!

#### Junyan Xu (Mar 16 2022 at 23:48):

Kevin Buzzard said:

I suspect that you can make $\mathbb{R}[X]$ into a linear ordered ring by demanding that $0<|X|$ but that $|X|<\epsilon$ for all positive $\epsilon$, and then following your nose

This is just the lexicographic order on R^(order_dual N) (restricted to finsupp), right?

#### Kevin Wilson (Mar 26 2022 at 20:32):

Hi again! I've now gotten several PRs merged, including the fact that sqrt 1 = 1 and Moebius function is multiplicative! Always amazing to be a first time contributor to a project :-)

A quick question as I continue slowly merging in these 3kloc: I still have a lot of lemmas that I couldn't find a good representation of in mathlib but which are very useful for analytic number theory. For instance, these two:

theorem integral_tendsto_of_has_deriv_at {a b : ℝ} {f f' : ℝ → ℝ}
(hderiv : ∀ x ∈ Ici a, has_deriv_at f (f' x) x)
(hvanish : tendsto f at_top (𝓝 b))
(hint : ∀ (b : ℝ), b ∈ Ici a → interval_integrable f' volume a b) :
tendsto (λ (b : ℝ), ∫ y in a..b, f' y) at_top (𝓝 (b - f a)) := ...


and its consequence:

lemma integral_rpow_tendsto_at_top (a r : ℝ) (ha : 0 < a) (hr : r < -1):
tendsto (λ (y : ℝ), ∫ (x : ℝ) in a..y, x ^ r) at_top (𝓝 (-a ^ (r + 1) / (r + 1))) := ...


My general question: What is the etiquette for figuring out _where_ a lemma should go? E.g., should I just continue posting on this now very long thread, or should I post in something like "Is there code for X?"

And a follow up: If this is the appropriate forum, where's the best place to put those above lemmas? :-)

Thanks again!

#### Yaël Dillies (Mar 26 2022 at 20:33):

A great way to figure this out is to look up the lemmas you used in the proof and see whether you can stick yours in their file.

#### Kevin Wilson (Mar 26 2022 at 20:38):

Thanks! That's been my strategy so far, but this one had me a little stumped b/c OTOH, it's basically identical to a lemma in the docs#interval_integral and OTOH, there's an entire file docs#measure_theory.ae_cover which is sort of meant to handle these things.

Is it better to "take a guess" and post a PR and discuss there, or would you all prefer a discussion on Zulip?

:-)

#### Kevin Wilson (Mar 26 2022 at 20:41):

(Also, sorry about the docs links, was trying to figure out how exactly they worked!)

In the spirit of asking, do y'all have a preference before I make a PR for those two lemmas?

#### Yaël Dillies (Mar 26 2022 at 20:46):

Personally, no. The measure theory library is quite alien to me! Yury G. Kudryashov will have opinions, however.

#### Kevin Wilson (Mar 26 2022 at 20:52):

Excellent. I'll wait for a ruling before barging ahead on those!

Last updated: Dec 20 2023 at 11:08 UTC