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

[hwatheod]

Prerequisites

• 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 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 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:

lean4/src/Lean/Elab/Tactic/Omega/Frontend.lean

Lines 668 to 669 in dcccfb7

	let g ← g.falseOrByContra
	(useClassical := false) -- because all the hypotheses we can make use of are decidable

The change in #3828 was this:

lean4/src/Lean/Elab/Tactic/FalseOrByContra.lean

Lines 38 to 41 in dcccfb7

	| .forallE _ _ _ _
	| .app (.const ``Not _) _ =>
	-- We set the transparency back to default; otherwise this breaks when run by a `simp` discharger.
	falseOrByContra (← withTransparency default g.intro1P).2 useClassical

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

lean4/src/Lean/Elab/Tactic/FalseOrByContra.lean

Lines 46 to 51 in dcccfb7

	| some false =>
	try some <$> g.applyConst ``Decidable.byContradiction
	catch _ => pure none
	| none =>
	try some <$> g.applyConst ``Decidable.byContradiction
	catch _ => some <$> g.applyConst ``Classical.byContradiction

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 #4073