feat: omega using Fin.isLt (#591)

leanprover-community · Feb 6, 2024 · 546f933 · 546f933
1 parent 325604c
commit 546f933
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/Std/Tactic/Omega/OmegaM.lean b/Std/Tactic/Omega/OmegaM.lean
@@ -136,6 +136,8 @@ def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do
       | _, (``Int.natAbs, #[x]) =>
         r := r.insert (mkApp (.const ``Int.le_natAbs []) x)
         r := r.insert (mkApp (.const ``Int.neg_le_natAbs []) x)
+      | _, (``Fin.val, #[n, i]) =>
+        r := r.insert (mkApp2 (.const ``Fin.isLt []) n i)
       | _, _ => pure ()
     return r
   | (``HDiv.hDiv, #[_, _, _, _, x, k]) => match natCast? k with

diff --git a/test/omega/test.lean b/test/omega/test.lean
@@ -379,3 +379,5 @@ example (i j : Nat) (p : i ≥ j) : True := by
   let k := l
   have _ : i ≥ k := by omega
   trivial
+
+example (i : Fin 7) : (i : Nat) < 8 := by omega