From e482303508716552c01c8a183da96dec17982c13 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 6 May 2024 14:36:26 +1000 Subject: [PATCH] chore: allow omega to use classicality, in case Decidable instances are too big --- src/Lean/Elab/Tactic/Omega/Frontend.lean | 1 - tests/lean/run/omega.lean | 6 +++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean index a382690a9cdb..fe2bbd733cbb 100644 --- a/src/Lean/Elab/Tactic/Omega/Frontend.lean +++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean @@ -666,7 +666,6 @@ open Lean Elab Tactic Parser.Tactic def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do liftMetaFinishingTactic fun g => do let g ← g.falseOrByContra - (useClassical := false) -- because all the hypotheses we can make use of are decidable g.withContext do let hyps := (← getLocalHyps).toList trace[omega] "analyzing {hyps.length} hypotheses:\n{← hyps.mapM inferType}" diff --git a/tests/lean/run/omega.lean b/tests/lean/run/omega.lean index 73d029b6a3ef..5c6b59331fe3 100644 --- a/tests/lean/run/omega.lean +++ b/tests/lean/run/omega.lean @@ -377,8 +377,12 @@ example (i j : Nat) (p : i ≥ j) : True := by -- From https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Nat.2Emul_sub_mod/near/428107094 example (a b : Nat) (h : a % b + 1 = 0) : False := by omega -/-! ### Fin -/ +-- From https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/omega.20regression.20in.204.2E8.2E0-rc1/near/437150155 +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 +/-! ### Fin -/ -- Test `<` example (n : Nat) (i j : Fin n) (h : i < j) : (i : Nat) < n - 1 := by omega