chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream (#3579)

src/Init/Data/BitVec/Lemmas.lean

@@ -70,7 +70,7 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
   else
     have w_pos := Nat.pos_of_ne_zero w_zero
     have r : i ≤ w - 1 := by
-      simp [Nat.le_sub_iff_add_le w_pos, Nat.add_succ]
+      simp [Nat.le_sub_iff_add_le w_pos]
       exact i_lt
     have q_lt : w - 1 - i < w := by
       simp only [Nat.sub_sub]

src/Init/Data/Int/DivModLemmas.lean

@@ -760,7 +760,7 @@ theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int}
 
 @[simp] protected theorem div_one : ∀ a : Int, a.div 1 = a
   | (n:Nat) => congrArg ofNat (Nat.div_one _)
-  | -[n+1] => by simp [Int.div, neg_ofNat_succ]
+  | -[n+1] => by simp [Int.div, neg_ofNat_succ]; rfl
 
 @[simp] protected theorem div_neg : ∀ a b : Int, a.div (-b) = -(a.div b)
   | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl

src/Init/Data/Int/Lemmas.lean

@@ -153,7 +153,7 @@ theorem subNatNat_sub (h : n ≤ m) (k : Nat) : subNatNat (m - n) k = subNatNat
 theorem subNatNat_add (m n k : Nat) : subNatNat (m + n) k = m + subNatNat n k := by
   cases n.lt_or_ge k with
   | inl h' =>
-    simp [subNatNat_of_lt h', succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]
+    simp [subNatNat_of_lt h', sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h')]
     conv => lhs; rw [← Nat.sub_add_cancel (Nat.le_of_lt h')]
     apply subNatNat_add_add
   | inr h' => simp [subNatNat_of_le h',
@@ -169,12 +169,11 @@ theorem subNatNat_add_negSucc (m n k : Nat) :
     rw [subNatNat_sub h', Nat.add_comm]
   | inl h' =>
     have h₂ : m < n + succ k := Nat.lt_of_lt_of_le h' (le_add_right _ _)
-    have h₃ : m ≤ n + k := le_of_succ_le_succ h₂
     rw [subNatNat_of_lt h', subNatNat_of_lt h₂]
-    simp [Nat.add_comm]
-    rw [← add_succ, succ_pred_eq_of_pos (Nat.sub_pos_of_lt h'), add_succ, succ_sub h₃,
-      Nat.pred_succ]
-    rw [Nat.add_comm n, Nat.add_sub_assoc (Nat.le_of_lt h')]
+    simp only [pred_eq_sub_one, negSucc_add_negSucc, succ_eq_add_one, negSucc.injEq]
+    rw [Nat.add_right_comm, sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h'), Nat.sub_sub,
+      ← Nat.add_assoc, succ_sub_succ_eq_sub, Nat.add_comm n,Nat.add_sub_assoc (Nat.le_of_lt h'),
+      Nat.add_comm]
 
 protected theorem add_assoc : ∀ a b c : Int, a + b + c = a + (b + c)
   | (m:Nat), (n:Nat), c => aux1 ..
@@ -188,15 +187,15 @@ protected theorem add_assoc : ∀ a b c : Int, a + b + c = a + (b + c)
   | (m:Nat), -[n+1], -[k+1] => by
     rw [Int.add_comm, Int.add_comm m, Int.add_comm m, ← aux2, Int.add_comm -[k+1]]
   | -[m+1], -[n+1], -[k+1] => by
-    simp [add_succ, Nat.add_comm, Nat.add_left_comm, neg_ofNat_succ]
+    simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
 where
   aux1 (m n : Nat) : ∀ c : Int, m + n + c = m + (n + c)
     | (k:Nat) => by simp [Nat.add_assoc]
     | -[k+1]  => by simp [subNatNat_add]
   aux2 (m n k : Nat) : -[m+1] + -[n+1] + k = -[m+1] + (-[n+1] + k) := by
-    simp [add_succ]
+    simp
     rw [Int.add_comm, subNatNat_add_negSucc]
-    simp [add_succ, succ_add, Nat.add_comm]
+    simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
 
 protected theorem add_left_comm (a b c : Int) : a + (b + c) = b + (a + c) := by
   rw [← Int.add_assoc, Int.add_comm a, Int.add_assoc]
@@ -391,7 +390,7 @@ theorem ofNat_mul_subNatNat (m n k : Nat) :
     | inl h =>
       have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
       simp [subNatNat_of_lt h, subNatNat_of_lt h']
-      rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h), ← neg_ofNat_succ, Nat.mul_sub_left_distrib,
+      rw [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), ← neg_ofNat_succ, Nat.mul_sub_left_distrib,
         ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]; rfl
     | inr h =>
       have h' : succ m * k ≤ succ m * n := Nat.mul_le_mul_left _ h
@@ -406,7 +405,7 @@ theorem negSucc_mul_subNatNat (m n k : Nat) :
   | inl h =>
     have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
     rw [subNatNat_of_lt h, subNatNat_of_le (Nat.le_of_lt h')]
-    simp [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h), Nat.mul_sub_left_distrib]
+    simp [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), Nat.mul_sub_left_distrib]
   | inr h => cases Nat.lt_or_ge k n with
     | inl h' =>
       have h₁ : succ m * n > succ m * k := Nat.mul_lt_mul_of_pos_left h' (Nat.succ_pos m)
@@ -422,12 +421,12 @@ protected theorem mul_add : ∀ a b c : Int, a * (b + c) = a * b + a * c
     simp [negOfNat_eq_subNatNat_zero]; rw [← subNatNat_add]; rfl
   | (m:Nat), -[n+1],  (k:Nat) => by
     simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, ← subNatNat_add]; rfl
-  | (m:Nat), -[n+1],  -[k+1]  => by simp; rw [← Nat.left_distrib, succ_add]; rfl
+  | (m:Nat), -[n+1],  -[k+1]  => by simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]
   | -[m+1],  (n:Nat), (k:Nat) => by simp [Nat.mul_comm]; rw [← Nat.right_distrib, Nat.mul_comm]
   | -[m+1],  (n:Nat), -[k+1]  => by
     simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, ← subNatNat_add]; rfl
   | -[m+1],  -[n+1],  (k:Nat) => by simp [negOfNat_eq_subNatNat_zero]; rw [← subNatNat_add]; rfl
-  | -[m+1],  -[n+1],  -[k+1]  => by simp; rw [← Nat.left_distrib, succ_add]; rfl
+  | -[m+1],  -[n+1],  -[k+1]  => by simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]
 
 protected theorem add_mul (a b c : Int) : (a + b) * c = a * c + b * c := by
   simp [Int.mul_comm, Int.mul_add]

src/Init/Data/Nat/Basic.lean

@@ -148,9 +148,12 @@ theorem add_succ (n m : Nat) : n + succ m = succ (n + m) :=
 theorem add_one (n : Nat) : n + 1 = succ n :=
   rfl
 
-theorem succ_eq_add_one (n : Nat) : succ n = n + 1 :=
+@[simp] theorem succ_eq_add_one (n : Nat) : succ n = n + 1 :=
   rfl
 
+@[simp] theorem add_one_ne_zero (n : Nat) : n + 1 ≠ 0 := nofun
+@[simp] theorem zero_ne_add_one (n : Nat) : 0 ≠ n + 1 := nofun
+
 protected theorem add_comm : ∀ (n m : Nat), n + m = m + n
   | n, 0   => Eq.symm (Nat.zero_add n)
   | n, m+1 => by
@@ -283,7 +286,7 @@ theorem succ_sub_succ (n m : Nat) : succ n - succ m = n - m :=
 theorem sub_add_eq (a b c : Nat) : a - (b + c) = a - b - c := by
   induction c with
   | zero => simp
-  | succ c ih => simp [Nat.add_succ, Nat.sub_succ, ih]
+  | succ c ih => simp only [Nat.add_succ, Nat.sub_succ, ih]
 
 protected theorem lt_of_lt_of_le {n m k : Nat} : n < m → m ≤ k → n < k :=
   Nat.le_trans
@@ -632,8 +635,6 @@ protected theorem zero_ne_one : 0 ≠ (1 : Nat) :=
 @[simp] theorem succ_ne_zero (n : Nat) : succ n ≠ 0 :=
   fun h => Nat.noConfusion h
 
-theorem add_one_ne_zero (n) : n + 1 ≠ 0 := succ_ne_zero _
-
 /-! # mul + order -/
 
 theorem mul_le_mul_left {n m : Nat} (k : Nat) (h : n ≤ m) : k * n ≤ k * m :=
@@ -742,6 +743,11 @@ theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by
 theorem succ_pred_eq_of_pos : ∀ {n}, 0 < n → succ (pred n) = n
   | _+1, _ => rfl
 
+theorem sub_one_add_one_eq_of_pos : ∀ {n}, 0 < n → (n - 1) + 1 = n
+  | _+1, _ => rfl
+
+@[simp] theorem pred_eq_sub_one : pred n = n - 1 := rfl
+
 /-! # sub theorems -/
 
 theorem add_sub_self_left (a b : Nat) : (a + b) - a = b := by
@@ -778,7 +784,7 @@ theorem sub_succ_lt_self (a i : Nat) (h : i < a) : a - (i + 1) < a - i := by
 
 theorem sub_ne_zero_of_lt : {a b : Nat} → a < b → b - a ≠ 0
   | 0, 0, h      => absurd h (Nat.lt_irrefl 0)
-  | 0, succ b, _ => by simp
+  | 0, succ b, _ => by simp only [Nat.sub_zero, ne_eq, not_false_eq_true]
   | succ a, 0, h => absurd h (Nat.not_lt_zero a.succ)
   | succ a, succ b, h => by rw [Nat.succ_sub_succ]; exact sub_ne_zero_of_lt (Nat.lt_of_succ_lt_succ h)
 
@@ -796,7 +802,7 @@ theorem add_sub_of_le {a b : Nat} (h : a ≤ b) : a + (b - a) = b := by
 protected theorem add_sub_add_right (n k m : Nat) : (n + k) - (m + k) = n - m := by
   induction k with
   | zero => simp
-  | succ k ih => simp [add_succ, add_succ, succ_sub_succ, ih]
+  | succ k ih => simp [← Nat.add_assoc, ih]
 
 protected theorem add_sub_add_left (k n m : Nat) : (k + n) - (k + m) = n - m := by
   rw [Nat.add_comm k n, Nat.add_comm k m, Nat.add_sub_add_right]

src/Init/Data/Nat/Bitwise/Basic.lean

@@ -63,7 +63,7 @@ theorem shiftRight_succ (m n) : m >>> (n + 1) = (m >>> n) / 2 := rfl
 
 theorem shiftRight_add (m n : Nat) : ∀ k, m >>> (n + k) = (m >>> n) >>> k
   | 0 => rfl
-  | k + 1 => by simp [add_succ, shiftRight_add, shiftRight_succ]
+  | k + 1 => by simp [← Nat.add_assoc, shiftRight_add _ _ k, shiftRight_succ]
 
 theorem shiftRight_eq_div_pow (m : Nat) : ∀ n, m >>> n = m / 2 ^ n
   | 0 => (Nat.div_one _).symm

src/Init/Data/Nat/Div.lean

@@ -293,7 +293,7 @@ theorem sub_mul_div (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p
         rw [mul_succ] at h₁
         exact h₁
       rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃]
-      simp [add_one, Nat.pred_succ, mul_succ, Nat.sub_sub]
+      simp [Nat.pred_succ, mul_succ, Nat.sub_sub]
 
 theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - succ x) / n = p - succ (x / n) := by
   have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun n0 => by

src/Init/Data/Nat/Lemmas.lean

@@ -19,7 +19,6 @@ and later these lemmas should be organised into other files more systematically.
 -/
 
 namespace Nat
-
 /-! ## add -/
 
 protected theorem add_add_add_comm (a b c d : Nat) : (a + b) + (c + d) = (a + c) + (b + d) := by
@@ -781,7 +780,7 @@ theorem shiftRight_succ_inside : ∀m n, m >>> (n+1) = (m/2) >>> n
 
 theorem shiftLeft_shiftLeft (m n : Nat) : ∀ k, (m <<< n) <<< k = m <<< (n + k)
   | 0 => rfl
-  | k + 1 => by simp [add_succ, shiftLeft_shiftLeft _ _ k, shiftLeft_succ]
+  | k + 1 => by simp [← Nat.add_assoc, shiftLeft_shiftLeft _ _ k, shiftLeft_succ]
 
 theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x + y / m := by
   match x with

src/Init/Prelude.lean

@@ -1485,6 +1485,7 @@ instance [ShiftRight α] : HShiftRight α α α where
   hShiftRight a b := ShiftRight.shiftRight a b
 
 open HAdd (hAdd)
+open HSub (hSub)
 open HMul (hMul)
 open HPow (hPow)
 open HAppend (hAppend)
@@ -2053,7 +2054,7 @@ instance : OfNat (Fin (n+1)) i where
   ofNat := Fin.ofNat i
 ```
 -/
-abbrev USize.size : Nat := Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)
+abbrev USize.size : Nat := hAdd (hSub (hPow 2 System.Platform.numBits) 1) 1
 
 theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
   show Or (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 4294967296) (Eq (Nat.succ (Nat.sub (hPow 2 System.Platform.numBits) 1)) 18446744073709551616) from

tests/lean/guessLexFailures.lean.expected.out

@@ -146,4 +146,4 @@ guessLexFailures.lean:131:14-131:31: error: failed to prove termination, possibl
   - Use `termination_by` to specify a different well-founded relation
   - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
 m n✝ n : Nat
-⊢ n < Nat.succ n✝
+⊢ n < n✝ + 1

tests/lean/matchMultAlt.lean

@@ -24,7 +24,7 @@ def h (x : Nat) : Nat :=
 example : h x > 0 := by
   match x with
   | 0 | 1 => decide
-  | x + 2 => simp [h, Nat.add_succ]
+  | x + 2 => simp [h]
 
 inductive StrOrNum where
   | S (s : String)

tests/lean/run/ac_rfl.lean

@@ -12,7 +12,7 @@ instance : LawfulCommIdentity HMul.hMul 1 where right_id := Nat.mul_one
   ⟨Nat.le_of_succ_le_succ, Nat.succ_le_succ⟩
 
 @[simp] theorem add_le_add_right_iff {x y z : Nat} : x + z ≤ y + z ↔ x ≤ y := by
-  induction z <;> simp_all [Nat.add_succ]
+  induction z <;> simp_all [← Nat.add_assoc]
 
 set_option linter.unusedVariables false in
 theorem le_ext : ∀ {x y : Nat} (h : ∀ z, z ≤ x ↔ z ≤ y), x = y

tests/lean/run/eqnsAtSimp.lean

@@ -15,4 +15,4 @@ end
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
   induction x with
   | zero => simp [isEven]
-  | succ x ih => simp [Nat.mul_succ, Nat.add_succ, isEven, isOdd, ih]
+  | succ x ih => simp [Nat.mul_succ, isEven, isOdd, ih]

tests/lean/run/eqnsAtSimp2.lean

@@ -13,7 +13,7 @@ end
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
   induction x with
   | zero => simp
-  | succ x ih => simp [Nat.mul_succ, Nat.add_succ, ih]
+  | succ x ih => simp [Nat.mul_succ, ih]
 
 def f (x : Nat) : Nat :=
   match x with

tests/lean/run/simp3.lean

@@ -7,7 +7,6 @@ theorem ex2 (x : Nat) : f ((fun a => f (f a)) x) = x := by simp
 
 opaque g (x : Nat) : Nat
 @[simp] axiom gEq (x : Nat) : g x = match x with | 0 => 1 | x+1 => 2
-@[simp] theorem add1 (x : Nat) : x + 1 = x.succ := rfl
 
 theorem ex3 (x : Nat) : g (x + 1) = 2 := by simp
 

tests/lean/run/simpRwBug.lean

@@ -1,4 +1,4 @@
 open Nat
 
 theorem add_assoc (m n k : Nat) : m + n + k = m + (n + k) :=
-  Nat.recOn (motive := fun k => m + n + k = m + (n + k)) k rfl (fun k ih => by simp [Nat.add_succ, ih]; done)
+  Nat.recOn (motive := fun k => m + n + k = m + (n + k)) k rfl (fun k ih => by simp [Nat.add_assoc, ih]; done)

tests/lean/run/where1.lean

@@ -23,7 +23,7 @@ where
     | nil => simp [reverse.loop]
     | cons a as ih =>
       show (reverse.loop as (a::bs)).length = (a :: as).length + bs.length
-      simp [ih, Nat.add_succ, Nat.succ_add]
+      simp [ih, Nat.add_assoc, Nat.succ_add]
 
 def h : Nat -> Nat
   | 0    => g 0