Deterministic timeout when proving a theorem

Stream: general

[Donald Sebastian Leung]

So I'm using Lean v3.7.2 with mathlib commit 732f7109c5cb2ece35481c200faa38fbbb4dc995 and encountered a deterministic timeout when trying to prove a theorem, which is certainly a first for me:

Preloaded.lean:

inductive times_3_plus_5 : set ℕ
| start :
    times_3_plus_5 1
| times_3 : ∀ n,
    times_3_plus_5 n →
    times_3_plus_5 (n * 3)
| plus_5 : ∀ n,
    times_3_plus_5 n →
    times_3_plus_5 (n + 5)

def decide (n : ℕ) : bool :=
  match n % 5 with
  | 0 := ff
  | 2 := 27 ≤ n
  | 4 := 9 ≤ n
  | _ := tt
  end

def SUBMISSION := ∀ n, times_3_plus_5 n ↔ decide n = tt
notation `SUBMISSION` := SUBMISSION

Solution.lean:

import Preloaded tactic data.nat.modeq

open times_3_plus_5 nat nat.modeq

theorem decide_works (n : ℕ) :
  times_3_plus_5 n ↔ decide n = tt :=
begin
  split; simp [decide]; intros h,
  { induction h,
    case start : { refl },
    case times_3 : m hm ihm {
      have hm5 : m % 5 < 5 := mod_lt m dec_trivial,
      interval_cases (m % 5),
      { rw lh at ihm, contradiction },
      { have hm1 : m % 5 = 1 % 5, by assumption,
        have hm3 : m * 3 % 5 = 1 * 3 % 5 := modeq_mul_right _ hm1,
        rw hm3,
        refl },
      { rw lh at ihm,
        simp [decide] at *,
        have hm2 : m % 5 = 2 % 5, by assumption,
        have hm3 : m * 3 % 5 = 2 * 3 % 5 := modeq_mul_right _ hm2,
        rw hm3,
        refl },
      { have hm3 : m % 5 = 3 % 5, by assumption,
        have hm4 : m * 3 % 5 = 4 := modeq_mul_right _ hm3,
        rw hm4,
        simp [decide],
        generalize h : m * 3 = m',
        iterate 9 { all_goals { try { cases m' } } },
        { rw h at hm4; contradiction },
        { omega },
        { omega },
        { have hm1 : m = 1, by omega, subst hm1, cases lh },
        { omega },
        { omega },
        { have hm2 : m = 2, by omega, subst hm2, cases lh },
        { omega },
        { omega },
        { omega } },
      { sorry }
    },
    case plus_5 : { sorry } },
  { sorry }
end

As far as I can see, all the tactics I've used so far succeed, but I get a red squiggly line just below the theorem in theorem decide_works ..., and upon hovering my mouse over it, it says (deterministic) timeout. The thing is, I've written proofs that take way longer than this one to compile (> 30s compared to maybe about 10s on this one) and have not seen such an error before so was this timing restriction added recently, or am I missing something?

[Kenny Lau]

yay you're translating more kata

[Kenny Lau]

deterministic timeout has always existed (and always will)

[Kenny Lau]

the multitude of omega may or may not be the cause

[Donald Sebastian Leung]

So a tactic-mode proof cannot have too many steps? In that case maybe I'll try extracting out a few lemmas and see if it helps.

[Mario Carneiro]

You can turn off the timeout, and I think it is disabled by default if you run lean via the command line

[Donald Sebastian Leung]

Thanks. In any case, it seems that it was indeed the excessive use of omega which caused the timeout. I pulled out all uses of omega into separate lemmas and that seems to have solved my timeout issues, at least for now.

[Kevin Buzzard]

I think there is some underlying weirdness going on here. Here's a situation where I prove one goal with omega in two different situations, and it takes 0.08 seconds in the first and 3 seconds in the second one on my machine, to solve exactly the same goal.

import  tactic data.nat.modeq

inductive times_3_plus_5 : set ℕ
| start :
    times_3_plus_5 1
| times_3 : ∀ n,
    times_3_plus_5 n →
    times_3_plus_5 (n * 3)
| plus_5 : ∀ n,
    times_3_plus_5 n →
    times_3_plus_5 (n + 5)

def decide (n : ℕ) : bool :=
  match n % 5 with
  | 0 := ff
  | 2 := 27 ≤ n
  | 4 := 9 ≤ n
  | _ := tt
  end

open times_3_plus_5 nat nat.modeq

-- I can make Lean solve the following goal in 0 seconds and in 3 seconds with the same tactic

/-
n m : ℕ,
hm : times_3_plus_5 m,
ihm : decide._match_1 m (m % 5) = tt,
hm5 : m % 5 < 5,
lh : m % 5 = 3,
hm3 : m % 5 = 3 % 5,
hm4 : m * 3 % 5 = 4,
h : m * 3 = 7
⊢ 9 ≤ 7
-/

set_option profiler true

example (n m : ℕ)
(hm : times_3_plus_5 m)
(ihm : decide._match_1 m (m % 5) = tt)
(hm5 : m % 5 < 5)
(lh : m % 5 = 3)
(hm3 : m % 5 = 3 % 5)
(hm4 : m * 3 % 5 = 4)
(h : m * 3 = 7)
: 9 ≤ 7 := by omega -- <- finishes almost instantly

-- Now look in the middle of a proof

theorem decide_works (n : ℕ) :
  times_3_plus_5 n ↔ decide n = tt :=
begin
  split; simp [decide]; intros h,
  { induction h,
    case start : { refl },
    case times_3 : m hm ihm {
      have hm5 : m % 5 < 5 := mod_lt m dec_trivial,
      interval_cases (m % 5),
      { rw lh at ihm, contradiction },
      { have hm1 : m % 5 = 1 % 5, by assumption,
        have hm3 : m * 3 % 5 = 1 * 3 % 5 := modeq_mul_right _ hm1,
        rw hm3,
        refl },
      { rw lh at ihm,
        simp [decide] at *,
        have hm2 : m % 5 = 2 % 5, by assumption,
        have hm3 : m * 3 % 5 = 2 * 3 % 5 := modeq_mul_right _ hm2,
        rw hm3,
        refl },
      { have hm3 : m % 5 = 3 % 5, by assumption,
        have hm4 : m * 3 % 5 = 4 := modeq_mul_right _ hm3,
        rw hm4,
        simp [decide],
        generalize h : m * 3 = m',
        iterate 9 { all_goals { try { cases m' } } },
        { rw h at hm4; contradiction },
        { omega },
        { omega },
        { have hm1 : m = 1, by omega, subst hm1, cases lh },
        { omega },
        { omega },
        { have hm2 : m = 2, by omega, subst hm2, cases lh },
        { omega}, -- <- this omega takes 3 seconds; replace with sorry and observe profiler change
        sorry,sorry},sorry},sorry},sorry,end -- <- look at profiler output here

[Kevin Buzzard]

@Gabriel Ebner how can that happen?

[Kevin Buzzard]

How do I begin to debug this? All I know is how to turn the profiler on. Are there hidden metavariable goals?

[Kevin Buzzard]

Aah! If I type recover before the omega, then all of a sudden I have 5 goals.

[Kevin Buzzard]

Does this indicate that something is not clearing up as it should be?

[Kevin Buzzard]

Oh -- is that actually expected behaviour of recover when one is in a sub-{} block?

[Kevin Buzzard]

example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q :=
begin
  split,
  { recover, exact hq, exact hp},
end

Maybe I'm back to square 1.

[Gabriel Ebner]

I can see two possible ways this could happen: 1) 7 is not the same as 7. You could enable pp.all and check if the two goals are actually the same. 2) omega is non-deterministic because it depends on the state of the caches, the order of the assumptions, the names of the assumptions, the hash codes of the expressions, etc.

[Gabriel Ebner]

I hope that omega only looks at the current goal and not at other metavariables. So I don't think it's got anything to do with recover.

[Kevin Buzzard]

7 is indeed not the same as 7. They're both nats though.

[Kevin Buzzard]

(nat.succ (nat.succ (nat.succ (nat.succ (nat.succ (nat.succ (nat.succ nat.zero))))))) v (@bit1.{0} nat nat.has_one nat.has_add (@bit1.{0} nat nat.has_one nat.has_add (@has_one.one.{0} nat nat.has_one)))

[Kevin Buzzard]

Oh nice Gabriel -- this is exactly it!

[Kevin Buzzard]

import tactic.omega

set_option profiler true

example (m : ℕ)
(hm5 : m % 5 < 5)
(lh : m % 5 = 3)
(hm3 : m % 5 = 3 % 5)
(hm4 : m * 3 % 5 = 4)
(h : m * 3 = 7)
: 9 ≤ 7 := begin
 omega -- <- finishes almost instantly
end

example (m : ℕ)
(hm5 : m % 5 < 5)
(lh : m % 5 = 3)
(hm3 : m % 5 = 3 % 5)
(hm4 : m * 3 % 5 = 4)
(h : m * 3 = 7)
: 9 ≤ (nat.succ (nat.succ (nat.succ (nat.succ (nat.succ (nat.succ (nat.succ nat.zero))))))) := begin
 omega -- <- takes three seconds
end

[Kevin Buzzard]

The prettyprinter displays them both as 7 and they're both nats

[Gabriel Ebner]

Here's what's happening: as a preprocessing step, omega replaces nat.succ by + 1: https://github.com/leanprover-community/mathlib/blob/f723f37531502d76e9f7a3a27c225884918a70b5/src/tactic/omega/nat/main.lean#L24 So instead of 7 it sees 0 + 1 + 1 + 1 + 1 + 1 + 1 +1.

[Kevin Buzzard]

#2376

[Kevin Buzzard]

@Donald Sebastian Leung there is some issue with omega taking too long, but in your code above if you replace iterate 9 { all_goals { try { cases m' } } }, with iterate 9 { all_goals { try { cases m'; simp } } }, you might be back on track.