omega regression in 4.8.0-rc1

Stream: lean4

[Ted Hwa]

Hi all, I've been using Lean for about 2 months now and I really like it. I've been thinking of things to formalize and it's really helped me learn the system.

With the recent 4.8.0-rc1 release, I ran into a regression in omega which I filed at lean4#4054. I believe I've found the underlying issue (in the Github thread I wrote down all the debugging details, if you are interested). I will summarize here. However, as a new user, I don't know what the best fix would be.

The minimized example is:

example (x: Nat):
    x < 2 →
    (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2) ∧
    (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2 → x < 3)
:= by omega

This works in 4.7.0 but fails in 4.8.0-rc1. However, if you remove any of the 0 = 0 then it works in 4.8.0-rc1.

I traced the issue down to this:

example: (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2) ∧
    (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2 → x < 3) := by
  apply Decidable.byContradiction  -- Failed to synthesize Decidable

-- Removing one of the 0 = 0 on the second line
example: (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2) ∧
    (0 = 0 → 0 = 0 → 0 = 0 → x < 2 → x < 3) := by
  apply Decidable.byContradiction  -- works ok

This turns out to be due to a limit in synthInstance.maxSize. With set_option synthInstance.maxSize 256 then the original omega works in 4.8.0-rc1.

It appears that the reason it works in 4.7.0 but not 4.8.0-rc1 is due to lean4#3828. In 4.7.0, within the omega tactic which calls falseOrByContradiction, when Decidable.byContradiction fails it would fall back to Classical.byContradiction (useClassical := none), which succeeds because it doesn't need to synthesize a Decidable instance. But after the above change in 4.8.0-rc1, it simply drops the hypothesis when Decidable.byContradiction fails (useClassical := false). Even though omegaTactic sets useClassical := false, there is a recursive call which changes useClassical := none in 4.7.0 but in 4.8.0-rc1 it retains the value false.

What should be the fix here? One could simply set useClassical := none in the omega tactic, but that means potentially picking up some hypotheses to omega that are useless anyway (there is a comment about this in the omegaTactic code).

I also looked into why the synthInstance.maxSize limit was exceeded. I tried this trace:

set_option trace.Meta.synthInstance.newAnswer true in
example: (0 = 0  → 0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2)  := by
  apply Decidable.byContradiction

In the trace, with each new 0 = 0, I see an exponentially growing sequence of numbers 3, 9, 21, 45, 93 (these numbers are 3*(2^n-1) ). I don't really understand the details here but it seems strange to me that adding a new 0 = 0 causes an exponential growth in size.

Well, that was a long first message! I hope this is helpful in resolving this issue.

[Kim Morrison]

Curiously the exponential growth stops at the point of the last example: further 0 = 0 instead results in linear growth in [Meta.synthInstance.newAnswer] size: 95, val: instDecidableForall lines...

[Kim Morrison]

Hmm, this minimization isn't quite correct. While it's true that

example (x: Nat):
    x < 2 →
    (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2) ∧
    (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2 → x < 3)
:= by omega

worked in v4.7.0 but now fails in v4.8.0-rc1

[Kim Morrison]

example: (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2) ∧
    (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2 → x < 3) := by
  apply Decidable.byContradiction  -- Failed to synthesize Decidable

fails on both!

[Kim Morrison]

@Ted Hwa, I think the right solution here is just to remove useClassical := false in omega.

[Kim Morrison]

lean4#4073

[Ted Hwa]

Curiously the exponential growth stops at the point of the last example: further 0 = 0 instead results in linear growth in [Meta.synthInstance.newAnswer] size: 95, val: instDecidableForall lines...

It's even stranger. If you increase synthInstance.maxSize to 256 (say) and add one more 0=0, then you do see the next exponential growth number 189, but then if you add yet another, it's linear again. It seems like the exponential growth continues until it hits the limit, then it becomes linear.