feat: add missing theorems for + 1 and - 1 normal form (#4242)

`Nat.succ_eq_add_one` and `Nat.pred_eq_sub_one` are now simp lemmas. For
theorems about `Nat.succ` or `Nat.pred` without corresponding theorem
for `+ 1` or `- 1`, this adds the corresponding theorem.

src/Init/Data/Nat/Basic.lean

@@ -200,6 +200,9 @@ protected theorem eq_zero_of_add_eq_zero_left (h : n + m = 0) : m = 0 :=
 theorem mul_succ (n m : Nat) : n * succ m = n * m + n :=
   rfl
 
+theorem mul_add_one (n m : Nat) : n * (m + 1) = n * m + n :=
+  rfl
+
 @[simp] protected theorem zero_mul : ∀ (n : Nat), 0 * n = 0
   | 0      => rfl
   | succ n => mul_succ 0 n ▸ (Nat.zero_mul n).symm ▸ rfl
@@ -209,6 +212,8 @@ theorem succ_mul (n m : Nat) : (succ n) * m = (n * m) + m := by
   | zero => rfl
   | succ m ih => rw [mul_succ, add_succ, ih, mul_succ, add_succ, Nat.add_right_comm]
 
+theorem add_one_mul (n m : Nat) : (n + 1) * m = (n * m) + m := succ_mul n m
+
 protected theorem mul_comm : ∀ (n m : Nat), n * m = m * n
   | n, 0      => (Nat.zero_mul n).symm ▸ (Nat.mul_zero n).symm ▸ rfl
   | n, succ m => (mul_succ n m).symm ▸ (succ_mul m n).symm ▸ (Nat.mul_comm n m).symm ▸ rfl
@@ -256,8 +261,18 @@ theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m := succ_le_succ
 
 theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m := succ_le_succ
 
+theorem le_of_lt_add_one {n m : Nat} : n < m + 1 → n ≤ m := le_of_succ_le_succ
+
+theorem lt_add_one_of_le {n m : Nat} : n ≤ m → n < m + 1 := succ_le_succ
+
 @[simp] protected theorem sub_zero (n : Nat) : n - 0 = n := rfl
 
+theorem not_add_one_le_zero (n : Nat) : ¬ n + 1 ≤ 0 := nofun
+
+theorem not_add_one_le_self : (n : Nat) → ¬ n + 1 ≤ n := Nat.not_succ_le_self
+
+theorem add_one_pos (n : Nat) : 0 < n + 1 := Nat.zero_lt_succ n
+
 theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
   induction m with
   | zero      => exact rfl
@@ -271,6 +286,8 @@ theorem pred_lt : ∀ {n : Nat}, n ≠ 0 → pred n < n
   | zero,   h => absurd rfl h
   | succ _, _ => lt_succ_of_le (Nat.le_refl _)
 
+theorem sub_one_lt : ∀ {n : Nat}, n ≠ 0 → n - 1 < n := pred_lt
+
 theorem sub_le (n m : Nat) : n - m ≤ n := by
   induction m with
   | zero      => exact Nat.le_refl (n - 0)
@@ -340,6 +357,8 @@ theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
 
 @[simp] theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
 
+@[simp] protected theorem lt_add_one (n : Nat) : n < n + 1 := lt.base n
+
 protected theorem le_total (m n : Nat) : m ≤ n ∨ n ≤ m :=
   match Nat.lt_or_ge m n with
   | Or.inl h => Or.inl (Nat.le_of_lt h)
@@ -370,19 +389,35 @@ theorem le_or_eq_of_le_succ {m n : Nat} (h : m ≤ succ n) : m ≤ n ∨ m = suc
        have : succ m ≤ succ n := succ_le_of_lt this
        Or.inl (le_of_succ_le_succ this))
 
+theorem le_or_eq_of_le_add_one {m n : Nat} (h : m ≤ n + 1) : m ≤ n ∨ m = n + 1 :=
+  le_or_eq_of_le_succ h
+
 theorem le_add_right : ∀ (n k : Nat), n ≤ n + k
   | n, 0   => Nat.le_refl n
   | n, k+1 => le_succ_of_le (le_add_right n k)
 
 theorem le_add_left (n m : Nat): n ≤ m + n :=
   Nat.add_comm n m ▸ le_add_right n m
 
+theorem le_of_add_right_le {n m k : Nat} (h : n + k ≤ m) : n ≤ m :=
+  Nat.le_trans (le_add_right n k) h
+
+theorem le_add_right_of_le {n m k : Nat} (h : n ≤ m) : n ≤ m + k :=
+  Nat.le_trans h (le_add_right m k)
+
+theorem lt_of_add_one_le {n m : Nat} (h : n + 1 ≤ m) : n < m := h
+
+theorem add_one_le_of_lt {n m : Nat} (h : n < m) : n + 1 ≤ m := h
+
 protected theorem lt_add_left (c : Nat) (h : a < b) : a < c + b :=
   Nat.lt_of_lt_of_le h (Nat.le_add_left ..)
 
 protected theorem lt_add_right (c : Nat) (h : a < b) : a < b + c :=
   Nat.lt_of_lt_of_le h (Nat.le_add_right ..)
 
+theorem lt_of_add_right_lt {n m k : Nat} (h : n + k < m) : n < m :=
+  Nat.lt_of_le_of_lt (Nat.le_add_right ..) h
+
 theorem le.dest : ∀ {n m : Nat}, n ≤ m → Exists (fun k => n + k = m)
   | zero,   zero,   _ => ⟨0, rfl⟩
   | zero,   succ n, _ => ⟨succ n, Nat.add_comm 0 (succ n) ▸ rfl⟩
@@ -537,9 +572,14 @@ protected theorem le_iff_lt_or_eq {n m : Nat} : n ≤ m ↔ n < m ∨ n = m :=
 
 protected theorem lt_succ_iff : m < succ n ↔ m ≤ n := ⟨le_of_lt_succ, lt_succ_of_le⟩
 
+protected theorem lt_add_one_iff : m < n + 1 ↔ m ≤ n := ⟨le_of_lt_succ, lt_succ_of_le⟩
+
 protected theorem lt_succ_iff_lt_or_eq : m < succ n ↔ m < n ∨ m = n :=
   Nat.lt_succ_iff.trans Nat.le_iff_lt_or_eq
 
+protected theorem lt_add_one_iff_lt_or_eq : m < n + 1 ↔ m < n ∨ m = n :=
+  Nat.lt_add_one_iff.trans Nat.le_iff_lt_or_eq
+
 protected theorem eq_of_lt_succ_of_not_lt (hmn : m < n + 1) (h : ¬ m < n) : m = n :=
   (Nat.lt_succ_iff_lt_or_eq.1 hmn).resolve_left h
 
@@ -571,12 +611,18 @@ attribute [simp] zero_lt_succ
 
 theorem succ_ne_self (n) : succ n ≠ n := Nat.ne_of_gt (lt_succ_self n)
 
+theorem add_one_ne_self (n) : n + 1 ≠ n := Nat.ne_of_gt (lt_succ_self n)
+
 theorem succ_le : succ n ≤ m ↔ n < m := .rfl
 
+theorem add_one_le_iff : n + 1 ≤ m ↔ n < m := .rfl
+
 theorem lt_succ : m < succ n ↔ m ≤ n := ⟨le_of_lt_succ, lt_succ_of_le⟩
 
 theorem lt_succ_of_lt (h : a < b) : a < succ b := le_succ_of_le h
 
+theorem lt_add_one_of_lt (h : a < b) : a < b + 1 := le_succ_of_le h
+
 theorem succ_pred_eq_of_ne_zero : ∀ {n}, n ≠ 0 → succ (pred n) = n
   | _+1, _ => rfl
 
@@ -596,6 +642,9 @@ theorem pred_inj : ∀ {a b}, 0 < a → 0 < b → pred a = pred b → a = b
 theorem pred_ne_self : ∀ {a}, a ≠ 0 → pred a ≠ a
   | _+1, _ => (succ_ne_self _).symm
 
+theorem sub_one_ne_self : ∀ {a}, a ≠ 0 → a - 1 ≠ a
+  | _+1, _ => (succ_ne_self _).symm
+
 theorem pred_lt_self : ∀ {a}, 0 < a → pred a < a
   | _+1, _ => lt_succ_self _
 
@@ -628,9 +677,17 @@ theorem le_sub_one_of_lt : a < b → a ≤ b - 1 := Nat.le_pred_of_lt
 
 theorem lt_of_le_pred (h : 0 < m) : n ≤ pred m → n < m := (le_pred_iff_lt h).1
 
+theorem lt_of_le_sub_one (h : 0 < m) : n ≤ m - 1 → n < m := (le_pred_iff_lt h).1
+
+protected theorem le_sub_one_iff_lt (h : 0 < m) : n ≤ m - 1 ↔ n < m :=
+  ⟨Nat.lt_of_le_sub_one h, Nat.le_sub_one_of_lt⟩
+
 theorem exists_eq_succ_of_ne_zero : ∀ {n}, n ≠ 0 → Exists fun k => n = succ k
   | _+1, _ => ⟨_, rfl⟩
 
+theorem exists_eq_add_one_of_ne_zero : ∀ {n}, n ≠ 0 → Exists fun k => n = k + 1
+  | _+1, _ => ⟨_, rfl⟩
+
 /-! # Basic theorems for comparing numerals -/
 
 theorem ctor_eq_zero : Nat.zero = 0 :=
@@ -686,6 +743,9 @@ theorem eq_of_mul_eq_mul_right {n m k : Nat} (hm : 0 < m) (h : n * m = k * m) :
 protected theorem pow_succ (n m : Nat) : n^(succ m) = n^m * n :=
   rfl
 
+protected theorem pow_add_one (n m : Nat) : n^(m + 1) = n^m * n :=
+  rfl
+
 protected theorem pow_zero (n : Nat) : n^0 = 1 := rfl
 
 theorem pow_le_pow_of_le_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i
@@ -737,9 +797,15 @@ theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := by
   exact absurd h (Nat.not_lt_zero _)
   apply Nat.noConfusion
 
-theorem pred_lt' {n m : Nat} (h : m < n) : pred n < n :=
+theorem pred_lt_of_lt {n m : Nat} (h : m < n) : pred n < n :=
   pred_lt (not_eq_zero_of_lt h)
 
+set_option linter.missingDocs false in
+@[deprecated (since := "2024-06-01")] abbrev pred_lt' := @pred_lt_of_lt
+
+theorem sub_one_lt_of_lt {n m : Nat} (h : m < n) : n - 1 < n :=
+  sub_one_lt (not_eq_zero_of_lt h)
+
 /-! # pred theorems -/
 
 @[simp] protected theorem pred_zero : pred 0 = 0 := rfl
@@ -750,12 +816,21 @@ theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by
   | zero => contradiction
   | succ => rfl
 
+theorem sub_one_add_one {a : Nat} (h : a ≠ 0) : a - 1 + 1 = a := by
+  induction a with
+  | zero => contradiction
+  | succ => rfl
+
 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
 
+theorem eq_zero_or_eq_sub_one_add_one : ∀ {n}, n = 0 ∨ n = n - 1 + 1
+  | 0 => Or.inl rfl
+  | _+1 => Or.inr rfl
+
 @[simp] theorem pred_eq_sub_one : pred n = n - 1 := rfl
 
 /-! # sub theorems -/
@@ -806,6 +881,9 @@ theorem add_sub_of_le {a b : Nat} (h : a ≤ b) : a + (b - a) = b := by
     have : a ≤ b := Nat.le_of_succ_le h
     rw [sub_succ, Nat.succ_add, ← Nat.add_succ, Nat.succ_pred hne, ih this]
 
+theorem sub_one_cancel : ∀ {a b : Nat}, 0 < a → 0 < b → a - 1 = b - 1 → a = b
+  | _+1, _+1, _, _ => congrArg _
+
 @[simp] protected theorem sub_add_cancel {n m : Nat} (h : m ≤ n) : n - m + m = n := by
   rw [Nat.add_comm, Nat.add_sub_of_le h]
 
@@ -857,6 +935,17 @@ protected theorem sub_lt_sub_left : ∀ {k m n : Nat}, k < m → k < n → m - n
   | zero => rfl
   | succ n ih => simp only [ih, Nat.sub_succ]; decide
 
+protected theorem sub_lt_sub_right : ∀ {a b c : Nat}, c ≤ a → a < b → a - c < b - c
+  | 0, _, _, hle, h => by
+    rw [Nat.eq_zero_of_le_zero hle, Nat.sub_zero, Nat.sub_zero]
+    exact h
+  | _, _, 0, _, h => by
+    rw [Nat.sub_zero, Nat.sub_zero]
+    exact h
+  | _+1, _+1, _+1, hle, h => by
+    rw [Nat.add_sub_add_right, Nat.add_sub_add_right]
+    exact Nat.sub_lt_sub_right (le_of_succ_le_succ hle) (lt_of_succ_lt_succ h)
+
 protected theorem sub_self_add (n m : Nat) : n - (n + m) = 0 := by
   show (n + 0) - (n + m) = 0
   rw [Nat.add_sub_add_left, Nat.zero_sub]
@@ -935,6 +1024,9 @@ protected theorem sub_le_sub_right {n m : Nat} (h : n ≤ m) : ∀ k, n - k ≤
   | 0   => h
   | z+1 => pred_le_pred (Nat.sub_le_sub_right h z)
 
+protected theorem sub_le_add_right_sub (a i j : Nat) : a - i ≤ a + j - i :=
+  Nat.sub_le_sub_right (Nat.le_add_right ..) ..
+
 protected theorem lt_of_sub_ne_zero (h : n - m ≠ 0) : m < n :=
   Nat.not_le.1 (mt Nat.sub_eq_zero_of_le h)
 
@@ -947,6 +1039,9 @@ protected theorem lt_of_sub_pos (h : 0 < n - m) : m < n :=
 protected theorem lt_of_sub_eq_succ (h : m - n = succ l) : n < m :=
   Nat.lt_of_sub_pos (h ▸ Nat.zero_lt_succ _)
 
+protected theorem lt_of_sub_eq_sub_one (h : m - n = l + 1) : n < m :=
+  Nat.lt_of_sub_pos (h ▸ Nat.zero_lt_succ _)
+
 protected theorem sub_lt_left_of_lt_add {n k m : Nat} (H : n ≤ k) (h : k < n + m) : k - n < m := by
   have := Nat.sub_le_sub_right (succ_le_of_lt h) n
   rwa [Nat.add_sub_cancel_left, Nat.succ_sub H] at this
@@ -974,21 +1069,35 @@ protected theorem sub_eq_iff_eq_add {c : Nat} (h : b ≤ a) : a - b = c ↔ a =
 protected theorem sub_eq_iff_eq_add' {c : Nat} (h : b ≤ a) : a - b = c ↔ a = b + c := by
   rw [Nat.add_comm, Nat.sub_eq_iff_eq_add h]
 
-theorem mul_pred_left (n m : Nat) : pred n * m = n * m - m := by
+/-! ## Mul sub distrib -/
+
+theorem pred_mul (n m : Nat) : pred n * m = n * m - m := by
   cases n with
   | zero   => simp
   | succ n => rw [Nat.pred_succ, succ_mul, Nat.add_sub_cancel]
 
-/-! ## Mul sub distrib -/
+set_option linter.missingDocs false in
+@[deprecated (since := "2024-06-01")] abbrev mul_pred_left := @pred_mul
+
+protected theorem sub_one_mul  (n m : Nat) : (n - 1) * m = n * m - m := by
+  cases n with
+  | zero   => simp
+  | succ n =>
+    rw [Nat.add_sub_cancel, add_one_mul, Nat.add_sub_cancel]
+
+theorem mul_pred (n m : Nat) : n * pred m = n * m - n := by
+  rw [Nat.mul_comm, pred_mul, Nat.mul_comm]
 
-theorem mul_pred_right (n m : Nat) : n * pred m = n * m - n := by
-  rw [Nat.mul_comm, mul_pred_left, Nat.mul_comm]
+set_option linter.missingDocs false in
+@[deprecated (since := "2024-06-01")] abbrev mul_pred_right := @mul_pred
 
+theorem mul_sub_one (n m : Nat) : n * (m - 1) = n * m - n := by
+  rw [Nat.mul_comm, Nat.sub_one_mul , Nat.mul_comm]
 
 protected theorem mul_sub_right_distrib (n m k : Nat) : (n - m) * k = n * k - m * k := by
   induction m with
   | zero => simp
-  | succ m ih => rw [Nat.sub_succ, Nat.mul_pred_left, ih, succ_mul, Nat.sub_sub]; done
+  | succ m ih => rw [Nat.sub_succ, Nat.pred_mul, ih, succ_mul, Nat.sub_sub]; done
 
 protected theorem mul_sub_left_distrib (n m k : Nat) : n * (m - k) = n * m - n * k := by
   rw [Nat.mul_comm, Nat.mul_sub_right_distrib, Nat.mul_comm m n, Nat.mul_comm n k]

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

@@ -90,6 +90,10 @@ noncomputable def div2Induction {motive : Nat → Sort u}
   unfold testBit
   simp [shiftRight_succ_inside]
 
+@[simp] theorem testBit_add_one (x i : Nat) : testBit x (i + 1) = testBit (x/2) i := by
+  unfold testBit
+  simp [shiftRight_succ_inside]
+
 theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) := by
   induction i generalizing x with
   | zero =>

src/Init/Data/Nat/Gcd.lean

@@ -43,6 +43,9 @@ def gcd (m n : @& Nat) : Nat :=
 theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) := by
   rw [gcd]; rfl
 
+theorem gcd_add_one (x y : Nat) : gcd (x + 1) y = gcd (y % (x + 1)) (x + 1) := by
+  rw [gcd]; rfl
+
 @[simp] theorem gcd_one_left (n : Nat) : gcd 1 n = 1 := by
   rw [gcd_succ, mod_one]
   rfl

src/Init/Data/Nat/Lemmas.lean

@@ -101,6 +101,10 @@ protected theorem one_sub : ∀ n, 1 - n = if n = 0 then 1 else 0
 theorem succ_sub_sub_succ (n m k) : succ n - m - succ k = n - m - k := by
   rw [Nat.sub_sub, Nat.sub_sub, add_succ, succ_sub_succ]
 
+theorem add_sub_sub_add_right (n m k l : Nat) :
+    (n + l) - m - (k + l) = n - m - k := by
+  rw [Nat.sub_sub, Nat.sub_sub, ←Nat.add_assoc, Nat.add_sub_add_right]
+
 protected theorem sub_right_comm (m n k : Nat) : m - n - k = m - k - n := by
   rw [Nat.sub_sub, Nat.sub_sub, Nat.add_comm]
 
@@ -176,10 +180,12 @@ protected theorem sub_add_lt_sub (h₁ : m + k ≤ n) (h₂ : 0 < k) : n - (m +
   rw [← Nat.sub_sub]; exact Nat.sub_lt_of_pos_le h₂ (Nat.le_sub_of_add_le' h₁)
 
 theorem sub_one_lt_of_le (h₀ : 0 < a) (h₁ : a ≤ b) : a - 1 < b :=
-  Nat.lt_of_lt_of_le (Nat.pred_lt' h₀) h₁
+  Nat.lt_of_lt_of_le (Nat.pred_lt_of_lt h₀) h₁
 
 theorem sub_lt_succ (a b) : a - b < succ a := lt_succ_of_le (sub_le a b)
 
+theorem sub_lt_add_one (a b) : a - b < a + 1 := lt_add_one_of_le (sub_le a b)
+
 theorem sub_one_sub_lt (h : i < n) : n - 1 - i < n := by
   rw [Nat.sub_right_comm]; exact Nat.sub_one_lt_of_le (Nat.sub_pos_of_lt h) (Nat.sub_le ..)
 
@@ -479,6 +485,9 @@ protected theorem mul_lt_mul_of_lt_of_lt {a b c d : Nat} (hac : a < c) (hbd : b
 theorem succ_mul_succ (a b) : succ a * succ b = a * b + a + b + 1 := by
   rw [succ_mul, mul_succ]; rfl
 
+theorem add_one_mul_add_one (a b : Nat) : (a + 1) * (b + 1) = a * b + a + b + 1 := by
+  rw [add_one_mul, mul_add_one]; rfl
+
 theorem mul_le_add_right (m k n : Nat) : k * m ≤ m + n ↔ (k-1) * m ≤ n := by
   match k with
   | 0 =>
@@ -562,6 +571,9 @@ theorem add_mod (a b n : Nat) : (a + b) % n = ((a % n) + (b % n)) % n := by
 theorem pow_succ' {m n : Nat} : m ^ n.succ = m * m ^ n := by
   rw [Nat.pow_succ, Nat.mul_comm]
 
+theorem pow_add_one' {m n : Nat} : m ^ (n + 1) = m * m ^ n := by
+  rw [Nat.pow_add_one, Nat.mul_comm]
+
 @[simp] theorem pow_eq {m n : Nat} : m.pow n = m ^ n := rfl
 
 theorem one_shiftLeft (n : Nat) : 1 <<< n = 2 ^ n := by rw [shiftLeft_eq, Nat.one_mul]

src/Init/Prelude.lean

@@ -1071,11 +1071,15 @@ This type is special-cased by both the kernel and the compiler:
   library (usually [GMP](https://gmplib.org/)).
 -/
 inductive Nat where
-  /-- `Nat.zero`, normally written `0 : Nat`, is the smallest natural number.
-  This is one of the two constructors of `Nat`. -/
+  /-- `Nat.zero`, is the smallest natural number. This is one of the two
+  constructors of `Nat`. Using `Nat.zero` should usually be avoided in favor of
+  `0 : Nat` or simply `0`, in order to remain compatible with the simp normal
+  form defined by `Nat.zero_eq`. -/
   | zero : Nat
   /-- The successor function on natural numbers, `succ n = n + 1`.
-  This is one of the two constructors of `Nat`. -/
+  This is one of the two constructors of `Nat`. Using `succ n` should usually
+  be avoided in favor of `n + 1`, in order to remain compatible with the simp
+  normal form defined by `Nat.succ_eq_add_one`. -/
   | succ (n : Nat) : Nat
 
 instance : Inhabited Nat where

src/Init/WFTactics.lean

@@ -32,7 +32,7 @@ before `omega` is available.
 -/
 syntax "decreasing_trivial_pre_omega" : tactic
 macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
-macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
+macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt_of_lt; assumption) -- i-1 < i if j < i
 macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt; assumption)  -- i-1 < i if i ≠ 0