feat: tag lemmas

src/Init/Data/UInt/Bitwise.lean

@@ -13,17 +13,17 @@ macro "declare_bitwise_uint_theorems" typeName:ident bits:term:arg : command =>
 `(
 namespace $typeName
 
-@[simp] protected theorem toBitVec_add {a b : $typeName} : (a + b).toBitVec = a.toBitVec + b.toBitVec := rfl
-@[simp] protected theorem toBitVec_sub {a b : $typeName} : (a - b).toBitVec = a.toBitVec - b.toBitVec := rfl
-@[simp] protected theorem toBitVec_mul {a b : $typeName} : (a * b).toBitVec = a.toBitVec * b.toBitVec := rfl
-@[simp] protected theorem toBitVec_div {a b : $typeName} : (a / b).toBitVec = a.toBitVec / b.toBitVec := rfl
-@[simp] protected theorem toBitVec_mod {a b : $typeName} : (a % b).toBitVec = a.toBitVec % b.toBitVec := rfl
-@[simp] protected theorem toBitVec_not {a : $typeName} : (~~~a).toBitVec = ~~~a.toBitVec := rfl
-@[simp] protected theorem toBitVec_and (a b : $typeName) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec := rfl
-@[simp] protected theorem toBitVec_or (a b : $typeName) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec := rfl
-@[simp] protected theorem toBitVec_xor (a b : $typeName) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec := rfl
-@[simp] protected theorem toBitVec_shiftLeft (a b : $typeName) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % $bits) := rfl
-@[simp] protected theorem toBitVec_shiftRight (a b : $typeName) : (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % $bits) := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_add {a b : $typeName} : (a + b).toBitVec = a.toBitVec + b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_sub {a b : $typeName} : (a - b).toBitVec = a.toBitVec - b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_mul {a b : $typeName} : (a * b).toBitVec = a.toBitVec * b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_div {a b : $typeName} : (a / b).toBitVec = a.toBitVec / b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_mod {a b : $typeName} : (a % b).toBitVec = a.toBitVec % b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_not {a : $typeName} : (~~~a).toBitVec = ~~~a.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_and (a b : $typeName) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_or (a b : $typeName) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_xor (a b : $typeName) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_shiftLeft (a b : $typeName) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % $bits) := rfl
+@[simp, int_toBitVec] protected theorem toBitVec_shiftRight (a b : $typeName) : (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % $bits) := rfl
 
 @[simp] protected theorem toNat_and (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := by simp [toNat]
 @[simp] protected theorem toNat_or (a b : $typeName) : (a ||| b).toNat = a.toNat ||| b.toNat := by simp [toNat]
@@ -44,27 +44,27 @@ declare_bitwise_uint_theorems UInt32 32
 declare_bitwise_uint_theorems UInt64 64
 declare_bitwise_uint_theorems USize System.Platform.numBits
 
-@[simp]
+@[simp, int_toBitVec]
 theorem Bool.toBitVec_toUInt8 {b : Bool} :
     b.toUInt8.toBitVec = (BitVec.ofBool b).setWidth 8 := by
   cases b <;> simp [toUInt8]
 
-@[simp]
+@[simp, int_toBitVec]
 theorem Bool.toBitVec_toUInt16 {b : Bool} :
     b.toUInt16.toBitVec = (BitVec.ofBool b).setWidth 16 := by
   cases b <;> simp [toUInt16]
 
-@[simp]
+@[simp, int_toBitVec]
 theorem Bool.toBitVec_toUInt32 {b : Bool} :
     b.toUInt32.toBitVec = (BitVec.ofBool b).setWidth 32 := by
   cases b <;> simp [toUInt32]
 
-@[simp]
+@[simp, int_toBitVec]
 theorem Bool.toBitVec_toUInt64 {b : Bool} :
     b.toUInt64.toBitVec = (BitVec.ofBool b).setWidth 64 := by
   cases b <;> simp [toUInt64]
 
-@[simp]
+@[simp, int_toBitVec]
 theorem Bool.toBitVec_toUSize {b : Bool} :
     b.toUSize.toBitVec = (BitVec.ofBool b).setWidth System.Platform.numBits := by
   cases b

src/Init/Data/UInt/Lemmas.lean

@@ -41,9 +41,9 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
   theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
     rw [toNat, toBitVec_eq_of_lt h]
 
-  theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl
+  @[int_toBitVec] theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl
 
-  theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
+  @[int_toBitVec] theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
 
   theorem le_iff_toNat_le {a b : $typeName} : a ≤ b ↔ a.toNat ≤ b.toNat := .rfl
 
@@ -74,6 +74,11 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
   protected theorem toBitVec_inj {a b : $typeName} : a.toBitVec = b.toBitVec ↔ a = b :=
     Iff.intro eq_of_toBitVec_eq toBitVec_eq_of_eq
 
+  open $typeName (eq_of_toBitVec_eq toBitVec_eq_of_eq) in
+  @[int_toBitVec]
+  protected theorem eq_iff_toBitVec_eq {a b : $typeName} : a = b ↔ a.toBitVec = b.toBitVec :=
+    Iff.intro toBitVec_eq_of_eq eq_of_toBitVec_eq
+
   open $typeName (eq_of_toBitVec_eq) in
   protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by
     rcases a with ⟨⟨_⟩⟩; rcases b with ⟨⟨_⟩⟩; simp_all [val]
@@ -82,10 +87,19 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
   protected theorem val_inj {a b : $typeName} : a.val = b.val ↔ a = b :=
     Iff.intro eq_of_val_eq (congrArg val)
 
+  open $typeName (eq_of_toBitVec_eq) in
+  protected theorem toBitVec_ne_of_ne {a b : $typeName} (h : a ≠ b) : a.toBitVec ≠ b.toBitVec :=
+    fun h' => h (eq_of_toBitVec_eq h')
+
   open $typeName (toBitVec_eq_of_eq) in
   protected theorem ne_of_toBitVec_ne {a b : $typeName} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b :=
     fun h' => absurd (toBitVec_eq_of_eq h') h
 
+  open $typeName (ne_of_toBitVec_ne toBitVec_ne_of_ne) in
+  @[int_toBitVec]
+  protected theorem ne_iff_toBitVec_ne {a b : $typeName} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec :=
+    Iff.intro toBitVec_ne_of_ne ne_of_toBitVec_ne
+
   open $typeName (ne_of_toBitVec_ne) in
   protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := by
     apply ne_of_toBitVec_ne
@@ -159,7 +173,7 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
   @[simp]
   theorem val_ofNat (n : Nat) : val (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
 
-  @[simp]
+  @[simp, int_toBitVec]
   theorem toBitVec_ofNat (n : Nat) : toBitVec (no_index (OfNat.ofNat n)) = BitVec.ofNat _ n := rfl
 
   @[simp]

tests/lean/run/int_toBitVec.lean

@@ -0,0 +1,44 @@
+example (a b c d e : UInt8) : ((a + (b * c)) = (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec = b.toBitVec - d.toBitVec / e.toBitVec) := by
+  simp only [int_toBitVec]
+
+example (a b c d e : UInt16) : ((a + (b * c)) = (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec = b.toBitVec - d.toBitVec / e.toBitVec) := by
+  simp only [int_toBitVec]
+
+example (a b c d e : UInt32) : ((a + (b * c)) = (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec = b.toBitVec - d.toBitVec / e.toBitVec) := by
+  simp only [int_toBitVec]
+
+example (a b c d e : UInt64) : ((a + (b * c)) = (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec = b.toBitVec - d.toBitVec / e.toBitVec) := by
+  simp only [int_toBitVec]
+
+example (a b c d e : USize) : ((a + (b * c)) = (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec = b.toBitVec - d.toBitVec / e.toBitVec) := by
+  simp only [int_toBitVec]
+
+example (a b c d e : UInt8) : ((a + (b * c)) < (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec < b.toBitVec - d.toBitVec / e.toBitVec) := by
+  simp only [int_toBitVec]
+
+example (a b c d e : UInt16) : ((a + (b * c)) < (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec < b.toBitVec - d.toBitVec / e.toBitVec) := by
+  simp only [int_toBitVec]
+
+example (a b c d e : UInt32) : ((a + (b * c)) < (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec < b.toBitVec - d.toBitVec / e.toBitVec) := by
+  simp only [int_toBitVec]
+
+example (a b c d e : UInt64) : ((a + (b * c)) < (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec < b.toBitVec - d.toBitVec / e.toBitVec) := by
+  simp only [int_toBitVec]
+
+example (a b c d e : USize) : ((a + (b * c)) < (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec < b.toBitVec - d.toBitVec / e.toBitVec) := by
+  simp only [int_toBitVec]
+
+example (a b c d e : UInt8) : ((a + (b * c)) ≤ (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec ≤ b.toBitVec - d.toBitVec / e.toBitVec) := by
+  simp only [int_toBitVec]
+
+example (a b c d e : UInt16) : ((a + (b * c)) ≤ (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec ≤ b.toBitVec - d.toBitVec / e.toBitVec) := by
+  simp only [int_toBitVec]
+
+example (a b c d e : UInt32) : ((a + (b * c)) ≤ (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec ≤ b.toBitVec - d.toBitVec / e.toBitVec) := by
+  simp only [int_toBitVec]
+
+example (a b c d e : UInt64) : ((a + (b * c)) ≤ (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec ≤ b.toBitVec - d.toBitVec / e.toBitVec) := by
+  simp only [int_toBitVec]
+
+example (a b c d e : USize) : ((a + (b * c)) ≤ (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec ≤ b.toBitVec - d.toBitVec / e.toBitVec) := by
+  simp only [int_toBitVec]