From 69e33efa2f9a260119c97d64a29a4e41e7c1c4b7 Mon Sep 17 00:00:00 2001
From: Joe Hendrix <joe@lean-fro.org>
Date: Wed, 28 Feb 2024 16:25:40 -0800
Subject: [PATCH] chore: One sided BitVec.toNat equality lemmas (#3533)

---
 src/Init/Data/BitVec/Lemmas.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 6b6da02000..1a4c12bba1 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -198,6 +198,24 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
   apply eq_of_toNat_eq
   simp
 
+/-- Moves one-sided left toNat equality to BitVec equality. -/
+theorem toNat_eq_nat (x : BitVec w) (y : Nat)
+  : (x.toNat = y) ↔ (y < 2^w ∧ (x = y#w)) := by
+  apply Iff.intro
+  · intro eq
+    simp at eq
+    have lt := x.isLt
+    simp [eq] at lt
+    simp [←eq, lt, x.isLt]
+  · intro eq
+    simp [Nat.mod_eq_of_lt, eq]
+
+/-- Moves one-sided right toNat equality to BitVec equality. -/
+theorem nat_eq_toNat (x : BitVec w) (y : Nat)
+  : (y = x.toNat) ↔ (y < 2^w ∧ (x = y#w)) := by
+  rw [@eq_comm _ _ x.toNat]
+  apply toNat_eq_nat
+
 @[simp] theorem getLsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
     getLsb (zeroExtend' ge x) i = getLsb x i := by
   simp [getLsb, toNat_zeroExtend']