Compute pairs of divisors

Stream: general

[Oliver Nash]

Here's a silly lemma which is very useful when working on crystallographic root systems:

lemma foo {a b : ℤ}
    (h₀ : a = 0 ↔ b = 0)
    (h₁ : a * b ∈ ({0, 1, 2, 3, 4} : Set ℤ)) :
    (a, b) ∈ ({
        (0, 0),
        (1, 1), (-1, -1),
        (1, 2), (2, 1), (-1, -2), (-2, -1),
        (1, 3), (3, 1), (-1, -3), (-3, -1),
        (4, 1), (1, 4), (-4, -1), (-1, -4), (2, 2), (-2, -2)} : Set (ℤ × ℤ)) := by
  sorry

I have two questions:

1. What is the best proof with tactics available today?
2. What tactic could we write to crush something like this? Computers are supposed to be good at goals like this; I shouldn't have to spoonfeed the proof to it.

[Eric Wieser]

aesop makes a lot of progress

[Eric Wieser]

I think an Int.divisorsAntidiagonal (with negative entries from Nat.divisorsAntidiagonal) might help here, since then you could adjust a * b into finset membership

[Oliver Nash]

Thanks; this is a great answer to 1, and probably I'll use it.

However I'm still interested in 2. I think we're a bit too used to writing definitions / lemmas to cater for missing tactics

[Kevin Buzzard]

+1 for 2.

But one thing Heather's metaprogramming course at Imperial has taught me is that before you write the tactic, you write the proof which you expect the tactic to come up with, and trying to do this is quite messy. You need all kinds of subtleties, e.g. "a * b = x obviously only has finitely many integer solutions, except when x = 0 but fortunately some other hypothesis deals with this case"

[Eric Wieser]

Right, I think writing the def I describe is also essential to implement 2; we have to teach the computer how to exhaustively iterate elements with a certain product somehow

[Oliver Nash]

Can't we hope for a more general approach? I mean factorisation of integers is decidable, so this entire lemma should just be by decide (in an ideal world).

[Johan Commelin]

Yeah, I think decide ought to be able to do this.

[Eric Wieser]

Oliver Nash said:

I mean factorisation of integers is decidable,

Sure, but you have to teach Lean this!

[Kevin Buzzard]

I am unclear about how this is a finite decision problem given that a * b = 0 is a possibility.

[Johan Commelin]

a = 0 \iff b = 0

[Johan Commelin]

Can't decide notice that?

[Johan Commelin]

Hmm, I'm quite frustrated that the shortest proof I have is

import Mathlib

lemma foo {a b : ℤ}
    (h₀ : a = 0 ↔ b = 0)
    (h₁ : a * b ∈ ({0, 1, 2, 3, 4} : Finset ℤ)) :
    (a, b) ∈ ({
        (0, 0),
        (1, 1), (-1, -1),
        (1, 2), (2, 1), (-1, -2), (-2, -1),
        (1, 3), (3, 1), (-1, -3), (-3, -1),
        (4, 1), (1, 4), (-4, -1), (-1, -4), (2, 2), (-2, -2)} : Finset (ℤ × ℤ)) := by
  generalize hn : a * b = n
  rw [hn] at h₁
  obtain rfl|hn₀ := eq_or_ne n 0
  · obtain rfl : a = 0 := by simpa [h₀] using hn
    obtain rfl : b = 0 := by simp at h₀; exact h₀
    decide +kernel
  have han : a.natAbs ≤ n.natAbs := Nat.le_of_dvd (by omega) (by subst n; simp)
  obtain rfl : b = n / a := by
    obtain rfl|ha := eq_or_ne a 0
    · subst n; simp_all
    · exact (Int.ediv_eq_of_eq_mul_right ha hn.symm).symm
  lift n to ℕ using (by clear hn han h₀; revert n; decide)
  simp only [Int.natAbs_ofNat] at han
  generalize ha' : a.natAbs = a'
  rw [ha'] at han
  rw [a.natAbs_eq_iff] at ha'
  have hn4 : n ≤ 4 := by simp at h₁; omega
  interval_cases n
  all_goals
    interval_cases a' <;> rcases ha' with rfl|rfl <;> decide

[Johan Commelin]

Ok, I should say that while aesop make a lot of progress, I find the generated proofs too slow to be usable in practice.

[Damiano Testa]

Johan, I would be very surprised if an automated proof of this fact ended up being shorter than your attempt!

[Damiano Testa]

Btw, every once in a while there are requests that look like they could use the junk dream-tactic. In this case, my vision of junk would add a \ne 0 and b \ne 0 hypotheses, possibly making other automation easier.

[Damiano Testa]

In fact, I always think of junk as an extension of nontrivial, except for specific values that are marked as junk, such as 0, \top, \bot and similar.

[Eric Wieser]

import Mathlib


def Int.divisorsAntidiagonal (z : ℤ) : Finset (ℤ × ℤ) :=
  ((Finset.Ico (-|z|) (0 : ℤ)).disjUnion (Finset.Ioc 0 (|z|)) sorry).filterMap
    (fun x => let y := z / x; if x * y = z then (x, y) else none)
    (fun x₁ x₂ (x, y) hx₁ hx₂ => by
      aesop)

theorem Int.mem_divisorsAntidiagonal_iff {xy : ℤ × ℤ} {z} :
    xy ∈ Int.divisorsAntidiagonal z ↔ xy.1 * xy.2 = z ∧ z ≠ 0 := by
  sorry

theorem Int.mem_divisorsAntidiagonal_iff' {x y z : ℤ} (hz : z ≠ 0):
    (x, y) ∈ Int.divisorsAntidiagonal z ↔ x * y = z := by
  rw [Int.mem_divisorsAntidiagonal_iff]
  simp [hz]

-- replace with a simproc
@[simp]
theorem Int.divisorsAntidiagonal_one : Int.divisorsAntidiagonal 1 = {(-1, -1), (1, 1)} := rfl
@[simp]
theorem Int.divisorsAntidiagonal_two : Int.divisorsAntidiagonal 2 = {(-2, -1), (-1, -2), (1, 2), (2, 1)} := rfl
@[simp]
theorem Int.divisorsAntidiagonal_three : Int.divisorsAntidiagonal 3 = {(-3, -1), (-1, -3), (1, 3), (3, 1)} := rfl
@[simp]
theorem Int.divisorsAntidiagonal_four : Int.divisorsAntidiagonal 4 = {(-4, -1), (-2, -2), (-1, -4), (1, 4), (2, 2), (4, 1)} := rfl

lemma foo {a b : ℤ}
    (h₀ : a = 0 ↔ b = 0)
    (h₁ : a * b ∈ ({0, 1, 2, 3, 4} : Set ℤ)) :
    (a, b) ∈ ({
        (0, 0),
        (1, 1), (-1, -1),
        (1, 2), (2, 1), (-1, -2), (-2, -1),
        (1, 3), (3, 1), (-1, -3), (-3, -1),
        (4, 1), (1, 4), (-4, -1), (-1, -4), (2, 2), (-2, -2)} : Set (ℤ × ℤ)) := by
  simp [← Int.mem_divisorsAntidiagonal_iff'] at h₁
  aesop

[Eric Wieser]

sorry and simproc left as an exercise to the reader

[Notification Bot]

19 messages were moved here from #general > golf request by Yaël Dillies.

[Yaël Dillies]

Related to this thread, I am improving performance of docs#Nat.divisorsAntidiagonal in #21910

[Yaël Dillies]

I've now opened #21912 to define Int.divisorsAntidiag. The proofs work locally but apparently not in CI :thinking: Help wanted!

[Yaël Dillies]

Sorry, I am stupid. I forgot to commit some other changes