From 5030e613a2cc509d666e993c3feb3c58df2d4fc0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Feb 2022 17:18:50 -0800
Subject: [PATCH] feat: add `isSimpCnstrTarget`

---
 src/Lean/Meta/Tactic/LinearArith/Main.lean | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Tactic/LinearArith/Main.lean b/src/Lean/Meta/Tactic/LinearArith/Main.lean
index 66daeb8d9b..fcc2e1fe10 100644
--- a/src/Lean/Meta/Tactic/LinearArith/Main.lean
+++ b/src/Lean/Meta/Tactic/LinearArith/Main.lean
@@ -7,8 +7,25 @@ import Lean.Meta.Tactic.LinearArith.Nat
 
 namespace Lean.Meta.Linear
 
+/-- Quick filter simpCnstr? -/
+private partial def isSimpCnstrTarget (e : Expr) : Bool :=
+  let f := e.getAppFn
+  if !f.isConst then
+    false
+  else
+    let n := f.constName!
+    if n == ``Eq || n == ``LT.lt || n == ``LE.le || n == ``GT.gt || n == ``GE.ge then
+      true
+    else if n == ``Not && e.getAppNumArgs == 1 then
+      isSimpCnstrTarget e.appArg!
+    else
+      false
+
 def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
-  -- TODO: add support for `Int` and arbitrary ordered comm rings
-  Nat.simpCnstr? e
+  if isSimpCnstrTarget e then
+    -- TODO: add support for `Int` and arbitrary ordered comm rings
+    Nat.simpCnstr? e
+  else
+    return none
 
 end Lean.Meta.Linear