Large-ish computation without Lean.ofReduceBool

Stream: general

[Daniel Weber]

I'm trying to prove the theorem that every consecutive sequence of up to 16 integers contains one which is coprime to all the others. It's fairly easy to show that it suffices to check up to the primorial of m, and this can simply be checked with native_decide:

import Mathlib.NumberTheory.Primorial
import Mathlib.Tactic.Peel

@[reducible]
def prop1 (m n : ℕ) : Prop :=
  ∃ k < m, ∀ v < m, v ≠ k → Nat.Coprime (n + k) (n + v)

lemma l1 : ∀ m < 16, ∀ n < primorial m, prop1 (m + 1) n := by native_decide

lemma dvd_primorial_of_prime_of_le (p : ℕ) (hp : Nat.Prime p) (n : ℕ) (h : p ≤ n) : p ∣ primorial n := by
  apply Finset.dvd_prod_of_mem
  simp [hp]
  omega

lemma l2 {m n : ℕ} : prop1 m n ↔ prop1 m (n % primorial (m-1)) := by
  apply not_iff_not.mp
  simp_all only [not_exists, not_and, not_forall, Classical.not_imp,
    Nat.Prime.not_coprime_iff_dvd]
  peel with x hx y hy hxy p hp
  wlog hxy : x < y generalizing x y
  · exact and_comm.trans <| this y hy x hx (by omega) (by omega) |>.trans and_comm
  by_cases this : p ∣ y - x
  · replace : p ≤ y - x := Nat.le_of_dvd (by omega) this
    replace : p ∣ primorial (m - 1) := dvd_primorial_of_prime_of_le p hp (m-1) (by omega)
    replace : p ∣ n - n % primorial (m - 1) := this.trans (Nat.dvd_sub_mod n)
    have hn : n % primorial (m - 1) ≤ n := Nat.mod_le _ _
    apply and_congr
    repeat {
      convert (Nat.dvd_add_iff_left (n := n - n % primorial (m-1)) this).symm using 2
      omega
    }
  · apply iff_of_false
    repeat {
      intro nh
      apply this
      convert Nat.dvd_sub' nh.2 nh.1 using 1
      omega
    }

lemma l3 (m : ℕ) (hm : m < 16) (n : ℕ) : prop1 (m + 1) n :=
  l2.mpr <| l1 _ hm _ (Nat.mod_lt _ (primorial_pos _))

#print axioms l3

Is there a to get the kernel to check this, without assuming Lean.ofReduceBool? Using decide it can only check up to 7, but in theory for verifying it up to 16 you only need a check about a million equations of the form a*x + b*y = 1, so I think it could be possible.
Does it seem possible? How could I go about that?
(I can of course prove it with a more sophisticated case analysis, like in S. S. Pillai's article On M consecutive integers — I, but I'm curious if it could be avoided)

[Kyle Miller]

I tried having the kernel reduce the decidable instance itself, rather than pre-reducing it in the elaborator like decide does, but after dozens of seconds of computation, it gets a deep recursion error

@[reducible]
def prop1 (m n : ℕ) : Prop :=
  ∃ k < m, ∀ v < m, v ≠ k → Nat.Coprime (n + k) (n + v)

open Lean Elab Tactic Meta in
/-- Trust that the statement is true, have the kernel check it. -/
elab "decide_true!" : tactic =>
  closeMainGoalUsing fun expectedType => do
    mkDecideProof expectedType

-- (kernel) deep recursion detected
lemma l1 : ∀ m < 16, ∀ n < primorial m, prop1 (m + 1) n := by
  decide_true!

[Daniel Weber]

Deciding Nat.Coprime is still a gcd calculation the kernel has to do, right? Would it be possible to compute coefficients for ax + by = 1 and directly use those?

[Kyle Miller]

Can you compute those faster than computing gcd? Mathlib uses the euclidean algorithm for gcd

[Daniel Weber]

No, but this computation doesn't have to occur in the kernel

[Daniel Weber]

Also, the kernel is still finding the correct value of k, right? Could that be moved outside of it?

[Kyle Miller]

I think the big recursion the kernel is doing is when it iterates up to primorial m

[Kyle Miller]

It gets up to 30030

[Daniel Weber]

Would making the decidable instance a tree help?

[Kyle Miller]

Here's something I did once to get deeper recursion: https://github.com/leanprover-community/mathlib4/blob/3b78a47b048ee856c6fa2bdf5c94dffb8b0223ad/Mathlib/NumberTheory/LucasLehmer.lean#L554-L573

[Kyle Miller]

There's also manually handling each top-level case, but I'm not sure how to keep going with the last five:

lemma l1 : ∀ m < 16, ∀ n < primorial m, prop1 (m + 1) n := by
  intro m hm
  interval_cases m
  · decide
  · decide
  · decide
  · decide
  · decide
  · decide
  · decide
  · set_option maxRecDepth 1000 in decide
  · set_option maxRecDepth 1000 in decide
  · set_option maxRecDepth 1000 in decide
  · set_option maxRecDepth 1000 in decide
  all_goals intro n hn; conv at hn => rhs; reduce
  -- five more goals

[Daniel Weber]

this seems to prevent the recursion depth error, but it simply takes forever

attribute [-instance] Nat.decidableLoHi

@[semireducible]
instance decidableLoHi' (lo hi : ℕ) (P : ℕ → Prop) [H : DecidablePred P] :
    Decidable (∀ x, lo ≤ x → x < hi → P x) := by
  by_cases h : lo < hi
  · by_cases h₂ : lo + 1 = hi
    · apply decidable_of_iff (P lo)
      constructor
      · intro h x hx1 hx2
        have : x = lo := by omega
        rwa [this]
      · intro h
        apply h <;> trivial
    · have t1 := decidableLoHi' lo ((lo + hi)/2) P
      have t2 := decidableLoHi' ((lo + hi)/2) hi P
      have := @instDecidableAnd _ _ t1 t2
      apply @decidable_of_iff _ _ _ this
      constructor
      · intro h x hx1 hx2
        cases Nat.lt_or_ge x ((lo + hi)/2)
        · apply h.1 <;> omega
        · apply h.2 <;> omega
      · intro h
        constructor
        · intro x hx1 hx2
          apply h <;> omega
        · intro x hx1 hx2
          apply h <;> omega
  · apply Decidable.isTrue
    intros
    omega

lemma l1 : ∀ m < 16, ∀ n, (0 ≤ n) → (n < primorial m) → prop1 (m + 1) n := by
  decide_true!

[Daniel Weber]

I managed to get this to work up to 12 (with a slightly heavy rfl), do you think there's a way to push it up to 16? Perhaps List.forall_ind could be made more kernel-friendly?

import Mathlib.NumberTheory.Primorial
import Mathlib.Tactic.Peel
import Mathlib.Tactic.Eval
import Mathlib.Tactic.IntervalCases
import Mathlib.Data.Int.GCD

@[reducible]
def prop1 (m n : ℕ) : Prop :=
  ∃ k < m, ∀ v < m, v ≠ k → Nat.Coprime (n + k) (n + v)

def List.forall_ind {α : Type*} : ℕ → (List α) → (ℕ → α → Bool) → Bool
| _, [], _ => true
| i, a :: r, f => bif (f i a) then List.forall_ind (i + 1) r f else false

theorem List.forall_iff {α : Type*} {i : ℕ} (l : List α) {f : ℕ → α → Bool} :
    List.forall_ind i l f ↔ ∀ j (hj : j < l.length), f (j + i) l[j] := by
  induction l generalizing i with
  | nil => simp [forall_ind]
  | cons a r hind =>
    simp [forall_ind, hind]
    conv => rhs; rw [← Nat.and_forall_add_one]
    simp [add_comm, ← add_assoc]

def prop2 (m n : ℕ) (k : ℕ × List (ℤ × ℤ)) : Bool :=
  have ⟨k, l⟩ := k
  (k < m) &&
    l.length == m-1 &&
    l.forall_ind 0 (fun i ⟨a, b⟩ ↦ (n + (k + 1 + i) % m) * a + (n + k) * b = 1)

partial def generateList (m n : ℕ) : ℕ × (List (ℤ × ℤ)) :=
  generateList.go m n 0 0 []
  where
  generateList.go (m n k i : ℕ) (acc : List (ℤ × ℤ)) : ℕ × (List (ℤ × ℤ)) :=
    if i = m - 1 then
      (k, acc.reverse)
    else
    let ⟨a, b⟩ := Nat.xgcd (n + (k + 1 + i) % m) (n + k)
    if a*(n + (k + 1 + i) % m)+b*(n + k) = 1 then
      generateList.go m n k (i + 1) ((a, b) :: acc)
    else
      generateList.go m n (k + 1) 0 []

partial def generateListList (m n : ℕ) : List (ℕ × (List (ℤ × ℤ))) :=
  (generateListList.go m n 0 []).reverse
  where
  generateListList.go (m n i : ℕ) (aux) :=
    if i = n then
      aux
    else
      generateListList.go m n (i + 1) (generateList m i :: aux)

partial def generateListListList (b : ℕ) (n : ℕ → ℕ) : List (List (ℕ × (List (ℤ × ℤ)))) :=
  (generateListListList.go b 0 []).reverse
  where
  generateListListList.go (b i : ℕ) (aux) : List (List (ℕ × (List (ℤ × ℤ)))) :=
    if i = b then
      aux
    else
      generateListListList.go b (i + 1) (generateListList (i + 1) (n i) :: aux)

theorem forall_forall_lt_prop1_iff (b : ℕ) (n : ℕ → ℕ) :
        (∀ m < b, ∀ i < n m, prop1 (m + 1) i) ↔ ∃ a : List (List (ℕ × (List (ℤ × ℤ)))),
    (a.length == b) && (a.forall_ind 0 (fun i k ↦ k.length == n i &&
      k.forall_ind 0 (fun j ⟨k, l⟩ ↦
      k < (i + 1) &&
      l.length == i &&
      l.forall_ind 0 (fun i2 ⟨a, b⟩ ↦ (j + (k + 1 + i2) % (i + 1)) * a + (j + k) * b == 1)
      ))) := by
  sorry

def test (v : ℕ) : Bool :=
  have a := generateListListList v primorial
  (a.length == v) && (a.forall_ind 0 (fun i k ↦ k.length == primorial i &&
      k.forall_ind 0 (fun j ⟨k, l⟩ ↦
      k < (i + 1) &&
      l.length == i &&
      l.forall_ind 0 (fun i2 ⟨a, b⟩ ↦ (j + (k + 1 + i2) % (i + 1)) * a + (j + k) * b == 1)
      )))

#eval test 16

lemma l1 : ∀ m < 12, ∀ n < primorial m, prop1 (m + 1) n := by
  simp only [forall_forall_lt_prop1_iff]
  use eval% generateListListList 12 primorial
  count_heartbeats rfl

[Joachim Breitner]

Daniel Weber said:

Perhaps List.forall_ind could be made more kernel-friendly?

Maybe try to define it with Nat.rec directly, to avoid the Nat.brecOn overhead. Just a blind guess, but curious if will help. Is that really the bottleneck?

[Daniel Weber]

It reduced about 31M heartbeats (out of 391M), using

def List.forall_ind {α : Type*} (l : List α) (f : ℕ → α → Bool) : ℕ → Bool :=
  l.rec (fun _ ↦ true) (fun x _ hind i ↦ (f i x).rec false (hind (i + 1)))

[Joachim Breitner]

Right, I've observed this 10x improvement in some cases as well, and am working on tooling that can maybe help achieving that (https://github.com/leanprover/lean4/issues/5806, which you already found), although it's unclear how convenient and universally applicable it will end up being.

[Daniel Weber]

It's not a 10x reduction, it's approximately a 10% reduction

[Daniel Weber]

Does the kernel know how to work with UInt more efficiently than Nat?

[Joachim Breitner]

Ah, misread your comment. I've seen 10x in some cases (e.g. our finite magma calculations)

[Joachim Breitner]

No, UInt are just slower Nat, and Array are just slower List. It's really no fun to write code for kernel reduction.

[Daniel Weber]

Using Nat.succ instead of i + 1 removed a few hundred thousand heartbeats

[Joachim Breitner]

Right. Getting rid of Fin (of it is involved) also helps a lot.
See https://github.com/teorth/equational_theories/pull/477 for an attempt to automate some of these transformations. Doing it always is not effective, but if you have single very slow proofs maybe it helps already.

[Daniel Weber]

Even when using native decide, though, it's much slower then I would've expected - most of that seems to be because docs#Nat.decidableBallLT isn't implemented tail-recursively