unused simp lemma

src/Init/Core.lean

@@ -1592,7 +1592,6 @@ gen_injective_theorems% MProd
 gen_injective_theorems% NonScalar
 gen_injective_theorems% Option
 gen_injective_theorems% PLift
-gen_injective_theorems% PULift
 gen_injective_theorems% PNonScalar
 gen_injective_theorems% PProd
 gen_injective_theorems% Prod

src/Init/Data/BitVec/Lemmas.lean

@@ -541,9 +541,13 @@ theorem toInt_ne {x y : BitVec n} : x.toInt ≠ y.toInt ↔ x ≠ y  := by
   unfold BitVec.ofInt
   simp
 
-theorem toInt_ofNat {n : Nat} (x : Nat) : (BitVec.ofNat n x).toInt = (x : Int).bmod (2^n) := by
+theorem toInt_ofNat' {n : Nat} (x : Nat) : (BitVec.ofNat n x).toInt = (x : Int).bmod (2^n) := by
   simp [toInt_eq_toNat_bmod, -Int.natCast_pow]
 
+theorem toInt_ofNat {n : Nat} (x : Nat) :
+    (no_index (OfNat.ofNat (α := BitVec n) x)).toInt = (x : Int).bmod (2^n) :=
+  toInt_ofNat' x
+
 @[simp, grind =] theorem toInt_ofFin {w : Nat} (x : Fin (2^w)) :
     (BitVec.ofFin x).toInt = Int.bmod x (2^w) := by
   grind [toInt_eq_toNat_bmod]
@@ -915,7 +919,7 @@ theorem extractLsb_toNat (hi lo : Nat) (x : BitVec n) :
 @[simp, grind =]
 theorem toInt_extractLsb' {s m : Nat} {x : BitVec n} :
     (extractLsb' s m x).toInt = ((x.toNat >>> s) : Int).bmod (2 ^ m) := by
-  simp [extractLsb', toInt_ofNat]
+  simp [extractLsb', toInt_ofNat']
 
 @[simp, grind =]
 theorem toInt_extractLsb {hi lo : Nat} {x : BitVec n} :
@@ -1703,7 +1707,7 @@ theorem toFin_ushiftRight {x : BitVec w} {n : Nat} :
 @[simp, grind =]
 theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} :
     (x >>> n).getMsbD i = (decide (i < w) && (!decide (i < n) && x.getMsbD (i - n))) := by
-  grind (splits := 10)
+  grind (splits := 11)
 
 @[simp]
 theorem msb_ushiftRight {x : BitVec w} {n : Nat} :
@@ -2105,7 +2109,7 @@ theorem toFin_signExtend (x : BitVec w) :
 
 @[simp, grind =] theorem signExtend_or {x y : BitVec w} :
     (x ||| y).signExtend v = (x.signExtend v) ||| (y.signExtend v) := by
-  grind (splits := 11)
+  grind (splits := 12)
 
 @[simp, grind =] theorem signExtend_xor {x y : BitVec w} :
     (x ^^^ y).signExtend v = (x.signExtend v) ^^^ (y.signExtend v) := by
@@ -2745,7 +2749,7 @@ theorem toNat_neg_of_pos {x : BitVec n} (h : 0#n < x) :
 theorem toInt_neg {x : BitVec w} :
     (-x).toInt = (-x.toInt).bmod (2 ^ w) := by
   rw [← BitVec.zero_sub, toInt_sub]
-  simp [BitVec.toInt_ofNat]
+  simp
 
 @[simp]
 theorem toInt_neg_of_not_negOverflow {x : BitVec w} (h : ¬ negOverflow x):
@@ -4619,7 +4623,7 @@ creating a bitvector from the the negative of that number.
 theorem neg_ofNat_eq_ofInt_neg {w : Nat} {x : Nat} :
     - BitVec.ofNat w x = BitVec.ofInt w (- x) := by
   apply BitVec.eq_of_toInt_eq
-  simp [BitVec.toInt_neg, BitVec.toInt_ofNat]
+  simp [BitVec.toInt_neg, BitVec.toInt_ofNat']
 
 @[simp]
 theorem neg_toInt_neg {x : BitVec w} (h : x.msb = false) :

src/Init/Data/SInt/Lemmas.lean

@@ -128,6 +128,28 @@ theorem ISize.toNat_toBitVec_ofNat_of_lt {n : Nat} (h : n < 2^32) :
 theorem ISize.toInt_ofInt {n : Int} : toInt (ofInt n) = n.bmod ISize.size := by
   rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt]
 
+@[simp] theorem Int8.toInt_ofNat' {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int8.size := by
+  rw [toInt, toBitVec_ofNat', BitVec.toInt_ofNat']
+@[simp] theorem Int16.toInt_ofNat' {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int16.size := by
+  rw [toInt, toBitVec_ofNat', BitVec.toInt_ofNat']
+@[simp] theorem Int32.toInt_ofNat' {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int32.size := by
+  rw [toInt, toBitVec_ofNat', BitVec.toInt_ofNat']
+@[simp] theorem Int64.toInt_ofNat' {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int64.size := by
+  rw [toInt, toBitVec_ofNat', BitVec.toInt_ofNat']
+@[simp] theorem ISize.toInt_ofNat' {n : Nat} : toInt (ofNat n) = (n : Int).bmod ISize.size := by
+  rw [toInt, toBitVec_ofNat', BitVec.toInt_ofNat']
+
+theorem Int8.toInt_ofNat {n : Nat} : toInt (no_index (OfNat.ofNat n)) = (n : Int).bmod Int8.size := by
+  rw [toInt, toBitVec_ofNat, BitVec.toInt_ofNat]
+theorem Int16.toInt_ofNat {n : Nat} : toInt (no_index (OfNat.ofNat n)) = (n : Int).bmod Int16.size := by
+  rw [toInt, toBitVec_ofNat, BitVec.toInt_ofNat]
+theorem Int32.toInt_ofNat {n : Nat} : toInt (no_index (OfNat.ofNat n)) = (n : Int).bmod Int32.size := by
+  rw [toInt, toBitVec_ofNat, BitVec.toInt_ofNat]
+theorem Int64.toInt_ofNat {n : Nat} : toInt (no_index (OfNat.ofNat n)) = (n : Int).bmod Int64.size := by
+  rw [toInt, toBitVec_ofNat, BitVec.toInt_ofNat]
+theorem ISize.toInt_ofNat {n : Nat} : toInt (no_index (OfNat.ofNat n)) = (n : Int).bmod ISize.size := by
+  rw [toInt, toBitVec_ofNat, BitVec.toInt_ofNat]
+
 theorem Int8.toInt_ofInt_of_le {n : Int} (hn : -2^7 ≤ n) (hn' : n < 2^7) : toInt (ofInt n) = n := by
   rw [toInt, toBitVec_ofInt, BitVec.toInt_ofInt_eq_self (by decide) hn hn']
 theorem Int16.toInt_ofInt_of_le {n : Int} (hn : -2^15 ≤ n) (hn' : n < 2^15) : toInt (ofInt n) = n := by
@@ -166,17 +188,6 @@ theorem Int32.ofInt_eq_ofNat {n : Nat} : ofInt n = ofNat n := toBitVec.inj (by s
 theorem Int64.ofInt_eq_ofNat {n : Nat} : ofInt n = ofNat n := toBitVec.inj (by simp)
 theorem ISize.ofInt_eq_ofNat {n : Nat} : ofInt n = ofNat n := toBitVec.inj (by simp)
 
-@[simp] theorem Int8.toInt_ofNat {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int8.size := by
-  rw [← ofInt_eq_ofNat, toInt_ofInt]
-@[simp] theorem Int16.toInt_ofNat {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int16.size := by
-  rw [← ofInt_eq_ofNat, toInt_ofInt]
-@[simp] theorem Int32.toInt_ofNat {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int32.size := by
-  rw [← ofInt_eq_ofNat, toInt_ofInt]
-@[simp] theorem Int64.toInt_ofNat {n : Nat} : toInt (ofNat n) = (n : Int).bmod Int64.size := by
-  rw [← ofInt_eq_ofNat, toInt_ofInt]
-@[simp] theorem ISize.toInt_ofNat {n : Nat} : toInt (ofNat n) = (n : Int).bmod ISize.size := by
-  rw [← ofInt_eq_ofNat, toInt_ofInt]
-
 theorem Int8.neg_ofNat {n : Nat} : -ofNat n = ofInt (-n) := by
   rw [← neg_ofInt, ofInt_eq_ofNat]
 theorem Int16.neg_ofNat {n : Nat} : -ofNat n = ofInt (-n) := by

src/Init/Grind/Module/Basic.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 import Init.Data.Int.Order
-import Init.Grind.ToInt
+import all Init.Grind.ToInt
 
 namespace Lean.Grind
 
@@ -237,17 +237,17 @@ theorem eq_zero_of_mul_eq_zero {α : Type u} [NatModule α] [NoNatZeroDivisors
 
 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
+instance [ToInt α (IntInterval.co lo hi)] [IntModule α] [ToInt.Zero α (IntInterval.co lo hi)] [ToInt.Add α (IntInterval.co lo hi)] : ToInt.Neg α (IntInterval.co lo hi) where
   toInt_neg x := by
     have := (ToInt.Add.toInt_add (-x) x).symm
     rw [IntModule.neg_add_cancel, ToInt.Zero.toInt_zero, ← ToInt.Zero.wrap_zero (α := α)] at this
-    rw [ToInt.wrap_eq_wrap_iff] at this
+    rw [IntInterval.wrap_eq_wrap_iff] at this
     simp at this
     rw [← ToInt.wrap_toInt]
-    rw [ToInt.wrap_eq_wrap_iff]
+    rw [IntInterval.wrap_eq_wrap_iff]
     simpa
 
-instance [ToInt α (some lo) (some hi)] [IntModule α] [ToInt.Add α (some lo) (some hi)] [ToInt.Neg α (some lo) (some hi)] : ToInt.Sub α (some lo) (some hi) :=
-  ToInt.Sub.of_sub_eq_add_neg IntModule.sub_eq_add_neg
+instance [ToInt α (IntInterval.co lo hi)] [IntModule α] [ToInt.Add α (IntInterval.co lo hi)] [ToInt.Neg α (IntInterval.co lo hi)] : ToInt.Sub α (IntInterval.co lo hi) :=
+  ToInt.Sub.of_sub_eq_add_neg IntModule.sub_eq_add_neg (by simp)
 
 end Lean.Grind

src/Init/Grind/Ring.lean

@@ -11,3 +11,4 @@ import Init.Grind.Ring.Poly
 import Init.Grind.Ring.Field
 import Init.Grind.Ring.Envelope
 import Init.Grind.Ring.OfSemiring
+import Init.Grind.Ring.ToInt

src/Init/Grind/Ring/ToInt.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Grind.Ring.Basic
+import Init.Grind.ToInt
+
+namespace Lean.Grind
+
+/-- A `ToInt` instance on a semiring preserves powers if it preserves numerals and multiplication. -/
+def ToInt.pow_of_semiring [Semiring α] [ToInt α I] [ToInt.OfNat α I] [ToInt.Mul α I]
+    (h₁ : I.isFinite) (h₂ : 1 ∈ I) : ToInt.Pow α I where
+  toInt_pow x n := by
+    induction n with
+    | zero =>
+      rw [Semiring.pow_zero]
+      rw [ToInt.OfNat.toInt_ofNat _ h₂]
+      rw [Int.pow_zero]
+      rw [(I.wrap_eq_self_iff (IntInterval.nonEmpty_of_mem h₂) _).mpr h₂]
+      rfl
+    | succ n ih =>
+      rw [Semiring.pow_succ]
+      rw [ToInt.Mul.toInt_mul]
+      conv => lhs; rw [← ToInt.wrap_toInt I x]
+      rw [ih]
+      rw [← I.wrap_mul h₁]
+      rw [Int.pow_succ]
+
+end Lean.Grind

src/Init/Grind/ToInt.lean

@@ -25,144 +25,146 @@ 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
+/-- An interval in the integers (either finite, half-infinite, or infinite). -/
+inductive IntInterval : Type where
+  | /-- The finite interval `[lo, hi)`. -/
+    co (lo hi : Int)
+  | /-- The half-infinite interval `[lo, ∞)`. -/
+    ci (lo : Int)
+  | /-- The half-infinite interval `(-∞, hi)`. -/
+    io (hi : Int)
+  | /-- The infinite interval `(-∞, ∞)`. -/
+    ii
+
+namespace IntInterval
+
+/-- The interval `[0, 2^n)`. -/
+abbrev uint (n : Nat) := IntInterval.co 0 (2 ^ n)
+/-- The interval `[-2^(n-1), 2^(n-1))`. -/
+abbrev sint (n : Nat) := IntInterval.co (-(2 ^ (n - 1))) (2 ^ (n - 1))
+
+/-- The lower bound of the interval, if finite. -/
+def lo? (i : IntInterval) : Option Int :=
+  match i with
+  | co lo _ => some lo
+  | ci lo => some lo
+  | io _ => none
+  | ii => none
+
+/-- The upper bound of the interval, if finite. -/
+def hi? (i : IntInterval) : Option Int :=
+  match i with
+  | co _ hi => some hi
+  | ci _ => none
+  | io hi => some hi
+  | ii => none
 
 @[simp]
-def ToInt.wrap (lo? hi? : Option Int) (x : Int) : Int :=
-  match lo?, hi? with
-  | some lo, some hi => (x - lo) % (hi - lo) + lo
-  | _, _ => x
+def nonEmpty (i : IntInterval) : Bool :=
+  match i with
+  | co lo hi => lo < hi
+  | ci _ => true
+  | io _ => true
+  | ii => true
 
-/--
-The embedding into the integers takes `0` to `0`.
--/
-class ToInt.Zero (α : Type u) [Zero α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where
-  /-- The embedding takes `0` to `0`. -/
-  toInt_zero : toInt (0 : α) = 0
+@[simp]
+def isFinite (i : IntInterval) : Bool :=
+  match i with
+  | co _ _ => true
+  | ci _
+  | io _
+  | ii => false
 
-/--
-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)
+def mem (i : IntInterval) (x : Int) : Prop :=
+  match i with
+  | co lo hi => lo ≤ x ∧ x < hi
+  | ci lo => lo ≤ x
+  | io hi => x < hi
+  | ii => True
 
-/--
-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)
+instance : Membership Int IntInterval where
+  mem := mem
 
-/--
-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)
+@[simp] theorem mem_co (lo hi : Int) (x : Int) : x ∈ IntInterval.co lo hi ↔ lo ≤ x ∧ x < hi := by rfl
+@[simp] theorem mem_ci (lo : Int) (x : Int) : x ∈ IntInterval.ci lo ↔ lo ≤ x := by rfl
+@[simp] theorem mem_io (hi : Int) (x : Int) : x ∈ IntInterval.io hi ↔ x < hi := by rfl
+@[simp] theorem mem_ii (x : Int) : x ∈ IntInterval.ii ↔ True := by rfl
 
-/--
-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)
+theorem nonEmpty_of_mem {x : Int} {i : IntInterval} (h : x ∈ i) : i.nonEmpty := by
+  cases i <;> simp_all <;> omega
 
-/--
-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)
+@[simp]
+def wrap (i : IntInterval) (x : Int) : Int :=
+  match i with
+  | co lo hi => (x - lo) % (hi - lo) + lo
+  | ci lo => max x lo
+  | io hi => min x (hi - 1)
+  | ii => x
 
-/--
-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
-  /--
-  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
+theorem wrap_wrap (i : IntInterval) (x : Int) :
+    wrap i (wrap i x) = wrap i x := by
+  cases i <;> simp [wrap] <;> omega
 
-/--
-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
+theorem wrap_mem (i : IntInterval) (h : i.nonEmpty) (x : Int) :
+    i.wrap x ∈ i := by
+  match i with
+  | co lo hi =>
+    simp [wrap]
+    simp at h
+    constructor
+    · apply Int.le_add_of_nonneg_left
+      apply Int.emod_nonneg
+      omega
+    · have := Int.emod_lt (x - lo) (b := hi - lo) (by omega)
+      omega
+  | ci lo =>
+    simp [wrap]
+    omega
+  | io hi =>
+    simp [wrap]
+    omega
+  | ii =>
+    simp [wrap]
 
-/--
-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
+theorem wrap_eq_self_iff (i : IntInterval) (h : i.nonEmpty) (x : Int) :
+    i.wrap x = x ↔ x ∈ i := by
+  match i with
+  | co lo hi =>
+    simp [wrap]
+    simp at h
+    constructor
+    · have := Int.emod_lt (x - lo) (b := hi - lo) (by omega)
+      have := Int.emod_nonneg (x - lo) (b := hi - lo) (by omega)
+      omega
+    · intro w
+      rw [Int.emod_eq_of_lt] <;> omega
+  | ci lo =>
+    simp [wrap]
+    omega
+  | io hi =>
+    simp [wrap]
+    omega
+  | ii =>
+    simp [wrap]
 
-/--
-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]
-  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 + y - lo -
-        (x - lo - (hi - lo) * ((x - lo) / (hi - lo)) + lo +
-          (y - lo - (hi - lo) * ((y - lo) / (hi - lo)) + lo) - lo)) =
-        (hi - lo) * ((x - lo) / (hi - lo) + (y - lo) / (hi - lo)) := by
+theorem wrap_add {i : IntInterval} (h : i.isFinite) (x y : Int) :
+    i.wrap (x + y) = i.wrap (i.wrap x + i.wrap y) := by
+  match i with
+  | co lo hi =>
+    simp [wrap]
+    rw [Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.emod_def (x - lo), Int.emod_def (y - lo)]
+    have : (x + y - lo - (x - lo - (hi - lo) * ((x - lo) / (hi - lo)) + lo + (y - lo - (hi - lo) * ((y - lo) / (hi - lo)) + lo) - lo)) =
+      (hi - lo) * ((x - lo) / (hi - lo) + (y - lo) / (hi - lo)) := by
       simp only [Int.mul_add]
       omega
     rw [this]
     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
+theorem wrap_mul {i : IntInterval} (h : i.isFinite) (x y : Int) :
+    i.wrap (x * y) = i.wrap (i.wrap x * i.wrap y) := by
+  match i with
+  | co lo hi =>
+    dsimp [wrap]
     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
@@ -177,21 +179,10 @@ theorem ToInt.wrap_mul (lo? hi? : Option Int) (x y : Int) :
     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
-  simp only [wrap]
-  split
-  · have := ToInt.le_toInt (x := x) rfl
-    have := ToInt.toInt_lt (x := x) rfl
-    rw [Int.emod_eq_of_lt (by omega) (by omega)]
-    omega
-  · rfl
-
-theorem ToInt.wrap_eq_bmod {i : Int} (h : 0 ≤ i) :
-    ToInt.wrap (some (-i)) (some i) x = x.bmod ((2 * i).toNat) := by
+theorem wrap_eq_bmod {i : Int} (h : 0 ≤ i) :
+    (IntInterval.co (-i) i).wrap  x = x.bmod ((2 * i).toNat) := by
+  dsimp only [wrap]
   match i, h with
   | (i : Nat), _ =>
     have : (2 * (i : Int)).toNat = 2 * i := by omega
@@ -228,21 +219,138 @@ theorem ToInt.wrap_eq_bmod {i : Int} (h : 0 ≤ i) :
         rw [this]
         exact Int.dvd_mul_right ..
 
-theorem ToInt.wrap_eq_wrap_iff :
-    ToInt.wrap (some lo) (some hi) x = ToInt.wrap (some lo) (some hi) y ↔ (x - y) % (hi - lo) = 0 := by
+theorem wrap_eq_wrap_iff :
+    (IntInterval.co lo hi).wrap x = (IntInterval.co lo hi).wrap y ↔ (x - y) % (hi - lo) = 0 := by
   simp only [wrap]
   rw [Int.add_left_inj]
   rw [Int.emod_eq_emod_iff_emod_sub_eq_zero]
-  have : x - lo - (y - lo)  = x - y := by omega
+  have : x - lo - (y - lo) = x - y := by omega
   rw [this]
 
+end IntInterval
+
+/--
+`ToInt α I` asserts that `α` can be embedded faithfully into an interval `I` in the integers.
+-/
+class ToInt (α : Type u) (range : outParam IntInterval) where
+  /-- The embedding function. -/
+  toInt : α → Int
+  /-- The embedding function is injective. -/
+  toInt_inj : ∀ x y, toInt x = toInt y → x = y
+  /-- The embedding function lands in the interval. -/
+  toInt_mem : ∀ x, toInt x ∈ range
+
+/--
+The embedding into the integers takes `0` to `0`.
+-/
+class ToInt.Zero (α : Type u) [Zero α] (I : outParam IntInterval) [ToInt α I] where
+  /-- The embedding takes `0` to `0`. -/
+  toInt_zero : toInt (0 : α) = 0
+
+/--
+The embedding into the integers takes numerals in the range interval to themselves.
+-/
+class ToInt.OfNat (α : Type u) [∀ n, OfNat α n] (I : outParam IntInterval) [ToInt α I] where
+  /-- The embedding takes `OfNat` to `OfNat`. -/
+  toInt_ofNat : ∀ n : Nat, (n : Int) ∈ I → toInt (OfNat.ofNat n : α) = n
+
+/--
+The embedding into the integers takes addition to addition, wrapped into the range interval.
+-/
+class ToInt.Add (α : Type u) [Add α] (I : outParam IntInterval) [ToInt α I] where
+  /-- The embedding takes addition to addition, wrapped into the range interval. -/
+  toInt_add : ∀ x y : α, toInt (x + y) = I.wrap (toInt x + toInt y)
+
+/--
+The embedding into the integers takes negation to negation, wrapped into the range interval.
+-/
+class ToInt.Neg (α : Type u) [Neg α] (I : outParam IntInterval) [ToInt α I] where
+  /-- The embedding takes negation to negation, wrapped into the range interval. -/
+  toInt_neg : ∀ x : α, toInt (-x) = I.wrap (-toInt x)
+
+/--
+The embedding into the integers takes subtraction to subtraction, wrapped into the range interval.
+-/
+class ToInt.Sub (α : Type u) [Sub α] (I : outParam IntInterval) [ToInt α I] where
+  /-- The embedding takes subtraction to subtraction, wrapped into the range interval. -/
+  toInt_sub : ∀ x y : α, toInt (x - y) = I.wrap (toInt x - toInt y)
+
+/--
+The embedding into the integers takes multiplication to multiplication, wrapped into the range interval.
+-/
+class ToInt.Mul (α : Type u) [Mul α] (I : outParam IntInterval) [ToInt α I] where
+  /-- The embedding takes multiplication to multiplication, wrapped into the range interval. -/
+  toInt_mul : ∀ x y : α, toInt (x * y) = I.wrap (toInt x * toInt y)
+
+/--
+The embedding into the integers takes exponentiation to exponentiation, wrapped into the range interval.
+-/
+class ToInt.Pow (α : Type u) [HPow α Nat α] (I : outParam IntInterval) [ToInt α I] where
+  /-- The embedding takes exponentiation to exponentiation, wrapped into the range interval. -/
+  toInt_pow : ∀ x : α, ∀ n : Nat, toInt (x ^ n) = I.wrap (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 α] (I : outParam IntInterval) [ToInt α I] where
+  /--
+  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 α] (I : outParam IntInterval) [ToInt α I] 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 α] (I : outParam IntInterval) [ToInt α I] 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 α] (I : outParam IntInterval) [ToInt α I] where
+  /-- The embedding is strictly monotone with respect to `<`. -/
+  lt_iff : ∀ x y : α, x < y ↔ toInt x < toInt y
+
+open IntInterval
+namespace ToInt
+
+/-! ## Helper theorems -/
+
+theorem Zero.wrap_zero (I : IntInterval) [_root_.Zero α] [ToInt α I] [ToInt.Zero α I] :
+    I.wrap 0 = 0 := by
+  have := toInt_mem (0 : α)
+  rw [I.wrap_eq_self_iff (I.nonEmpty_of_mem this)]
+  rwa [ToInt.Zero.toInt_zero] at this
+
+@[simp]
+theorem wrap_toInt (I : IntInterval) [ToInt α I] (x : α) :
+    I.wrap (toInt x) = toInt x := by
+  rw [I.wrap_eq_self_iff (I.nonEmpty_of_mem (toInt_mem x))]
+  exact ToInt.toInt_mem x
+
 /-- Construct a `ToInt.Sub` instance from a `ToInt.Add` and `ToInt.Neg` instance and
 a `sub_eq_add_neg` assumption. -/
-def ToInt.Sub.of_sub_eq_add_neg {α : Type u} [_root_.Add α] [_root_.Neg α] [_root_.Sub α]
+def Sub.of_sub_eq_add_neg {α : Type u} [_root_.Add α] [_root_.Neg α] [_root_.Sub α]
     (sub_eq_add_neg : ∀ x y : α, x - y = x + -y)
-    {lo? hi? : Option Int} [ToInt α lo? hi?] [Add α lo? hi?] [Neg α lo? hi?] : ToInt.Sub α lo? hi? where
+    {I : IntInterval} (h : I.isFinite) [ToInt α I] [Add α I] [Neg α I] : ToInt.Sub α I where
   toInt_sub x y := by
     rw [sub_eq_add_neg, ToInt.Add.toInt_add, ToInt.Neg.toInt_neg, Int.sub_eq_add_neg]
-    conv => rhs; rw [ToInt.wrap_add, ToInt.wrap_toInt]
+    conv => rhs; rw [wrap_add h, ToInt.wrap_toInt]
+
+end ToInt
 
 end Lean.Grind

src/Init/GrindInstances/Ring/BitVec.lean

@@ -9,6 +9,7 @@ prelude
 import Init.Grind.Ring.Basic
 import Init.GrindInstances.ToInt
 import all Init.Data.BitVec.Basic
+import all Init.Grind.ToInt
 
 namespace Lean.Grind
 
@@ -35,8 +36,15 @@ instance : IsCharP (BitVec w) (2 ^ w) := IsCharP.mk' _ _
   (ofNat_eq_zero_iff := fun x => by simp [BitVec.toNat_eq])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
-example : ToInt.Add (BitVec w) (some 0) (some (2^w)) := inferInstance
-example : ToInt.Neg (BitVec w) (some 0) (some (2^w)) := inferInstance
-example : ToInt.Sub (BitVec w) (some 0) (some (2^w)) := inferInstance
+example : ToInt.Add (BitVec w) (.uint w) := inferInstance
+example : ToInt.Neg (BitVec w) (.uint w) := inferInstance
+example : ToInt.Sub (BitVec w) (.uint w) := inferInstance
+
+instance [i : NeZero w] : ToInt.Pow (BitVec w) (.uint w) :=
+  ToInt.pow_of_semiring (by simp) (by
+    match w, i with
+    | w + 1, _ =>
+      have : 1 < 2 ^ (w + 1) := Nat.one_lt_two_pow' w
+      simpa [Int.pow_succ] using Int.ofNat_lt.mpr this)
 
 end Lean.Grind

src/Init/GrindInstances/Ring/Fin.lean

@@ -104,21 +104,21 @@ instance (n : Nat) [NeZero n] : IsCharP (Fin n) n := IsCharP.mk' _ _
     simp only [Nat.zero_mod]
     simp only [Fin.mk.injEq])
 
-example [NeZero n] : ToInt.Neg (Fin n) (some 0) (some n) := inferInstance
-example [NeZero n] : ToInt.Sub (Fin n) (some 0) (some n) := inferInstance
+example [NeZero n] : ToInt.Neg (Fin n) (.co 0 n) := inferInstance
+example [NeZero n] : ToInt.Sub (Fin n) (.co 0 n) := inferInstance
 
-instance [i : NeZero n] : ToInt.Pow (Fin n) (some 0) (some n) where
+instance [i : NeZero n] : ToInt.Pow (Fin n) (.co 0 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]
+        simp [IntInterval.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]
+        ← IntInterval.wrap_mul (by simp), Int.pow_succ, ToInt.wrap_toInt]
 
 end Fin
 

src/Init/GrindInstances/Ring/SInt.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 import Init.Grind.Ring.Basic
+import all Init.Grind.ToInt
 import Init.GrindInstances.ToInt
 import all Init.Data.BitVec.Basic
 import all Init.Data.SInt.Basic
@@ -47,9 +48,11 @@ instance : IsCharP Int8 (2 ^ 8) := IsCharP.mk' _ _
       ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
-example : ToInt.Add Int8 (some (-(2^7))) (some (2^7)) := inferInstance
-example : ToInt.Neg Int8 (some (-(2^7))) (some (2^7)) := inferInstance
-example : ToInt.Sub Int8 (some (-(2^7))) (some (2^7)) := inferInstance
+example : ToInt.Add Int8 (.sint 8) := inferInstance
+example : ToInt.Neg Int8 (.sint 8) := inferInstance
+example : ToInt.Sub Int8 (.sint 8) := inferInstance
+
+instance : ToInt.Pow Int8 (.sint 8) := ToInt.pow_of_semiring (by simp) (by simp)
 
 instance : NatCast Int16 where
   natCast x := Int16.ofNat x
@@ -84,9 +87,11 @@ instance : IsCharP Int16 (2 ^ 16) := IsCharP.mk' _ _
       ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
-example : ToInt.Add Int16 (some (-(2^15))) (some (2^15)) := inferInstance
-example : ToInt.Neg Int16 (some (-(2^15))) (some (2^15)) := inferInstance
-example : ToInt.Sub Int16 (some (-(2^15))) (some (2^15)) := inferInstance
+example : ToInt.Add Int16 (.sint 16) := inferInstance
+example : ToInt.Neg Int16 (.sint 16) := inferInstance
+example : ToInt.Sub Int16 (.sint 16) := inferInstance
+
+instance : ToInt.Pow Int16 (.sint 16) := ToInt.pow_of_semiring (by simp) (by simp)
 
 instance : NatCast Int32 where
   natCast x := Int32.ofNat x
@@ -121,9 +126,11 @@ instance : IsCharP Int32 (2 ^ 32) := IsCharP.mk' _ _
       ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
-example : ToInt.Add Int32 (some (-(2^31))) (some (2^31)) := inferInstance
-example : ToInt.Neg Int32 (some (-(2^31))) (some (2^31)) := inferInstance
-example : ToInt.Sub Int32 (some (-(2^31))) (some (2^31)) := inferInstance
+example : ToInt.Add Int32 (.sint 32) := inferInstance
+example : ToInt.Neg Int32 (.sint 32) := inferInstance
+example : ToInt.Sub Int32 (.sint 32) := inferInstance
+
+instance : ToInt.Pow Int32 (.sint 32) := ToInt.pow_of_semiring (by simp) (by simp)
 
 instance : NatCast Int64 where
   natCast x := Int64.ofNat x
@@ -158,9 +165,11 @@ instance : IsCharP Int64 (2 ^ 64) := IsCharP.mk' _ _
       ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
-example : ToInt.Add Int64 (some (-(2^63))) (some (2^63)) := inferInstance
-example : ToInt.Neg Int64 (some (-(2^63))) (some (2^63)) := inferInstance
-example : ToInt.Sub Int64 (some (-(2^63))) (some (2^63)) := inferInstance
+example : ToInt.Add Int64 (.sint 64) := inferInstance
+example : ToInt.Neg Int64 (.sint 64) := inferInstance
+example : ToInt.Sub Int64 (.sint 64) := inferInstance
+
+instance : ToInt.Pow Int64 (.sint 64) := ToInt.pow_of_semiring (by simp) (by simp)
 
 instance : NatCast ISize where
   natCast x := ISize.ofNat x
@@ -196,8 +205,13 @@ instance : IsCharP ISize (2 ^ numBits) := IsCharP.mk' _ _
       ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
-example : ToInt.Add ISize (some (-(2^(numBits-1)))) (some (2^(numBits-1))) := inferInstance
-example : ToInt.Neg ISize (some (-(2^(numBits-1)))) (some (2^(numBits-1))) := inferInstance
-example : ToInt.Sub ISize (some (-(2^(numBits-1)))) (some (2^(numBits-1))) := inferInstance
+example : ToInt.Add ISize (.sint numBits) := inferInstance
+example : ToInt.Neg ISize (.sint numBits) := inferInstance
+example : ToInt.Sub ISize (.sint numBits) := inferInstance
+
+instance : ToInt.Pow ISize (.sint numBits) :=
+  ToInt.pow_of_semiring (by simp) (by
+    rcases System.Platform.numBits_eq with h | h <;>
+    simp [h])
 
 end Lean.Grind

src/Init/GrindInstances/Ring/UInt.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 import Init.Grind.Ring.Basic
-import Init.GrindInstances.ToInt
+import all Init.GrindInstances.ToInt
 import all Init.Data.UInt.Basic
 import Init.Data.UInt.Lemmas
 
@@ -151,9 +151,11 @@ instance : IsCharP UInt8 256 := IsCharP.mk' _ _
     simp [this, UInt8.ofNat_eq_iff_mod_eq_toNat])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
-example : ToInt.Add UInt8 (some 0) (some (2^8)) := inferInstance
-example : ToInt.Neg UInt8 (some 0) (some (2^8)) := inferInstance
-example : ToInt.Sub UInt8 (some 0) (some (2^8)) := inferInstance
+example : ToInt.Add UInt8 (.uint 8) := inferInstance
+example : ToInt.Neg UInt8 (.uint 8) := inferInstance
+example : ToInt.Sub UInt8 (.uint 8) := inferInstance
+
+instance : ToInt.Pow UInt8 (.uint 8) := ToInt.pow_of_semiring (by simp) (by simp)
 
 instance : CommRing UInt16 where
   add_assoc := UInt16.add_assoc
@@ -181,9 +183,11 @@ instance : IsCharP UInt16 65536 := IsCharP.mk' _ _
     simp [this, UInt16.ofNat_eq_iff_mod_eq_toNat])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
-example : ToInt.Add UInt16 (some 0) (some (2^16)) := inferInstance
-example : ToInt.Neg UInt16 (some 0) (some (2^16)) := inferInstance
-example : ToInt.Sub UInt16 (some 0) (some (2^16)) := inferInstance
+example : ToInt.Add UInt16 (.uint 16) := inferInstance
+example : ToInt.Neg UInt16 (.uint 16) := inferInstance
+example : ToInt.Sub UInt16 (.uint 16) := inferInstance
+
+instance : ToInt.Pow UInt16 (.uint 16) := ToInt.pow_of_semiring (by simp) (by simp)
 
 instance : CommRing UInt32 where
   add_assoc := UInt32.add_assoc
@@ -211,9 +215,11 @@ instance : IsCharP UInt32 4294967296 := IsCharP.mk' _ _
     simp [this, UInt32.ofNat_eq_iff_mod_eq_toNat])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
-example : ToInt.Add UInt32 (some 0) (some (2^32)) := inferInstance
-example : ToInt.Neg UInt32 (some 0) (some (2^32)) := inferInstance
-example : ToInt.Sub UInt32 (some 0) (some (2^32)) := inferInstance
+example : ToInt.Add UInt32 (.uint 32) := inferInstance
+example : ToInt.Neg UInt32 (.uint 32) := inferInstance
+example : ToInt.Sub UInt32 (.uint 32) := inferInstance
+
+instance : ToInt.Pow UInt32 (.uint 32) := ToInt.pow_of_semiring (by simp) (by simp)
 
 instance : CommRing UInt64 where
   add_assoc := UInt64.add_assoc
@@ -241,9 +247,11 @@ instance : IsCharP UInt64 18446744073709551616 := IsCharP.mk' _ _
     simp [this, UInt64.ofNat_eq_iff_mod_eq_toNat])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
-example : ToInt.Add UInt64 (some 0) (some (2^64)) := inferInstance
-example : ToInt.Neg UInt64 (some 0) (some (2^64)) := inferInstance
-example : ToInt.Sub UInt64 (some 0) (some (2^64)) := inferInstance
+example : ToInt.Add UInt64 (.uint 64) := inferInstance
+example : ToInt.Neg UInt64 (.uint 64) := inferInstance
+example : ToInt.Sub UInt64 (.uint 64) := inferInstance
+
+instance : ToInt.Pow UInt64 (.uint 64) := ToInt.pow_of_semiring (by simp) (by simp)
 
 instance : CommRing USize where
   add_assoc := USize.add_assoc
@@ -273,8 +281,15 @@ instance : IsCharP USize (2 ^ numBits) := IsCharP.mk' _ _
     simp [this, USize.ofNat_eq_iff_mod_eq_toNat])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
-example : ToInt.Add USize (some 0) (some (2^numBits)) := inferInstance
-example : ToInt.Neg USize (some 0) (some (2^numBits)) := inferInstance
-example : ToInt.Sub USize (some 0) (some (2^numBits)) := inferInstance
+example : ToInt.Add USize (.uint numBits) := inferInstance
+example : ToInt.Neg USize (.uint numBits) := inferInstance
+example : ToInt.Sub USize (.uint numBits) := inferInstance
+
+instance : ToInt.Pow USize (.uint numBits) :=
+  ToInt.pow_of_semiring (by simp) (by
+    have := numBits_pos
+    have : numBits = numBits - 1 + 1 := by omega
+    have : 1 < 2 ^ numBits := by rw [this]; exact Nat.one_lt_two_pow' (numBits - 1)
+    simpa using Int.ofNat_lt.mpr this)
 
 end Lean.Grind

src/Init/GrindInstances/ToInt.lean

@@ -8,6 +8,7 @@ module
 prelude
 import all Init.Grind.ToInt
 import Init.Grind.Module.Basic
+import Init.Grind.Ring.ToInt
 import Init.Data.Int.DivMod.Basic
 import Init.Data.Int.Lemmas
 import Init.Data.Int.Order
@@ -19,432 +20,550 @@ namespace Lean.Grind
 
 /-! ## Instances for concrete types-/
 
-instance : ToInt Int none none where
+instance : ToInt Int .ii where
   toInt := id
   toInt_inj := by simp
-  le_toInt := by simp
-  toInt_lt := by simp
+  toInt_mem := by simp
 
 @[simp] theorem toInt_int (x : Int) : ToInt.toInt x = x := rfl
 
-instance : ToInt.Zero Int none none where
+instance : ToInt.Zero Int .ii where
   toInt_zero := by simp
 
-instance : ToInt.Add Int none none where
+instance : ToInt.OfNat Int .ii where
+  toInt_ofNat _ _ := rfl
+
+instance : ToInt.Add Int .ii where
   toInt_add := by simp
 
-instance : ToInt.Neg Int none none where
+instance : ToInt.Neg Int .ii where
   toInt_neg x := by simp
 
-instance : ToInt.Sub Int none none where
+instance : ToInt.Sub Int .ii where
   toInt_sub x y := by simp
 
-instance : ToInt.Mul Int none none where
+instance : ToInt.Mul Int .ii where
   toInt_mul x y := by simp
 
-instance : ToInt.Pow Int none none where
+instance : ToInt.Pow Int .ii where
   toInt_pow x n := by simp
 
-instance : ToInt.Mod Int none none where
+instance : ToInt.Mod Int .ii where
   toInt_mod x y := by simp
 
-instance : ToInt.Div Int none none where
+instance : ToInt.Div Int .ii where
   toInt_div x y := by simp
 
-instance : ToInt.LE Int none none where
+instance : ToInt.LE Int .ii where
   le_iff x y := by simp
 
-instance : ToInt.LT Int none none where
+instance : ToInt.LT Int .ii where
   lt_iff x y := by simp
 
-instance : ToInt Nat (some 0) none where
+instance : ToInt Nat (.ci 0) where
   toInt := Nat.cast
   toInt_inj x y := Int.ofNat_inj.mp
-  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x
-  toInt_lt := by simp
+  toInt_mem := by simp
 
 @[simp] theorem toInt_nat (x : Nat) : ToInt.toInt x = (x : Int) := rfl
 
-instance : ToInt.Zero Nat (some 0) none where
+instance : ToInt.Zero Nat (.ci 0) where
   toInt_zero := by simp
 
-instance : ToInt.Add Nat (some 0) none where
-  toInt_add := by simp
+instance : ToInt.OfNat Nat (.ci 0) where
+  toInt_ofNat _ _ := rfl
 
-instance : ToInt.Mul Nat (some 0) none where
-  toInt_mul x y := by simp
+instance : ToInt.Add Nat (.ci 0) where
+  toInt_add := by simp <;> omega
 
-instance : ToInt.Pow Nat (some 0) none where
-  toInt_pow x n := by simp
+instance : ToInt.Mul Nat (.ci 0) where
+  toInt_mul x y := by
+    dsimp only [IntInterval.wrap]
+    rw [Int.max_eq_left]
+    simp only [toInt_nat, Int.natCast_mul]
+    simp [toInt_nat, ← Int.natCast_mul]
 
-instance : ToInt.Mod Nat (some 0) none where
+instance : ToInt.Pow Nat (.ci 0) where
+  toInt_pow x n := by
+    dsimp only [IntInterval.wrap]
+    rw [Int.max_eq_left]
+    simp only [toInt_nat, Int.natCast_pow]
+    simp [toInt_nat, ← Int.natCast_pow]
+
+instance : ToInt.Sub Nat (.ci 0) where
+  toInt_sub x y := by simp; omega
+
+instance : ToInt.Mod Nat (.ci 0) where
   toInt_mod x y := by simp
 
-instance : ToInt.Div Nat (some 0) none where
+instance : ToInt.Div Nat (.ci 0) where
   toInt_div x y := by simp
 
-instance : ToInt.LE Nat (some 0) none where
+instance : ToInt.LE Nat (.ci 0) where
   le_iff x y := by simp
 
-instance : ToInt.LT Nat (some 0) none where
+instance : ToInt.LT Nat (.ci 0) where
   lt_iff x y := by simp
 
 -- Mathlib will add a `ToInt ℕ+ (some 1) none` instance.
 
-instance : ToInt (Fin n) (some 0) (some n) where
+instance : ToInt (Fin n) (.co 0 n) where
   toInt x := x.val
   toInt_inj x y w := Fin.eq_of_val_eq (Int.ofNat_inj.mp w)
-  le_toInt {lo x} w := by simp only [Option.some.injEq] at w; subst w; exact Int.natCast_nonneg x
-  toInt_lt {hi x} w := by simp only [Option.some.injEq] at w; subst w; exact Int.ofNat_lt.mpr x.isLt
+  toInt_mem := by simp
 
 @[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
+instance [NeZero n] : ToInt.Zero (Fin n) (.co 0 n) where
   toInt_zero := rfl
 
-instance : ToInt.Add (Fin n) (some 0) (some n) where
+instance [NeZero n] : ToInt.OfNat (Fin n) (.co 0 n) where
+  toInt_ofNat x h := by
+    simp at h
+    change ((x % n : Nat) : Int) = _
+    rw [Nat.mod_eq_of_lt h]
+
+instance : ToInt.Add (Fin n) (.co 0 n) where
   toInt_add x y := 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
+instance : ToInt.Mul (Fin n) (.co 0 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
+instance : ToInt.Mod (Fin n) (.co 0 n) where
   toInt_mod _ _ := rfl
 
-instance : ToInt.Div (Fin n) (some 0) (some n) where
+instance : ToInt.Div (Fin n) (.co 0 n) where
   toInt_div _ _ := rfl
 
-instance : ToInt.LE (Fin n) (some 0) (some n) where
+instance : ToInt.LE (Fin n) (.co 0 n) where
   le_iff x y := by simpa using Fin.le_def
 
-instance : ToInt.LT (Fin n) (some 0) (some n) where
+instance : ToInt.LT (Fin n) (.co 0 n) where
   lt_iff x y := by simpa using Fin.lt_def
 
-instance : ToInt UInt8 (some 0) (some (2^8)) where
+instance : ToInt UInt8 (.uint 8) where
   toInt x := (x.toNat : Int)
   toInt_inj x y w := UInt8.toNat_inj.mp (Int.ofNat_inj.mp w)
-  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
-  toInt_lt {hi x} w := by simp at w; subst w; exact Int.lt_toNat.mp (UInt8.toNat_lt x)
+  toInt_mem x := by simpa using Int.lt_toNat.mp (UInt8.toNat_lt x)
 
 @[simp] theorem toInt_uint8 (x : UInt8) : ToInt.toInt x = (x.toNat : Int) := rfl
 
-instance : ToInt.Zero UInt8 (some 0) (some (2^8)) where
+instance : ToInt.Zero UInt8 (.uint 8) where
   toInt_zero := by simp
 
-instance : ToInt.Add UInt8 (some 0) (some (2^8)) where
+instance : ToInt.OfNat UInt8 (.uint 8) where
+  toInt_ofNat x h := by
+    simp only [IntInterval.mem_co] at h
+    change ((x % 2^8 : Nat) : Int) = _
+    rw [Nat.mod_eq_of_lt (by omega)]
+
+instance : ToInt.Add UInt8 (.uint 8) where
   toInt_add x y := by simp
 
-instance : ToInt.Mul UInt8 (some 0) (some (2^8)) where
+instance : ToInt.Mul UInt8 (.uint 8) where
   toInt_mul x y := by simp
 
-instance : ToInt.Mod UInt8 (some 0) (some (2^8)) where
+-- The `ToInt.Pow` instance is defined in `Init.GrindInstances.Ring.UInt`,
+-- as it is convenient to use the ring structure.
+
+instance : ToInt.Mod UInt8 (.uint 8) where
   toInt_mod x y := by simp
 
-instance : ToInt.Div UInt8 (some 0) (some (2^8)) where
+instance : ToInt.Div UInt8 (.uint 8) where
   toInt_div x y := by simp
 
-instance : ToInt.LE UInt8 (some 0) (some (2^8)) where
+instance : ToInt.LE UInt8 (.uint 8) where
   le_iff x y := by simpa using UInt8.le_iff_toBitVec_le
 
-instance : ToInt.LT UInt8 (some 0) (some (2^8)) where
+instance : ToInt.LT UInt8 (.uint 8) where
   lt_iff x y := by simpa using UInt8.lt_iff_toBitVec_lt
 
-instance : ToInt UInt16 (some 0) (some (2^16)) where
+instance : ToInt UInt16 (.uint 16) where
   toInt x := (x.toNat : Int)
   toInt_inj x y w := UInt16.toNat_inj.mp (Int.ofNat_inj.mp w)
-  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
-  toInt_lt {hi x} w := by simp at w; subst w; exact Int.lt_toNat.mp (UInt16.toNat_lt x)
+  toInt_mem x := by simpa using Int.lt_toNat.mp (UInt16.toNat_lt x)
 
 @[simp] theorem toInt_uint16 (x : UInt16) : ToInt.toInt x = (x.toNat : Int) := rfl
 
-instance : ToInt.Zero UInt16 (some 0) (some (2^16)) where
+instance : ToInt.Zero UInt16 (.uint 16) where
   toInt_zero := by simp
 
-instance : ToInt.Add UInt16 (some 0) (some (2^16)) where
+instance : ToInt.OfNat UInt16 (.uint 16) where
+  toInt_ofNat x h := by
+    simp only [IntInterval.mem_co] at h
+    change ((x % 2^16 : Nat) : Int) = _
+    rw [Nat.mod_eq_of_lt (by omega)]
+
+instance : ToInt.Add UInt16 (.uint 16) where
   toInt_add x y := by simp
 
-instance : ToInt.Mul UInt16 (some 0) (some (2^16)) where
+instance : ToInt.Mul UInt16 (.uint 16) where
   toInt_mul x y := by simp
 
-instance : ToInt.Mod UInt16 (some 0) (some (2^16)) where
+-- The `ToInt.Pow` instance is defined in `Init.GrindInstances.Ring.UInt`,
+-- as it is convenient to use the ring structure.
+
+instance : ToInt.Mod UInt16 (.uint 16) where
   toInt_mod x y := by simp
 
-instance : ToInt.Div UInt16 (some 0) (some (2^16)) where
+instance : ToInt.Div UInt16 (.uint 16) where
   toInt_div x y := by simp
 
-instance : ToInt.LE UInt16 (some 0) (some (2^16)) where
+instance : ToInt.LE UInt16 (.uint 16) where
   le_iff x y := by simpa using UInt16.le_iff_toBitVec_le
 
-instance : ToInt.LT UInt16 (some 0) (some (2^16)) where
+instance : ToInt.LT UInt16 (.uint 16) where
   lt_iff x y := by simpa using UInt16.lt_iff_toBitVec_lt
 
-instance : ToInt UInt32 (some 0) (some (2^32)) where
+instance : ToInt UInt32 (.uint 32) where
   toInt x := (x.toNat : Int)
   toInt_inj x y w := UInt32.toNat_inj.mp (Int.ofNat_inj.mp w)
-  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
-  toInt_lt {hi x} w := by simp at w; subst w; exact Int.lt_toNat.mp (UInt32.toNat_lt x)
+  toInt_mem x := by simpa using Int.lt_toNat.mp (UInt32.toNat_lt x)
 
 @[simp] theorem toInt_uint32 (x : UInt32) : ToInt.toInt x = (x.toNat : Int) := rfl
 
-instance : ToInt.Zero UInt32 (some 0) (some (2^32)) where
+instance : ToInt.Zero UInt32 (.uint 32) where
   toInt_zero := by simp
 
-instance : ToInt.Add UInt32 (some 0) (some (2^32)) where
+instance : ToInt.OfNat UInt32 (.uint 32) where
+  toInt_ofNat x h := by
+    simp only [IntInterval.mem_co] at h
+    change ((x % 2^32 : Nat) : Int) = _
+    rw [Nat.mod_eq_of_lt (by omega)]
+
+instance : ToInt.Add UInt32 (.uint 32) where
   toInt_add x y := by simp
 
-instance : ToInt.Mul UInt32 (some 0) (some (2^32)) where
+instance : ToInt.Mul UInt32 (.uint 32) where
   toInt_mul x y := by simp
 
-instance : ToInt.Mod UInt32 (some 0) (some (2^32)) where
+-- The `ToInt.Pow` instance is defined in `Init.GrindInstances.Ring.UInt`,
+-- as it is convenient to use the ring structure.
+
+instance : ToInt.Mod UInt32 (.uint 32) where
   toInt_mod x y := by simp
 
-instance : ToInt.Div UInt32 (some 0) (some (2^32)) where
+instance : ToInt.Div UInt32 (.uint 32) where
   toInt_div x y := by simp
 
-instance : ToInt.LE UInt32 (some 0) (some (2^32)) where
+instance : ToInt.LE UInt32 (.uint 32) where
   le_iff x y := by simpa using UInt32.le_iff_toBitVec_le
 
-instance : ToInt.LT UInt32 (some 0) (some (2^32)) where
+instance : ToInt.LT UInt32 (.uint 32) where
   lt_iff x y := by simpa using UInt32.lt_iff_toBitVec_lt
 
-instance : ToInt UInt64 (some 0) (some (2^64)) where
+instance : ToInt UInt64 (.uint 64) where
   toInt x := (x.toNat : Int)
   toInt_inj x y w := UInt64.toNat_inj.mp (Int.ofNat_inj.mp w)
-  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
-  toInt_lt {hi x} w := by simp at w; subst w; exact Int.lt_toNat.mp (UInt64.toNat_lt x)
+  toInt_mem x := by simpa using Int.lt_toNat.mp (UInt64.toNat_lt x)
 
 @[simp] theorem toInt_uint64 (x : UInt64) : ToInt.toInt x = (x.toNat : Int) := rfl
 
-instance : ToInt.Zero UInt64 (some 0) (some (2^64)) where
+instance : ToInt.Zero UInt64 (.uint 64) where
   toInt_zero := by simp
 
-instance : ToInt.Add UInt64 (some 0) (some (2^64)) where
+instance : ToInt.OfNat UInt64 (.uint 64) where
+  toInt_ofNat x h := by
+    simp only [IntInterval.mem_co] at h
+    change ((x % 2^64 : Nat) : Int) = _
+    rw [Nat.mod_eq_of_lt (by omega)]
+
+instance : ToInt.Add UInt64 (.uint 64) where
   toInt_add x y := by simp
 
-instance : ToInt.Mul UInt64 (some 0) (some (2^64)) where
+instance : ToInt.Mul UInt64 (.uint 64) where
   toInt_mul x y := by simp
 
-instance : ToInt.Mod UInt64 (some 0) (some (2^64)) where
+-- The `ToInt.Pow` instance is defined in `Init.GrindInstances.Ring.UInt`,
+-- as it is convenient to use the ring structure.
+
+instance : ToInt.Mod UInt64 (.uint 64) where
   toInt_mod x y := by simp
 
-instance : ToInt.Div UInt64 (some 0) (some (2^64)) where
+instance : ToInt.Div UInt64 (.uint 64) where
   toInt_div x y := by simp
 
-instance : ToInt.LE UInt64 (some 0) (some (2^64)) where
+instance : ToInt.LE UInt64 (.uint 64) where
   le_iff x y := by simpa using UInt64.le_iff_toBitVec_le
 
-instance : ToInt.LT UInt64 (some 0) (some (2^64)) where
+instance : ToInt.LT UInt64 (.uint 64) where
   lt_iff x y := by simpa using UInt64.lt_iff_toBitVec_lt
 
-instance : ToInt USize (some 0) (some (2^System.Platform.numBits)) where
+instance : ToInt USize (.uint System.Platform.numBits) where
   toInt x := (x.toNat : Int)
   toInt_inj x y w := USize.toNat_inj.mp (Int.ofNat_inj.mp w)
-  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
-  toInt_lt {hi x} w := by
-    simp at w; subst w
+  toInt_mem x := by
+    simp only [IntInterval.mem_co, Int.ofNat_zero_le, true_and]
     rw [show (2 : Int) ^ System.Platform.numBits = (2 ^ System.Platform.numBits : Nat) by simp,
       Int.ofNat_lt]
     exact USize.toNat_lt_two_pow_numBits x
 
 @[simp] theorem toInt_usize (x : USize) : ToInt.toInt x = (x.toNat : Int) := rfl
 
-instance : ToInt.Zero USize (some 0) (some (2^System.Platform.numBits)) where
+instance : ToInt.Zero USize (.uint System.Platform.numBits) where
   toInt_zero := by simp
 
-instance : ToInt.Add USize (some 0) (some (2^System.Platform.numBits)) where
+instance : ToInt.OfNat USize (.uint System.Platform.numBits) where
+  toInt_ofNat x h := by
+    simp only [IntInterval.mem_co] at h
+    replace h : x < 2^System.Platform.numBits := by
+      suffices (x : Int) < ((2^System.Platform.numBits : Nat) : Int) by
+        exact Int.ofNat_lt.mp this
+      simpa using h.2
+    change ((x % 2^System.Platform.numBits : Nat) : Int) = _
+    rw [Nat.mod_eq_of_lt (by omega)]
+
+instance : ToInt.Add USize (.uint System.Platform.numBits) where
   toInt_add x y := by simp
 
-instance : ToInt.Mul USize (some 0) (some (2^System.Platform.numBits)) where
+instance : ToInt.Mul USize (.uint System.Platform.numBits) where
   toInt_mul x y := by simp
 
-instance : ToInt.Mod USize (some 0) (some (2^System.Platform.numBits)) where
+-- The `ToInt.Pow` instance is defined in `Init.GrindInstances.Ring.UInt`,
+-- as it is convenient to use the ring structure.
+
+instance : ToInt.Mod USize (.uint System.Platform.numBits) where
   toInt_mod x y := by simp
 
-instance : ToInt.Div USize (some 0) (some (2^System.Platform.numBits)) where
+instance : ToInt.Div USize (.uint System.Platform.numBits) where
   toInt_div x y := by simp
 
-instance : ToInt.LE USize (some 0) (some (2^System.Platform.numBits)) where
+instance : ToInt.LE USize (.uint System.Platform.numBits) where
   le_iff x y := by simpa using USize.le_iff_toBitVec_le
 
-instance : ToInt.LT USize (some 0) (some (2^System.Platform.numBits)) where
+instance : ToInt.LT USize (.uint System.Platform.numBits) where
   lt_iff x y := by simpa using USize.lt_iff_toBitVec_lt
 
-instance : ToInt Int8 (some (-2^7)) (some (2^7)) where
+instance : ToInt Int8 (.sint 8) where
   toInt x := x.toInt
   toInt_inj x y w := Int8.toInt_inj.mp w
-  le_toInt {lo x} w := by simp at w; subst w; exact Int8.le_toInt x
-  toInt_lt {hi x} w := by simp at w; subst w; exact Int8.toInt_lt x
+  toInt_mem x := by simp; exact ⟨Int8.le_toInt x, Int8.toInt_lt x⟩
 
 @[simp] theorem toInt_int8 (x : Int8) : ToInt.toInt x = (x.toInt : Int) := rfl
 
-instance : ToInt.Zero Int8 (some (-2^7)) (some (2^7)) where
+instance : ToInt.Zero Int8 (.sint 8) where
   toInt_zero := by
     --  simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
     change (0 : Int8).toInt = _
     rw [Int8.toInt_zero]
 
-instance : ToInt.Add Int8 (some (-2^7)) (some (2^7)) where
+instance : ToInt.OfNat Int8 (.sint 8) where
+  toInt_ofNat x h := by
+    simp only [IntInterval.mem_co] at h
+    rw [toInt_int8, Int8.toInt_ofNat, Int8.size, Int.bmod_eq_emod, if_neg, Int.emod_eq_of_lt] <;>
+      omega
+
+instance : ToInt.Add Int8 (.sint 8) 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
+instance : ToInt.Mul Int8 (.sint 8) where
   toInt_mul x y := by
     simp [Int.bmod_eq_emod]
     split <;> · simp; omega
 
+-- The `ToInt.Pow` instance is defined in `Init.GrindInstances.Ring.SInt`,
+-- as it is convenient to use the ring structure.
+
 -- 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`.
 
-instance : ToInt.LE Int8 (some (-2^7)) (some (2^7)) where
+instance : ToInt.LE Int8 (.sint 8) where
   le_iff x y := by simpa using Int8.le_iff_toInt_le
 
-instance : ToInt.LT Int8 (some (-2^7)) (some (2^7)) where
+instance : ToInt.LT Int8 (.sint 8) where
   lt_iff x y := by simpa using Int8.lt_iff_toInt_lt
 
-instance : ToInt Int16 (some (-2^15)) (some (2^15)) where
+instance : ToInt Int16 (.sint 16) where
   toInt x := x.toInt
   toInt_inj x y w := Int16.toInt_inj.mp w
-  le_toInt {lo x} w := by simp at w; subst w; exact Int16.le_toInt x
-  toInt_lt {hi x} w := by simp at w; subst w; exact Int16.toInt_lt x
+  toInt_mem x := by simp; exact ⟨Int16.le_toInt x, Int16.toInt_lt x⟩
 
 @[simp] theorem toInt_int16 (x : Int16) : ToInt.toInt x = (x.toInt : Int) := rfl
 
-instance : ToInt.Zero Int16 (some (-2^15)) (some (2^15)) where
+instance : ToInt.Zero Int16 (.sint 16) where
   toInt_zero := by
     -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
     change (0 : Int16).toInt = _
     rw [Int16.toInt_zero]
 
-instance : ToInt.Add Int16 (some (-2^15)) (some (2^15)) where
+instance : ToInt.OfNat Int16 (.sint 16) where
+  toInt_ofNat x h := by
+    simp only [IntInterval.mem_co] at h
+    rw [toInt_int16, Int16.toInt_ofNat, Int16.size, Int.bmod_eq_emod, if_neg, Int.emod_eq_of_lt] <;>
+      omega
+
+instance : ToInt.Add Int16 (.sint 16) 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
+instance : ToInt.Mul Int16 (.sint 16) 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
+-- The `ToInt.Pow` instance is defined in `Init.GrindInstances.Ring.SInt`,
+-- as it is convenient to use the ring structure.
+
+instance : ToInt.LE Int16 (.sint 16) where
   le_iff x y := by simpa using Int16.le_iff_toInt_le
 
-instance : ToInt.LT Int16 (some (-2^15)) (some (2^15)) where
+instance : ToInt.LT Int16 (.sint 16) where
   lt_iff x y := by simpa using Int16.lt_iff_toInt_lt
 
-instance : ToInt Int32 (some (-2^31)) (some (2^31)) where
+instance : ToInt Int32 (.sint 32) where
   toInt x := x.toInt
   toInt_inj x y w := Int32.toInt_inj.mp w
-  le_toInt {lo x} w := by simp at w; subst w; exact Int32.le_toInt x
-  toInt_lt {hi x} w := by simp at w; subst w; exact Int32.toInt_lt x
+  toInt_mem x := by simp; exact ⟨Int32.le_toInt x, Int32.toInt_lt x⟩
 
 @[simp] theorem toInt_int32 (x : Int32) : ToInt.toInt x = (x.toInt : Int) := rfl
 
-instance : ToInt.Zero Int32 (some (-2^31)) (some (2^31)) where
+instance : ToInt.Zero Int32 (.sint 32) where
   toInt_zero := by
     -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
     change (0 : Int32).toInt = _
     rw [Int32.toInt_zero]
 
-instance : ToInt.Add Int32 (some (-2^31)) (some (2^31)) where
+instance : ToInt.OfNat Int32 (.sint 32) where
+  toInt_ofNat x h := by
+    simp only [IntInterval.mem_co] at h
+    rw [toInt_int32, Int32.toInt_ofNat, Int32.size, Int.bmod_eq_emod, if_neg, Int.emod_eq_of_lt] <;>
+      omega
+
+instance : ToInt.Add Int32 (.sint 32) 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
+instance : ToInt.Mul Int32 (.sint 32) 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
+-- The `ToInt.Pow` instance is defined in `Init.GrindInstances.Ring.SInt`,
+-- as it is convenient to use the ring structure.
+
+instance : ToInt.LE Int32 (.sint 32) where
   le_iff x y := by simpa using Int32.le_iff_toInt_le
 
-instance : ToInt.LT Int32 (some (-2^31)) (some (2^31)) where
+instance : ToInt.LT Int32 (.sint 32) where
   lt_iff x y := by simpa using Int32.lt_iff_toInt_lt
 
-instance : ToInt Int64 (some (-2^63)) (some (2^63)) where
+instance : ToInt Int64 (.sint 64) where
   toInt x := x.toInt
   toInt_inj x y w := Int64.toInt_inj.mp w
-  le_toInt {lo x} w := by simp at w; subst w; exact Int64.le_toInt x
-  toInt_lt {hi x} w := by simp at w; subst w; exact Int64.toInt_lt x
+  toInt_mem x := by simp; exact ⟨Int64.le_toInt x, Int64.toInt_lt x⟩
 
 @[simp] theorem toInt_int64 (x : Int64) : ToInt.toInt x = (x.toInt : Int) := rfl
 
-instance : ToInt.Zero Int64 (some (-2^63)) (some (2^63)) where
+instance : ToInt.Zero Int64 (.sint 64) where
   toInt_zero := by
     -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error!
     change (0 : Int64).toInt = _
     rw [Int64.toInt_zero]
 
-instance : ToInt.Add Int64 (some (-2^63)) (some (2^63)) where
+instance : ToInt.OfNat Int64 (.sint 64) where
+  toInt_ofNat x h := by
+    simp only [IntInterval.mem_co] at h
+    rw [toInt_int64, Int64.toInt_ofNat, Int64.size, Int.bmod_eq_emod, if_neg, Int.emod_eq_of_lt] <;>
+      omega
+
+instance : ToInt.Add Int64 (.sint 64) 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
+instance : ToInt.Mul Int64 (.sint 64) 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
+-- The `ToInt.Pow` instance is defined in `Init.GrindInstances.Ring.SInt`,
+-- as it is convenient to use the ring structure.
+
+instance : ToInt.LE Int64 (.sint 64) where
   le_iff x y := by simpa using Int64.le_iff_toInt_le
 
-instance : ToInt.LT Int64 (some (-2^63)) (some (2^63)) where
+instance : ToInt.LT Int64 (.sint 64) where
   lt_iff x y := by simpa using Int64.lt_iff_toInt_lt
 
-instance : ToInt (BitVec v) (some 0) (some (2^v)) where
+instance : ToInt (BitVec v) (.uint v) where
   toInt x := (x.toNat : Int)
   toInt_inj x y w :=
     BitVec.eq_of_toNat_eq (Int.ofNat_inj.mp w)
-  le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat
-  toInt_lt {hi x} w := by
-    simp at w; subst w;
-    simpa using Int.ofNat_lt.mpr (BitVec.isLt x)
+  toInt_mem x := by simpa using Int.ofNat_lt.mpr (BitVec.isLt x)
 
 @[simp] theorem toInt_bitVec (x : BitVec v) : ToInt.toInt x = (x.toNat : Int) := rfl
 
-instance : ToInt.Zero (BitVec v) (some 0) (some (2^v)) where
+instance : ToInt.Zero (BitVec v) (.uint v) where
   toInt_zero := by simp
 
-instance : ToInt.Add (BitVec v) (some 0) (some (2^v)) where
+instance : ToInt.OfNat (BitVec v) (.uint v) where
+  toInt_ofNat x h := by
+    simp only [IntInterval.mem_co] at h
+    rw [toInt_bitVec]
+    simp only [BitVec.ofNat_eq_ofNat, BitVec.toNat_ofNat, Int.natCast_emod, Int.natCast_pow,
+      Int.cast_ofNat_Int]
+    rw [Int.emod_eq_of_lt] <;> omega
+
+instance : ToInt.Add (BitVec v) (.uint v) where
   toInt_add x y := by simp
 
-instance : ToInt.Mul (BitVec v) (some 0) (some (2^v)) where
+instance : ToInt.Mul (BitVec v) (.uint v) where
   toInt_mul x y := by simp
 
-instance : ToInt.Mod (BitVec v) (some 0) (some (2^v)) where
+-- The `ToInt.Pow` instance is defined in `Init.GrindInstances.Ring.BitVec`,
+-- as it is convenient to use the ring structure.
+
+instance : ToInt.Mod (BitVec v) (.uint v) where
   toInt_mod x y := by simp
 
-instance : ToInt.Div (BitVec v) (some 0) (some (2^v)) where
+instance : ToInt.Div (BitVec v) (.uint v) where
   toInt_div x y := by simp
 
-instance : ToInt.LE (BitVec v) (some 0) (some (2^v)) where
+instance : ToInt.LE (BitVec v) (.uint v) where
   le_iff x y := by simpa using BitVec.le_def
 
-instance : ToInt.LT (BitVec v) (some 0) (some (2^v)) where
+instance : ToInt.LT (BitVec v) (.uint v) where
   lt_iff x y := by simpa using BitVec.lt_def
 
-instance : ToInt ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+instance : ToInt ISize (.sint System.Platform.numBits) where
   toInt x := x.toInt
   toInt_inj x y w := ISize.toInt_inj.mp w
-  le_toInt {lo x} w := by simp at w; subst w; exact ISize.two_pow_numBits_le_toInt x
-  toInt_lt {hi x} w := by simp at w; subst w; exact ISize.toInt_lt_two_pow_numBits x
+  toInt_mem x := by simp; exact ⟨ISize.two_pow_numBits_le_toInt x, ISize.toInt_lt_two_pow_numBits x⟩
 
 @[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
+instance : ToInt.Zero ISize (.sint System.Platform.numBits) 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
+instance : ToInt.OfNat ISize (.sint System.Platform.numBits) where
+  toInt_ofNat x h := by
+    simp only [IntInterval.mem_co] at h
+    rw [toInt_isize]
+    simp only [ISize.toInt_ofNat, ISize.size]
+    have := System.Platform.numBits_pos
+    have : System.Platform.numBits - 1 + 1 = System.Platform.numBits := by omega
+    rw [Int.bmod_eq_of_le]
+    · simp
+      rw [← this, Int.pow_succ']
+      omega
+    · rw [← this, Nat.pow_succ']
+      simp
+      omega
+
+instance : ToInt.Add ISize (.sint System.Platform.numBits) where
   toInt_add x y := by
-    rw [toInt_isize, ISize.toInt_add, ToInt.wrap_eq_bmod (Int.pow_nonneg (by decide))]
+    rw [toInt_isize, ISize.toInt_add, IntInterval.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
@@ -454,9 +573,9 @@ instance : ToInt.Add ISize (some (-2^(System.Platform.numBits-1))) (some (2^(Sys
       simp
     simp [p₁, p₂]
 
-instance : ToInt.Mul ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+instance : ToInt.Mul ISize (.sint System.Platform.numBits) where
   toInt_mul x y := by
-    rw [toInt_isize, ISize.toInt_mul, ToInt.wrap_eq_bmod (Int.pow_nonneg (by decide))]
+    rw [toInt_isize, ISize.toInt_mul, IntInterval.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
@@ -466,10 +585,10 @@ instance : ToInt.Mul ISize (some (-2^(System.Platform.numBits-1))) (some (2^(Sys
       simp
     simp [p₁, p₂]
 
-instance instToIntLEISize : ToInt.LE ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+instance : ToInt.LE ISize (.sint System.Platform.numBits) where
   le_iff x y := by simpa using ISize.le_iff_toInt_le
 
-instance instToIntLTISize : ToInt.LT ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where
+instance : ToInt.LT ISize (.sint System.Platform.numBits) where
   lt_iff x y := by simpa using ISize.lt_iff_toInt_lt
 
 end Lean.Grind

src/Init/Prelude.lean

@@ -890,27 +890,6 @@ theorem ULift.up_down {α : Type u} (b : ULift.{v} α) : Eq (up (down b)) b := r
 /-- Bijection between `α` and `ULift.{v} α` -/
 theorem ULift.down_up {α : Type u} (a : α) : Eq (down (up.{v} a)) a := rfl
 
-/--
-Lifts a type or proposition to a higher universe level.
-
-`PULift α` wraps a value of type `α`. It is a generalization of
-`PLift` that allows lifting values who's type may live in `Sort s`.
-It also subsumes `PLift`.
--/
--- The universe variable `r` is written first so that `ULift.{r} α` can be used
--- when `s` can be inferred from the type of `α`.
-structure PULift.{r, s} (α : Sort s) : Sort (max s r 1) where
-  /-- Wraps a value to increase its type's universe level. -/
-  up ::
-  /-- Extracts a wrapped value from a universe-lifted type. -/
-  down : α
-
-/-- Bijection between `α` and `PULift.{v} α` -/
-theorem PULift.up_down {α : Sort u} (b : PULift.{v} α) : Eq (up (down b)) b := rfl
-
-/-- Bijection between `α` and `PULift.{v} α` -/
-theorem PULift.down_up {α : Sort u} (a : α) : Eq (down (up.{v} a)) a := rfl
-
 /--
 Either a proof that `p` is true or a proof that `p` is false. This is equivalent to a `Bool` paired
 with a proof that the `Bool` is `true` if and only if `p` is true.

src/Lean/Elab/Tactic/Monotonicity.lean

@@ -184,12 +184,11 @@ def solveMonoStep (failK : ∀ {α}, Expr → Array Name → MetaM α := @defaul
     -- A recursive call
     if let some hmono ← solveMonoCall α inst_α e then
       trace[Elab.Tactic.monotonicity] "Found recursive call {e}:{indentExpr hmono}"
-      let hmonoType ← inferType hmono
-      unless ← isDefEq hmonoType type do
+      unless ← goal.checkedAssign hmono do
         trace[Elab.Tactic.monotonicity] "Failed to assign {hmono} : {← inferType hmono} to goal"
         failK f #[]
-      goal.assign hmono
       return []
+
     let monoThms ← withLocalDeclD `f f.bindingDomain! fun f =>
       -- The discrimination tree does not like open terms
       findMonoThms (e.instantiate1 f)

src/Lean/Meta/Constructions/NoConfusion.lean

@@ -10,6 +10,10 @@ import Lean.Meta.CompletionName
 import Lean.Meta.Constructions.NoConfusionLinear
 
 
+register_builtin_option backwards.linearNoConfusionType : Bool := {
+  defValue := true
+  descr    := "use the linear-size construction for the `noConfusionType` declaration of an inductive type. Set to false to use the previous, simpler but quadratic-size construction. "
+}
 
 namespace Lean
 
@@ -24,7 +28,11 @@ def mkNoConfusionCore (declName : Name) : MetaM Unit := do
   let recInfo ← getConstInfo (mkRecName declName)
   unless recInfo.levelParams.length > indVal.levelParams.length do return
 
-  let useLinear ← NoConfusionLinear.canUse
+  let useLinear ←
+    if backwards.linearNoConfusionType.get (← getOptions) then
+      NoConfusionLinear.deps.allM (hasConst · (skipRealize := true))
+    else
+      pure false
 
   if useLinear then
     NoConfusionLinear.mkWithCtorType declName

src/Lean/Meta/Constructions/NoConfusionLinear.lean

@@ -37,24 +37,14 @@ namespace Lean.NoConfusionLinear
 
 open Meta
 
-
-register_builtin_option backwards.linearNoConfusionType : Bool := {
-  defValue := true
-  descr    := "use the linear-size construction for the `noConfusionType` declaration of an inductive type. Set to false to use the previous, simpler but quadratic-size construction. "
-}
-
 /--
 List of constants that the linear `noConfusionType` construction depends on.
 -/
-private def deps : Array Lean.Name :=
-  #[ ``cond, ``ULift, ``Eq.ndrec, ``Not, ``dite, ``Nat.decEq, ``Nat.blt ]
+def deps : Array Lean.Name :=
+  #[ ``Nat.lt, ``cond, ``Nat, ``PUnit, ``Eq, ``Not, ``dite, ``Nat.decEq, ``Nat.blt ]
 
-def canUse : MetaM Bool := do
-  unless backwards.linearNoConfusionType.get (← getOptions) do return false
-  unless (← NoConfusionLinear.deps.allM (hasConst · (skipRealize := true))) do return false
-  return true
-
-def mkNatLookupTable (n : Expr) (type : Expr) (es : Array Expr) (default : Expr) : MetaM Expr := do
+def mkNatLookupTable (n : Expr) (es : Array Expr) (default : Expr) : MetaM Expr := do
+  let type ← inferType default
   let u ← getLevel type
   let rec go (start stop : Nat) (hstart : start < stop := by omega) (hstop : stop ≤ es.size := by omega) : MetaM Expr := do
     if h : start + 1 = stop then
@@ -69,55 +59,6 @@ def mkNatLookupTable (n : Expr) (type : Expr) (es : Array Expr) (default : Expr)
   else
     go 0 es.size
 
--- Right-associates the top-most `max`s to work around #5695 for prettier code
-private def reassocMax (l : Level) : Level :=
-  let lvls := maxArgs l #[]
-  let last := lvls.back!
-  lvls.pop.foldr mkLevelMax last
-where
-  maxArgs (l : Level) (lvls : Array Level) : Array Level :=
-  match l with
-  | .max l1 l2 => maxArgs l2 (maxArgs l1 lvls)
-  | _ => lvls.push l
-
-/--
-Takes the max of the levels of the given expressions.
--/
-def maxLevels (es : Array Expr) (default : Expr) : MetaM Level := do
-  let mut maxLevel ← getLevel default
-  for e in es do
-    let l ← getLevel e
-    maxLevel := mkLevelMax' maxLevel l
-  return reassocMax maxLevel.normalize
-
-private def mkPULift (r : Level) (t : Expr) : MetaM Expr := do
-  let s ← getLevel t
-  return mkApp (mkConst `PULift [r,s]) t
-
-private def withMkPULiftUp (t : Expr) (k : Expr → MetaM Expr) : MetaM Expr := do
-  let t  ← whnf t
-  if t.isAppOfArity `PULift 1 then
-    let t' := t.appArg!
-    let e ← k t'
-    return mkApp2 (mkConst `PULift.up (t.appFn!.constLevels!)) t' e
-  else
-    throwError "withMkPULiftUp: expected PULift type, got {t}"
-
-private def mkPULiftDown (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  if t.isAppOfArity `PULift 1 then
-    let t' := t.appArg!
-    return mkApp2 (mkConst `PULift.down t.appFn!.constLevels!) t' e
-  else
-    throwError "mkULiftDown: expected ULift type, got {t}"
-
-def mkNatLookupTableLifting (n : Expr) (es : Array Expr) (default : Expr) : MetaM Expr := do
-  let u ← maxLevels es default
-  let default ← mkPULift u default
-  let u' := reassocMax (mkLevelMax' u 1).normalize
-  let es ← es.mapM (mkPULift u)
-  mkNatLookupTable n (.sort u') es default
-
 def mkWithCtorTypeName (indName : Name) : Name :=
   Name.str indName "noConfusionType" |>.str "withCtorType"
 
@@ -134,15 +75,18 @@ def mkWithCtorType (indName : Name) : MetaM Unit := do
   let v::us := casesOnInfo.levelParams.map mkLevelParam | panic! "unexpected universe levels on `casesOn`"
   let indTyCon := mkConst indName us
   let indTyKind ← inferType indTyCon
-  let e ← forallBoundedTelescope indTyKind info.numParams fun xs _ => do
+  let indLevel ← getLevel indTyKind
+  let e ← forallBoundedTelescope indTyKind info.numParams fun xs  _ => do
     withLocalDeclD `P (mkSort v.succ) fun P => do
     withLocalDeclD `ctorIdx (mkConst ``Nat) fun ctorIdx => do
+      let default ← mkArrow (mkConst ``PUnit [indLevel]) P
       let es ← info.ctors.toArray.mapM fun ctorName => do
         let ctor := mkAppN (mkConst ctorName us) xs
         let ctorType ← inferType ctor
-        forallTelescope ctorType fun ys _ =>
+        let argType ← forallTelescope ctorType fun ys _ =>
           mkForallFVars ys P
-      let e ← mkNatLookupTableLifting ctorIdx es P
+        mkArrow (mkConst ``PUnit [indLevel]) argType
+      let e ← mkNatLookupTable ctorIdx es default
       mkLambdaFVars ((xs.push P).push ctorIdx) e
 
   let declName := mkWithCtorTypeName indName
@@ -165,6 +109,7 @@ def mkWithCtor (indName : Name) : MetaM Unit := do
   let v::us := casesOnInfo.levelParams.map mkLevelParam | panic! "unexpected universe levels on `casesOn`"
   let indTyCon := mkConst indName us
   let indTyKind ← inferType indTyCon
+  let indLevel ← getLevel indTyKind
   let e ← forallBoundedTelescope indTyKind info.numParams fun xs t => do
     withLocalDeclD `P (mkSort v.succ) fun P => do
     withLocalDeclD `ctorIdx (mkConst ``Nat) fun ctorIdx => do
@@ -189,7 +134,7 @@ def mkWithCtor (indName : Name) : MetaM Unit := do
               let heq := mkApp3 (mkConst ``Eq [1]) (mkConst ``Nat) ctorIdx (mkRawNatLit i)
               let «then» ← withLocalDeclD `h heq fun h => do
                 let e ← mkEqNDRec (motive := withCtorTypeNameApp) k h
-                let e ← mkPULiftDown e
+                let e := mkApp e (mkConst ``PUnit.unit [indLevel])
                 let e := mkAppN e zs
                 -- ``Eq.ndrec
                 mkLambdaFVars #[h] e
@@ -246,16 +191,15 @@ def mkNoConfusionTypeLinear (indName : Name) : MetaM Unit := do
                 let alt := mkAppN alt xs
                 let alt := mkApp alt PType
                 let alt := mkApp alt (mkRawNatLit i)
-                let k ← withMkPULiftUp (← inferType alt).bindingDomain! fun t =>
-                  forallTelescopeReducing t fun zs2 _ => do
-                    let eqs ← (Array.zip zs1 zs2).filterMapM fun (z1,z2) => do
-                      if (← isProof z1) then
-                        return none
-                      else
-                        return some (← mkEqHEq z1 z2)
-                    let k ← mkArrowN eqs P
-                    let k ← mkArrow k P
-                    mkLambdaFVars zs2 k
+                let k ← forallTelescopeReducing (← inferType alt).bindingDomain! fun zs2 _ => do
+                  let eqs ← (Array.zip zs1 zs2[1:]).filterMapM fun (z1,z2) => do
+                    if (← isProof z1) then
+                      return none
+                    else
+                      return some (← mkEqHEq z1 z2)
+                  let k ← mkArrowN eqs P
+                  let k ← mkArrow k P
+                  mkLambdaFVars zs2 k
                 let alt := mkApp alt k
                 let alt := mkApp alt P
                 let alt := mkAppN alt ys

tests/lean/run/8894.lean

@@ -1,50 +0,0 @@
-open Lean.Order
-
-def A : Type := Prop
-def B : Type := Prop
-
-instance : Lean.Order.PartialOrder A where
-  rel := sorry
-  rel_refl := sorry
-  rel_trans := sorry
-  rel_antisymm := sorry
-
-instance : Lean.Order.PartialOrder B where
-  rel := sorry
-  rel_refl := sorry
-  rel_trans := sorry
-  rel_antisymm := sorry
-
-instance : Lean.Order.CCPO A where
-  csup := sorry
-  csup_spec := sorry
-
-instance : Lean.Order.CCPO B where
-  csup := sorry
-  csup_spec := sorry
-
-/--
-error: Could not prove 'tick' to be monotone in its recursive calls:
-  Cannot eliminate recursive call in
-    tock (n + 1)
--/
-#guard_msgs in
-mutual
-  def tick (n : Nat): A :=
-    tock (n + 1)
-  partial_fixpoint
-
-  def tock (n : Nat) : B :=
-    tick (n + 1)
-  partial_fixpoint
-end
-
-mutual
-  def tick2 (n : Nat): A :=
-    tock2 (n + 1)
-  partial_fixpoint
-
-  def tock2 (n : Nat) : A :=
-    tick2 (n + 1)
-  partial_fixpoint
-end

tests/lean/run/grind_toint_instances.lean

@@ -0,0 +1,153 @@
+open Lean.Grind
+
+#synth ToInt.Add Nat (.ci 0)
+variable (n : Nat) in
+#synth ToInt.Add (Fin n) (.co 0 n)
+#synth ToInt.Add UInt8 (.uint 8)
+#synth ToInt.Add UInt16 (.uint 16)
+#synth ToInt.Add UInt32 (.uint 32)
+#synth ToInt.Add UInt64 (.uint 64)
+#synth ToInt.Add USize (.uint System.Platform.numBits)
+#synth ToInt.Add Int8 (.sint 8)
+#synth ToInt.Add Int16 (.sint 16)
+#synth ToInt.Add Int32 (.sint 32)
+#synth ToInt.Add Int64 (.sint 64)
+#synth ToInt.Add ISize (.sint System.Platform.numBits)
+variable (w : Nat) in
+#synth ToInt.Add (BitVec w) (.uint w)
+
+#synth ToInt.Mul Nat (.ci 0)
+variable (n : Nat) in
+#synth ToInt.Mul (Fin n) (.co 0 n)
+#synth ToInt.Mul UInt8 (.uint 8)
+#synth ToInt.Mul UInt16 (.uint 16)
+#synth ToInt.Mul UInt32 (.uint 32)
+#synth ToInt.Mul UInt64 (.uint 64)
+#synth ToInt.Mul USize (.uint System.Platform.numBits)
+#synth ToInt.Mul Int8 (.sint 8)
+#synth ToInt.Mul Int16 (.sint 16)
+#synth ToInt.Mul Int32 (.sint 32)
+#synth ToInt.Mul Int64 (.sint 64)
+#synth ToInt.Mul ISize (.sint System.Platform.numBits)
+variable (w : Nat) in
+#synth ToInt.Mul (BitVec w) (.uint w)
+
+#synth ToInt.OfNat Nat (.ci 0)
+variable (n : Nat) [NeZero n] in
+#synth ToInt.OfNat (Fin n) (.co 0 n)
+#synth ToInt.OfNat UInt8 (.uint 8)
+#synth ToInt.OfNat UInt16 (.uint 16)
+#synth ToInt.OfNat UInt32 (.uint 32)
+#synth ToInt.OfNat UInt64 (.uint 64)
+#synth ToInt.OfNat USize (.uint System.Platform.numBits)
+#synth ToInt.OfNat Int8 (.sint 8)
+#synth ToInt.OfNat Int16 (.sint 16)
+#synth ToInt.OfNat Int32 (.sint 32)
+#synth ToInt.OfNat Int64 (.sint 64)
+#synth ToInt.OfNat ISize (.sint System.Platform.numBits)
+variable (w : Nat) in
+#synth ToInt.OfNat (BitVec w) (.uint w)
+
+#synth ToInt.Pow Nat (.ci 0)
+variable (n : Nat) [NeZero n] in
+#synth ToInt.Pow (Fin n) (.co 0 n)
+#synth ToInt.Pow UInt8 (.uint 8)
+#synth ToInt.Pow UInt16 (.uint 16)
+#synth ToInt.Pow UInt32 (.uint 32)
+#synth ToInt.Pow UInt64 (.uint 64)
+#synth ToInt.Pow USize (.uint System.Platform.numBits)
+#synth ToInt.Pow Int8 (.sint 8)
+#synth ToInt.Pow Int16 (.sint 16)
+#synth ToInt.Pow Int32 (.sint 32)
+#synth ToInt.Pow Int64 (.sint 64)
+#synth ToInt.Pow ISize (.sint System.Platform.numBits)
+variable (w : Nat) [NeZero w] in
+#synth ToInt.Pow (BitVec w) (.uint w)
+
+-- No `Neg` instance for `Nat`. (But there is a `Sub` instance, below.)
+variable (n : Nat) [NeZero n] in
+#synth ToInt.Neg (Fin n) (.co 0 n)
+#synth ToInt.Neg UInt8 (.uint 8)
+#synth ToInt.Neg UInt16 (.uint 16)
+#synth ToInt.Neg UInt32 (.uint 32)
+#synth ToInt.Neg UInt64 (.uint 64)
+#synth ToInt.Neg USize (.uint System.Platform.numBits)
+#synth ToInt.Neg Int8 (.sint 8)
+#synth ToInt.Neg Int16 (.sint 16)
+#synth ToInt.Neg Int32 (.sint 32)
+#synth ToInt.Neg Int64 (.sint 64)
+#synth ToInt.Neg ISize (.sint System.Platform.numBits)
+variable (w : Nat) in
+#synth ToInt.Neg (BitVec w) (.uint w)
+
+#synth ToInt.Sub Nat (.ci 0)
+variable (n : Nat) [NeZero n] in
+#synth ToInt.Sub (Fin n) (.co 0 n)
+#synth ToInt.Sub UInt8 (.uint 8)
+#synth ToInt.Sub UInt16 (.uint 16)
+#synth ToInt.Sub UInt32 (.uint 32)
+#synth ToInt.Sub UInt64 (.uint 64)
+#synth ToInt.Sub USize (.uint System.Platform.numBits)
+#synth ToInt.Sub Int8 (.sint 8)
+#synth ToInt.Sub Int16 (.sint 16)
+#synth ToInt.Sub Int32 (.sint 32)
+#synth ToInt.Sub Int64 (.sint 64)
+#synth ToInt.Sub ISize (.sint System.Platform.numBits)
+variable (w : Nat) in
+#synth ToInt.Sub (BitVec w) (.uint w)
+
+#synth ToInt.Mod Nat (.ci 0)
+variable (n : Nat) [NeZero n] in
+#synth ToInt.Mod (Fin n) (.co 0 n)
+#synth ToInt.Mod UInt8 (.uint 8)
+#synth ToInt.Mod UInt16 (.uint 16)
+#synth ToInt.Mod UInt32 (.uint 32)
+#synth ToInt.Mod UInt64 (.uint 64)
+#synth ToInt.Mod USize (.uint System.Platform.numBits)
+-- No `Mod` instances for signed integers.
+variable (w : Nat) [NeZero w] in
+#synth ToInt.Mod (BitVec w) (.uint w)
+
+#synth ToInt.Div Nat (.ci 0)
+variable (n : Nat) [NeZero n] in
+#synth ToInt.Div (Fin n) (.co 0 n)
+#synth ToInt.Div UInt8 (.uint 8)
+#synth ToInt.Div UInt16 (.uint 16)
+#synth ToInt.Div UInt32 (.uint 32)
+#synth ToInt.Div UInt64 (.uint 64)
+#synth ToInt.Div USize (.uint System.Platform.numBits)
+-- No `Div` instances for signed integers.
+variable (w : Nat) [NeZero w] in
+#synth ToInt.Div (BitVec w) (.uint w)
+
+#synth ToInt.LE Nat (.ci 0)
+variable (n : Nat) in
+#synth ToInt.LE (Fin n) (.co 0 n)
+#synth ToInt.LE UInt8 (.uint 8)
+#synth ToInt.LE UInt16 (.uint 16)
+#synth ToInt.LE UInt32 (.uint 32)
+#synth ToInt.LE UInt64 (.uint 64)
+#synth ToInt.LE USize (.uint System.Platform.numBits)
+#synth ToInt.LE Int8 (.sint 8)
+#synth ToInt.LE Int16 (.sint 16)
+#synth ToInt.LE Int32 (.sint 32)
+#synth ToInt.LE Int64 (.sint 64)
+#synth ToInt.LE ISize (.sint System.Platform.numBits)
+variable (w : Nat) in
+#synth ToInt.LE (BitVec w) (.uint w)
+
+#synth ToInt.LT Nat (.ci 0)
+variable (n : Nat) in
+#synth ToInt.LT (Fin n) (.co 0 n)
+#synth ToInt.LT UInt8 (.uint 8)
+#synth ToInt.LT UInt16 (.uint 16)
+#synth ToInt.LT UInt32 (.uint 32)
+#synth ToInt.LT UInt64 (.uint 64)
+#synth ToInt.LT USize (.uint System.Platform.numBits)
+#synth ToInt.LT Int8 (.sint 8)
+#synth ToInt.LT Int16 (.sint 16)
+#synth ToInt.LT Int32 (.sint 32)
+#synth ToInt.LT Int64 (.sint 64)
+#synth ToInt.LT ISize (.sint System.Platform.numBits)
+variable (w : Nat) in
+#synth ToInt.LT (BitVec w) (.uint w)

tests/lean/run/ind_whnf.lean

@@ -4,7 +4,7 @@ inductive Expr : id Type
 
 partial def Expr.fold (f : Nat → α → α) : Expr → α → α
   | var n,    a => f n a
-  | app _ as, a => as.foldl (init := a) fun a e => fold f e a
+  | app s as, a => as.foldl (init := a) fun a e => fold f e a
 
 def Expr.isVar : Expr → Bool
   | var _ => true

tests/lean/run/issue8962.lean

@@ -1,40 +0,0 @@
--- This triggered a bug in the linear-size `noConfusionType` construction
--- which confused the kernel when producing the `noConfusion` lemma.
-
-set_option debug.skipKernelTC true
-set_option pp.universes true
-
--- Works
-
-inductive S where
-| a {α : Sort u} {β : Type v} (f : α → β)
-| b
-
-/--
-info: @[reducible] protected def S.noConfusionType.withCtorType.{u_1, u, v} : Type u_1 → Nat → Type (max u u_1 (v + 1)) :=
-fun P ctorIdx =>
-  bif Nat.blt ctorIdx 1 then
-    PULift.{max (u + 1) (u_1 + 1) (v + 2), max (max (u + 1) (u_1 + 1)) (v + 2)}
-      ({α : Sort u} → {β : Type v} → (α → β) → P)
-  else PULift.{max (u + 1) (u_1 + 1) (v + 2), u_1 + 1} P
--/
-#guard_msgs in
-#print S.noConfusionType.withCtorType
-
--- Didn't work
-
-inductive T where
-| a {α : Sort u} {β : Sort v} (f : α → β)
-| b
-
-/--
-info: @[reducible] protected def T.noConfusionType.withCtorType.{u_1, u, v} : Type u_1 →
-  Nat → Sort (max (u + 1) (u_1 + 1) (v + 1) (imax u v)) :=
-fun P ctorIdx =>
-  bif Nat.blt ctorIdx 1 then
-    PULift.{max (u + 1) (u_1 + 1) (v + 1) (imax u v), max (max (max (u + 1) (u_1 + 1)) (v + 1)) (imax u v)}
-      ({α : Sort u} → {β : Sort v} → (α → β) → P)
-  else PULift.{max (u + 1) (u_1 + 1) (v + 1) (imax u v), u_1 + 1} P
--/
-#guard_msgs in
-#print T.noConfusionType.withCtorType

tests/lean/run/linearNoConfusion.lean

@@ -12,60 +12,53 @@ inductive Vec.{u} (α : Type) : Nat → Type u where
   | nil : Vec α 0
   | cons {n} : α → Vec α n → Vec α (n + 1)
 
-
 @[reducible] protected def Vec.noConfusionType.withCtorType'.{u_1, u} :
-  Type → Type u_1 → Nat → Type (max u u_1) :=
-fun α P ctorIdx =>
-  bif Nat.blt ctorIdx 1 then PULift.{max (u+1) (u_1+1)} P
-  else PULift.{max (u+1) (u_1+1)} ({n : Nat} → α → Vec.{u} α n → P)
+    Type → Type u_1 → Nat → Type (max (u + 1) u_1) := fun α P ctorIdx =>
+  bif Nat.blt ctorIdx 1
+  then PUnit.{u + 2} → P
+  else PUnit.{u + 2} → {n : Nat} → α → Vec.{u} α n → P
 
 /--
-info: @[reducible] protected def Vec.noConfusionType.withCtorType.{u_1, u} : Type → Type u_1 → Nat → Type (max u u_1) :=
-fun α P ctorIdx =>
-  bif Nat.blt ctorIdx 1 then PULift.{max (u + 1) (u_1 + 1), u_1 + 1} P
-  else PULift.{max (u + 1) (u_1 + 1), max (u + 1) (u_1 + 1)} ({n : Nat} → α → Vec.{u} α n → P)
+info: @[reducible] protected def Vec.noConfusionType.withCtorType.{u_1, u} : Type → Type u_1 → Nat → Type (max (u + 1) u_1) :=
+fun α P ctorIdx => bif ctorIdx.blt 1 then PUnit → P else PUnit → {n : Nat} → α → Vec α n → P
 -/
 #guard_msgs in
-set_option pp.universes true in
 #print Vec.noConfusionType.withCtorType
 
 example : @Vec.noConfusionType.withCtorType.{u_1,u} = @Vec.noConfusionType.withCtorType'.{u_1,u} := rfl
 
-
 @[reducible] protected noncomputable def Vec.noConfusionType.withCtor'.{u_1, u} : (α : Type) →
   (P : Type u_1) → (ctorIdx : Nat) → Vec.noConfusionType.withCtorType' α P ctorIdx → P → (a : Nat) → Vec.{u} α a → P :=
 fun _α _P ctorIdx k k' _a x =>
   Vec.casesOn x
-    (if h : ctorIdx = 0 then (Eq.ndrec k h).down else k')
-    (fun a a_1 => if h : ctorIdx = 1 then (Eq.ndrec k h).down a a_1 else k')
+    (if h : ctorIdx = 0 then Eq.ndrec k h PUnit.unit else k')
+    (fun a a_1 => if h : ctorIdx = 1 then Eq.ndrec k h PUnit.unit a a_1 else k')
 
 /--
 info: @[reducible] protected def Vec.noConfusionType.withCtor.{u_1, u} : (α : Type) →
   (P : Type u_1) → (ctorIdx : Nat) → Vec.noConfusionType.withCtorType α P ctorIdx → P → (a : Nat) → Vec α a → P :=
 fun α P ctorIdx k k' a x =>
-  Vec.casesOn x (if h : ctorIdx = 0 then (h ▸ k).down else k') fun {n} a a_1 =>
-    if h : ctorIdx = 1 then (h ▸ k).down a a_1 else k'
+  Vec.casesOn x (if h : ctorIdx = 0 then (h ▸ k) PUnit.unit else k') fun {n} a a_1 =>
+    if h : ctorIdx = 1 then (h ▸ k) PUnit.unit a a_1 else k'
 -/
 #guard_msgs in
 #print Vec.noConfusionType.withCtor
 
 example : @Vec.noConfusionType.withCtor.{u_1,u} = @Vec.noConfusionType.withCtor'.{u_1,u} := rfl
 
-
 @[reducible] protected def Vec.noConfusionType'.{u_1, u} : {α : Type} →
   {a : Nat} → Sort u_1 → Vec.{u} α a → Vec α a → Sort u_1 :=
 fun {α} {a} P x1 x2 =>
   Vec.casesOn x1
-    (Vec.noConfusionType.withCtor' α (Sort u_1) 0 ⟨P → P⟩ P a x2)
-    (fun {n} a_1 a_2 => Vec.noConfusionType.withCtor' α (Sort u_1) 1 ⟨fun {n_1} a a_3 => (n = n_1 → a_1 = a → a_2 ≍ a_3 → P) → P⟩ P a x2)
+    (Vec.noConfusionType.withCtor' α (Sort u_1) 0 (fun _x => P → P) P a x2)
+    (fun {n} a_1 a_2 => Vec.noConfusionType.withCtor' α (Sort u_1) 1 (fun _x {n_1} a a_3 => (n = n_1 → a_1 = a → a_2 ≍ a_3 → P) → P) P a x2)
 
 /--
 info: @[reducible] protected def Vec.noConfusionType.{u_1, u} : {α : Type} →
   {a : Nat} → Sort u_1 → Vec α a → Vec α a → Sort u_1 :=
 fun {α} {a} P x1 x2 =>
-  Vec.casesOn x1 (Vec.noConfusionType.withCtor α (Sort u_1) 0 { down := P → P } P a x2) fun {n} a_1 a_2 =>
-    Vec.noConfusionType.withCtor α (Sort u_1) 1 { down := fun {n_1} a a_3 => (n = n_1 → a_1 = a → a_2 ≍ a_3 → P) → P } P
-      a x2
+  Vec.casesOn x1 (Vec.noConfusionType.withCtor α (Sort u_1) 0 (fun x => P → P) P a x2) fun {n} a_1 a_2 =>
+    Vec.noConfusionType.withCtor α (Sort u_1) 1 (fun x {n_1} a a_3 => (n = n_1 → a_1 = a → a_2 ≍ a_3 → P) → P) P a x2
 -/
 #guard_msgs in
 #print Vec.noConfusionType
@@ -91,9 +84,3 @@ run_meta do
 -- inductive Enum.{u} : Type u where | a | b
 -- set_option pp.universes true in
 -- #print noConfusionTypeEnum
-
--- A possibly tricky universes case (resulting universe cannot be decremented)
-
-inductive UnivTest.{u,v} (α : Sort v): Sort (max u v 1) where
-  | mk1 : UnivTest α
-  | mk2 : (x : α) → UnivTest α