Easiest way to do casework on factors of nat

Stream: general

[Praneeth Kolichala]

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]

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

[Mario Carneiro]

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

[Bhavik Mehta]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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]

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]

you still have to sort the factors at the end though

[Bhavik Mehta]

true

[Bhavik Mehta]

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]

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

[Bhavik Mehta]

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

[Mario Carneiro]

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

[Bhavik Mehta]

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]

(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]

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

[Bhavik Mehta]

I think so too

[Bhavik Mehta]

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]

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]

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]

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]

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]

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

Do we have the lemma that says this?

[Eric Wieser]

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]

that looks like the conv mode tactic

[Mario Carneiro]

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

[Eric Wieser]

the earlier lemmas are certainly gaps in mathlib

I PR'ddivisors_mul and a helper lemma in #17041