fix: replace unary Nat.succ simp rules with simprocs

src/Init/Core.lean

@@ -1308,14 +1308,19 @@ gen_injective_theorems% Fin
 gen_injective_theorems% Array
 gen_injective_theorems% Sum
 gen_injective_theorems% PSum
-gen_injective_theorems% Nat
 gen_injective_theorems% Option
 gen_injective_theorems% List
 gen_injective_theorems% Except
 gen_injective_theorems% EStateM.Result
 gen_injective_theorems% Lean.Name
 gen_injective_theorems% Lean.Syntax
 
+theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ → m = n :=
+  fun x => Nat.noConfusion x id
+
+theorem Nat.succ.injEq (u v : Nat) : (u.succ = v.succ) = (u = v) :=
+  Eq.propIntro Nat.succ.inj (congrArg Nat.succ)
+
 @[simp] theorem beq_iff_eq [BEq α] [LawfulBEq α] (a b : α) : a == b ↔ a = b :=
   ⟨eq_of_beq, by intro h; subst h; exact LawfulBEq.rfl⟩
 

src/Init/Data/BitVec/Lemmas.lean

@@ -728,8 +728,7 @@ theorem toNat_cons' {x : BitVec w} :
   rw [← BitVec.msb, msb_cons]
 
 @[simp] theorem getMsb_cons_succ : (cons a x).getMsb (i + 1) = x.getMsb i := by
-  simp [cons, cond_eq_if]
-  omega
+  simp [cons, Nat.le_add_left 1 i]
 
 theorem truncate_succ (x : BitVec w) :
     truncate (i+1) x = cons (getLsb x i) (truncate i x) := by

src/Init/Data/Bool.lean

@@ -220,6 +220,12 @@ due to `beq_iff_eq`.
 
 /-! ### coercision related normal forms -/
 
+theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :
+    (a == b) = decide (a = b) := by
+  cases h : a == b
+  · simp [ne_of_beq_false h]
+  · simp [eq_of_beq h]
+
 @[simp] theorem not_eq_not : ∀ {a b : Bool}, ¬a = !b ↔ a = b := by decide
 
 @[simp] theorem not_not_eq : ∀ {a b : Bool}, ¬(!a) = b ↔ a = b := by decide
@@ -230,6 +236,11 @@ due to `beq_iff_eq`.
 @[simp] theorem coe_false_iff_true  : ∀(a b : Bool), (a = false ↔ b) ↔ (!a) = b := by decide
 @[simp] theorem coe_false_iff_false : ∀(a b : Bool), (a = false ↔ b = false) ↔ (!a) = (!b) := by decide
 
+/-! ### beq properties -/
+
+theorem beq_comm {α} [BEq α] [LawfulBEq α] {a b : α} : (a == b) = (b == a) :=
+  (Bool.coe_iff_coe (a == b) (b == a)).mp (by simp [@eq_comm α])
+
 /-! ### xor -/
 
 theorem false_xor : ∀ (x : Bool), xor false x = x := false_bne

src/Init/Data/Fin/Lemmas.lean

@@ -541,7 +541,7 @@ theorem pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w
     ∀ {a b : Fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha = b.pred hb ↔ a = b
   | ⟨0, _⟩, _, ha, _ => by simp only [mk_zero, ne_eq, not_true] at ha
   | ⟨i + 1, _⟩, ⟨0, _⟩, _, hb => by simp only [mk_zero, ne_eq, not_true] at hb
-  | ⟨i + 1, hi⟩, ⟨j + 1, hj⟩, ha, hb => by simp [ext_iff]
+  | ⟨i + 1, hi⟩, ⟨j + 1, hj⟩, ha, hb => by simp [ext_iff, Nat.succ.injEq]
 
 @[simp] theorem pred_one {n : Nat} :
     Fin.pred (1 : Fin (n + 2)) (Ne.symm (Fin.ne_of_lt one_pos)) = 0 := rfl
@@ -683,6 +683,7 @@ and `cast` defines the inductive step using `motive i.succ`, inducting downwards
 termination_by n + 1 - i
 decreasing_by decreasing_with
   -- FIXME: we put the proof down here to avoid getting a dummy `have` in the definition
+  try simp only [Nat.succ_sub_succ_eq_sub]
   exact Nat.add_sub_add_right .. ▸ Nat.sub_lt_sub_left i.2 (Nat.lt_succ_self i)
 
 @[simp] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :

src/Init/Data/List/Lemmas.lean

@@ -249,12 +249,14 @@ theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a
 theorem get?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length ≤ n →
   (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length)
 | [], _, n, _ => rfl
-| a :: l, _, n+1, h₁ => by rw [cons_append]; simp [get?_append_right (Nat.lt_succ.1 h₁)]
+| a :: l, _, n+1, h₁ => by
+  rw [cons_append]
+  simp [Nat.succ_sub_succ_eq_sub, get?_append_right (Nat.lt_succ.1 h₁)]
 
 theorem get?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l →
     get? l.reverse i = get? l j
   | [], _, _, _ => rfl
-  | a::l, i, 0, h => by simp at h; simp [h, get?_append_right]
+  | a::l, i, 0, h => by simp [Nat.succ.injEq] at h; simp [h, get?_append_right, Nat.succ.injEq]
   | a::l, i, j+1, h => by
     have := Nat.succ.inj h; simp at this ⊢
     rw [get?_append, get?_reverse' _ j this]

src/Init/Data/Nat.lean

@@ -19,3 +19,4 @@ import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Mod
 import Init.Data.Nat.Lcm
 import Init.Data.Nat.Compare
+import Init.Data.Nat.Simproc

src/Init/Data/Nat/Basic.lean

@@ -174,7 +174,7 @@ protected theorem add_right_comm (n m k : Nat) : (n + m) + k = (n + k) + m := by
 protected theorem add_left_cancel {n m k : Nat} : n + m = n + k → m = k := by
   induction n with
   | zero => simp
-  | succ n ih => simp [succ_add]; intro h; apply ih h
+  | succ n ih => simp [succ_add, succ.injEq]; intro h; apply ih h
 
 protected theorem add_right_cancel {n m k : Nat} (h : n + m = k + m) : n = k := by
   rw [Nat.add_comm n m, Nat.add_comm k m] at h
@@ -248,7 +248,7 @@ theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m := succ_le_succ
 
 @[simp] protected theorem sub_zero (n : Nat) : n - 0 = n := rfl
 
-@[simp] theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
+theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
   induction m with
   | zero      => exact rfl
   | succ m ih => apply congrArg pred ih
@@ -574,7 +574,7 @@ theorem eq_zero_or_eq_succ_pred : ∀ n, n = 0 ∨ n = succ (pred n)
   | 0 => .inl rfl
   | _+1 => .inr rfl
 
-theorem succ_inj' : succ a = succ b ↔ a = b := ⟨succ.inj, congrArg _⟩
+theorem succ_inj' : succ a = succ b ↔ a = b := (Nat.succ.injEq a b).to_iff
 
 theorem succ_le_succ_iff : succ a ≤ succ b ↔ a ≤ b := ⟨le_of_succ_le_succ, succ_le_succ⟩
 
@@ -802,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 [← Nat.add_assoc, ih]
+  | succ k ih => simp [← Nat.add_assoc, succ_sub_succ_eq_sub, 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/Lemmas.lean

@@ -9,6 +9,7 @@ import Init.Data.Bool
 import Init.Data.Int.Pow
 import Init.Data.Nat.Bitwise.Basic
 import Init.Data.Nat.Lemmas
+import Init.Data.Nat.Simproc
 import Init.TacticsExtra
 import Init.Omega
 
@@ -271,15 +272,15 @@ theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
   induction i generalizing n x with
   | zero =>
     match n with
-    | 0 => simp
+    | 0 => simp [succ_sub_succ_eq_sub]
     | n+1 =>
       simp [not_decide_mod_two_eq_one]
       omega
   | succ i ih =>
     simp only [testBit_succ]
     match n with
     | 0 =>
-      simp [decide_eq_false]
+      simp [decide_eq_false, succ_sub_succ_eq_sub]
     | n+1 =>
       rw [Nat.two_pow_succ_sub_succ_div_two, ih]
       · simp [Nat.succ_lt_succ_iff]

src/Init/Data/Nat/Lemmas.lean

@@ -88,7 +88,7 @@ protected theorem add_pos_right (m) (h : 0 < n) : 0 < m + n :=
   Nat.lt_of_lt_of_le h (Nat.le_add_left ..)
 
 protected theorem add_self_ne_one : ∀ n, n + n ≠ 1
-  | n+1, h => by rw [Nat.succ_add, Nat.succ_inj'] at h; contradiction
+  | n+1, h => by rw [Nat.succ_add, Nat.succ.injEq] at h; contradiction
 
 /-! ## sub -/
 

src/Init/Data/Nat/Linear.lean

@@ -580,7 +580,7 @@ attribute [-simp] Nat.right_distrib Nat.left_distrib
 
 theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul (k+1)).denote ctx = c.denote ctx := by
   cases c; rename_i eq lhs rhs
-  have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp
+  have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp [Nat.succ.injEq]
   have : ¬ (k == 0) → (k + 1 == 1) = false := fun h => beq_false_of_ne (this (ne_of_beq_false (Bool.of_not_eq_true h)))
   have : ¬ ((k + 1 == 0) = true)  := fun h => absurd (eq_of_beq h) (Nat.succ_ne_zero k)
   have : (1 == (0 : Nat)) = false := rfl

src/Init/Data/Nat/Simproc.lean

@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2023 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix
+-/
+prelude
+import Init.Data.Bool
+import Init.Data.Nat.Basic
+import Init.Data.Nat.Lemmas
+
+/-!
+This contains lemmas used by the Nat simprocs for simplifying arithmetic
+addition offsets.
+-/
+namespace Nat.Simproc
+
+/- Sub proofs -/
+
+theorem sub_add_eq_comm (a b c : Nat) : a - (b + c) = a - c - b := by
+  rw [Nat.add_comm b c]
+  exact Nat.sub_add_eq a c b
+
+theorem add_sub_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : a + b - (c + d) = a - (c + (d-b)) := by
+  induction b generalizing a c d with
+  | zero =>
+    simp
+  | succ b ind =>
+    match d with
+    | 0 =>
+      contradiction
+    | d + 1 =>
+      have g := Nat.le_of_succ_le_succ h
+      rw [Nat.add_succ a, Nat.add_succ c, Nat.succ_sub_succ, Nat.succ_sub_succ,
+          ind _ _ g]
+
+theorem add_sub_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : a + b - (c + d) = a + (b - d) - c := by
+  rw [Nat.add_comm c d, Nat.sub_add_eq, Nat.add_sub_assoc h a]
+
+theorem add_sub_le (a : Nat) {b c : Nat} (h : b ≤ c) : a + b - c = a - (c - b) := by
+  have p := add_sub_add_le a 0 h
+  simp only [Nat.zero_add] at p
+  exact p
+
+/- Eq proofs -/
+
+theorem add_eq_gt (a : Nat) {b c : Nat} (h : b > c) : (a + b = c) = False :=
+  eq_false (Nat.ne_of_gt (Nat.lt_of_lt_of_le h (le_add_left b a)))
+
+theorem eq_add_gt (a : Nat) {b c : Nat} (h : c > a) : (a = b + c) = False := by
+  rw [@Eq.comm Nat a (b + c)]
+  exact add_eq_gt b h
+
+theorem add_eq_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : (a + b = c + d) = (a = c + (d - b)) := by
+  have g : b ≤ c + d := Nat.le_trans h (le_add_left d c)
+  rw [← Nat.add_sub_assoc h, @Eq.comm _ a, Nat.sub_eq_iff_eq_add g, @Eq.comm _ (a + b)]
+
+theorem add_eq_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : (a + b = c + d) = (a + (b - d) = c) := by
+  rw [@Eq.comm _ (a + b) _, add_eq_add_le c a h, @Eq.comm _ _ c]
+
+theorem add_eq_le (a : Nat) {b c : Nat} (h : b ≤ c) : (a + b = c) = (a = c - b) := by
+  have r := add_eq_add_le a 0 h
+  simp only [Nat.zero_add] at r
+  exact r
+
+theorem eq_add_le {a : Nat} (b : Nat) {c : Nat} (h : c ≤ a) : (a = b + c) = (b = a - c) := by
+  rw [@Eq.comm Nat a (b + c)]
+  exact add_eq_le b h
+
+/- Lemmas for lifting Eq proofs to beq -/
+
+theorem beqEqOfEqEq {a b c d : Nat} (p : (a = b) = (c = d)) : (a == b) = (c == d) := by
+  simp only [Bool.beq_eq_decide_eq, p]
+
+theorem beqFalseOfEqFalse {a b : Nat} (p : (a = b) = False) : (a == b) = false := by
+  simp [Bool.beq_eq_decide_eq, p]
+
+theorem bneEqOfEqEq {a b c d : Nat} (p : (a = b) = (c = d)) : (a != b) = (c != d) := by
+  simp only [bne, beqEqOfEqEq p]
+
+theorem bneTrueOfEqFalse {a b : Nat} (p : (a = b) = False) : (a != b) = true := by
+  simp [bne, beqFalseOfEqFalse p]
+
+/- le proofs -/
+
+theorem add_le_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : (a + b ≤ c + d) = (a ≤ c + (d - b)) := by
+  rw [← Nat.add_sub_assoc h, Nat.le_sub_iff_add_le]
+  exact Nat.le_trans h (le_add_left d c)
+
+theorem add_le_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : (a + b ≤ c + d) = (a + (b - d) ≤ c) := by
+  rw [← Nat.add_sub_assoc h, Nat.sub_le_iff_le_add]
+
+theorem add_le_le (a : Nat) {b c : Nat} (h : b ≤ c) : (a + b ≤ c) = (a ≤ c - b) := by
+  have r := add_le_add_le a 0 h
+  simp only [Nat.zero_add] at r
+  exact r
+
+theorem add_le_gt (a : Nat) {b c : Nat} (h : b > c) : (a + b ≤ c) = False :=
+  eq_false (Nat.not_le_of_gt (Nat.lt_of_lt_of_le h (le_add_left b a)))
+
+theorem le_add_le (a : Nat) {b c : Nat} (h : a ≤ c) : (a ≤ b + c) = True :=
+  eq_true (Nat.le_trans h (le_add_left c b))
+
+theorem le_add_ge (a : Nat) {b c : Nat} (h : a ≥ c) : (a ≤ b + c) = (a - c ≤ b) := by
+  have r := add_le_add_ge 0 b h
+  simp only [Nat.zero_add] at r
+  exact r
+
+end Nat.Simproc