refactor: Defs and Lemmas files for Bitvec (#4899)

The `Core` file was just dumped from Lean3 core. I've split it into `Defs` and `Lemmas` in the style of the `List` folder for example.

Mathlib.lean

@@ -1154,8 +1154,8 @@ import Mathlib.Data.Analysis.Topology
 import Mathlib.Data.Array.Basic
 import Mathlib.Data.Array.Defs
 import Mathlib.Data.BinaryHeap
-import Mathlib.Data.Bitvec.Basic
-import Mathlib.Data.Bitvec.Core
+import Mathlib.Data.Bitvec.Defs
+import Mathlib.Data.Bitvec.Lemmas
 import Mathlib.Data.Bool.AllAny
 import Mathlib.Data.Bool.Basic
 import Mathlib.Data.Bool.Count

Mathlib/Data/Bitvec/Core.lean → Mathlib/Data/Bitvec/Defs.lean

@@ -303,57 +303,19 @@ protected def toNat {n : Nat} (v : Bitvec n) : Nat :=
   bitsToNat (toList v)
 #align bitvec.to_nat Bitvec.toNat
 
-theorem bitsToNat_toList {n : ℕ} (x : Bitvec n) : Bitvec.toNat x = bitsToNat (Vector.toList x) :=
-  rfl
-#align bitvec.bits_to_nat_to_list Bitvec.bitsToNat_toList
-
-attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.mul_comm Nat.mul_assoc
-
-attribute [local simp] Nat.zero_add Nat.add_zero Nat.one_mul Nat.mul_one Nat.zero_mul Nat.mul_zero
-
--- mul_left_comm
-theorem toNat_append {m : ℕ} (xs : Bitvec m) (b : Bool) :
-    Bitvec.toNat (xs++ₜb ::ᵥ nil) = Bitvec.toNat xs * 2 + Bitvec.toNat (b ::ᵥ nil) := by
-  cases' xs with xs P
-  simp [bitsToNat_toList]; clear P
-  unfold bitsToNat
-  -- porting note: was `unfold List.foldl`, which now unfolds to an ugly match
-  rw [List.foldl, List.foldl]
-  -- generalize the accumulator of foldl
-  generalize h : 0 = x
-  conv in addLsb x b =>
-    rw [← h]
-  clear h
-  simp
-  induction' xs with x xs xs_ih generalizing x
-  · simp
-    unfold addLsb
-    simp [Nat.mul_succ]
-  · simp
-    apply xs_ih
-#align bitvec.to_nat_append Bitvec.toNat_append
-
--- Porting Note: the mathlib3port version of the proof was :
---  simp [bits_to_nat_to_list]
---  unfold bits_to_nat add_lsb List.foldl cond
---  simp [cond_to_bool_mod_two]
-theorem bits_toNat_decide (n : ℕ) : Bitvec.toNat (decide (n % 2 = 1) ::ᵥ nil) = n % 2 := by
-  simp [bitsToNat_toList]
-  unfold bitsToNat addLsb List.foldl
-  simp [Nat.cond_decide_mod_two, -Bool.cond_decide]
-#align bitvec.bits_to_nat_to_bool Bitvec.bits_toNat_decide
-
-theorem ofNat_succ {k n : ℕ} :
-    Bitvec.ofNat (succ k) n = Bitvec.ofNat k (n / 2)++ₜdecide (n % 2 = 1) ::ᵥ nil :=
-  rfl
-#align bitvec.of_nat_succ Bitvec.ofNat_succ
-
-theorem toNat_ofNat {k n : ℕ} : Bitvec.toNat (Bitvec.ofNat k n) = n % 2 ^ k := by
-  induction' k with k ih generalizing n
-  · simp [Nat.mod_one]
-    rfl
-  · rw [ofNat_succ, toNat_append, ih, bits_toNat_decide, mod_pow_succ, Nat.mul_comm]
-#align bitvec.to_nat_of_nat Bitvec.toNat_ofNat
+instance (n : ℕ) : Preorder (Bitvec n) :=
+  Preorder.lift Bitvec.toNat
+
+/-- convert `fin` to `Bitvec` -/
+def ofFin {n : ℕ} (i : Fin <| 2 ^ n) : Bitvec n :=
+  Bitvec.ofNat _ i.val
+#align bitvec.of_fin Bitvec.ofFin
+
+/-- convert `Bitvec` to `fin` -/
+def toFin {n : ℕ} (i : Bitvec n) : Fin (2 ^ n) :=
+  i.toNat
+#align bitvec.to_fin Bitvec.toFin
+
 
 /-- Return the integer encoded by the input bitvector -/
 protected def toInt : ∀ {n : Nat}, Bitvec n → Int

Mathlib/Data/Bitvec/Basic.lean → Mathlib/Data/Bitvec/Lemmas.lean

@@ -8,7 +8,7 @@ Authors: Simon Hudon
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathlib.Data.Bitvec.Core
+import Mathlib.Data.Bitvec.Defs
 import Mathlib.Data.Fin.Basic
 import Mathlib.Tactic.NormNum
 
@@ -20,24 +20,68 @@ This file contains theorems about bitvectors and their coercions to
 -/
 namespace Bitvec
 
-instance (n : ℕ) : Preorder (Bitvec n) :=
-  Preorder.lift Bitvec.toNat
-
-/-- convert `fin` to `Bitvec` -/
-def ofFin {n : ℕ} (i : Fin <| 2 ^ n) : Bitvec n :=
-  Bitvec.ofNat _ i.val
-#align bitvec.of_fin Bitvec.ofFin
+open Nat
+
+theorem bitsToNat_toList {n : ℕ} (x : Bitvec n) : Bitvec.toNat x = bitsToNat (Vector.toList x) :=
+  rfl
+#align bitvec.bits_to_nat_to_list Bitvec.bitsToNat_toList
+
+attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.mul_comm Nat.mul_assoc
+
+attribute [local simp] Nat.zero_add Nat.add_zero Nat.one_mul Nat.mul_one Nat.zero_mul Nat.mul_zero
+
+local infixl:65 "++ₜ" => Vector.append
+
+-- mul_left_comm
+theorem toNat_append {m : ℕ} (xs : Bitvec m) (b : Bool) :
+    Bitvec.toNat (xs++ₜb ::ᵥ Vector.nil) =
+      Bitvec.toNat xs * 2 + Bitvec.toNat (b ::ᵥ Vector.nil) := by
+  cases' xs with xs P
+  simp [bitsToNat_toList]; clear P
+  unfold bitsToNat
+  -- porting note: was `unfold List.foldl`, which now unfolds to an ugly match
+  rw [List.foldl, List.foldl]
+  -- generalize the accumulator of foldl
+  generalize h : 0 = x
+  conv in addLsb x b =>
+    rw [← h]
+  clear h
+  simp
+  induction' xs with x xs xs_ih generalizing x
+  · simp
+    unfold addLsb
+    simp [Nat.mul_succ]
+  · simp
+    apply xs_ih
+#align bitvec.to_nat_append Bitvec.toNat_append
+
+-- Porting Note: the mathlib3port version of the proof was :
+--  simp [bits_to_nat_to_list]
+--  unfold bits_to_nat add_lsb List.foldl cond
+--  simp [cond_to_bool_mod_two]
+theorem bits_toNat_decide (n : ℕ) : Bitvec.toNat (decide (n % 2 = 1) ::ᵥ Vector.nil) = n % 2 := by
+  simp [bitsToNat_toList]
+  unfold bitsToNat addLsb List.foldl
+  simp [Nat.cond_decide_mod_two, -Bool.cond_decide]
+#align bitvec.bits_to_nat_to_bool Bitvec.bits_toNat_decide
+
+theorem ofNat_succ {k n : ℕ} :
+    Bitvec.ofNat k.succ n = Bitvec.ofNat k (n / 2)++ₜdecide (n % 2 = 1) ::ᵥ Vector.nil :=
+  rfl
+#align bitvec.of_nat_succ Bitvec.ofNat_succ
+
+theorem toNat_ofNat {k n : ℕ} : Bitvec.toNat (Bitvec.ofNat k n) = n % 2 ^ k := by
+  induction' k with k ih generalizing n
+  · simp [Nat.mod_one]
+    rfl
+  · rw [ofNat_succ, toNat_append, ih, bits_toNat_decide, mod_pow_succ, Nat.mul_comm]
+#align bitvec.to_nat_of_nat Bitvec.toNat_ofNat
 
 theorem ofFin_val {n : ℕ} (i : Fin <| 2 ^ n) : (ofFin i).toNat = i.val := by
   rw [ofFin, toNat_ofNat, Nat.mod_eq_of_lt]
   apply i.is_lt
 #align bitvec.of_fin_val Bitvec.ofFin_val
 
-/-- convert `Bitvec` to `fin` -/
-def toFin {n : ℕ} (i : Bitvec n) : Fin (2 ^ n) :=
-  i.toNat
-#align bitvec.to_fin Bitvec.toFin
-
 theorem addLsb_eq_twice_add_one {x b} : addLsb x b = 2 * x + cond b 1 0 := by
   simp [addLsb, two_mul]
 #align bitvec.add_lsb_eq_twice_add_one Bitvec.addLsb_eq_twice_add_one

Mathlib/Data/Num/Bitwise.lean

@@ -9,7 +9,7 @@ Authors: Mario Carneiro
 ! if you have ported upstream changes.
 -/
 import Mathlib.Data.Num.Basic
-import Mathlib.Data.Bitvec.Core
+import Mathlib.Data.Bitvec.Defs
 
 /-!
 # Bitwise operations using binary representation of integers