test: additional tests from issue #4413

It must fail quickly for `n : UInt64`

src/Init/Data/BitVec/Basic.lean

@@ -198,7 +198,7 @@ instance : Add (BitVec n) := ⟨BitVec.add⟩
 Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
 modulo `2^n`.
 -/
-protected def sub (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + (2^n - y.toNat))
+protected def sub (x y : BitVec n) : BitVec n := .ofNat n ((2^n - y.toNat) + x.toNat)
 instance : Sub (BitVec n) := ⟨BitVec.sub⟩
 
 /--

src/Init/Data/BitVec/Lemmas.lean

@@ -1045,10 +1045,10 @@ theorem ofInt_add {n} (x y : Int) : BitVec.ofInt n (x + y) =
 
 /-! ### sub/neg -/
 
-theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n (x.toNat + (2^n - y.toNat)) := by rfl
+theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := by rfl
 
 @[simp, bv_toNat] theorem toNat_sub {n} (x y : BitVec n) :
-  (x - y).toNat = ((x.toNat + (2^n - y.toNat)) % 2^n) := rfl
+  (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
 @[simp] theorem toFin_sub (x y : BitVec n) : (x - y).toFin = toFin x - toFin y := rfl
 
 @[simp] theorem ofFin_sub (x : Fin (2^n)) (y : BitVec n) : .ofFin x - y = .ofFin (x - y.toFin) :=
@@ -1057,7 +1057,7 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n (x.toNat + (2^n - y.toNa
   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 (x + (2^n - y % 2^n)) := by
+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]
 
 @[simp] protected theorem sub_zero (x : BitVec n) : x - 0#n = x := by apply eq_of_toNat_eq ; simp
@@ -1065,7 +1065,7 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
 @[simp] protected theorem sub_self (x : BitVec n) : x - x = 0#n := by
   apply eq_of_toNat_eq
   simp only [toNat_sub]
-  rw [Nat.add_sub_of_le]
+  rw [Nat.add_comm, Nat.add_sub_of_le]
   · simp
   · exact Nat.le_of_lt x.isLt
 
@@ -1079,14 +1079,15 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
 theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
   apply eq_of_toNat_eq
   simp
+  rw [Nat.add_comm]
 
 @[simp] theorem neg_zero (n:Nat) : -BitVec.ofNat n 0 = BitVec.ofNat n 0 := by apply eq_of_toNat_eq ; simp
 
 theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by
   apply eq_of_toNat_eq
   have y_toNat_le := Nat.le_of_lt y.isLt
-  rw [toNat_sub, toNat_add, Nat.mod_add_mod, Nat.add_assoc, ← Nat.add_sub_assoc y_toNat_le,
-    Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel]
+  rw [toNat_sub, toNat_add, Nat.add_comm, Nat.mod_add_mod, Nat.add_assoc, ← Nat.add_sub_assoc y_toNat_le,
+      Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel]
 
 theorem sub_add_cancel (x y : BitVec w) : x - y + y = x := by
   rw [sub_toAdd, BitVec.add_assoc, BitVec.add_comm _ y,

src/Init/Data/Fin/Basic.lean

@@ -66,7 +66,24 @@ protected def mul : Fin n → Fin n → Fin n
 
 /-- Subtraction modulo `n` -/
 protected def sub : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + (n - b)) % n, mlt h⟩
+  /-
+  The definition of `Fin.sub` has been updated to improve performance.
+  The right-hand-side of the following `match` was originally
+  ```
+  ⟨(a + (n - b)) % n, mlt h⟩
+  ```
+  This caused significant performance issues when testing definitional equality,
+  such as `x =?= x - 1` where `x : Fin n` and `n` is a big number,
+  as Lean spent a long time reducing
+  ```
+  ((n - 1) + x.val) % n
+  ```
+  For example, this was an issue for `Fin 2^64` (i.e., `UInt64`).
+  This change improves performance by leveraging the fact that `Nat.add` is defined
+  using recursion on the second argument.
+  See issue #4413.
+  -/
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨((n - b) + a) % n, mlt h⟩
 
 /-!
 Remark: land/lor can be defined without using (% n), but

src/Init/Data/Fin/Lemmas.lean

@@ -24,7 +24,7 @@ theorem mod_def (a m : Fin n) : a % m = Fin.mk (a % m) (Nat.lt_of_le_of_lt (Nat.
 
 theorem mul_def (a b : Fin n) : a * b = Fin.mk ((a * b) % n) (Nat.mod_lt _ a.size_pos) := rfl
 
-theorem sub_def (a b : Fin n) : a - b = Fin.mk ((a + (n - b)) % n) (Nat.mod_lt _ a.size_pos) := rfl
+theorem sub_def (a b : Fin n) : a - b = Fin.mk (((n - b) + a) % n) (Nat.mod_lt _ a.size_pos) := rfl
 
 theorem size_pos' : ∀ [Nonempty (Fin n)], 0 < n | ⟨i⟩ => i.size_pos
 
@@ -762,16 +762,16 @@ theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right
 
 /-! ### sub -/
 
-protected theorem coe_sub (a b : Fin n) : ((a - b : Fin n) : Nat) = (a + (n - b)) % n := by
+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 (x : Nat) (lt : 0 < n) (y : Fin n) :
-    Fin.ofNat' x lt - y = Fin.ofNat' (x + (n - y.val)) lt := by
+    Fin.ofNat' x lt - y = Fin.ofNat' ((n - y.val) + x) lt := by
   apply Fin.eq_of_val_eq
   simp [Fin.ofNat', Fin.sub_def]
 
 @[simp] theorem sub_ofNat' (x : Fin n) (y : Nat) (lt : 0 < n) :
-    x - Fin.ofNat' y lt = Fin.ofNat' (x.val + (n - y % n)) lt := by
+    x - Fin.ofNat' y lt = Fin.ofNat' ((n - y % n) + x.val) lt := by
   apply Fin.eq_of_val_eq
   simp [Fin.ofNat', Fin.sub_def]
 
@@ -782,7 +782,7 @@ private theorem _root_.Nat.mod_eq_sub_of_lt_two_mul {x n} (h₁ : n ≤ x) (h₂
 theorem coe_sub_iff_le {a b : Fin n} : (↑(a - b) : Nat) = a - b ↔ b ≤ a := by
   rw [sub_def, le_def]
   dsimp only
-  if h : n ≤ a + (n - b) then
+  if h : n ≤ (n - b) + a then
     rw [Nat.mod_eq_sub_of_lt_two_mul h]
     all_goals omega
   else
@@ -792,7 +792,7 @@ theorem coe_sub_iff_le {a b : Fin n} : (↑(a - b) : Nat) = a - b ↔ b ≤ a :=
 theorem coe_sub_iff_lt {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b := by
   rw [sub_def, lt_def]
   dsimp only
-  if h : n ≤ a + (n - b) then
+  if h : n ≤ (n - b) + a then
     rw [Nat.mod_eq_sub_of_lt_two_mul h]
     all_goals omega
   else

src/Init/Omega/Int.lean

@@ -187,7 +187,7 @@ theorem ofNat_val_add {x y : Fin n} :
     (((x + y : Fin n)) : Int) = ((x : Int) + (y : Int)) % n := rfl
 
 theorem ofNat_val_sub {x y : Fin n} :
-    (((x - y : Fin n)) : Int) = ((x : Int) + ((n - y : Nat) : Int)) % n := rfl
+    (((x - y : Fin n)) : Int) = (((n - y : Nat) + (x : Int) : Int)) % n := rfl
 
 theorem ofNat_val_mul {x y : Fin n} :
     (((x * y : Fin n)) : Int) = ((x : Int) * (y : Int)) % n := rfl

tests/lean/run/4413.lean

@@ -0,0 +1,49 @@
+structure Note where
+  pitch : UInt64
+  start : Nat
+
+def Note.containsNote (n1 n2 : Note) : Prop :=
+  n1.start ≤ n2.start
+
+def Note.lowerSemitone (n : Note) : Note :=
+  { n with pitch := n.pitch - 1 }
+
+theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
+    n.containsNote (Note.lowerSemitone n) := by
+  simp [Note.containsNote, Note.lowerSemitone]
+
+/--
+error: type mismatch
+  rfl
+has type
+  n = n : Prop
+but is expected to have type
+  n = n - 1 : Prop
+-/
+#guard_msgs in
+set_option maxRecDepth 100 in
+set_option maxHeartbeats 100 in
+example (n : UInt64) : n = n - 1 :=
+  rfl
+
+namespace Ex2
+
+def lowerSemitone := fun (n : Note) => Note.mk (n.1 - 0) n.2
+
+set_option maxRecDepth 100 in
+theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
+    0 ≤ (lowerSemitone n).start :=
+  (Nat.zero_le (Note.start n))
+
+end Ex2
+
+namespace Ex3
+
+def lowerSemitone := fun (n : Note) => Note.mk (n.1 + 100) n.2
+
+set_option maxRecDepth 200 in
+theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
+    0 ≤ (lowerSemitone n).start :=
+  (Nat.zero_le (Note.start n))
+
+end Ex3