missing theorem

src/Init/Data/BitVec/Basic.lean

@@ -227,20 +227,6 @@ SMT-LIB name: `bvmul`.
 protected def mul (x y : BitVec n) : BitVec n := BitVec.ofNat n (x.toNat * y.toNat)
 instance : Mul (BitVec n) := ⟨.mul⟩
 
-/--
-Raises a bitvector to a natural number power. Usually accessed via the `^` operator.
-
-Note that this is currently an inefficient implementation,
-and should be replaced via an `@[extern]` with a native implementation.
-See https://github.com/leanprover/lean4/issues/7887.
--/
-protected def pow (x : BitVec n) (y : Nat) : BitVec n :=
-  match y with
-  | 0 => 1
-  | y + 1 => x.pow y * x
-instance : Pow (BitVec n) Nat where
-  pow x y := x.pow y
-
 /--
 Unsigned division of bitvectors using the Lean convention where division by zero returns zero.
 Usually accessed via the `/` operator.

src/Init/Data/BitVec/Lemmas.lean

@@ -3653,13 +3653,6 @@ theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := b
 @[simp, bitvec_to_nat] theorem toNat_mul (x y : BitVec n) : (x * y).toNat = (x.toNat * y.toNat) % 2 ^ n := rfl
 @[simp] theorem toFin_mul (x y : BitVec n) : (x * y).toFin = (x.toFin * y.toFin) := rfl
 
-theorem ofNat_mul {n} (x y : Nat) : BitVec.ofNat n (x * y) = BitVec.ofNat n x * BitVec.ofNat n y := by
-  apply eq_of_toNat_eq
-  simp [BitVec.ofNat, Fin.ofNat'_mul]
-
-theorem ofNat_mul_ofNat {n} (x y : Nat) : BitVec.ofNat n x * BitVec.ofNat n y = BitVec.ofNat n (x * y) :=
-  (ofNat_mul x y).symm
-
 protected theorem mul_comm (x y : BitVec w) : x * y = y * x := by
   apply eq_of_toFin_eq; simpa using Fin.mul_comm ..
 instance : Std.Commutative (fun (x y : BitVec w) => x * y) := ⟨BitVec.mul_comm⟩
@@ -3753,22 +3746,6 @@ theorem setWidth_mul (x y : BitVec w) (h : i ≤ w) :
   have dvd : 2^i ∣ 2^w := Nat.pow_dvd_pow _ h
   simp [bitvec_to_nat, h, Nat.mod_mod_of_dvd _ dvd]
 
-/-! ### pow -/
-
-@[simp]
-protected theorem pow_zero {x : BitVec w} : x ^ 0 = 1#w := rfl
-
-protected theorem pow_succ {x : BitVec w} : x ^ (n + 1) = x ^ n * x := rfl
-
-@[simp]
-protected theorem pow_one {x : BitVec w} : x ^ 1 = x := by simp [BitVec.pow_succ]
-
-protected theorem pow_add {x : BitVec w} {n m : Nat}: x ^ (n + m) = (x ^ n) * (x ^ m):= by
-  induction m with
-  | zero => simp
-  | succ m ih =>
-    rw [← Nat.add_assoc, BitVec.pow_succ, ih, BitVec.mul_assoc, BitVec.pow_succ]
-
 /-! ### le and lt -/
 
 @[bitvec_to_nat] theorem le_def {x y : BitVec n} :

src/Init/Data/Fin/Lemmas.lean

@@ -976,16 +976,6 @@ theorem coe_sub_iff_lt {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b
 
 /-! ### mul -/
 
-theorem ofNat'_mul [NeZero n] (x : Nat) (y : Fin n) :
-    Fin.ofNat' n x * y = Fin.ofNat' n (x * y.val) := by
-  apply Fin.eq_of_val_eq
-  simp [Fin.ofNat', Fin.mul_def]
-
-theorem mul_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
-    x * Fin.ofNat' n y = Fin.ofNat' n (x.val * y) := by
-  apply Fin.eq_of_val_eq
-  simp [Fin.ofNat', Fin.mul_def]
-
 theorem val_mul {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n
   | ⟨_, _⟩, ⟨_, _⟩ => rfl
 

src/Init/Data/Int/Basic.lean

@@ -420,8 +420,6 @@ instance : IntCast Int where intCast n := n
 protected def Int.cast {R : Type u} [IntCast R] : Int → R :=
   IntCast.intCast
 
-@[simp] theorem Int.cast_eq (x : Int) : Int.cast x = x := rfl
-
 -- see the notes about coercions into arbitrary types in the module doc-string
 instance [IntCast R] : CoeTail Int R where coe := Int.cast
 

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -2145,11 +2145,6 @@ theorem bmod_pos (x : Int) (m : Nat) (p : x % m < (m + 1) / 2) : bmod x m = x %
 theorem bmod_neg (x : Int) (m : Nat) (p : x % m ≥ (m + 1) / 2) : bmod x m = (x % m) - m := by
   simp [bmod_def, Int.not_lt.mpr p]
 
-theorem bmod_eq_emod (x : Int) (m : Nat) : bmod x m = x % m - if x % m ≥ (m + 1) / 2 then m else 0 := by
-  split
-  · rwa [bmod_neg]
-  · rw [bmod_pos] <;> simp_all
-
 @[simp]
 theorem bmod_one_is_zero (x : Int) : Int.bmod x 1 = 0 := by
   simp [Int.bmod]
@@ -2378,18 +2373,6 @@ theorem bmod_neg_bmod : bmod (-(bmod x n)) n = bmod (-x) n := by
   apply (bmod_add_cancel_right x).mp
   rw [Int.add_left_neg, ← add_bmod_bmod, Int.add_left_neg]
 
-theorem dvd_iff_bmod_eq_zero {a : Nat} {b : Int} : (a : Int) ∣ b ↔ b.bmod a = 0 := by
-  rw [dvd_iff_emod_eq_zero, bmod]
-  split <;> rename_i h
-  · rfl
-  · simp only [Int.not_lt] at h
-    match a with
-    | 0 => omega
-    | a + 1 =>
-      have : b % (a+1) < a + 1 := emod_lt b (by omega)
-      simp_all
-      omega
-
 /-! Helper theorems for `dvd` simproc -/
 
 protected theorem dvd_eq_true_of_mod_eq_zero {a b : Int} (h : b % a == 0) : (a ∣ b) = True := by

src/Init/Data/Int/Order.lean

@@ -603,14 +603,6 @@ theorem toNat_mul {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a * b).toNat = a.
   match a, b, eq_ofNat_of_zero_le ha, eq_ofNat_of_zero_le hb with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => rfl
 
-/--
-Variant of `Int.toNat_sub` taking non-negativity hypotheses,
-rather than expecting the arguments to be casts of natural numbers.
--/
-theorem toNat_sub'' {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a - b).toNat = a.toNat - b.toNat :=
-  match a, b, eq_ofNat_of_zero_le ha, eq_ofNat_of_zero_le hb with
-  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => toNat_sub _ _
-
 theorem toNat_add_nat {a : Int} (ha : 0 ≤ a) (n : Nat) : (a + n).toNat = a.toNat + n :=
   match a, eq_ofNat_of_zero_le ha with | _, ⟨_, rfl⟩ => rfl
 

src/Init/Data/SInt/Basic.lean

@@ -239,17 +239,6 @@ Examples:
 @[extern "lean_int8_div"]
 protected def Int8.div (a b : Int8) : Int8 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
 /--
-The power operation, raising an 8-bit signed integer to a natural number power,
-wrapping around on overflow. Usually accessed via the `^` operator.
-
-This function is currently *not* overridden at runtime with an efficient implementation,
-and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
--/
-protected def Int8.pow (x : Int8) (n : Nat) : Int8 :=
-  match n with
-  | 0 => 1
-  | n + 1 => Int8.mul (Int8.pow x n) x
-/--
 The modulo operator for 8-bit signed integers, which computes the remainder when dividing one
 integer by another with the T-rounding convention used by `Int8.div`. Usually accessed via the `%`
 operator.
@@ -377,7 +366,6 @@ instance : Inhabited Int8 where
 instance : Add Int8         := ⟨Int8.add⟩
 instance : Sub Int8         := ⟨Int8.sub⟩
 instance : Mul Int8         := ⟨Int8.mul⟩
-instance : Pow Int8 Nat     := ⟨Int8.pow⟩
 instance : Mod Int8         := ⟨Int8.mod⟩
 instance : Div Int8         := ⟨Int8.div⟩
 instance : LT Int8          := ⟨Int8.lt⟩
@@ -610,17 +598,6 @@ Examples:
 @[extern "lean_int16_div"]
 protected def Int16.div (a b : Int16) : Int16 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
 /--
-The power operation, raising a 16-bit signed integer to a natural number power,
-wrapping around on overflow. Usually accessed via the `^` operator.
-
-This function is currently *not* overridden at runtime with an efficient implementation,
-and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
--/
-protected def Int16.pow (x : Int16) (n : Nat) : Int16 :=
-  match n with
-  | 0 => 1
-  | n + 1 => Int16.mul (Int16.pow x n) x
-/--
 The modulo operator for 16-bit signed integers, which computes the remainder when dividing one
 integer by another with the T-rounding convention used by `Int16.div`. Usually accessed via the `%`
 operator.
@@ -748,7 +725,6 @@ instance : Inhabited Int16 where
 instance : Add Int16         := ⟨Int16.add⟩
 instance : Sub Int16         := ⟨Int16.sub⟩
 instance : Mul Int16         := ⟨Int16.mul⟩
-instance : Pow Int16 Nat     := ⟨Int16.pow⟩
 instance : Mod Int16         := ⟨Int16.mod⟩
 instance : Div Int16         := ⟨Int16.div⟩
 instance : LT Int16          := ⟨Int16.lt⟩
@@ -997,17 +973,6 @@ Examples:
 @[extern "lean_int32_div"]
 protected def Int32.div (a b : Int32) : Int32 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
 /--
-The power operation, raising a 32-bit signed integer to a natural number power,
-wrapping around on overflow. Usually accessed via the `^` operator.
-
-This function is currently *not* overridden at runtime with an efficient implementation,
-and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
--/
-protected def Int32.pow (x : Int32) (n : Nat) : Int32 :=
-  match n with
-  | 0 => 1
-  | n + 1 => Int32.mul (Int32.pow x n) x
-/--
 The modulo operator for 32-bit signed integers, which computes the remainder when dividing one
 integer by another with the T-rounding convention used by `Int32.div`. Usually accessed via the `%`
 operator.
@@ -1135,7 +1100,6 @@ instance : Inhabited Int32 where
 instance : Add Int32         := ⟨Int32.add⟩
 instance : Sub Int32         := ⟨Int32.sub⟩
 instance : Mul Int32         := ⟨Int32.mul⟩
-instance : Pow Int32 Nat     := ⟨Int32.pow⟩
 instance : Mod Int32         := ⟨Int32.mod⟩
 instance : Div Int32         := ⟨Int32.div⟩
 instance : LT Int32          := ⟨Int32.lt⟩
@@ -1404,17 +1368,6 @@ Examples:
 @[extern "lean_int64_div"]
 protected def Int64.div (a b : Int64) : Int64 := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
 /--
-The power operation, raising a 64-bit signed integer to a natural number power,
-wrapping around on overflow. Usually accessed via the `^` operator.
-
-This function is currently *not* overridden at runtime with an efficient implementation,
-and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
--/
-protected def Int64.pow (x : Int64) (n : Nat) : Int64 :=
-  match n with
-  | 0 => 1
-  | n + 1 => Int64.mul (Int64.pow x n) x
-/--
 The modulo operator for 64-bit signed integers, which computes the remainder when dividing one
 integer by another with the T-rounding convention used by `Int64.div`. Usually accessed via the `%`
 operator.
@@ -1542,7 +1495,6 @@ instance : Inhabited Int64 where
 instance : Add Int64         := ⟨Int64.add⟩
 instance : Sub Int64         := ⟨Int64.sub⟩
 instance : Mul Int64         := ⟨Int64.mul⟩
-instance : Pow Int64 Nat     := ⟨Int64.pow⟩
 instance : Mod Int64         := ⟨Int64.mod⟩
 instance : Div Int64         := ⟨Int64.div⟩
 instance : LT Int64          := ⟨Int64.lt⟩
@@ -1794,17 +1746,6 @@ Examples:
 @[extern "lean_isize_div"]
 protected def ISize.div (a b : ISize) : ISize := ⟨⟨BitVec.sdiv a.toBitVec b.toBitVec⟩⟩
 /--
-The power operation, raising a word-sized signed integer to a natural number power,
-wrapping around on overflow. Usually accessed via the `^` operator.
-
-This function is currently *not* overridden at runtime with an efficient implementation,
-and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
--/
-protected def ISize.pow (x : ISize) (n : Nat) : ISize :=
-  match n with
-  | 0 => 1
-  | n + 1 => ISize.mul (ISize.pow x n) x
-/--
 The modulo operator for word-sized signed integers, which computes the remainder when dividing one
 integer by another with the T-rounding convention used by `ISize.div`. Usually accessed via the `%`
 operator.
@@ -1934,7 +1875,6 @@ instance : Inhabited ISize where
 instance : Add ISize         := ⟨ISize.add⟩
 instance : Sub ISize         := ⟨ISize.sub⟩
 instance : Mul ISize         := ⟨ISize.mul⟩
-instance : Pow ISize Nat     := ⟨ISize.pow⟩
 instance : Mod ISize         := ⟨ISize.mod⟩
 instance : Div ISize         := ⟨ISize.div⟩
 instance : LT ISize          := ⟨ISize.lt⟩

src/Init/Data/SInt/Lemmas.lean

@@ -2625,17 +2625,6 @@ instance : Std.LawfulCommIdentity (α := ISize) (· * ·) 1 where
 @[simp] theorem Int64.zero_mul {a : Int64} : 0 * a = 0 := Int64.toBitVec_inj.1 BitVec.zero_mul
 @[simp] theorem ISize.zero_mul {a : ISize} : 0 * a = 0 := ISize.toBitVec_inj.1 BitVec.zero_mul
 
-@[simp] protected theorem Int8.pow_zero (x : Int8) : x ^ 0 = 1 := rfl
-protected theorem Int8.pow_succ (x : Int8) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
-@[simp] protected theorem Int16.pow_zero (x : Int16) : x ^ 0 = 1 := rfl
-protected theorem Int16.pow_succ (x : Int16) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
-@[simp] protected theorem Int32.pow_zero (x : Int32) : x ^ 0 = 1 := rfl
-protected theorem Int32.pow_succ (x : Int32) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
-@[simp] protected theorem Int64.pow_zero (x : Int64) : x ^ 0 = 1 := rfl
-protected theorem Int64.pow_succ (x : Int64) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
-@[simp] protected theorem ISize.pow_zero (x : ISize) : x ^ 0 = 1 := rfl
-protected theorem ISize.pow_succ (x : ISize) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
-
 protected theorem Int8.mul_add {a b c : Int8} : a * (b + c) = a * b + a * c :=
     Int8.toBitVec_inj.1 BitVec.mul_add
 protected theorem Int16.mul_add {a b c : Int16} : a * (b + c) = a * b + a * c :=

src/Init/Data/UInt/Basic.lean

@@ -58,17 +58,6 @@ This function is overridden at runtime with an efficient implementation.
 @[extern "lean_uint8_div"]
 protected def UInt8.div (a b : UInt8) : UInt8 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 /--
-The power operation, raising an 8-bit unsigned integer to a natural number power,
-wrapping around on overflow. Usually accessed via the `^` operator.
-
-This function is currently *not* overridden at runtime with an efficient implementation,
-and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
--/
-protected def UInt8.pow (x : UInt8) (n : Nat) : UInt8 :=
-  match n with
-  | 0 => 1
-  | n + 1 => UInt8.mul (UInt8.pow x n) x
-/--
 The modulo operator for 8-bit unsigned integers, which computes the remainder when dividing one
 integer by another. Usually accessed via the `%` operator.
 
@@ -143,7 +132,6 @@ protected def UInt8.le (a b : UInt8) : Prop := a.toBitVec ≤ b.toBitVec
 instance : Add UInt8       := ⟨UInt8.add⟩
 instance : Sub UInt8       := ⟨UInt8.sub⟩
 instance : Mul UInt8       := ⟨UInt8.mul⟩
-instance : Pow UInt8 Nat   := ⟨UInt8.pow⟩
 instance : Mod UInt8       := ⟨UInt8.mod⟩
 
 set_option linter.deprecated false in
@@ -270,17 +258,6 @@ This function is overridden at runtime with an efficient implementation.
 @[extern "lean_uint16_div"]
 protected def UInt16.div (a b : UInt16) : UInt16 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 /--
-The power operation, raising a 16-bit unsigned integer to a natural number power,
-wrapping around on overflow. Usually accessed via the `^` operator.
-
-This function is currently *not* overridden at runtime with an efficient implementation,
-and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
--/
-protected def UInt16.pow (x : UInt16) (n : Nat) : UInt16 :=
-  match n with
-  | 0 => 1
-  | n + 1 => UInt16.mul (UInt16.pow x n) x
-/--
 The modulo operator for 16-bit unsigned integers, which computes the remainder when dividing one
 integer by another. Usually accessed via the `%` operator.
 
@@ -318,7 +295,7 @@ This function is overridden at runtime with an efficient implementation.
 @[extern "lean_uint16_lor"]
 protected def UInt16.lor (a b : UInt16) : UInt16 := ⟨a.toBitVec ||| b.toBitVec⟩
 /--
-Bitwise exclusive or for 16-bit unsigned integers. Usually accessed via the `^^^` operator.
+Bitwise exclusive or for 8-bit unsigned integers. Usually accessed via the `^^^` operator.
 
 Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
 integers are set.
@@ -355,7 +332,6 @@ protected def UInt16.le (a b : UInt16) : Prop := a.toBitVec ≤ b.toBitVec
 instance : Add UInt16       := ⟨UInt16.add⟩
 instance : Sub UInt16       := ⟨UInt16.sub⟩
 instance : Mul UInt16       := ⟨UInt16.mul⟩
-instance : Pow UInt16 Nat   := ⟨UInt16.pow⟩
 instance : Mod UInt16       := ⟨UInt16.mod⟩
 
 set_option linter.deprecated false in
@@ -484,17 +460,6 @@ This function is overridden at runtime with an efficient implementation.
 @[extern "lean_uint32_div"]
 protected def UInt32.div (a b : UInt32) : UInt32 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 /--
-The power operation, raising a 32-bit unsigned integer to a natural number power,
-wrapping around on overflow. Usually accessed via the `^` operator.
-
-This function is currently *not* overridden at runtime with an efficient implementation,
-and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
--/
-protected def UInt32.pow (x : UInt32) (n : Nat) : UInt32 :=
-  match n with
-  | 0 => 1
-  | n + 1 => UInt32.mul (UInt32.pow x n) x
-/--
 The modulo operator for 32-bit unsigned integers, which computes the remainder when dividing one
 integer by another. Usually accessed via the `%` operator.
 
@@ -569,7 +534,6 @@ protected def UInt32.le (a b : UInt32) : Prop := a.toBitVec ≤ b.toBitVec
 instance : Add UInt32       := ⟨UInt32.add⟩
 instance : Sub UInt32       := ⟨UInt32.sub⟩
 instance : Mul UInt32       := ⟨UInt32.mul⟩
-instance : Pow UInt32 Nat   := ⟨UInt32.pow⟩
 instance : Mod UInt32       := ⟨UInt32.mod⟩
 
 set_option linter.deprecated false in
@@ -660,17 +624,6 @@ This function is overridden at runtime with an efficient implementation.
 @[extern "lean_uint64_div"]
 protected def UInt64.div (a b : UInt64) : UInt64 := ⟨BitVec.udiv a.toBitVec b.toBitVec⟩
 /--
-The power operation, raising a 64-bit unsigned integer to a natural number power,
-wrapping around on overflow. Usually accessed via the `^` operator.
-
-This function is currently *not* overridden at runtime with an efficient implementation,
-and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
--/
-protected def UInt64.pow (x : UInt64) (n : Nat) : UInt64 :=
-  match n with
-  | 0 => 1
-  | n + 1 => UInt64.mul (UInt64.pow x n) x
-/--
 The modulo operator for 64-bit unsigned integers, which computes the remainder when dividing one
 integer by another. Usually accessed via the `%` operator.
 
@@ -745,7 +698,6 @@ protected def UInt64.le (a b : UInt64) : Prop := a.toBitVec ≤ b.toBitVec
 instance : Add UInt64       := ⟨UInt64.add⟩
 instance : Sub UInt64       := ⟨UInt64.sub⟩
 instance : Mul UInt64       := ⟨UInt64.mul⟩
-instance : Pow UInt64 Nat   := ⟨UInt64.pow⟩
 instance : Mod UInt64       := ⟨UInt64.mod⟩
 
 set_option linter.deprecated false in
@@ -766,7 +718,7 @@ This function is overridden at runtime with an efficient implementation.
 @[extern "lean_uint64_complement"]
 protected def UInt64.complement (a : UInt64) : UInt64 := ⟨~~~a.toBitVec⟩
 /--
-Negation of 64-bit unsigned integers, computed modulo `UInt64.size`.
+Negation of 32-bit unsigned integers, computed modulo `UInt64.size`.
 
 `UInt64.neg a` is equivalent to `18_446_744_073_709_551_615 - a + 1`.
 
@@ -867,17 +819,6 @@ This function is overridden at runtime with an efficient implementation.
 @[extern "lean_usize_div"]
 protected def USize.div (a b : USize) : USize := ⟨a.toBitVec / b.toBitVec⟩
 /--
-The power operation, raising a word-sized unsigned integer to a natural number power,
-wrapping around on overflow. Usually accessed via the `^` operator.
-
-This function is currently *not* overridden at runtime with an efficient implementation,
-and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
--/
-protected def USize.pow (x : USize) (n : Nat) : USize :=
-  match n with
-  | 0 => 1
-  | n + 1 => USize.mul (USize.pow x n) x
-/--
 The modulo operator for word-sized unsigned integers, which computes the remainder when dividing one
 integer by another. Usually accessed via the `%` operator.
 
@@ -1011,7 +952,6 @@ def USize.toUInt64 (a : USize) : UInt64 :=
   UInt64.ofNatLT a.toBitVec.toNat (Nat.lt_of_lt_of_le a.toBitVec.isLt USize.size_le)
 
 instance : Mul USize       := ⟨USize.mul⟩
-instance : Pow USize Nat   := ⟨USize.pow⟩
 instance : Mod USize       := ⟨USize.mod⟩
 
 set_option linter.deprecated false in

src/Init/Data/UInt/Lemmas.lean

@@ -2767,17 +2767,6 @@ instance : Std.LawfulCommIdentity (α := USize) (· * ·) 1 where
 @[simp] theorem UInt64.zero_mul {a : UInt64} : 0 * a = 0 := UInt64.toBitVec_inj.1 BitVec.zero_mul
 @[simp] theorem USize.zero_mul {a : USize} : 0 * a = 0 := USize.toBitVec_inj.1 BitVec.zero_mul
 
-@[simp] protected theorem UInt8.pow_zero (x : UInt8) : x ^ 0 = 1 := rfl
-protected theorem UInt8.pow_succ (x : UInt8) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
-@[simp] protected theorem UInt16.pow_zero (x : UInt16) : x ^ 0 = 1 := rfl
-protected theorem UInt16.pow_succ (x : UInt16) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
-@[simp] protected theorem UInt32.pow_zero (x : UInt32) : x ^ 0 = 1 := rfl
-protected theorem UInt32.pow_succ (x : UInt32) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
-@[simp] protected theorem UInt64.pow_zero (x : UInt64) : x ^ 0 = 1 := rfl
-protected theorem UInt64.pow_succ (x : UInt64) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
-@[simp] protected theorem USize.pow_zero (x : USize) : x ^ 0 = 1 := rfl
-protected theorem USize.pow_succ (x : USize) (n : Nat) : x ^ (n + 1) = x ^ n * x := rfl
-
 protected theorem UInt8.mul_add {a b c : UInt8} : a * (b + c) = a * b + a * c :=
     UInt8.toBitVec_inj.1 BitVec.mul_add
 protected theorem UInt16.mul_add {a b c : UInt16} : a * (b + c) = a * b + a * c :=

src/Init/Grind/Tactics.lean

@@ -70,11 +70,6 @@ structure Config where
   canonHeartbeats : Nat := 1000
   /-- If `ext` is `true`, `grind` uses extensionality theorems available in the environment. -/
   ext : Bool := true
-  /--
-  If `funext` is `true`, `grind` creates new opportunities for applying function extensionality by case-splitting
-  on equalities between lambda expressions.
-  -/
-  funext : Bool := true
   /-- If `verbose` is `false`, additional diagnostics information is not collected. -/
   verbose : Bool := true
   /-- If `clean` is `true`, `grind` uses `expose_names` and only generates accessible names. -/

src/Lean/Log.lean

@@ -53,12 +53,6 @@ register_builtin_option warningAsError : Bool := {
   descr    := "treat warnings as errors"
 }
 
-/-- If `infoAsError` is set to `true`, then information messages are treated as errors. -/
-register_builtin_option infoAsError : Bool := {
-  defValue := false
-  descr    := "treat information messages as errors"
-}
-
 /--
 Log the message `msgData` at the position provided by `ref` with the given `severity`.
 If `getRef` has position information but `ref` does not, we use `getRef`.
@@ -67,14 +61,7 @@ We use the `fileMap` to find the line and column numbers for the error message.
 def logAt (ref : Syntax) (msgData : MessageData)
     (severity : MessageSeverity := MessageSeverity.error) (isSilent : Bool := false) : m Unit :=
   unless severity == .error && msgData.hasSyntheticSorry do
-    let o ← getOptions
-    let severity :=
-      if severity == .warning && warningAsError.get o then
-        .error
-      else if severity == .information && infoAsError.get o then
-        .error
-      else
-        severity
+    let severity := if severity == .warning && warningAsError.get (← getOptions) then .error else severity
     let ref    := replaceRef ref (← MonadLog.getRef)
     let pos    := ref.getPos?.getD 0
     let endPos := ref.getTailPos?.getD pos
@@ -95,7 +82,7 @@ def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit :=
 
 /-- Log a new warning message using the given message data. The position is provided by `ref`. -/
 def logWarningAt [MonadOptions m] (ref : Syntax) (msgData : MessageData) : m Unit := do
-  logAt ref msgData MessageSeverity.warning
+  logAt ref msgData .warning
 
 /-- Log a new information message using the given message data. The position is provided by `ref`. -/
 def logInfoAt (ref : Syntax) (msgData : MessageData) : m Unit :=

src/Lean/Meta/Tactic/Grind.lean

@@ -52,8 +52,6 @@ builtin_initialize registerTraceClass `grind.split.candidate
 builtin_initialize registerTraceClass `grind.split.resolved
 builtin_initialize registerTraceClass `grind.beta
 builtin_initialize registerTraceClass `grind.mbtc
-builtin_initialize registerTraceClass `grind.ext
-builtin_initialize registerTraceClass `grind.ext.candidate
 
 /-! Trace options for `grind` developers -/
 builtin_initialize registerTraceClass `grind.debug
@@ -78,6 +76,5 @@ builtin_initialize registerTraceClass `grind.debug.proveEq
 builtin_initialize registerTraceClass `grind.debug.pushNewFact
 builtin_initialize registerTraceClass `grind.debug.ematch.activate
 builtin_initialize registerTraceClass `grind.debug.appMap
-builtin_initialize registerTraceClass `grind.debug.ext
 
 end Lean

src/Lean/Meta/Tactic/Grind/Ext.lean

@@ -35,7 +35,6 @@ def instantiateExtTheorem (thm : Ext.ExtTheorem) (e : Expr) : GoalM Unit := with
   if proof'.hasMVar || prop'.hasMVar then
     reportIssue! "failed to apply extensionality theorem `{thm.declName}` for {indentExpr e}\nresulting terms contain metavariables"
     return ()
-  trace[grind.ext] "{prop'}"
   addNewRawFact proof' prop' ((← getGeneration e) + 1)
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -207,65 +207,6 @@ private def propagateUnitLike (a : Expr) (generation : Nat) : GoalM Unit := do
         internalize unit generation
         pushEq a unit <| (← mkEqRefl unit)
 
-/-- Returns `true` if we can ignore `ext` for functions occurring as arguments of a `declName`-application. -/
-private def extParentsToIgnore (declName : Name) : Bool :=
-  declName == ``Eq || declName == ``HEq || declName == ``dite || declName == ``ite
-  || declName == ``Exists || declName == ``Subtype
-
-/--
-Given a term `e` that occurs as the argument at position `i` of an `f`-application `parent?`,
-we consider `e` as a candidate for case-splitting. For every other argument `e'` that also appears
-at position `i` in an `f`-application and has the same type as `e`, we add the case-split candidate `e = e'`.
-
-When performing the case split, we consider the following two cases:
-- `e = e'`, which may introduce a new congruence between the corresponding `f`-applications.
-- `¬(e = e')`, which may trigger extensionality theorems for the type of `e`.
-
-This feature enables `grind` to solve examples such as:
-```lean
-example (f : (Nat → Nat) → Nat) : a = b → f (fun x => a + x) = f (fun x => b + x) := by
-  grind
-```
--/
-private def addSplitCandidatesForExt (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := do
-  let some parent := parent? | return ()
-  unless parent.isApp do return ()
-  let f := parent.getAppFn
-  if let .const declName _ := f then
-    if extParentsToIgnore declName then return ()
-  let type ← inferType e
-  -- Remark: we currently do not perform function extensionality on functions that produce a type that is not a proposition.
-  -- We may add an option to enable that in the future.
-  let u? ← typeFormerTypeLevel type
-  if u? != .none && u? != some .zero then return ()
-  let mut i  := parent.getAppNumArgs
-  let mut it := parent
-  repeat
-    if !it.isApp then return ()
-    i := i - 1
-    let arg := it.appArg!
-    if isSameExpr arg e then
-      found f i type
-    it := it.appFn!
-where
-  found (f : Expr) (i : Nat) (type : Expr) : GoalM Unit := do
-    trace[grind.debug.ext] "{f}, {i}, {e}"
-    let others := (← get).termsAt.find? (f, i) |>.getD []
-    for (e', type') in others do
-      if (← withDefault <| isDefEq type type') then
-        let eq := mkApp3 (mkConst ``Eq [← getLevel type]) type e e'
-        let eq ← shareCommon eq
-        internalize eq generation
-        trace_goal[grind.ext.candidate] "{eq}"
-        addSplitCandidate eq
-    modify fun s => { s with termsAt := s.termsAt.insert (f, i) ((e, type) :: others) }
-    return ()
-
-/-- Applies `addSplitCandidatesForExt` if `funext` is enabled. -/
-private def addSplitCandidatesForFunext (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := do
-  unless (← getConfig).funext do return ()
-  addSplitCandidatesForExt e generation parent?
-
 @[export lean_grind_internalize]
 private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := withIncRecDepth do
   if (← alreadyInternalized e) then
@@ -288,10 +229,7 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt
   | .fvar .. =>
     mkENode' e generation
     checkAndAddSplitCandidate e
-  | .letE .. =>
-    mkENode' e generation
-  | .lam .. =>
-    addSplitCandidatesForFunext e generation parent?
+  | .letE .. | .lam .. =>
     mkENode' e generation
   | .forallE _ d b _ =>
     mkENode' e generation

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -529,13 +529,6 @@ structure Goal where
   arith      : Arith.State := {}
   /-- State of the clean name generator. -/
   clean      : Clean.State := {}
-  /--
-  Mapping from pairs `(f, i)` to a list of `(e, type)`.
-  The meaning is: `e : type` is lambda expression that occurs at argument `i` of an `f`-application.
-  We use this information to add case-splits for triggering extensionality theorems.
-  See `addSplitCandidatesForExt`.
-  -/
-  termsAt    : PHashMap (Expr × Nat) (List (Expr × Expr)) := {}
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=

tests/lean/grind/clear_aux_decls.lean

@@ -250,16 +250,19 @@ def normalize (l : AList (fun _ : Nat => Bool)) :
   | .ite (var v)      t e =>
     match h : l.lookup v with
     | none =>
-      have ⟨t', _⟩ := normalize (l.insert v true) t
-      have ⟨e', _⟩ := normalize (l.insert v false) e
+      have ⟨t', ht₁, ht₂, ht₃⟩ := normalize (l.insert v true) t
+      have ⟨e', he₁, he₂, he₃⟩ := normalize (l.insert v false) e
       ⟨if t' = e' then t' else .ite (var v) t' e', by
         refine ⟨fun f => ?_, ?_, fun w b => ?_⟩
         · -- eval = eval
           simp only [apply_ite, eval_ite_var]
           cases hfv : f v
           · simp_all
+            congr
+            ◾
+          · simp [h, ht₁]
+            congr
             ◾
-          · ◾
         · -- normalized
           split
           · ◾

tests/lean/run/grind_bintree.lean

@@ -1,128 +0,0 @@
-set_option grind.warning false
-reset_grind_attrs%
-
-attribute [grind] List.append_assoc List.cons_append List.nil_append
-
-inductive Tree (β : Type v) where
-  | leaf
-  | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
-  deriving Repr
-
-def Tree.contains (t : Tree β) (k : Nat) : Bool :=
-  match t with
-  | leaf => false
-  | node left key _ right =>
-    if k < key then
-      left.contains k
-    else if key < k then
-      right.contains k
-    else
-      true
-
-def Tree.find? (t : Tree β) (k : Nat) : Option β :=
-  match t with
-  | leaf => none
-  | node left key value right =>
-    if k < key then
-      left.find? k
-    else if key < k then
-      right.find? k
-    else
-      some value
-
-def Tree.insert (t : Tree β) (k : Nat) (v : β) : Tree β :=
-  match t with
-  | leaf => node leaf k v leaf
-  | node left key value right =>
-    if k < key then
-      node (left.insert k v) key value right
-    else if key < k then
-      node left key value (right.insert k v)
-    else
-      node left k v right
-
-def Tree.toList (t : Tree β) : List (Nat × β) :=
-  match t with
-  | leaf => []
-  | node l k v r => l.toList ++ [(k, v)] ++ r.toList
-
-def Tree.toListTR (t : Tree β) : List (Nat × β) :=
-  go t []
-where
-  go (t : Tree β) (acc : List (Nat × β)) : List (Nat × β) :=
-    match t with
-    | leaf => acc
-    | node l k v r => go l ((k, v) :: go r acc)
-
-theorem Tree.toList_eq_toListTR (t : Tree β)
-        : t.toList = t.toListTR := by
-  simp [toListTR, go t []]
-where
-  go (t : Tree β) (acc : List (Nat × β))
-     : toListTR.go t acc = t.toList ++ acc := by
-    induction t generalizing acc <;> grind [toListTR.go, toList]
-
-@[csimp] theorem Tree.toList_eq_toListTR_csimp
-                 : @Tree.toList = @Tree.toListTR := by
-  grind [toList_eq_toListTR]
-
-inductive ForallTree (p : Nat → β → Prop) : Tree β → Prop
-  | leaf : ForallTree p .leaf
-  | node :
-     ForallTree p left →
-     p key value →
-     ForallTree p right →
-     ForallTree p (.node left key value right)
-
-inductive BST : Tree β → Prop
-  | leaf : BST .leaf
-  | node :
-     ForallTree (fun k _ => k < key) left →
-     ForallTree (fun k _ => key < k) right →
-     BST left → BST right →
-     BST (.node left key value right)
-
-attribute [local simp, grind] Tree.insert
-
-theorem Tree.forall_insert_of_forall
-        (h₁ : ForallTree p t) (h₂ : p key value)
-        : ForallTree p (t.insert key value) := by
-  induction h₁ <;> grind [ForallTree.node, ForallTree.leaf]
-
-theorem Tree.bst_insert_of_bst
-        {t : Tree β} (h : BST t) (key : Nat) (value : β)
-        : BST (t.insert key value) := by
-  -- TODO: improve `grind` `funext` support, and minimize the number of splits
-  induction h <;> grind (splits := 12) [BST.node, BST.leaf, ForallTree.leaf, forall_insert_of_forall]
-
-def BinTree (β : Type u) := { t : Tree β // BST t }
-
-def BinTree.mk : BinTree β :=
-  ⟨.leaf, .leaf⟩
-
-def BinTree.contains (b : BinTree β) (k : Nat) : Bool :=
-  b.val.contains k
-
-def BinTree.find? (b : BinTree β) (k : Nat) : Option β :=
-  b.val.find? k
-
-def BinTree.insert (b : BinTree β) (k : Nat) (v : β) : BinTree β :=
-  ⟨b.val.insert k v, b.val.bst_insert_of_bst b.property k v⟩
-
-attribute [local simp, local grind]
-  BinTree.mk BinTree.contains BinTree.find?
-  BinTree.insert Tree.find? Tree.contains Tree.insert
-
-theorem BinTree.find_mk (k : Nat)
-        : BinTree.mk.find? k = (none : Option β) := by
-  grind [Tree.find?]
-
-theorem BinTree.find_insert (b : BinTree β) (k : Nat) (v : β)
-        : (b.insert k v).find? k = some v := by
-  let ⟨t, h⟩ := b; simp
-  induction t <;> simp <;> grind [BST]
-
-theorem BinTree.find_insert_of_ne (b : BinTree β) (ne : k ≠ k') (v : β)
-        : (b.insert k v).find? k' = b.find? k' := by
-  let ⟨t, h⟩ := b; simp
-  induction t <;> simp <;> grind [BST]

tests/lean/run/grind_funext.lean

@@ -1,6 +0,0 @@
-example (f : (Nat → Nat) → Nat) : a = b → f (fun x => a + x) = f (fun x => b + x) := by
-  grind
-
-example (f : (Nat → Nat) → Nat) : a = b → f (fun x => a + x) = f (fun x => b + x) := by
-  fail_if_success grind -funext
-  sorry