chore: remove some @[simp]s from Fin lemmas (#5379)

These were dubious simps, barely used, that hurt confluence.
leanprover · Sep 18, 2024 · 77cd700 · 77cd700
1 parent a6a06a6
commit 77cd700
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 6 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -1511,7 +1511,8 @@ Definition of bitvector addition as a nat.
   x + .ofFin y = .ofFin (x.toFin + y) := rfl
 
 theorem ofNat_add {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]
+  apply eq_of_toNat_eq
+  simp [BitVec.ofNat, Fin.ofNat'_add]
 
 theorem ofNat_add_ofNat {n} (x y : Nat) : BitVec.ofNat n x + BitVec.ofNat n y = BitVec.ofNat n (x + y) :=
   (ofNat_add x y).symm
@@ -1565,10 +1566,12 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN
   rfl
 @[simp] theorem sub_ofFin (x : BitVec n) (y : Fin (2^n)) : x - .ofFin y = .ofFin (x.toFin - y) :=
   rfl
+
 -- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
 -- If `x` and `n` are not literals, applying this theorem eagerly may not be a good idea.
 theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y = .ofNat n ((2^n - y % 2^n) + x) := by
-  apply eq_of_toNat_eq ; simp [BitVec.ofNat]
+  apply eq_of_toNat_eq
+  simp [BitVec.ofNat, Fin.ofNat'_sub]
 
 @[simp] protected theorem sub_zero (x : BitVec n) : x - 0#n = x := by apply eq_of_toNat_eq ; simp
 

diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
@@ -750,12 +750,12 @@ theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right
 
 /-! ### add -/
 
-@[simp] theorem ofNat'_add [NeZero n] (x : Nat) (y : Fin n) :
+theorem ofNat'_add [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.add_def]
 
-@[simp] theorem add_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
+theorem add_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.add_def]
@@ -765,12 +765,12 @@ theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right
 protected theorem coe_sub (a b : Fin n) : ((a - b : Fin n) : Nat) = ((n - b) + a) % n := by
   cases a; cases b; rfl
 
-@[simp] theorem ofNat'_sub [NeZero n] (x : Nat) (y : Fin n) :
+theorem ofNat'_sub [NeZero n] (x : Nat) (y : Fin n) :
     Fin.ofNat' n x - y = Fin.ofNat' n ((n - y.val) + x) := by
   apply Fin.eq_of_val_eq
   simp [Fin.ofNat', Fin.sub_def]
 
-@[simp] theorem sub_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
+theorem sub_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
     x - Fin.ofNat' n y = Fin.ofNat' n ((n - y % n) + x.val) := by
   apply Fin.eq_of_val_eq
   simp [Fin.ofNat', Fin.sub_def]