## Stream: general

### Topic: Easiest way to do casework on factors of nat

#### Praneeth Kolichala (Oct 11 2022 at 00:14):

What is the easiest way to go prove something like

example (n : ℕ) : n ∣ 100 ↔ n = 1 ∨ n = 2 ∨ n = 4 ∨ n = 5 ∨ n = 10 ∨ n = 20 ∨ n = 25 ∨ n = 50 ∨ n = 100 := sorry


(really only the forward direction is important; backwards should be trivial by cases and norm_num or something).

The motivation is that I was thinking about how I would formalize the solutions to certain competition problems, and this kind of casework occurs somewhat frequently in number theory problems.

#### Mario Carneiro (Oct 11 2022 at 00:33):

Isn't there a function that returns the set of factors of an integer?

#### Mario Carneiro (Oct 11 2022 at 00:43):

There is, but there is no norm_num extension for it like I thought.

#### Bhavik Mehta (Oct 11 2022 at 00:51):

There's docs#nat.factors, which does have a norm_num extension, while needs docs#nat.divisors which doesn't

#### Mario Carneiro (Oct 11 2022 at 00:54):

import number_theory.divisors

example (n : ℕ) : n ∣ 100 ↔ n = 1 ∨ n = 2 ∨ n = 4 ∨ n = 5 ∨ n = 10 ∨ n = 20 ∨ n = 25 ∨ n = 50 ∨ n = 100 :=
begin
have : nat.divisors 100 = ⟨quot.mk _ [1, 2, 4, 5, 10, 20, 25, 50, 100], _⟩ := rfl,
rw [← nat.mem_divisors.trans (and_iff_left (by norm_num : 100 ≠ 0)), this],
change n ∈ (_:list _) ↔ _,
simp,
end


a proper norm_num extension would make this a lot faster

#### Bhavik Mehta (Oct 11 2022 at 01:06):

Here's a slightly silly but faster proof

import number_theory.divisors
import data.finset.pointwise

open nat

section

open_locale pointwise

lemma divisors_mul {m n : ℕ}  :
(m * n).divisors = m.divisors * n.divisors :=
begin
rcases m.eq_zero_or_pos with rfl | hm,
{ simp },
rcases n.eq_zero_or_pos with rfl | hn,
{ simp },
ext i,
simp only [hm.ne', hn.ne', finset.mem_mul, mem_divisors, ne.def, nat.mul_eq_zero, or_self,
not_false_iff, and_true, exists_and_distrib_left],
split,
{ intro h',
obtain ⟨⟨⟨i₁, hi₁⟩, i₂, hi₂⟩, rfl⟩ := prod_dvd_and_dvd_of_dvd_prod h',
exact ⟨i₁, hi₁, i₂, hi₂, rfl⟩ },
rintro ⟨y, hy, x, hx, rfl⟩,
exact mul_dvd_mul hy hx,
end

open finset

lemma insert_mul {α : Type*} [decidable_eq α] [has_mul α] {x : α} {s t : finset α} :
insert x s * t = x • t ∪ s * t :=
begin
rw [finset.mul_def, insert_eq, union_product, image_union, ←finset.mul_def, ←finset.mul_def,
singleton_mul, smul_finset_def],
refl
end

lemma smul_finset_insert {α : Type*} [decidable_eq α] [has_mul α] {x y : α} {s : finset α} :
x • insert y s = insert (x * y) (x • s) :=
by rw [insert_eq, smul_finset_union, smul_finset_singleton, insert_eq, smul_eq_mul]

end

example (n : ℕ) :
n ∣ 100 ↔ n = 1 ∨ n = 2 ∨ n = 4 ∨ n = 5 ∨ n = 10 ∨ n = 20 ∨ n = 25 ∨ n = 50 ∨ n = 100 :=
begin
have h₁ : n ∣ 100 ↔ n ∈ divisors (2 ^ 2 * 5 ^ 2), { norm_num },
rw [h₁, divisors_mul, nat.divisors_prime_pow prime_two,
divisors_prime_pow (show nat.prime 5, by norm_num)],
norm_num [finset.range_succ, insert_mul, smul_finset_insert, finset.singleton_mul],
rw ←eq_iff_iff,
ac_refl
end


the earlier lemmas are certainly gaps in mathlib - the idea is to show divisors of 100 are products of divisors of 4 and 25, which we have explicit expressions for, then norm_num and set calculations to finish

#### Bhavik Mehta (Oct 11 2022 at 01:10):

I think - by the way - that this approach would be better for norm_num than trying to check divisibility of every number from 1..n, in particular using the existing extension for nat.factors, then my new divisors_mul. And maybe using lists instead of finsets?

#### Mario Carneiro (Oct 11 2022 at 01:27):

My thinking for the norm_num extension was to exhaustively list all divisors up to sqrt n and mirror them to get the rest (in order, to boot). This is the same cost as nat.factors since it also does divisibility tests up to sqrt n

#### Bhavik Mehta (Oct 11 2022 at 01:31):

I thought nat.factors doesn't do divisibility tests up to sqrt n, because once you get the smallest factor you divide by it, so less needs to be checked

#### Bhavik Mehta (Oct 11 2022 at 01:32):

For instance for nat.factors 1024, we never check if 30 divides 1024, even though 30 < sqrt 1024 (I think, I might be misunderstanding?)

#### Mario Carneiro (Oct 11 2022 at 03:12):

Oh, no you are right. That's only if you get lucky though, if the number is prime then you really do have to go all the way up to sqrt n

#### Bhavik Mehta (Oct 11 2022 at 19:06):

Agreed. That said, the average number of prime factors of n is log log n, while the average number of divisors is log n, so I think overall (amortized) this saves a log factor? Though it's probably likely there are other factors involved here (no pun intended) and the only real way to compare is benchmarking

#### Mario Carneiro (Oct 11 2022 at 19:12):

you still have to sort the factors at the end though

true

#### Bhavik Mehta (Oct 11 2022 at 19:13):

might be able to get away with a clever merge sort though, because each of the lists you get along the way will come sorted - eg above it was {1,2,4} * {1,5,25}

#### Mario Carneiro (Oct 11 2022 at 19:14):

sure, I mean any sort is a bunch of merge sorts

#### Bhavik Mehta (Oct 11 2022 at 19:15):

true but here we can prove that the inputs {1,2,4} and {1,5,25} are sorted by construction

#### Mario Carneiro (Oct 11 2022 at 19:15):

but we are essentially linearizing a high-dimensional cube here, so there are still linearly many ordering relations to work out

#### Bhavik Mehta (Oct 11 2022 at 19:16):

my hope was that this would be less costly than proving the other things between 1 and sqrt n aren't factors, especially because the cube is in log log n dimensions (on average)

#### Mario Carneiro (Oct 11 2022 at 19:17):

(by linearly many I mean in the number of points in the cube which is log n, the size of the output here)

#### Mario Carneiro (Oct 11 2022 at 19:19):

I think it is likely to be more asymptotically efficient, but also a lot more complicated than just iterating which will result in code similar to the nat.factors implementation

I think so too

#### Bhavik Mehta (Oct 12 2022 at 17:17):

I realised there might be a nicer way to do this - we can compute the list of divisors using the VM, and it's enough to just produce a proof that the list is correct, and for that it suffices to proof we have a sublist of the correct list (ie everything we have is a divisor) and we have the right number of things. The first we can even do in pairs, and one multiplication will deal with two elements of the list; and the number of divisors can already be computed from nat.factors

#### Mario Carneiro (Oct 12 2022 at 17:21):

I'm assuming you are still looking for a computationally efficient way to find all the divisors, rather than one that is less work to implement?

#### Mario Carneiro (Oct 12 2022 at 17:23):

I agree that it is more or less a required bit of work to multiply the divisors in the list in pairs to get the target number. But what of all the other numbers that we haven't multiplied? You still need to eliminate the possibility of a large prime factor of the target number

#### Bhavik Mehta (Oct 12 2022 at 18:14):

Mario Carneiro said:

I'm assuming you are still looking for a computationally efficient way to find all the divisors, rather than one that is less work to implement?

I'm not too sure to be honest - but I suspect this idea isn't too much more work to implement than yours, while also being a lot more efficient?

#### Bhavik Mehta (Oct 12 2022 at 18:16):

Mario Carneiro said:

I agree that it is more or less a required bit of work to multiply the divisors in the list in pairs to get the target number. But what of all the other numbers that we haven't multiplied? You still need to eliminate the possibility of a large prime factor of the target number

I think this is eliminated if we have a proof of the number of divisors (because the given list is a sublist of the list of divisors, and it has the same length, therefore they're equal). And we can calculate the number of divisors relatively easily by using the existing nat.factors extension

#### Eric Wieser (Oct 17 2022 at 05:34):

and the number of divisors can already be computed from nat.factors

Do we have the lemma that says this?

#### Eric Wieser (Oct 17 2022 at 05:36):

Relatedly, should we have a norm_num_rhs tactic so that we can write the following?

have : nat.divisors 100 = _ := by norm_num_rhs


#### Mario Carneiro (Oct 17 2022 at 05:37):

that looks like the conv mode tactic

#### Mario Carneiro (Oct 17 2022 at 05:39):

example : true :=
begin
have : nat.factors 100 = _ := by conv {norm_num},
-- this: 100.factors = [2, 2, 5, 5]
end


#### Eric Wieser (Oct 18 2022 at 09:14):

the earlier lemmas are certainly gaps in mathlib

I PR'ddivisors_mul and a helper lemma in #17041

Last updated: Aug 03 2023 at 10:10 UTC