Merge remote-tracking branch 'origin/master' into ToInt_instances

src/Init/Grind/Module/Basic.lean

@@ -240,7 +240,7 @@ end NoNatZeroDivisors
 instance [ToInt α (some lo) (some hi)] [IntModule α] [ToInt.Zero α (some lo) (some hi)] [ToInt.Add α (some lo) (some hi)] : ToInt.Neg α (some lo) (some hi) where
   toInt_neg x := by
     have := (ToInt.Add.toInt_add (-x) x).symm
-    rw [IntModule.neg_add_cancel, ToInt.Zero.toInt_zero] at this
+    rw [IntModule.neg_add_cancel, ToInt.Zero.toInt_zero, ← ToInt.Zero.wrap_zero (α := α)] at this
     rw [ToInt.wrap_eq_wrap_iff] at this
     simp at this
     rw [← ToInt.wrap_toInt]

src/Init/Grind/ToInt.lean

@@ -25,10 +25,19 @@ These typeclasses are used solely in the `grind` tactic to lift linear inequalit
 
 namespace Lean.Grind
 
+/--
+`ToInt α lo? hi?` asserts that `α` can be embedded faithfully into the interval `[lo, hi)` in the integers,
+when `lo? = some lo` and `hi? = some hi`, and similarly can be embedded into a half-infinite or infinite interval when
+`lo? = none` or `hi? = none`.
+-/
 class ToInt (α : Type u) (lo? hi? : outParam (Option Int)) where
+  /-- The embedding function. -/
   toInt : α → Int
+  /-- The embedding function is injective. -/
   toInt_inj : ∀ x y, toInt x = toInt y → x = y
+  /-- The lower bound, if present, gives a lower bound on the embedding function. -/
   le_toInt : lo? = some lo → lo ≤ toInt x
+  /-- The upper bound, if present, gives an upper bound on the embedding function. -/
   toInt_lt : hi? = some hi → toInt x < hi
 
 @[simp]
@@ -37,31 +46,102 @@ def ToInt.wrap (lo? hi? : Option Int) (x : Int) : Int :=
   | some lo, some hi => (x - lo) % (hi - lo) + lo
   | _, _ => x
 
+/--
+The embedding into the integers takes `0` to `0`.
+-/
 class ToInt.Zero (α : Type u) [Zero α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
-  toInt_zero : toInt (0 : α) = wrap lo? hi? 0
+  /-- The embedding takes `0` to `0`. -/
+  toInt_zero : toInt (0 : α) = 0
 
+/--
+The embedding into the integers takes addition to addition, wrapped into the range interval.
+-/
 class ToInt.Add (α : Type u) [Add α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  /-- The embedding takes addition to addition, wrapped into the range interval. -/
   toInt_add : ∀ x y : α, toInt (x + y) = wrap lo? hi? (toInt x + toInt y)
 
+/--
+The embedding into the integers takes negation to negation, wrapped into the range interval.
+-/
 class ToInt.Neg (α : Type u) [Neg α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  /-- The embedding takes negation to negation, wrapped into the range interval. -/
   toInt_neg : ∀ x : α, toInt (-x) = wrap lo? hi? (-toInt x)
 
+/--
+The embedding into the integers takes subtraction to subtraction, wrapped into the range interval.
+-/
 class ToInt.Sub (α : Type u) [Sub α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  /-- The embedding takes subtraction to subtraction, wrapped into the range interval. -/
   toInt_sub : ∀ x y : α, toInt (x - y) = wrap lo? hi? (toInt x - toInt y)
 
+/--
+The embedding into the integers takes multiplication to multiplication, wrapped into the range interval.
+-/
+class ToInt.Mul (α : Type u) [Mul α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  /-- The embedding takes multiplication to multiplication, wrapped into the range interval. -/
+  toInt_mul : ∀ x y : α, toInt (x * y) = wrap lo? hi? (toInt x * toInt y)
+
+/--
+The embedding into the integers takes exponentiation to exponentiation, wrapped into the range interval.
+-/
+class ToInt.Pow (α : Type u) [Pow α Nat] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  /-- The embedding takes exponentiation to exponentiation, wrapped into the range interval. -/
+  toInt_pow : ∀ x : α, ∀ n : Nat, toInt (x ^ n) = wrap lo? hi? (toInt x ^ n)
+
+/--
+The embedding into the integers takes modulo to modulo (without needing to wrap into the range interval).
+-/
 class ToInt.Mod (α : Type u) [Mod α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
-  /-- One might expect a `wrap` on the right hand side,
-  but in practice this stronger statement is usually true. -/
+  /--
+  The embedding takes modulo to modulo (without needing to wrap into the range interval).
+  One might expect a `wrap` on the right hand side,
+  but in practice this stronger statement is usually true.
+  -/
   toInt_mod : ∀ x y : α, toInt (x % y) = toInt x % toInt y
 
+/--
+The embedding into the integers takes division to division, wrapped into the range interval.
+-/
+class ToInt.Div (α : Type u) [Div α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  /--
+  The embedding takes division to division (without needing to wrap into the range interval).
+  One might expect a `wrap` on the right hand side,
+  but in practice this stronger statement is usually true.
+  -/
+  toInt_div : ∀ x y : α, toInt (x / y) = toInt x / toInt y
+
+/--
+The embedding into the integers is monotone.
+-/
 class ToInt.LE (α : Type u) [LE α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  /-- The embedding is monotone with respect to `≤`. -/
   le_iff : ∀ x y : α, x ≤ y ↔ toInt x ≤ toInt y
 
+/--
+The embedding into the integers is strictly monotone.
+-/
 class ToInt.LT (α : Type u) [LT α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
+  /-- The embedding is strictly monotone with respect to `<`. -/
   lt_iff : ∀ x y : α, x < y ↔ toInt x < toInt y
 
 /-! ## Helper theorems -/
 
+theorem ToInt.Zero.wrap_zero (lo? hi? : Option Int) [_root_.Zero α] [ToInt α lo? hi?] [ToInt.Zero α lo? hi?] :
+    ToInt.wrap lo? hi? (0 : Int) = 0 := by
+  match hlo : lo?, hhi : hi? with
+  | some lo, some hi =>
+    subst hlo hhi
+    have h := ToInt.Zero.toInt_zero (α := α)
+    have hlo:= ToInt.le_toInt (x := (0 : α)) (lo := lo) rfl
+    have hhi := ToInt.toInt_lt (x := (0 : α)) (hi := hi) rfl
+    simp only [h] at hlo hhi
+    unfold wrap
+    simp only [Int.zero_sub]
+    rw [Int.emod_eq_of_lt] <;> all_goals omega
+  | some lo, none
+  | none, some hi
+  | none, none => rfl
+
 theorem ToInt.wrap_add (lo? hi? : Option Int) (x y : Int) :
     ToInt.wrap lo? hi? (x + y) = ToInt.wrap lo? hi? (ToInt.wrap lo? hi? x + ToInt.wrap lo? hi? y) := by
   simp only [wrap]
@@ -78,6 +158,27 @@ theorem ToInt.wrap_add (lo? hi? : Option Int) (x y : Int) :
     exact Int.mul_emod_right ..
   · simp
 
+theorem ToInt.wrap_mul (lo? hi? : Option Int) (x y : Int) :
+    ToInt.wrap lo? hi? (x * y) = ToInt.wrap lo? hi? (ToInt.wrap lo? hi? x * ToInt.wrap lo? hi? y) := by
+  simp only [wrap]
+  split <;> rename_i lo hi
+  · dsimp
+    rw [Int.add_left_inj, Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.emod_def (x - lo), Int.emod_def (y - lo)]
+    have : x - lo - (hi - lo) * ((x - lo) / (hi - lo)) + lo = x - (hi - lo) * ((x - lo) / (hi - lo)) := by omega
+    rw [this]; clear this
+    have : y - lo - (hi - lo) * ((y - lo) / (hi - lo)) + lo = y - (hi - lo) * ((y - lo) / (hi - lo)) := by omega
+    rw [this]; clear this
+    have : x * y - lo - ((x - (hi - lo) * ((x - lo) / (hi - lo))) * (y - (hi - lo) * ((y - lo) / (hi - lo))) - lo) =
+      x * y - (x - (hi - lo) * ((x - lo) / (hi - lo))) * (y - (hi - lo) * ((y - lo) / (hi - lo))) := by omega
+    rw [this]; clear this
+    have : (x - (hi - lo) * ((x - lo) / (hi - lo))) * (y - (hi - lo) * ((y - lo) / (hi - lo))) =
+        x * y - (hi - lo) * (x * ((y - lo) / (hi - lo)) + (x - lo) / (hi - lo) * (y - (hi - lo) * ((y - lo) / (hi - lo)))) := by
+      conv => lhs; rw [Int.sub_mul, Int.mul_sub, Int.mul_left_comm, Int.sub_sub, Int.mul_assoc, ← Int.mul_add]
+    rw [this]; clear this
+    rw [Int.sub_sub_self]
+    apply Int.mul_emod_right
+  · simp
+
 @[simp]
 theorem ToInt.wrap_toInt (lo? hi? : Option Int) [ToInt α lo? hi?] (x : α) :
     ToInt.wrap lo? hi? (ToInt.toInt x) = ToInt.toInt x := by

src/Init/GrindInstances/Ring/Fin.lean

@@ -8,7 +8,7 @@ module
 prelude
 import all Init.Data.Zero
 import Init.Grind.Ring.Basic
-import Init.GrindInstances.ToInt
+import all Init.GrindInstances.ToInt
 import Init.Data.Fin.Lemmas
 
 namespace Lean.Grind
@@ -23,6 +23,9 @@ def npow [NeZero n] (x : Fin n) (y : Nat) : Fin n := npowRec y x
 instance [NeZero n] : HPow (Fin n) Nat (Fin n) where
   hPow := Fin.npow
 
+instance [NeZero n] : Pow (Fin n) Nat where
+  pow := Fin.npow
+
 @[simp] theorem pow_zero [NeZero n] (a : Fin n) : a ^ 0 = 1 := rfl
 @[simp] theorem pow_succ [NeZero n] (a : Fin n) (n : Nat) : a ^ (n+1) = a ^ n * a := rfl
 
@@ -104,6 +107,19 @@ instance (n : Nat) [NeZero n] : IsCharP (Fin n) n := IsCharP.mk' _ _
 example [NeZero n] : ToInt.Neg (Fin n) (some 0) (some n) := inferInstance
 example [NeZero n] : ToInt.Sub (Fin n) (some 0) (some n) := inferInstance
 
+instance [i : NeZero n] : ToInt.Pow (Fin n) (some 0) (some n) where
+  toInt_pow x k := by
+    induction k with
+    | zero =>
+      match n, i with
+      | 1, _ => rfl
+      | (n + 2), _ =>
+        simp [ToInt.wrap, Int.sub_zero, Int.add_zero]
+        rw [Int.emod_eq_of_lt] <;> omega
+    | succ k ih =>
+      rw [pow_succ, ToInt.Mul.toInt_mul, ih, ← ToInt.wrap_toInt,
+        ← ToInt.wrap_mul, Int.pow_succ, ToInt.wrap_toInt]
+
 end Fin
 
 end Lean.Grind

src/Init/GrindInstances/ToInt.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 import all Init.Grind.ToInt
+import Init.Grind.Module.Basic
 import Init.Data.Int.DivMod.Basic
 import Init.Data.Int.Lemmas
 import Init.Data.Int.Order
@@ -26,6 +27,9 @@ instance : ToInt Int none none where
 
 @[simp] theorem toInt_int (x : Int) : ToInt.toInt x = x := rfl
 
+instance : ToInt.Zero Int none none where
+  toInt_zero := by simp
+
 instance : ToInt.Add Int none none where
   toInt_add := by simp
 
@@ -35,9 +39,18 @@ instance : ToInt.Neg Int none none where
 instance : ToInt.Sub Int none none where
   toInt_sub x y := by simp
 
+instance : ToInt.Mul Int none none where
+  toInt_mul x y := by simp
+
+instance : ToInt.Pow Int none none where
+  toInt_pow x n := by simp
+
 instance : ToInt.Mod Int none none where
   toInt_mod x y := by simp
 
+instance : ToInt.Div Int none none where
+  toInt_div x y := by simp
+
 instance : ToInt.LE Int none none where
   le_iff x y := by simp
 
@@ -52,12 +65,24 @@ instance : ToInt Nat (some 0) none where
 
 @[simp] theorem toInt_nat (x : Nat) : ToInt.toInt x = (x : Int) := rfl
 
+instance : ToInt.Zero Nat (some 0) none where
+  toInt_zero := by simp
+
 instance : ToInt.Add Nat (some 0) none where
   toInt_add := by simp
 
+instance : ToInt.Mul Nat (some 0) none where
+  toInt_mul x y := by simp
+
+instance : ToInt.Pow Nat (some 0) none where
+  toInt_pow x n := by simp
+
 instance : ToInt.Mod Nat (some 0) none where
   toInt_mod x y := by simp
 
+instance : ToInt.Div Nat (some 0) none where
+  toInt_div x y := by simp
+
 instance : ToInt.LE Nat (some 0) none where
   le_iff x y := by simp
 
@@ -74,17 +99,26 @@ instance : ToInt (Fin n) (some 0) (some n) where
 
 @[simp] theorem toInt_fin (x : Fin n) : ToInt.toInt x = (x.val : Int) := rfl
 
+instance [NeZero n] : ToInt.Zero (Fin n) (some 0) (some n) where
+  toInt_zero := rfl
+
 instance : ToInt.Add (Fin n) (some 0) (some n) where
   toInt_add x y := by rfl
 
-instance [NeZero n] : ToInt.Zero (Fin n) (some 0) (some n) where
-  toInt_zero := by rfl
-
 -- The `ToInt.Neg` and `ToInt.Sub` instances are generated automatically from the `IntModule (Fin n)` instance.
+-- See `Init.GrindInstances.Ring.Fin`.
+
+instance : ToInt.Mul (Fin n) (some 0) (some n) where
+  toInt_mul x y := by rfl
+
+-- The `IoInt.Pow` instance is defined in `Init.GrindInstances.Ring.Fin`,
+-- since the power operation is only defined there.
 
 instance : ToInt.Mod (Fin n) (some 0) (some n) where
-  toInt_mod x y := by
-    simp only [toInt_fin, Fin.mod_val, Int.natCast_emod]
+  toInt_mod _ _ := rfl
+
+instance : ToInt.Div (Fin n) (some 0) (some n) where
+  toInt_div _ _ := rfl
 
 instance : ToInt.LE (Fin n) (some 0) (some n) where
   le_iff x y := by simpa using Fin.le_def
@@ -100,15 +134,21 @@ instance : ToInt UInt8 (some 0) (some (2^8)) where
 
 @[simp] theorem toInt_uint8 (x : UInt8) : ToInt.toInt x = (x.toNat : Int) := rfl
 
-instance : ToInt.Add UInt8 (some 0) (some (2^8)) where
-  toInt_add x y := by simp
-
 instance : ToInt.Zero UInt8 (some 0) (some (2^8)) where
   toInt_zero := by simp
 
+instance : ToInt.Add UInt8 (some 0) (some (2^8)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Mul UInt8 (some 0) (some (2^8)) where
+  toInt_mul x y := by simp
+
 instance : ToInt.Mod UInt8 (some 0) (some (2^8)) where
   toInt_mod x y := by simp
 
+instance : ToInt.Div UInt8 (some 0) (some (2^8)) where
+  toInt_div x y := by simp
+
 instance : ToInt.LE UInt8 (some 0) (some (2^8)) where
   le_iff x y := by simpa using UInt8.le_iff_toBitVec_le
 
@@ -123,15 +163,21 @@ instance : ToInt UInt16 (some 0) (some (2^16)) where
 
 @[simp] theorem toInt_uint16 (x : UInt16) : ToInt.toInt x = (x.toNat : Int) := rfl
 
-instance : ToInt.Add UInt16 (some 0) (some (2^16)) where
-  toInt_add x y := by simp
-
 instance : ToInt.Zero UInt16 (some 0) (some (2^16)) where
   toInt_zero := by simp
 
+instance : ToInt.Add UInt16 (some 0) (some (2^16)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Mul UInt16 (some 0) (some (2^16)) where
+  toInt_mul x y := by simp
+
 instance : ToInt.Mod UInt16 (some 0) (some (2^16)) where
   toInt_mod x y := by simp
 
+instance : ToInt.Div UInt16 (some 0) (some (2^16)) where
+  toInt_div x y := by simp
+
 instance : ToInt.LE UInt16 (some 0) (some (2^16)) where
   le_iff x y := by simpa using UInt16.le_iff_toBitVec_le
 
@@ -146,15 +192,21 @@ instance : ToInt UInt32 (some 0) (some (2^32)) where
 
 @[simp] theorem toInt_uint32 (x : UInt32) : ToInt.toInt x = (x.toNat : Int) := rfl
 
-instance : ToInt.Add UInt32 (some 0) (some (2^32)) where
-  toInt_add x y := by simp
-
 instance : ToInt.Zero UInt32 (some 0) (some (2^32)) where
   toInt_zero := by simp
 
+instance : ToInt.Add UInt32 (some 0) (some (2^32)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Mul UInt32 (some 0) (some (2^32)) where
+  toInt_mul x y := by simp
+
 instance : ToInt.Mod UInt32 (some 0) (some (2^32)) where
   toInt_mod x y := by simp
 
+instance : ToInt.Div UInt32 (some 0) (some (2^32)) where
+  toInt_div x y := by simp
+
 instance : ToInt.LE UInt32 (some 0) (some (2^32)) where
   le_iff x y := by simpa using UInt32.le_iff_toBitVec_le
 
@@ -169,15 +221,21 @@ instance : ToInt UInt64 (some 0) (some (2^64)) where
 
 @[simp] theorem toInt_uint64 (x : UInt64) : ToInt.toInt x = (x.toNat : Int) := rfl
 
-instance : ToInt.Add UInt64 (some 0) (some (2^64)) where
-  toInt_add x y := by simp
-
 instance : ToInt.Zero UInt64 (some 0) (some (2^64)) where
   toInt_zero := by simp
 
+instance : ToInt.Add UInt64 (some 0) (some (2^64)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Mul UInt64 (some 0) (some (2^64)) where
+  toInt_mul x y := by simp
+
 instance : ToInt.Mod UInt64 (some 0) (some (2^64)) where
   toInt_mod x y := by simp
 
+instance : ToInt.Div UInt64 (some 0) (some (2^64)) where
+  toInt_div x y := by simp
+
 instance : ToInt.LE UInt64 (some 0) (some (2^64)) where
   le_iff x y := by simpa using UInt64.le_iff_toBitVec_le
 
@@ -196,15 +254,21 @@ instance : ToInt USize (some 0) (some (2^System.Platform.numBits)) where
 
 @[simp] theorem toInt_usize (x : USize) : ToInt.toInt x = (x.toNat : Int) := rfl
 
-instance : ToInt.Add USize (some 0) (some (2^System.Platform.numBits)) where
-  toInt_add x y := by simp
-
 instance : ToInt.Zero USize (some 0) (some (2^System.Platform.numBits)) where
   toInt_zero := by simp
 
+instance : ToInt.Add USize (some 0) (some (2^System.Platform.numBits)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Mul USize (some 0) (some (2^System.Platform.numBits)) where
+  toInt_mul x y := by simp
+
 instance : ToInt.Mod USize (some 0) (some (2^System.Platform.numBits)) where
   toInt_mod x y := by simp
 
+instance : ToInt.Div USize (some 0) (some (2^System.Platform.numBits)) where
+  toInt_div x y := by simp
+
 instance : ToInt.LE USize (some 0) (some (2^System.Platform.numBits)) where
   le_iff x y := by simpa using USize.le_iff_toBitVec_le
 
@@ -219,17 +283,21 @@ instance : ToInt Int8 (some (-2^7)) (some (2^7)) where
 
 @[simp] theorem toInt_int8 (x : Int8) : ToInt.toInt x = (x.toInt : Int) := rfl
 
-instance : ToInt.Add Int8 (some (-2^7)) (some (2^7)) where
-  toInt_add x y := by
-    simp [Int.bmod_eq_emod]
-    split <;> · simp; omega
-
 instance : ToInt.Zero Int8 (some (-2^7)) (some (2^7)) where
   toInt_zero := by
     --  simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
     change (0 : Int8).toInt = _
     rw [Int8.toInt_zero]
-    decide
+
+instance : ToInt.Add Int8 (some (-2^7)) (some (2^7)) where
+  toInt_add x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
+
+instance : ToInt.Mul Int8 (some (-2^7)) (some (2^7)) where
+  toInt_mul x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
 
 -- Note that we can not define `ToInt.Mod` instances for `Int8`,
 -- because the condition does not hold unless `0 ≤ x.toInt ∨ y.toInt ∣ x.toInt ∨ y = 0`.
@@ -248,17 +316,21 @@ instance : ToInt Int16 (some (-2^15)) (some (2^15)) where
 
 @[simp] theorem toInt_int16 (x : Int16) : ToInt.toInt x = (x.toInt : Int) := rfl
 
-instance : ToInt.Add Int16 (some (-2^15)) (some (2^15)) where
-  toInt_add x y := by
-    simp [Int.bmod_eq_emod]
-    split <;> · simp; omega
-
 instance : ToInt.Zero Int16 (some (-2^15)) (some (2^15)) where
   toInt_zero := by
     -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
     change (0 : Int16).toInt = _
     rw [Int16.toInt_zero]
-    decide
+
+instance : ToInt.Add Int16 (some (-2^15)) (some (2^15)) where
+  toInt_add x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
+
+instance : ToInt.Mul Int16 (some (-2^15)) (some (2^15)) where
+  toInt_mul x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
 
 instance : ToInt.LE Int16 (some (-2^15)) (some (2^15)) where
   le_iff x y := by simpa using Int16.le_iff_toInt_le
@@ -274,17 +346,21 @@ instance : ToInt Int32 (some (-2^31)) (some (2^31)) where
 
 @[simp] theorem toInt_int32 (x : Int32) : ToInt.toInt x = (x.toInt : Int) := rfl
 
-instance : ToInt.Add Int32 (some (-2^31)) (some (2^31)) where
-  toInt_add x y := by
-    simp [Int.bmod_eq_emod]
-    split <;> · simp; omega
-
 instance : ToInt.Zero Int32 (some (-2^31)) (some (2^31)) where
   toInt_zero := by
     -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
     change (0 : Int32).toInt = _
     rw [Int32.toInt_zero]
-    decide
+
+instance : ToInt.Add Int32 (some (-2^31)) (some (2^31)) where
+  toInt_add x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
+
+instance : ToInt.Mul Int32 (some (-2^31)) (some (2^31)) where
+  toInt_mul x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
 
 instance : ToInt.LE Int32 (some (-2^31)) (some (2^31)) where
   le_iff x y := by simpa using Int32.le_iff_toInt_le
@@ -300,17 +376,21 @@ instance : ToInt Int64 (some (-2^63)) (some (2^63)) where
 
 @[simp] theorem toInt_int64 (x : Int64) : ToInt.toInt x = (x.toInt : Int) := rfl
 
-instance : ToInt.Add Int64 (some (-2^63)) (some (2^63)) where
-  toInt_add x y := by
-    simp [Int.bmod_eq_emod]
-    split <;> · simp; omega
-
 instance : ToInt.Zero Int64 (some (-2^63)) (some (2^63)) where
   toInt_zero := by
     -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
     change (0 : Int64).toInt = _
     rw [Int64.toInt_zero]
-    decide
+
+instance : ToInt.Add Int64 (some (-2^63)) (some (2^63)) where
+  toInt_add x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
+
+instance : ToInt.Mul Int64 (some (-2^63)) (some (2^63)) where
+  toInt_mul x y := by
+    simp [Int.bmod_eq_emod]
+    split <;> · simp; omega
 
 instance : ToInt.LE Int64 (some (-2^63)) (some (2^63)) where
   le_iff x y := by simpa using Int64.le_iff_toInt_le
@@ -329,15 +409,21 @@ instance : ToInt (BitVec v) (some 0) (some (2^v)) where
 
 @[simp] theorem toInt_bitVec (x : BitVec v) : ToInt.toInt x = (x.toNat : Int) := rfl
 
-instance : ToInt.Add (BitVec v) (some 0) (some (2^v)) where
-  toInt_add x y := by simp
-
 instance : ToInt.Zero (BitVec v) (some 0) (some (2^v)) where
   toInt_zero := by simp
 
+instance : ToInt.Add (BitVec v) (some 0) (some (2^v)) where
+  toInt_add x y := by simp
+
+instance : ToInt.Mul (BitVec v) (some 0) (some (2^v)) where
+  toInt_mul x y := by simp
+
 instance : ToInt.Mod (BitVec v) (some 0) (some (2^v)) where
   toInt_mod x y := by simp
 
+instance : ToInt.Div (BitVec v) (some 0) (some (2^v)) where
+  toInt_div x y := by simp
+
 instance : ToInt.LE (BitVec v) (some 0) (some (2^v)) where
   le_iff x y := by simpa using BitVec.le_def
 
@@ -352,6 +438,10 @@ instance : ToInt ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.
 
 @[simp] theorem toInt_isize (x : ISize) : ToInt.toInt x = x.toInt := rfl
 
+instance : ToInt.Zero ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+  toInt_zero := by
+    rw [toInt_isize, ISize.toInt_zero]
+
 instance : ToInt.Add ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
   toInt_add x y := by
     rw [toInt_isize, ISize.toInt_add, ToInt.wrap_eq_bmod (Int.pow_nonneg (by decide))]
@@ -364,11 +454,17 @@ instance : ToInt.Add ISize (some (-2^(System.Platform.numBits-1))) (some (2^(Sys
       simp
     simp [p₁, p₂]
 
-instance : ToInt.Zero ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
-  toInt_zero := by
-    rw [toInt_isize]
-    rw [ISize.toInt_zero, ToInt.wrap_eq_bmod (Int.pow_nonneg (by decide))]
-    simp
+instance : ToInt.Mul ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+  toInt_mul x y := by
+    rw [toInt_isize, ISize.toInt_mul, ToInt.wrap_eq_bmod (Int.pow_nonneg (by decide))]
+    have p₁ : (2 : Int) * 2 ^ (System.Platform.numBits - 1) = 2 ^ System.Platform.numBits := by
+      have := System.Platform.numBits_pos
+      have : System.Platform.numBits - 1 + 1 = System.Platform.numBits := by omega
+      simp [← Int.pow_succ', this]
+    have p₂ : ((2 : Int) ^ System.Platform.numBits).toNat = 2 ^ System.Platform.numBits := by
+      rw [Int.toNat_pow_of_nonneg (by decide)]
+      simp
+    simp [p₁, p₂]
 
 instance instToIntLEISize : ToInt.LE ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
   le_iff x y := by simpa using ISize.le_iff_toInt_le