From 41a5c2bce466fdba4db5dae9a63cf00a409ee911 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Feb 2022 18:30:09 -0800
Subject: [PATCH] feat: add support for negation at `simpCnstr?`

---
 src/Lean/Meta/AppBuilder.lean             | 18 ++++++++++++++
 src/Lean/Meta/Tactic/LinearArith/Nat.lean | 30 ++++++++++++++++++++++-
 tests/lean/run/simpCnstr1.lean            | 10 +++++++-
 3 files changed, 56 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index b2aa39fb54..4210a03eaa 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -537,6 +537,24 @@ def mkSub (a b : Expr) : MetaM Expr := mkBinaryOp ``HSub ``HSub.hSub a b
 /-- Return `a * b` using a heterogeneous `*`. This method assumes `a` and `b` have the same type. -/
 def mkMul (a b : Expr) : MetaM Expr := mkBinaryOp ``HMul ``HMul.hMul a b
 
+/--
+  Return `a r b`, where `r` has name `rName` and is implemented using the typeclass `className`.
+  This method assumes `a` and `b` have the same type.
+  Examples of supported clases: `LE` and `LT`.
+  We use heterogeneous operators to ensure we have a uniform representation.
+  -/
+private def mkBinaryRel (className : Name) (rName : Name) (a b : Expr) : MetaM Expr := do
+  let aType ← inferType a
+  let u ← getDecLevel aType
+  let inst ← synthInstance (mkApp (mkConst className [u]) aType)
+  return mkApp4 (mkConst rName [u]) aType inst a b
+
+/-- Return `a ≤ b`. This method assumes `a` and `b` have the same type. -/
+def mkLE (a b : Expr) : MetaM Expr := mkBinaryRel ``LE ``LE.le a b
+
+/-- Return `a < b`. This method assumes `a` and `b` have the same type. -/
+def mkLT (a b : Expr) : MetaM Expr := mkBinaryRel ``LT ``LT.lt a b
+
 builtin_initialize registerTraceClass `Meta.appBuilder
 
 end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/LinearArith/Nat.lean b/src/Lean/Meta/Tactic/LinearArith/Nat.lean
index 5438f3308a..fb66c5373f 100644
--- a/src/Lean/Meta/Tactic/LinearArith/Nat.lean
+++ b/src/Lean/Meta/Tactic/LinearArith/Nat.lean
@@ -154,7 +154,7 @@ def toContextExpr (ctx : Array Expr) : MetaM Expr := do
 def reflTrue : Expr :=
   mkApp2 (mkConst ``Eq.refl [levelOne]) (mkConst ``Bool) (mkConst ``Bool.true)
 
-def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
+def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   let (some c, ctx) ← ToLinear.run (ToLinear.toLinearCnstr? e) | return none
   let c₁ := c.toPoly
   let c₂ := c₁.norm
@@ -172,4 +172,32 @@ def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   else
     return none
 
+def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
+  if let some arg := e.not? then
+    let mut eNew?   := none
+    let mut thmName := Name.anonymous
+    if arg.isAppOfArity ``LE.le 4 then
+      eNew?   := some (← mkLE (← mkAdd (arg.getArg! 3) (mkNatLit 1)) (arg.getArg! 2))
+      thmName := ``Nat.not_le_eq
+    else if arg.isAppOfArity ``GE.ge 4 then
+      eNew?   := some (← mkLE (← mkAdd (arg.getArg! 2) (mkNatLit 1)) (arg.getArg! 3))
+      thmName := ``Nat.not_ge_eq
+    else if arg.isAppOfArity ``LT.lt 4 then
+      eNew?   := some (← mkLE (arg.getArg! 3) (arg.getArg! 2))
+      thmName := ``Nat.not_lt_eq
+    else if arg.isAppOfArity ``GT.gt 4 then
+      eNew?   := some (← mkLE (arg.getArg! 2) (arg.getArg! 3))
+      thmName := ``Nat.not_gt_eq
+    if let some eNew := eNew? then
+      if let some (eNew', h₂) ← simpCnstrPos? eNew then
+        let h₁ := mkApp2 (mkConst thmName) (arg.getArg! 2) (arg.getArg! 3)
+        let h  := mkApp6 (mkConst ``Eq.trans [levelOne]) (mkSort levelZero) e eNew eNew' h₁ h₂
+        return some (eNew', h)
+      else
+        return none
+    else
+      return none
+  else
+    simpCnstrPos? e
+
 end Lean.Meta.Linear.Nat
diff --git a/tests/lean/run/simpCnstr1.lean b/tests/lean/run/simpCnstr1.lean
index 6ca53db386..3c47713ef7 100644
--- a/tests/lean/run/simpCnstr1.lean
+++ b/tests/lean/run/simpCnstr1.lean
@@ -3,7 +3,7 @@ import Lean
 open Lean in open Lean.Meta in
 def test (declName : Name) : MetaM Unit := do
   let info ← getConstInfo declName
-  forallTelescopeReducing info.type fun _ e => do
+  forallTelescope info.type fun _ e => do
     let some (e', p) ← Linear.simpCnstr? e | throwError "failed to simplify{indentExpr e}"
     check p
     unless (← isDefEq (← inferType p) (← mkEq e e')) do
@@ -20,6 +20,10 @@ axiom ex7 (a b : Nat) : a + a ≤ 8 + a + a + b
 axiom ex8 (a b c d : Nat) : b + a + c + d ≤ a + b + a + b
 axiom ex9 (a b : Nat) : a + b + 1 + a > b + 4 + a
 axiom ex10 (a b : Nat) : a + b + 1 + a ≥ b + 4 + a
+axiom ex11 (a b : Nat) : ¬ (a + b + 1 + a < b + 4 + a)
+axiom ex12 (a b : Nat) : ¬ (a + b + 1 + a > b + 4 + a)
+axiom ex13 (a b : Nat) : ¬ (a + b + 1 + a ≤ b + 4 + a)
+axiom ex14 (a b : Nat) : ¬ (a + b + 1 + a ≥ b + 4 + a)
 
 #eval test ``ex1
 #eval test ``ex2
@@ -31,3 +35,7 @@ axiom ex10 (a b : Nat) : a + b + 1 + a ≥ b + 4 + a
 #eval test ``ex8
 #eval test ``ex9
 #eval test ``ex10
+#eval test ``ex11
+#eval test ``ex12
+#eval test ``ex13
+#eval test ``ex14