MIL Ch9 WHNF Timeout

Stream: new members

[Luna]

While trying to solve isCoprime_Inf I got the following error while using apply?:

(deterministic) timeout at whnf, maximum number of heartbeats (200000) has been reached

What exactly does this mean and how do fix it? The code is below.

I was trying to find a theorem that states something along the lines of (c ≤ b) → (a ⊔ c) ≤ (a ⊔ b) in the following proof by using apply?

import Mathlib.RingTheory.Localization.Basic
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Data.ZMod.QuotientRing


variable {ι R : Type*} [CommRing R]
open Ideal Quotient Function

theorem isCoprime_Inf {I : Ideal R} {J : ι → Ideal R} {s : Finset ι}
    (hf : ∀ j ∈ s, IsCoprime I (J j)) : IsCoprime I (⨅ j ∈ s, J j) := by
  classical
  simp_rw [isCoprime_iff_add] at *
  induction s using Finset.induction with
  | empty =>
      simp
  | @insert i s _ hs =>
      rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
      set K := ⨅ j ∈ s, J j
      calc
        1 = I + K                  := by
          symm
          apply hs
          intro j jh
          exact hf j (Finset.mem_insert_of_mem jh)
        _ = I + K * (I + J i)      := by
          have : I + J i = 1 := hf i (Finset.mem_insert_self i s)
          simp [this]
        _ = (1 + K) * I + K * J i  := by ring
        _ = I + K * J i            := by simp
        _ = I ⊔ (K * J i)          := by rfl
        _ ≤ I ⊔ (K ⊓ J i)            := by apply?   -- <---- here is where the timeout is occurring
        _ = I + (K ⊓ J i)            := by rfl

[Ilmārs Cīrulis]

(Since nobody has answered)

Heartbeats can be understood as tiny bits of "time units". And there's default limit of them after which there is this announcement about timeout.

If one wants to increase this allowed limit, then it can be done in such way for some specific theorem:

set_option maxHeartbeats 1000000 in
theorem some_theorem : sorry := sorry

[Jakub Nowak]

It's what it says at the beginning "timeout". The rest are the details. It's deterministic timeout, because it counts the number of steps in the whnf function (weak head normal form reduction), not just time, e.g. 10 seconds. Otherwise compilation might have failed or not, depending on how fast computer you're compiling on, which would be undesirable. This number of steps it's called heartbeats.

The error also gives you line of code you can put before the theorem to increase the limit. You can try something like set_option maxHeartbeats 999999999, from my experience it often helps.

You can also use loogle the find the lemma you need:
@loogle (_ ⊔ _) ≤ (_ ⊔ _)
You can use loogle from the website, or directly from vscode, see "About" section on the website: https://loogle.lean-lang.org/

Btw, on Zulip, in the upper-right corner of the code you post there's a button "View in Lean4 playground". If you try to click this on the code you posted, you'll see that your code unfortunately doesn't work (and not because of apply?). I fixed it by removing two import lines that caused errors. You should always make sure the code you post works in the playground, if possible, this will make it easier for people to help you.

[loogle]

:search: sup_le_sup_left, sup_le_sup_right, and 15 more

[Luna]

Ah thanks. That makes since. I also edited the code so it works correctly in the lean playground.