bitvec_283 (#327)

This resolves #306. --------- Co-authored-by: Tobias Grosser <[email protected]>
opencompl · May 22, 2024 · 069ec67 · 069ec67
1 parent e23346c
commit 069ec67
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
@@ -211,6 +211,12 @@ lemma add_eq_xor (a b : BitVec 1) : a + b = a ^^^ b := by
   have hb : b = 0 ∨ b = 1 := width_one_cases _
   rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
 
+@[simp]
+lemma mul_eq_and (a b : BitVec 1) : a * b = a &&& b := by
+  have ha : a = 0 ∨ a = 1 := width_one_cases _
+  have hb : b = 0 ∨ b = 1 := width_one_cases _
+  rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp[h, h']))
+
 lemma toNat_neq_of_neq_ofNat {a : BitVec w} {n : Nat} (h : a ≠ n#w) : a.toNat ≠ n := by
   intros haeq
   have hn : n < 2 ^ w := by