From 0c43f0504733f44add6bfd22e5d7ad62fb0cb84b Mon Sep 17 00:00:00 2001
From: Vlad Tsyrklevich <vlad@tsyrklevich.net>
Date: Wed, 29 Jan 2025 14:52:57 +0100
Subject: [PATCH] feat: add BitVec add_self/self_add lemmas (#6848)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds simp lemmas proving `x + y = x ↔ x = 0` for BitVec, along
with symmetries, and then adds these to the bv_normalize simpset.
---
 src/Init/Data/BitVec/Lemmas.lean             | 22 ++++++++++++++++++++
 src/Std/Tactic/BVDecide/Normalize/Equal.lean | 20 ++++++++++++++++++
 tests/lean/run/bv_decide_rewriter.lean       |  6 ++++++
 3 files changed, 48 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index edc71c55b6..84a4f01c8f 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -2586,6 +2586,28 @@ protected theorem sub_left_inj {x y : BitVec w} (z : BitVec w) : (x - z = y - z)
 protected theorem sub_right_inj {x y : BitVec w} (z : BitVec w) : (z - x = z - y) ↔ x = y := by
   simp [sub_toAdd]
 
+/-! ### add self -/
+
+@[simp]
+protected theorem add_left_eq_self {x y : BitVec w} : x + y = y ↔ x = 0#w := by
+  conv => lhs; rhs; rw [← BitVec.zero_add y]
+  exact BitVec.add_left_inj y
+
+@[simp]
+protected theorem add_right_eq_self {x y : BitVec w} : x + y = x ↔ y = 0#w := by
+  rw [BitVec.add_comm]
+  exact BitVec.add_left_eq_self
+
+@[simp]
+protected theorem self_eq_add_right {x y : BitVec w} : x = x + y ↔ y = 0#w := by
+  rw [Eq.comm]
+  exact BitVec.add_right_eq_self
+
+@[simp]
+protected theorem self_eq_add_left {x y : BitVec w} : x = y + x ↔ y = 0#w := by
+  rw [BitVec.add_comm]
+  exact BitVec.self_eq_add_right
+
 /-! ### fill -/
 
 @[simp]
diff --git a/src/Std/Tactic/BVDecide/Normalize/Equal.lean b/src/Std/Tactic/BVDecide/Normalize/Equal.lean
index 389d8351d2..792e7a21ad 100644
--- a/src/Std/Tactic/BVDecide/Normalize/Equal.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/Equal.lean
@@ -45,5 +45,25 @@ theorem BitVec.add_right_inj (a b c : BitVec w) : (c + a == c + b) = (a == b) :=
 theorem BitVec.add_right_inj' (a b c : BitVec w) : (c + a == b + c) = (a == b) := by
   rw [BitVec.add_comm b c, add_right_inj]
 
+@[bv_normalize]
+theorem BitVec.add_left_eq_self (a b : BitVec w) : (a + b == b) = (a == 0#w) := by
+  rw [Bool.eq_iff_iff]
+  simp
+
+@[bv_normalize]
+theorem BitVec.add_right_eq_self (a b : BitVec w) : (a + b == a) = (b == 0#w) := by
+  rw [Bool.eq_iff_iff]
+  simp
+
+@[bv_normalize]
+theorem BitVec.self_eq_add_right (a b : BitVec w) : (a == a + b) = (b == 0#w) := by
+  rw [Bool.eq_iff_iff]
+  simp
+
+@[bv_normalize]
+theorem BitVec.self_eq_add_left (a b : BitVec w) : (a == b + a) = (b == 0#w) := by
+  rw [Bool.eq_iff_iff]
+  simp
+
 end Frontend.Normalize
 end Std.Tactic.BVDecide
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index 0b36cbcb1f..5a28d192b0 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/tests/lean/run/bv_decide_rewriter.lean
@@ -110,6 +110,12 @@ example (x y z : BitVec 16) : (x + z == z + y) = (x == y) := by bv_normalize
 example (x y z : BitVec 16) : (z + x == y + z) = (x == y) := by bv_normalize
 example (x y z : BitVec 16) : (z + x == z + y) = (x == y) := by bv_normalize
 
+-- add_left_eq_self / add_right_eq_self
+example (x y : BitVec 16) : (x + y == x) = (y == 0) := by bv_normalize
+example (x y : BitVec 16) : (x + y == y) = (x == 0) := by bv_normalize
+example (x y : BitVec 16) : (x == x + y) = (y == 0) := by bv_normalize
+example (x y : BitVec 16) : (x == y + x) = (y == 0) := by bv_normalize
+
 section
 
 example (x y : BitVec 256) : x * y = y * x := by