Integer divisors

Stream: new members

[Will Midwood]

Hi all,

I'm want to be able to construct a set of all integers that divide another integer 'x'. I understand there is something similar in mathlib with the nats, so I tried a similar implementation:

definition int_divisors (n : ℤ): finset ℤ := finset.filter (λ x : ℤ, x ∣ n) (finset.Ico -n.nat_abs (n+1).nat_abs)

This gives me an error, so I imagine that I am doing it incorrectly. Is this the right line of thinking or is there a more reasonable way to construct this set. Thank you!

[Alex J. Best]

something like what you have works, with a few changes, first you need the right imports to know that integers have finite intervals, then I use Icc (the closed interval) and bracket everything properly and lean is happy:

import data.int.interval

definition int_divisors (n : ℤ): finset ℤ := finset.filter (λ x : ℤ, x ∣ n) (finset.Icc (-n) n)

[Alex J. Best]

You can even check the implementation does what you think with

import data.int.interval

definition int_divisors (n : ℤ): finset ℤ := finset.filter (λ x : ℤ, x ∣ n) (finset.Icc (-n) n)
#eval int_divisors 6

[Kevin Buzzard]

This doesn't give the right answer for 0

[Alex J. Best]

What is "the right answer"?

[Alex J. Best]

Its a junk value right? Maybe the empty set is a better junk value? But that depends on what theorems you want I suppose

[Kevin Buzzard]

There's certainly a set of integers that divide 0. In the natural language description of the question there was no finiteness assumed but in the lean code there was; I was just pointing out the discrepancy

[Alex J. Best]

Ah I see, for sets there is a right answer indeed :wink:

[Alex J. Best]

I thought you were complaining that this has a different convention to the nat version (which sets divisors of zero to be empty)

[Kevin Buzzard]

Naah I was just being a pedant

[Mario Carneiro]

Kevin Buzzard said:

There's certainly a set of integers that divide 0.

Obviously these would be the zero-divisors.

[Junyan Xu]

There's also docs#polynomial.roots

[Kevin Buzzard]

Sure. The issue is whether one definitely wants to return a finite set in all cases (in which case you have to return a junk value for 0) or whether you are happy to return a set in all cases and perhaps later on a proof that it's finite if n!=0.

[Will Midwood]

Thanks everyone for the help! It's much appreciated!
Follow up question: How could I prove that the divisors of a set are equal to a given set? E.G:
⊢ int_divisors ↑5 = {-1, -↑5, 1, ↑5}
Thanks again!

[Kevin Buzzard]

What's with the up-arrows? And what definition are you using?

[Will Midwood]

Erm im not sure what the up arrows are, lean just adds them in for me. I believe its casting the 5 from nat to integer? But I'm unsure.
The definition I've used is:

definition int_divisors (n : ℤ): finset ℤ := finset.filter (λ x : ℤ, x ∣ n) (finset.Icc (-n) n)

[Kevin Buzzard]

yeah, Lean 3 wasn't really designed to do calculations; it's better at proving theorems.

[Kevin Buzzard]

Lean 4 will be better in this regard.

[Eric Wieser]

@Bhavik Mehta had an outline of how to write a norm_num extension to do this in another thread.

[Eric Wieser]

But in this case, I think probably refl might be able to prove this as 5 is pretty small

[Will Midwood]

I was hoping I could use this definition to define prime numbers. I.E p is prime if p > 1 and int_divisors p = {-1, -p, 1, p}

[Eric Wieser]

Or rw int_divisors, dec_trivial

[Kevin Buzzard]

This works:

import data.int.interval
import tactic

definition int_divisors (n : ℤ): finset ℤ := finset.filter (λ x : ℤ, x ∣ n) (finset.Icc (-n) n)

example : int_divisors 5 = {1,5,-1,-5} :=
begin
  unfold int_divisors,
  ext a,
  split,
  { simp only [finset.mem_filter, finset.mem_Icc, finset.mem_insert, finset.mem_singleton, and_imp],
    rintro h1 h2 h3,
    interval_cases a; -- now check all 11 cases
    try {cc};
    try {norm_num at h3}, },
  { simp only [finset.mem_insert, finset.mem_singleton, finset.mem_filter, finset.mem_Icc],
    rintro (rfl | rfl | rfl | rfl);
    norm_num, },
end

Sure you could use this to define prime numbers. But defining prime numbers and computing examples of prime numbers are two different things; Lean 3 is good at the first and not so good at the second.

[Kevin Buzzard]

Eric Wieser said:

Or rw int_divisors, dec_trivial

this works and is much quicker than my approach.

[Eric Wieser]

I would imagine it's much easier to define this in terms of nat.divisors

[Eric Wieser]

Since then you don't have to reprove everything from scratch

[Will Midwood]

I'm attempting to formalise my universities number theory course, and that's how we defined prime numbers.

[Matt Diamond]

@Will Midwood As Kevin said, "Lean 3 wasn't really designed to do calculations; it's better at proving theorems." One thing you could try to do is prove a theorem that states that your definition of prime numbers is equivalent to mathlib's definition of prime numbers. That might be a useful exercise.

[Matt Diamond]

something like this:

import data.nat.prime
import data.int.interval

def int_divisors (n : ℤ): finset ℤ := finset.filter (λ x : ℤ, x ∣ n) (finset.Icc (-n) n)

example (n : ℕ) : nat.prime n ↔ n > 1 ∧ int_divisors n = {-1, n, 1, n} := sorry

[Eric Wieser]

I think one of those ns should be -n

[Matt Diamond]

oh duh, whoops! fixed it

[Will Midwood]

Hey all, thanks for the feedback, I'm attempting the example you suggested @Matt Diamond , but I've run into a road block. This might be my inexperience with lean but essentially I now need to prove Euclid's Lemma:

p: ℕ
hp: 1 < p
hdp: int_divisors ↑p = {-1, -↑p, 1, ↑p}
ab: ℕ
hpp: prime_int p
⊢ p ∣ a * b → p ∣ a ∨ p ∣ b

with my definition of prime_int:

definition int_divisors (n : ℤ): set ℤ := {x : ℤ | x ∣ n}

definition prime_int (p : ℕ): Prop := (1 < p)∧(int_divisors p = {-1, -p, 1, p})

I'm not sure how I can work the with this definition here, so I would appreciate some help please :). I fear the answer may lie in my definition, but I'm hopeful that there's a way around it.

[Kevin Buzzard]

If you're making your own definition of prime then it's your problem to prove all the standard theorems about primes. If you look at the core Lean 3 / mathlib definitions you'll see that this is a non-trivial amount of work. Fortunately you can borrow some of it. Assume $p$ divides $ab$ and assume it doesn't divide $a$; you need to prove it divides $b$. You can do this by first showing that the gcd of $p$ and $a$ must be 1, then using Bezout's lemma to write 1 as a linear combination of $p$ and $a$, then multiply both sides by $b$. This is the standard proof in the books and if you're making your own primes then this is the kind of thing you have to formalise yourself.

An alternative approach would be to prove that your definition of prime coincides with Lean's definition of prime and then you have access to Lean's API for primes where this theorem will already be there.

[Matt Diamond]

An alternative approach would be to prove that your definition of prime coincides with Lean's definition of prime

I think that's what Will is currently trying to do

[Matt Diamond]

@Will Midwood Could you post the current state of your proof, including imports? That would make it easier for people to help.

[Will Midwood]

Good idea @Kevin Buzzard , how can I make the assumption that p doesn't divide a?

[Kevin Buzzard]

Assuming your goal is P \or Q then you can do a case split on whether P is true or not with cases hP : P, then you'll have two goals. You can resolve the first one with left, exact hP and then you can do right in the "not P" goal and you should be left in the situation we discussed earlier.

[Will Midwood]

This is my current proof @Matt Diamond :

definition prime_iff_prime_int (p : ℕ) : prime_int p ↔ nat.prime p :=
begin
  split,
  intro hp,
  rw nat.prime_iff,
  unfold prime,
  split,
  apply ne_zero_of_lt,
  rw prime_int at hp,
  exact hp.left,
  split,
  rw nat.is_unit_iff,
  rw ← ne,
  rw ne_iff_lt_or_gt,
  right,
  rw prime_int at hp,
  exact hp.left,
  intros a b,
  intro h,
end

With current state:

2 goals
  p : ℕ,
  hp : prime_int p,
  a b : ℕ,
  h : p ∣ a * b
  ⊢ p ∣ a ∨ p ∣ b

  p : ℕ
  ⊢ nat.prime p → prime_int p

I have a lot of imports as the file I'm writing is about 700 lines long, but I will post them as well if it's necessary

[Will Midwood]

import data.int.basic
import data.int.gcd
import data.int.modeq
import data.int.interval

import data.list.defs

import data.nat.basic
import data.nat.cast.defs
import data.nat.prime

import order.basic
import order.locally_finite

import algebra.associated
import algebra.big_operators.basic

import ring_theory.int.basic

import data.fin.basic

import logic.basic

import set_theory.zfc.basic

import tactic.suggest
import tactic.ring
import tactic.interactive

import analysis.normed.field.unit_ball

[Mario Carneiro]

Note that because lean does transitive imports and mathlib is heavily cross connected, you rarely need more than 3 or 4 imports because the more advanced ones imply all the earlier ones. The easiest way to make an #mwe is to copy the proof into a new file, put all those includes at the top, and then delete them as long as the proof continues to work

[Mario Carneiro]

However I don't think any of those imports contains prime_int, so this still isn't a #mwe saw your definition above. This is why it's better to post self contained examples

[Zhang Ruichong]

Thank you! However, is there a simple way to prove something like Nat.divisors 4 = {1,2,4} , in Lean4? You said that lean4 might be better at calculations.

[Eric Wieser]

The proof of that should be rfl