Compare commits

...

1 Commits

Author SHA1 Message Date
Kim Morrison
ef335988d9 chore: incorrect lemma resolution in omega 2024-05-13 08:50:11 +10:00
2 changed files with 5 additions and 1 deletions

View File

@@ -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

View File

@@ -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