From f74980ccee82ca2abdae65dcbc5571d4640ed076 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 13 May 2024 09:06:48 +1000 Subject: [PATCH] chore: incorrect lemma resolution in omega (#4141) Fixes #4138. --- src/Lean/Elab/Tactic/Omega/OmegaM.lean | 2 +- tests/lean/run/omega.lean | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Tactic/Omega/OmegaM.lean b/src/Lean/Elab/Tactic/Omega/OmegaM.lean index 57048157b7..0918433606 100644 --- a/src/Lean/Elab/Tactic/Omega/OmegaM.lean +++ b/src/Lean/Elab/Tactic/Omega/OmegaM.lean @@ -199,7 +199,7 @@ def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do | some _ => let b_pos := mkApp4 (.const ``LT.lt [0]) (.const ``Int []) (.const ``Int.instLTInt []) (toExpr (0 : Int)) b - let pow_pos := mkApp3 (.const ``Int.pos_pow_of_pos []) b exp (← mkDecideProof b_pos) + let pow_pos := mkApp3 (.const ``Lean.Omega.Int.pos_pow_of_pos []) b exp (← mkDecideProof b_pos) pure <| HashSet.empty.insert (mkApp3 (.const ``Int.emod_nonneg []) x k (mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) pow_pos)) |>.insert diff --git a/tests/lean/run/omega.lean b/tests/lean/run/omega.lean index 5c6b59331f..262ecfe2e0 100644 --- a/tests/lean/run/omega.lean +++ b/tests/lean/run/omega.lean @@ -426,6 +426,10 @@ example (x e : Nat) (hx : x < 2^(e.succ)) : x < 2^e * 2 := by omega -- Check that this works for integer base. example (x : Int) (e : Nat) (hx : x < (2 : Int)^(e+1)) : x < 2^e * 2 := by omega +example (n : Nat) (i : Int) (h2n : (2 : Int) ^ n = ↑((2 : Nat) ^ (n : Nat))) + (hlt : i % 2 ^ n < 2 ^ n) : 2 ^ n ≠ 0 := by + omega + /-! ### Ground terms -/ example : 2^7 < 165 := by omega