From a2a73e9611ddccbabbc3fe274c28b1da9e89b594 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Wed, 3 Jul 2024 03:28:36 +0200
Subject: [PATCH] feat: USize.and_toNat (#4629)

Split from #4583
---
 src/Init/Data/Fin/Bitwise.lean  | 15 +++++++++++++++
 src/Init/Data/UInt.lean         |  1 +
 src/Init/Data/UInt/Bitwise.lean | 24 ++++++++++++++++++++++++
 3 files changed, 40 insertions(+)
 create mode 100644 src/Init/Data/Fin/Bitwise.lean
 create mode 100644 src/Init/Data/UInt/Bitwise.lean

diff --git a/src/Init/Data/Fin/Bitwise.lean b/src/Init/Data/Fin/Bitwise.lean
new file mode 100644
index 0000000000..90aa01dbdd
--- /dev/null
+++ b/src/Init/Data/Fin/Bitwise.lean
@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+prelude
+import Init.Data.Nat.Bitwise
+import Init.Data.Fin.Basic
+
+namespace Fin
+
+@[simp] theorem and_val (a b : Fin n) : (a &&& b).val = a.val &&& b.val :=
+  Nat.mod_eq_of_lt (Nat.lt_of_le_of_lt Nat.and_le_left a.isLt)
+
+end Fin
diff --git a/src/Init/Data/UInt.lean b/src/Init/Data/UInt.lean
index 0b28b72cf1..1eb20a30e7 100644
--- a/src/Init/Data/UInt.lean
+++ b/src/Init/Data/UInt.lean
@@ -7,3 +7,4 @@ prelude
 import Init.Data.UInt.Basic
 import Init.Data.UInt.Log2
 import Init.Data.UInt.Lemmas
+import Init.Data.UInt.Bitwise
diff --git a/src/Init/Data/UInt/Bitwise.lean b/src/Init/Data/UInt/Bitwise.lean
new file mode 100644
index 0000000000..4c3a04571a
--- /dev/null
+++ b/src/Init/Data/UInt/Bitwise.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+prelude
+import Init.Data.UInt.Basic
+import Init.Data.Fin.Bitwise
+
+set_option hygiene false in
+macro "declare_bitwise_uint_theorems" typeName:ident : command =>
+`(
+namespace $typeName
+
+@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := Fin.and_val ..
+
+end $typeName
+)
+
+declare_bitwise_uint_theorems UInt8
+declare_bitwise_uint_theorems UInt16
+declare_bitwise_uint_theorems UInt32
+declare_bitwise_uint_theorems UInt64
+declare_bitwise_uint_theorems USize