a case where omega used to work in 4.7.0 and doesn't work in 4.8.0-rc1

[hwatheod]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

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

Lean 4.8.0-rc1 is unable to solve this, but lean 4.7.0 can. But if you delete any one of the clauses other than initial x < 2 (which would make the result false), then Lean 4.8.0-rc1 can solve it. Just the presence of the extraneous 0 = 0 seems to cause a problem. Changing any of the 0 = 0 to any other arbitrary statement seems to still exhibit the same issue.

Of course, this is not my original code. It's a far simplified version which still causes the same problem.

Steps to Reproduce

1. Install both lean 4.7.0 and 4.8.0-rc1
2. Under Lean 4.7.0, omega successfully proves the lemma.
3. Under 4.8.0-rc1,

   error: omega could not prove the goal:
   a possible counterexample may satisfy the constraints
   0 ≤ a ≤ 1
   where
   a := ↑x

Expected behavior: omega is able to prove the goal

Actual behavior: omega gives the error shown above

Versions

4.7.0 (works), 4.8.0-rc1 (fails) MacOS 12.7.4

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[hwatheod]

I added set_option trace.omega true.

In Lean 4.7.0, it starts with

[omega] analyzing 3 hypotheses:
    [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))]

but in Lean 4.8.0-rc1, it starts with

[omega] analyzing 2 hypotheses:
    [Nat, x < 2]

But when I remove one of the 0 = 0 then Lean 4.8.0-rc1 also shows "analyzing 3 hypotheses".
In 4.8.0-rc1, is omega is ignoring a hypothesis if it exceeds some complexity?

[hwatheod]

If I make either of these changes then it works:

Add open Classical to the top of the file

Add the tactic false_or_by_contra before omega

[hwatheod]

So, in both 4.7.0 and 4.8.0-rc1, we have the following behavior:

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

However, if you use apply Classical.byContradiction, then both cases work.

I think #3828 may be the issue.

The omegaTactic calls falseOrByContra with useClassical := false: https://github.com/leanprover/lean4/blob/dcccfb73cb247e9478220375ab7de03f7c67e505/src/Lean/Elab/Tactic/Omega/Frontend.lean#L668-L669

The change in #3828 was this:

https://github.com/leanprover/lean4/blob/dcccfb73cb247e9478220375ab7de03f7c67e505/src/Lean/Elab/Tactic/FalseOrByContra.lean#L38-L41

It recursively calls falseOrByContra preserving useClassical as false, leading to this code in the recursive call

https://github.com/leanprover/lean4/blob/dcccfb73cb247e9478220375ab7de03f7c67e505/src/Lean/Elab/Tactic/FalseOrByContra.lean#L46-L51

Since useClassical := false in the recursive call, when it tries to apply Decidable.byContradiction and fails, it returns none and we lose the hypothesis.

However, prior to the change in #3828, the recursive call was falseOrByContra (← g.intro1).2 so useClassical would become none in the recursive call. So in that case, it falls back on Classical.byContradiction (which then succeeds) when Decidable.byContradiction fails.

[hwatheod]

So, it seems that the Failed to synthesize Decidable is caused by a limit in synthInstance.maxSize. By doing set_option synthInstance.maxSize 256 then the original omega works.

[semorrison]

Closed by https://github.com/leanprover/lean4/pull/4073