feat: further shaking of Nat/Int/Omega (#3613)

src/Init/Control/Lawful/Basic.lean

@@ -6,7 +6,6 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 prelude
 import Init.SimpLemmas
 import Init.Meta
-import Init.Data.Ord
 
 open Function
 

src/Init/Data/Array/QSort.lean

@@ -10,7 +10,7 @@ namespace Array
 -- TODO: remove the [Inhabited α] parameters as soon as we have the tactic framework for automating proof generation and using Array.fget
 
 def qpartition (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat × Array α :=
-  if h : as.size = 0 then (0, as) else have : Inhabited α := ⟨as[0]'(by revert h; cases as.size <;> simp [Nat.zero_lt_succ])⟩ -- TODO: remove
+  if h : as.size = 0 then (0, as) else have : Inhabited α := ⟨as[0]'(by revert h; cases as.size <;> simp)⟩ -- TODO: remove
   let mid := (lo + hi) / 2
   let as  := if lt (as.get! mid) (as.get! lo) then as.swap! lo mid else as
   let as  := if lt (as.get! hi)  (as.get! lo) then as.swap! lo hi  else as

src/Init/Data/Int/DivMod.lean

@@ -158,6 +158,8 @@ instance : Div Int where
 instance : Mod Int where
   mod := Int.emod
 
+@[simp, norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
+
 /-!
 # `bmod` ("balanced" mod)
 

src/Init/Data/Int/DivModLemmas.lean

@@ -9,7 +9,6 @@ import Init.Data.Int.DivMod
 import Init.Data.Int.Order
 import Init.Data.Nat.Dvd
 import Init.RCases
-import Init.TacticsExtra
 
 /-!
 # Lemmas about integer division needed to bootstrap `omega`.
@@ -22,8 +21,6 @@ namespace Int
 
 /-! ### `/`  -/
 
-@[simp, norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
-
 @[simp] theorem zero_ediv : ∀ b : Int, 0 / b = 0
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => show -ofNat _ = _ by simp

src/Init/Data/List/BasicAux.lean

@@ -5,9 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.Nat.Linear
-import Init.Data.Array.Basic
-import Init.Data.List.Basic
-import Init.Util
 
 universe u
 

src/Init/Data/List/Lemmas.lean

@@ -6,7 +6,6 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 prelude
 import Init.Data.List.BasicAux
 import Init.Data.List.Control
-import Init.Data.Nat.Lemmas
 import Init.PropLemmas
 import Init.Control.Lawful.Basic
 import Init.Hints

src/Init/Data/Nat/Basic.lean

@@ -224,7 +224,7 @@ theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m := succ_le_succ
   | zero      => exact rfl
   | succ m ih => apply congrArg pred ih
 
-theorem pred_le : ∀ (n : Nat), pred n ≤ n
+@[simp] theorem pred_le : ∀ (n : Nat), pred n ≤ n
   | zero   => Nat.le.refl
   | succ _ => le_succ _
 
@@ -298,7 +298,8 @@ theorem eq_zero_or_pos : ∀ (n : Nat), n = 0 ∨ n > 0
 protected theorem pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n := (eq_zero_or_pos n).resolve_left
 
 theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
-theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
+
+@[simp] theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
 
 protected theorem le_total (m n : Nat) : m ≤ n ∨ n ≤ m :=
   match Nat.lt_or_ge m n with
@@ -337,6 +338,12 @@ theorem le_add_right : ∀ (n k : Nat), n ≤ n + k
 theorem le_add_left (n m : Nat): n ≤ m + n :=
   Nat.add_comm n m ▸ le_add_right n m
 
+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 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⟩
@@ -426,6 +433,9 @@ protected theorem add_lt_add_left {n m : Nat} (h : n < m) (k : Nat) : k + n < k
 protected theorem add_lt_add_right {n m : Nat} (h : n < m) (k : Nat) : n + k < m + k :=
   Nat.add_comm k m ▸ Nat.add_comm k n ▸ Nat.add_lt_add_left h k
 
+protected theorem lt_add_of_pos_right (h : 0 < k) : n < n + k :=
+  Nat.add_lt_add_left h n
+
 protected theorem zero_lt_one : 0 < (1:Nat) :=
   zero_lt_succ 0
 
@@ -516,6 +526,71 @@ protected theorem one_lt_two : 1 < 2 := Nat.succ_lt_succ Nat.zero_lt_one
 protected theorem eq_zero_of_not_pos (h : ¬0 < n) : n = 0 :=
   Nat.eq_zero_of_le_zero (Nat.not_lt.1 h)
 
+/-! ## succ/pred -/
+
+attribute [simp] zero_lt_succ
+
+theorem succ_ne_self (n) : succ n ≠ n := Nat.ne_of_gt (lt_succ_self n)
+
+theorem succ_le : succ n ≤ 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 succ_pred_eq_of_ne_zero : ∀ {n}, n ≠ 0 → succ (pred n) = n
+  | _+1, _ => rfl
+
+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_le_succ_iff : succ a ≤ succ b ↔ a ≤ b := ⟨le_of_succ_le_succ, succ_le_succ⟩
+
+theorem succ_lt_succ_iff : succ a < succ b ↔ a < b := ⟨lt_of_succ_lt_succ, succ_lt_succ⟩
+
+theorem pred_inj : ∀ {a b}, 0 < a → 0 < b → pred a = pred b → a = b
+  | _+1, _+1, _, _ => congrArg _
+
+theorem pred_ne_self : ∀ {a}, a ≠ 0 → pred a ≠ a
+  | _+1, _ => (succ_ne_self _).symm
+
+theorem pred_lt_self : ∀ {a}, 0 < a → pred a < a
+  | _+1, _ => lt_succ_self _
+
+theorem pred_lt_pred : ∀ {n m}, n ≠ 0 → n < m → pred n < pred m
+  | _+1, _+1, _, h => lt_of_succ_lt_succ h
+
+theorem pred_le_iff_le_succ : ∀ {n m}, pred n ≤ m ↔ n ≤ succ m
+  | 0, _ => ⟨fun _ => Nat.zero_le _, fun _ => Nat.zero_le _⟩
+  | _+1, _ => Nat.succ_le_succ_iff.symm
+
+theorem le_succ_of_pred_le : pred n ≤ m → n ≤ succ m := pred_le_iff_le_succ.1
+
+theorem pred_le_of_le_succ : n ≤ succ m → pred n ≤ m := pred_le_iff_le_succ.2
+
+theorem lt_pred_iff_succ_lt : ∀ {n m}, n < pred m ↔ succ n < m
+  | _, 0 => ⟨nofun, nofun⟩
+  | _, _+1 => Nat.succ_lt_succ_iff.symm
+
+theorem succ_lt_of_lt_pred : n < pred m → succ n < m := lt_pred_iff_succ_lt.1
+
+theorem lt_pred_of_succ_lt : succ n < m → n < pred m := lt_pred_iff_succ_lt.2
+
+theorem le_pred_iff_lt : ∀ {n m}, 0 < m → (n ≤ pred m ↔ n < m)
+  | 0, _+1, _ => ⟨fun _ => Nat.zero_lt_succ _, fun _ => Nat.zero_le _⟩
+  | _+1, _+1, _ => Nat.lt_pred_iff_succ_lt
+
+theorem le_pred_of_lt (h : n < m) : n ≤ pred m := (le_pred_iff_lt (Nat.zero_lt_of_lt h)).2 h
+
+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 exists_eq_succ_of_ne_zero : ∀ {n}, n ≠ 0 → Exists fun k => n = succ k
+  | _+1, _ => ⟨_, rfl⟩
 
 /-! # Basic theorems for comparing numerals -/
 
@@ -528,7 +603,7 @@ protected theorem one_ne_zero : 1 ≠ (0 : Nat) :=
 protected theorem zero_ne_one : 0 ≠ (1 : Nat) :=
   fun h => Nat.noConfusion h
 
-theorem succ_ne_zero (n : Nat) : succ n ≠ 0 :=
+@[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 _

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

@@ -333,7 +333,7 @@ private theorem eq_0_of_lt_one (x : Nat) : x < 1 ↔ x = 0 :=
       match x with
       | 0 => Eq.refl 0
       | _+1 => False.elim (not_lt_zero _ (Nat.lt_of_succ_lt_succ p)))
-    (fun p => by simp [p, Nat.zero_lt_succ])
+    (fun p => by simp [p])
 
 private theorem eq_0_of_lt (x : Nat) : x < 2^ 0 ↔ x = 0 := eq_0_of_lt_one x
 

src/Init/Data/Nat/Dvd.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 prelude
 import Init.Data.Nat.Div
+import Init.TacticsExtra
 
 namespace Nat
 
@@ -97,4 +98,10 @@ protected theorem mul_div_cancel' {n m : Nat} (H : n ∣ m) : n * (m / n) = m :=
 protected theorem div_mul_cancel {n m : Nat} (H : n ∣ m) : m / n * n = m := by
   rw [Nat.mul_comm, Nat.mul_div_cancel' H]
 
+@[simp] theorem mod_mod_of_dvd (a : Nat) (h : c ∣ b) : a % b % c = a % c := by
+  rw (config := {occs := .pos [2]}) [← mod_add_div a b]
+  have ⟨x, h⟩ := h
+  subst h
+  rw [Nat.mul_assoc, add_mul_mod_self_left]
+
 end Nat

src/Init/Data/Nat/Lemmas.lean

@@ -20,70 +20,6 @@ and later these lemmas should be organised into other files more systematically.
 
 namespace Nat
 
-/-! ## succ/pred -/
-
-attribute [simp] succ_ne_zero zero_lt_succ lt_succ_self Nat.pred_zero Nat.pred_succ Nat.pred_le
-
-theorem succ_ne_self (n) : succ n ≠ n := Nat.ne_of_gt (lt_succ_self n)
-
-theorem succ_le : succ n ≤ 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 succ_pred_eq_of_ne_zero : ∀ {n}, n ≠ 0 → succ (pred n) = n
-  | _+1, _ => rfl
-
-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_le_succ_iff : succ a ≤ succ b ↔ a ≤ b := ⟨le_of_succ_le_succ, succ_le_succ⟩
-
-theorem succ_lt_succ_iff : succ a < succ b ↔ a < b := ⟨lt_of_succ_lt_succ, succ_lt_succ⟩
-
-theorem pred_inj : ∀ {a b}, 0 < a → 0 < b → pred a = pred b → a = b
-  | _+1, _+1, _, _ => congrArg _
-
-theorem pred_ne_self : ∀ {a}, a ≠ 0 → pred a ≠ a
-  | _+1, _ => (succ_ne_self _).symm
-
-theorem pred_lt_self : ∀ {a}, 0 < a → pred a < a
-  | _+1, _ => lt_succ_self _
-
-theorem pred_lt_pred : ∀ {n m}, n ≠ 0 → n < m → pred n < pred m
-  | _+1, _+1, _, h => lt_of_succ_lt_succ h
-
-theorem pred_le_iff_le_succ : ∀ {n m}, pred n ≤ m ↔ n ≤ succ m
-  | 0, _ => ⟨fun _ => Nat.zero_le _, fun _ => Nat.zero_le _⟩
-  | _+1, _ => Nat.succ_le_succ_iff.symm
-
-theorem le_succ_of_pred_le : pred n ≤ m → n ≤ succ m := pred_le_iff_le_succ.1
-
-theorem pred_le_of_le_succ : n ≤ succ m → pred n ≤ m := pred_le_iff_le_succ.2
-
-theorem lt_pred_iff_succ_lt : ∀ {n m}, n < pred m ↔ succ n < m
-  | _, 0 => ⟨nofun, nofun⟩
-  | _, _+1 => Nat.succ_lt_succ_iff.symm
-
-theorem succ_lt_of_lt_pred : n < pred m → succ n < m := lt_pred_iff_succ_lt.1
-
-theorem lt_pred_of_succ_lt : succ n < m → n < pred m := lt_pred_iff_succ_lt.2
-
-theorem le_pred_iff_lt : ∀ {n m}, 0 < m → (n ≤ pred m ↔ n < m)
-  | 0, _+1, _ => ⟨fun _ => Nat.zero_lt_succ _, fun _ => Nat.zero_le _⟩
-  | _+1, _+1, _ => Nat.lt_pred_iff_succ_lt
-
-theorem lt_of_le_pred (h : 0 < m) : n ≤ pred m → n < m := (le_pred_iff_lt h).1
-
-theorem le_pred_of_lt (h : n < m) : n ≤ pred m := (le_pred_iff_lt (Nat.zero_lt_of_lt h)).2 h
-
-theorem exists_eq_succ_of_ne_zero : ∀ {n}, n ≠ 0 → ∃ k, n = succ k
-  | _+1, _ => ⟨_, rfl⟩
-
 /-! ## add -/
 
 protected theorem add_add_add_comm (a b c d : Nat) : (a + b) + (c + d) = (a + c) + (b + d) := by
@@ -131,15 +67,6 @@ protected theorem add_lt_add_of_lt_of_le {a b c d : Nat} (hlt : a < b) (hle : c
     a + c < b + d :=
   Nat.lt_of_le_of_lt (Nat.add_le_add_left hle _) (Nat.add_lt_add_right hlt _)
 
-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 ..)
-
-protected theorem lt_add_of_pos_right (h : 0 < k) : n < n + k :=
-  Nat.add_lt_add_left h n
-
 protected theorem lt_add_of_pos_left : 0 < k → n < k + n := by
   rw [Nat.add_comm]; exact Nat.lt_add_of_pos_right
 
@@ -249,8 +176,6 @@ theorem add_lt_of_lt_sub' {a b c : Nat} : b < c - a → a + b < c := by
 protected theorem sub_add_lt_sub (h₁ : m + k ≤ n) (h₂ : 0 < k) : n - (m + k) < n - m := by
   rw [← Nat.sub_sub]; exact Nat.sub_lt_of_pos_le h₂ (Nat.le_sub_of_add_le' h₁)
 
-theorem le_sub_one_of_lt : a < b → a ≤ b - 1 := Nat.le_pred_of_lt
-
 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₁
 
@@ -615,12 +540,6 @@ theorem le_of_mod_lt {a b : Nat} (h : a % b < a) : b ≤ a :=
 theorem mul_mod_mul_right (z x y : Nat) : (x * z) % (y * z) = (x % y) * z := by
   rw [Nat.mul_comm x z, Nat.mul_comm y z, Nat.mul_comm (x % y) z]; apply mul_mod_mul_left
 
-@[simp] theorem mod_mod_of_dvd (a : Nat) (h : c ∣ b) : a % b % c = a % c := by
-  rw (config := {occs := .pos [2]}) [← mod_add_div a b]
-  have ⟨x, h⟩ := h
-  subst h
-  rw [Nat.mul_assoc, add_mul_mod_self_left]
-
 theorem sub_mul_mod {x k n : Nat} (h₁ : n*k ≤ x) : (x - n*k) % n = x % n := by
   match k with
   | 0 => rw [Nat.mul_zero, Nat.sub_zero]

src/Init/Data/Nat/Linear.lean

@@ -4,10 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Coe
 import Init.ByCases
-import Init.Data.Nat.Basic
-import Init.Data.List.Basic
 import Init.Data.Prod
 
 namespace Nat.Linear
@@ -583,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; apply Nat.succ_ne_zero
+  have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp
   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/Log2.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
 prelude
-import Init.NotationExtra
 import Init.Data.Nat.Linear
 
 namespace Nat

src/Init/Omega/Int.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 prelude
-import Init.Data.Int.DivModLemmas
+import Init.Data.Int.DivMod
+import Init.Data.Int.Order
 import Init.Data.Nat.Basic
 
 /-!
@@ -48,7 +49,7 @@ theorem ofNat_shiftLeft_eq {x y : Nat} : (x <<< y : Int) = (x : Int) * (2 ^ y :
   simp [Nat.shiftLeft_eq]
 
 theorem ofNat_shiftRight_eq_div_pow {x y : Nat} : (x >>> y : Int) = (x : Int) / (2 ^ y : Nat) := by
-  simp [Nat.shiftRight_eq_div_pow]
+  simp only [Nat.shiftRight_eq_div_pow, Int.ofNat_ediv]
 
 -- FIXME these are insane:
 theorem lt_of_not_ge {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h