From 4e310ac63dee6acfbc6c46d8a48b3d506ce349d6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Feb 2022 18:27:13 -0800
Subject: [PATCH] feat: improve `SimpTheorem` preprocessor

---
 src/Init/SimpLemmas.lean                    |  4 ++++
 src/Lean/Meta/Tactic/Simp/SimpTheorems.lean |  9 +++++++++
 tests/lean/run/simpBool.lean                | 11 +++++++++++
 3 files changed, 24 insertions(+)
 create mode 100644 tests/lean/run/simpBool.lean

diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean
index 8d9bb7d9ed..8ff2c6f950 100644
--- a/src/Init/SimpLemmas.lean
+++ b/src/Init/SimpLemmas.lean
@@ -139,6 +139,10 @@ theorem dite_congr {s : Decidable b} [Decidable c]
 
 @[simp] theorem Bool.beq_to_eq (a b : Bool) : ((a == b) = true) = (a = b) := by cases a <;> cases b <;> decide
 @[simp] theorem Bool.not_beq_to_not_eq (a b : Bool) : ((!(a == b)) = true) = ¬(a = b) := by cases a <;> cases b <;> decide
+
+theorem Bool.of_not_eq_true {b : Bool} : ¬ (b = true) → b = false := by cases b <;> decide
+theorem Bool.of_not_eq_false {b : Bool} : ¬ (b = false) → b = true := by cases b <;> decide
+
 @[simp] theorem Bool.not_eq_true (b : Bool) : (¬ (b = true)) = (b = false) := by cases b <;> decide
 @[simp] theorem Bool.not_eq_false (b : Bool) : (¬ (b = false)) = (b = true) := by cases b <;> decide
 
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index 634285dfed..46d968ebf4 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -153,12 +153,21 @@ where
   else if let some (_, lhs, rhs) := type.ne? then
     if inv then
       throwError "invalid '←' modifier in rewrite rule to 'False'"
+    if rhs.isConstOf ``Bool.true then
+      return [(← mkAppM ``Bool.of_not_eq_true #[e], ← mkEq lhs (mkConst ``Bool.false))]
+    else if rhs.isConstOf ``Bool.false then
+      return [(← mkAppM ``Bool.of_not_eq_false #[e], ← mkEq lhs (mkConst ``Bool.true))]
     let type ← mkEq (← mkEq lhs rhs) (mkConst ``False)
     let e    ← mkEqFalse e
     return [(e, type)]
   else if let some p := type.not? then
     if inv then
       throwError "invalid '←' modifier in rewrite rule to 'False'"
+    if let some (_, lhs, rhs) := p.eq? then
+      if rhs.isConstOf ``Bool.true then
+        return [(← mkAppM ``Bool.of_not_eq_true #[e], ← mkEq lhs (mkConst ``Bool.false))]
+      else if rhs.isConstOf ``Bool.false then
+        return [(← mkAppM ``Bool.of_not_eq_false #[e], ← mkEq lhs (mkConst ``Bool.true))]
     let type ← mkEq p (mkConst ``False)
     let e    ← mkEqFalse e
     return [(e, type)]
diff --git a/tests/lean/run/simpBool.lean b/tests/lean/run/simpBool.lean
new file mode 100644
index 0000000000..217526d2b2
--- /dev/null
+++ b/tests/lean/run/simpBool.lean
@@ -0,0 +1,11 @@
+example (h : x ≠ true) : (x && y) = false := by
+  simp [h]
+
+example (h : ¬ (x = true)) : (x && y) = false := by
+  simp [h]
+
+example (h : x ≠ false) : (x && y) = y := by
+  simp [h]
+
+example (h : ¬ (x = false)) : (x && y) = y := by
+  simp [h]