From 84da11335540654028ac57cd0be32ae43586de89 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 28 Feb 2025 17:04:09 +0100
Subject: [PATCH] feat: add all bitwuzla level 1 if rewrites to bv_decide
 (#7275)

This PR adds all level 1 rewrites from Bitwuzla to the preprocessor of
bv_decide.
---
 src/Std/Tactic/BVDecide/Normalize/Bool.lean | 148 +++++++++++++++++++
 tests/lean/run/bv_decide_rewriter.lean      | 149 ++++++++++++++++++++
 2 files changed, 297 insertions(+)

diff --git a/src/Std/Tactic/BVDecide/Normalize/Bool.lean b/src/Std/Tactic/BVDecide/Normalize/Bool.lean
index 096646d00e..1627036c46 100644
--- a/src/Std/Tactic/BVDecide/Normalize/Bool.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/Bool.lean
@@ -6,6 +6,7 @@ Authors: Henrik Böving
 prelude
 import Init.SimpLemmas
 import Init.Data.Bool
+import Init.Data.BitVec.Lemmas
 
 /-!
 This module contains the `Bool` simplifying part of the `bv_normalize` simp set.
@@ -54,6 +55,153 @@ theorem Bool.not_xor : ∀ (a b : Bool), !(a ^^ b) = (a == b) := by decide
 @[bv_normalize]
 theorem Bool.or_elim : ∀ (a b : Bool), (a || b) = !(!a && !b) := by decide
 
+@[bv_normalize]
+theorem Bool.not_beq_one : ∀ (a : BitVec 1), (!(a == 1#1)) = (a == 0#1) := by
+  decide
+
+@[bv_normalize]
+theorem Bool.not_beq_zero : ∀ (a : BitVec 1), (!(a == 0#1)) = (a == 1#1) := by
+  decide
+
+@[bv_normalize]
+theorem Bool.not_one_beq : ∀ (a : BitVec 1), (!(1#1 == a)) = (a == 0#1) := by
+  decide
+
+@[bv_normalize]
+theorem Bool.not_zero_beq : ∀ (a : BitVec 1), (!(0#1 == a)) = (a == 1#1) := by
+  decide
+
+@[bv_normalize]
+theorem Bool.ite_same_then : ∀ (c t e : Bool), ((bif c then t else e) == t) = (c || (t == e)) := by
+  decide
+
+@[bv_normalize]
+theorem Bool.ite_same_then' : ∀ (c t e : Bool), (t == (bif c then t else e)) = (c || (t == e)) := by
+  decide
+
+@[bv_normalize]
+theorem Bool.ite_same_else : ∀ (c t e : Bool), ((bif c then t else e) == e) = (!c || (t == e)) := by
+  decide
+
+@[bv_normalize]
+theorem Bool.ite_same_else' :
+    ∀ (c t e : Bool), (e == (bif c then t else e)) = (!c || (t == e)) := by
+  decide
+
+@[bv_normalize]
+theorem BitVec.ite_same_then :
+    ∀ (c : Bool) (t e : BitVec w), ((bif c then t else e) == t) = (c || (t == e)) := by
+  intro c t e
+  cases c <;> simp [BEq.comm (a := t) (b := e)]
+
+@[bv_normalize]
+theorem BitVec.ite_same_then' :
+    ∀ (c : Bool) (t e : BitVec w), (t == (bif c then t else e)) = (c || (t == e)) := by
+  intro c t e
+  cases c <;> simp
+
+@[bv_normalize]
+theorem BitVec.ite_same_else :
+    ∀ (c : Bool) (t e : BitVec w), ((bif c then t else e) == e) = (!c || (t == e)) := by
+  intro c t e
+  cases c <;> simp
+
+@[bv_normalize]
+theorem BitVec.ite_same_else' :
+    ∀ (c : Bool) (t e : BitVec w), (e == (bif c then t else e)) = (!c || (t == e)) := by
+  intro c t e
+  cases c <;> simp [BEq.comm (a := t) (b := e)]
+
+@[bv_normalize]
+theorem Bool.ite_then_ite (cond : Bool) {a b c : α} :
+    (bif cond then (bif cond then a else b) else c) = (bif cond then a else c) := by
+  cases cond <;> simp
+
+@[bv_normalize]
+theorem Bool.ite_then_not_ite (cond : Bool) {a b c : Bool} :
+    (bif cond then !(bif cond then a else b) else c) = (bif cond then !a else c) := by
+  cases cond <;> simp
+
+@[bv_normalize]
+theorem BitVec.ite_then_not_ite (cond : Bool) {a b c : BitVec w} :
+    (bif cond then ~~~(bif cond then a else b) else c) = (bif cond then ~~~a else c) := by
+  cases cond <;> simp
+
+@[bv_normalize]
+theorem Bool.ite_else_ite (cond : Bool) {a b c : α} :
+    (bif cond then a else (bif cond then b else c)) = (bif cond then a else c) := by
+  cases cond <;> simp
+
+@[bv_normalize]
+theorem Bool.ite_else_not_ite (cond : Bool) {a b c : Bool} :
+    (bif cond then a else !(bif cond then b else c)) = (bif cond then a else !c) := by
+  cases cond <;> simp
+
+@[bv_normalize]
+theorem BitVec.ite_else_not_ite (cond : Bool) {a b c : BitVec w} :
+    (bif cond then a else ~~~(bif cond then b else c)) = (bif cond then a else ~~~c) := by
+  cases cond <;> simp
+
+@[bv_normalize]
+theorem Bool.ite_then_ite' (c0 c1 : Bool) {a b : α} :
+    (bif c0 then (bif c1 then a else b) else a) = (bif c0 && !c1 then b else a) := by
+  cases c0 <;> cases c1 <;> simp
+
+@[bv_normalize]
+theorem Bool.ite_then_not_ite' (c0 c1 : Bool) {a b : Bool} :
+    (bif c0 then !(bif c1 then !a else b) else a) = (bif c0 && !c1 then !b else a) := by
+  cases c0 <;> cases c1 <;> simp
+
+@[bv_normalize]
+theorem BitVec.ite_then_not_ite' (c0 c1 : Bool) {a b : BitVec w} :
+    (bif c0 then ~~~(bif c1 then ~~~a else b) else a) = (bif c0 && !c1 then ~~~b else a) := by
+  cases c0 <;> cases c1 <;> simp
+
+@[bv_normalize]
+theorem Bool.ite_else_ite' (c0 c1 : Bool) {a b : α} :
+    (bif c0 then a else (bif c1 then a else b)) = (bif !c0 && !c1 then b else a) := by
+  cases c0 <;> cases c1 <;> simp
+
+@[bv_normalize]
+theorem Bool.ite_else_not_ite' (c0 c1 : Bool) {a b : Bool} :
+    (bif c0 then a else !(bif c1 then !a else b)) = (bif !c0 && !c1 then !b else a) := by
+  cases c0 <;> cases c1 <;> simp
+
+@[bv_normalize]
+theorem BitVec.ite_else_not_ite' (c0 c1 : Bool) {a b : BitVec w} :
+    (bif c0 then a else ~~~(bif c1 then ~~~a else b)) = (bif !c0 && !c1 then ~~~b else a) := by
+  cases c0 <;> cases c1 <;> simp
+
+@[bv_normalize]
+theorem Bool.ite_then_ite'' (c0 c1 : Bool) {a b : α} :
+    (bif c0 then (bif c1 then b else a) else a) = (bif c0 && c1 then b else a) := by
+  cases c0 <;> cases c1 <;> simp
+
+@[bv_normalize]
+theorem Bool.ite_then_not_ite'' (c0 c1 : Bool) {a b : Bool} :
+    (bif c0 then !(bif c1 then b else !a) else a) = (bif c0 && c1 then !b else a) := by
+  cases c0 <;> cases c1 <;> simp
+
+@[bv_normalize]
+theorem BitVec.ite_then_not_ite'' (c0 c1 : Bool) {a b : BitVec w} :
+    (bif c0 then ~~~(bif c1 then b else ~~~a) else a) = (bif c0 && c1 then ~~~b else a) := by
+  cases c0 <;> cases c1 <;> simp
+
+@[bv_normalize]
+theorem Bool.ite_else_ite'' (c0 c1 : Bool) {a b : α} :
+    (bif c0 then a else (bif c1 then b else a)) = (bif !c0 && c1 then b else a) := by
+  cases c0 <;> cases c1 <;> simp
+
+@[bv_normalize]
+theorem Bool.ite_else_not_ite'' (c0 c1 : Bool) {a b : Bool} :
+    (bif c0 then a else !(bif c1 then b else !a)) = (bif !c0 && c1 then !b else a) := by
+  cases c0 <;> cases c1 <;> simp
+
+@[bv_normalize]
+theorem BitVec.ite_else_not_ite'' (c0 c1 : Bool) {a b : BitVec w} :
+    (bif c0 then a else ~~~(bif c1 then b else ~~~a )) = (bif !c0 && c1 then ~~~b else a) := by
+  cases c0 <;> cases c1 <;> simp
+
 theorem Bool.and_left (lhs rhs : Bool) (h : (lhs && rhs) = true) : lhs = true := by
   revert lhs rhs
   decide
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index 1d83e867de..c39dd2b8ba 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/tests/lean/run/bv_decide_rewriter.lean
@@ -282,6 +282,155 @@ example (a : BitVec 16) : a * 8#16 = a <<< 3 := by
 example (a : BitVec 16) : a + a = a <<< 1 := by
   bv_normalize
 
+-- NOT_EQUAL_BV1_BOOL
+example : ∀ (a : Bool), (!(a == true)) = (a == false) := by
+  bv_normalize
+
+example : ∀ (a : Bool), (!(a == false)) = (a == true) := by
+  bv_normalize
+
+example : ∀ (a : Bool), (!(true == a)) = (a == false) := by
+  bv_normalize
+
+example : ∀ (a : Bool), (!(false == a)) = (a == true) := by
+  bv_normalize
+
+example : ∀ (a : BitVec 1), (!(a == 1#1)) = (a == 0#1) := by
+  bv_normalize
+
+example : ∀ (a : BitVec 1), (!(a == 0#1)) = (a == 1#1) := by
+  bv_normalize
+
+example : ∀ (a : BitVec 1), (!(1#1 == a)) = (a == 0#1) := by
+  bv_normalize
+
+example : ∀ (a : BitVec 1), (!(0#1 == a)) = (a == 1#1) := by
+  bv_normalize
+
+-- ITE_SAME
+example : ∀ (c t e : Bool), ((bif c then t else e) == t) = (c || (t == e)) := by
+  bv_normalize
+
+example : ∀ (c t e : Bool), (t == (bif c then t else e)) = (c || (t == e)) := by
+  bv_normalize
+
+example : ∀ (c t e : Bool), ((bif c then t else e) == e) = (!c || (t == e)) := by
+  bv_normalize
+
+example : ∀ (c t e : Bool), (e == (bif c then t else e)) = (!c || (t == e)) := by
+  bv_normalize
+
+example : ∀ (c : Bool) (t e : BitVec 8), ((bif c then t else e) == t) = (c || (t == e)) := by
+  bv_normalize
+
+example : ∀ (c : Bool) (t e : BitVec 8), (t == (bif c then t else e)) = (c || (t == e)) := by
+  bv_normalize
+
+example : ∀ (c : Bool) (t e : BitVec 8), ((bif c then t else e) == e) = (!c || (t == e)) := by
+  bv_normalize
+
+example : ∀ (c : Bool) (t e : BitVec 8), (e == (bif c then t else e)) = (!c || (t == e)) := by
+  bv_normalize
+
+example (c : Bool) : ((if c then 1#1 else 0#1) == 1#1) ↔ c := by
+  bv_normalize
+
+-- ITE_THEN_ITE_1
+example (cond : Bool) {a b c d : Bool}
+    (h : (bif cond then (bif cond then a else b) else c) = d) :
+    (bif cond then a else c) = d := by
+  bv_normalize
+
+example (cond : Bool) {a b c d : Bool}
+    (h : (bif cond then !(bif cond then a else b) else c) = d) :
+    (bif cond then !a else c) = d := by
+  bv_normalize
+
+example (cond : Bool) {a b c d : BitVec 8}
+    (h : (bif cond then ~~~(bif cond then a else b) else c) = d) :
+    (bif cond then ~~~a else c) = d := by
+  bv_normalize
+
+-- ITE_ELSE_ITE_1
+example (cond : Bool) {a b c d : Bool}
+    (h : (bif cond then a else (bif cond then b else c)) = d) :
+    (bif cond then a else c) = d := by
+  bv_normalize
+
+example (cond : Bool) {a b c d : Bool}
+    (h : (bif cond then a else !(bif cond then b else c)) = d) :
+    (bif cond then a else !c) = d := by
+  bv_normalize
+
+example (cond : Bool) {a b c d : BitVec 8}
+    (h : (bif cond then a else ~~~(bif cond then b else c)) = d) :
+    (bif cond then a else ~~~c) = d := by
+  bv_normalize
+
+-- ITE_THEN_ITE_2
+example (c0 c1 : Bool) {a b d : Bool}
+    (h : (bif c0 then (bif c1 then a else b) else a) = d) :
+    (bif c0 && !c1 then b else a) = d := by
+  bv_normalize
+
+example (c0 c1 : Bool) {a b d : Bool}
+    (h : (bif c0 then !(bif c1 then !a else b) else a) = d) :
+    (bif c0 && !c1 then !b else a) = d := by
+  bv_normalize
+
+example (c0 c1 : Bool) {a b d : BitVec 8}
+    (h : (bif c0 then ~~~(bif c1 then ~~~a else b) else a) = d) :
+    (bif c0 && !c1 then ~~~b else a) = d := by
+  bv_normalize
+
+-- ITE_ELSE_ITE_2
+example (c0 c1 : Bool) {a b d : Bool}
+    (h : (bif c0 then a else (bif c1 then a else b)) = d) :
+    (bif !c0 && !c1 then b else a) = d := by
+  bv_normalize
+
+example (c0 c1 : Bool) {a b d : Bool}
+    (h : (bif c0 then a else !(bif c1 then !a else b)) = d) :
+    (bif !c0 && !c1 then !b else a) = d := by
+  bv_normalize
+
+example (c0 c1 : Bool) {a b d : BitVec 8}
+    (h : (bif c0 then a else ~~~(bif c1 then ~~~a else b)) = d) :
+    (bif !c0 && !c1 then ~~~b else a) = d := by
+  bv_normalize
+
+-- ITE_THEN_ITE_3
+example (c0 c1 : Bool) {a b d : Bool}
+    (h : (bif c0 then (bif c1 then b else a) else a) = d) :
+    (bif c0 && c1 then b else a) = d := by
+  bv_normalize
+
+example (c0 c1 : Bool) {a b d : Bool}
+    (h : (bif c0 then !(bif c1 then b else !a) else a) = d) :
+    (bif c0 && c1 then !b else a) = d := by
+  bv_normalize
+
+example (c0 c1 : Bool) {a b d : BitVec 8}
+    (h : (bif c0 then ~~~(bif c1 then b else ~~~a) else a) = d) :
+    (bif c0 && c1 then ~~~b else a) = d := by
+  bv_normalize
+
+-- ITE_ELSE_ITE_3
+example (c0 c1 : Bool) {a b d : Bool}
+    (h : (bif c0 then a else (bif c1 then b else a)) = d) :
+    (bif !c0 && c1 then b else a) = d := by
+  bv_normalize
+
+example (c0 c1 : Bool) {a b d : Bool}
+    (h : (bif c0 then a else !(bif c1 then b else !a)) = d) :
+    (bif !c0 && c1 then !b else a) = d := by
+  bv_normalize
+
+example (c0 c1 : Bool) {a b d : BitVec 8}
+    (h : (bif c0 then a else ~~~(bif c1 then b else ~~~a)) = d) :
+    (bif !c0 && c1 then ~~~b else a) = d := by
+  bv_normalize
+
 section
 
 example (x y : BitVec 256) : x * y = y * x := by