feat: more min/max lemmas for Nat (#196)

Std/Data/List/Lemmas.lean

@@ -177,7 +177,7 @@ theorem forall_mem_map_iff {f : α → β} {l : List α} {P : β → Prop} :
 @[simp] theorem length_zipWith (f : α → β → γ) (l₁ l₂) :
     length (zipWith f l₁ l₂) = min (length l₁) (length l₂) := by
   induction l₁ generalizing l₂ <;> cases l₂ <;>
-    simp_all [add_one, min_succ_succ, Nat.zero_min, Nat.min_zero]
+    simp_all [add_one, succ_min_succ, Nat.zero_min, Nat.min_zero]
 
 @[simp]
 theorem zipWith_map {μ} (f : γ → δ → μ) (g : α → γ) (h : β → δ) (l₁ : List α) (l₂ : List β) :
@@ -787,7 +787,7 @@ theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a
 @[simp] theorem length_take : ∀ (i : Nat) (l : List α), length (take i l) = min i (length l)
   | 0, l => by simp [Nat.zero_min]
   | succ n, [] => by simp [Nat.min_zero]
-  | succ n, _ :: l => by simp [Nat.min_succ_succ, add_one, length_take]
+  | succ n, _ :: l => by simp [Nat.succ_min_succ, add_one, length_take]
 
 theorem length_take_le (n) (l : List α) : length (take n l) ≤ n := by simp [Nat.min_le_left]
 

Std/Data/Nat/Lemmas.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Std.Logic
 import Std.Tactic.Basic
+import Std.Tactic.Alias
 import Std.Data.Nat.Init.Lemmas
 import Std.Data.Nat.Basic
 
@@ -453,48 +454,194 @@ protected theorem sub_add_lt_sub {n m k : Nat} (h₁ : m + k ≤ n) (h₂ : 0 <
 
 /-! ## min/max -/
 
+protected theorem min_eq_left {a b : Nat} (h : a ≤ b) : min a b = a := if_pos h
+
+protected theorem min_eq_right {a b : Nat} (h : b ≤ a) : min a b = b := by
+  rw [Nat.min_comm]; exact Nat.min_eq_left h
+
+protected theorem le_min_of_le_of_le {a b c : Nat} : a ≤ b → a ≤ c → a ≤ min b c := by
+  intros; cases Nat.le_total b c with
+  | inl h => rw [Nat.min_eq_left h]; assumption
+  | inr h => rw [Nat.min_eq_right h]; assumption
+
 protected theorem le_min {a b c : Nat} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c :=
   ⟨fun h => ⟨Nat.le_trans h (Nat.min_le_left ..), Nat.le_trans h (Nat.min_le_right ..)⟩,
-   fun ⟨h₁, h₂⟩ => by rw [Nat.min_def]; split <;> assumption⟩
+   fun ⟨h₁, h₂⟩ => Nat.le_min_of_le_of_le h₁ h₂⟩
 
 protected theorem lt_min {a b c : Nat} : a < min b c ↔ a < b ∧ a < c := Nat.le_min
 
-protected theorem min_eq_left {a b : Nat} (h : a ≤ b) : min a b = a := by simp [Nat.min_def, h]
+theorem succ_min_succ (x y) : min (succ x) (succ y) = succ (min x y) := by
+  cases Nat.le_total x y with
+  | inl h => rw [Nat.min_eq_left h, Nat.min_eq_left (Nat.succ_le_succ h)]
+  | inr h => rw [Nat.min_eq_right h, Nat.min_eq_right (Nat.succ_le_succ h)]
 
-protected theorem min_eq_right {a b : Nat} (h : b ≤ a) : min a b = b := by
-  rw [Nat.min_comm a b]; exact Nat.min_eq_left h
+@[simp] protected theorem min_self (a : Nat) : min a a = a := Nat.min_eq_left (Nat.le_refl _)
+
+@[simp] protected theorem zero_min (a) : min 0 a = 0 := Nat.min_eq_left (Nat.zero_le _)
+
+@[simp] protected theorem min_zero (a) : min a 0 = 0 := Nat.min_eq_right (Nat.zero_le _)
+
+protected theorem min_assoc : ∀ (a b c : Nat), min (min a b) c = min a (min b c)
+  | 0, _, _ => by rw [Nat.zero_min, Nat.zero_min, Nat.zero_min]
+  | _, 0, _ => by rw [Nat.zero_min, Nat.min_zero, Nat.zero_min]
+  | _, _, 0 => by rw [Nat.min_zero, Nat.min_zero, Nat.min_zero]
+  | _+1, _+1, _+1 => by simp only [Nat.succ_min_succ]; exact congrArg succ <| Nat.min_assoc ..
+
+protected theorem sub_sub_eq_min : ∀ (a b : Nat), a - (a - b) = min a b
+  | 0, _ => by rw [Nat.zero_sub, Nat.zero_min]
+  | _, 0 => by rw [Nat.sub_zero, Nat.sub_self, Nat.min_zero]
+  | _+1, _+1 => by
+    rw [Nat.succ_sub_succ, Nat.succ_min_succ, Nat.succ_sub (Nat.sub_le ..)]
+    exact congrArg succ <| Nat.sub_sub_eq_min ..
 
-protected theorem zero_min (a : Nat) : min 0 a = 0 := Nat.min_eq_left (zero_le a)
+protected theorem sub_eq_sub_min (n m : Nat) : n - m = n - min n m := by
+  cases Nat.le_total n m with
+  | inl h => rw [Nat.min_eq_left h, Nat.sub_eq_zero_of_le h, Nat.sub_self]
+  | inr h => rw [Nat.min_eq_right h]
 
-protected theorem min_zero (a : Nat) : min a 0 = 0 := Nat.min_eq_right (zero_le a)
+@[simp] protected theorem sub_add_min_cancel (n m : Nat) : n - m + min n m = n := by
+  rw [Nat.sub_eq_sub_min, Nat.sub_add_cancel (Nat.min_le_left ..)]
+
+protected theorem max_eq_right {a b : Nat} (h : a ≤ b) : max a b = b := if_pos h
+
+protected theorem max_eq_left {a b : Nat} (h : b ≤ a) : max a b = a := by
+  rw [Nat.max_comm]; exact Nat.max_eq_right h
+
+protected theorem succ_max_succ (x y) : max (succ x) (succ y) = succ (max x y) := by
+  cases Nat.le_total x y with
+  | inl h => rw [Nat.max_eq_right h, Nat.max_eq_right (Nat.succ_le_succ h)]
+  | inr h => rw [Nat.max_eq_left h, Nat.max_eq_left (Nat.succ_le_succ h)]
+
+protected theorem max_le_of_le_of_le {a b c : Nat} : a ≤ c → b ≤ c → max a b ≤ c := by
+  intros; cases Nat.le_total a b with
+  | inl h => rw [Nat.max_eq_right h]; assumption
+  | inr h => rw [Nat.max_eq_left h]; assumption
 
 protected theorem max_le {a b c : Nat} : max a b ≤ c ↔ a ≤ c ∧ b ≤ c :=
   ⟨fun h => ⟨Nat.le_trans (Nat.le_max_left ..) h, Nat.le_trans (Nat.le_max_right ..) h⟩,
-   fun ⟨h₁, h₂⟩ => by rw [Nat.max_def]; split <;> assumption⟩
+   fun ⟨h₁, h₂⟩ => Nat.max_le_of_le_of_le h₁ h₂⟩
 
-protected theorem max_eq_right {a b : Nat} (h : a ≤ b) : max a b = b := by
-  simp [Nat.max_def, h, Nat.not_lt.2 h]
+protected theorem max_lt {a b c : Nat} : max a b < c ↔ a < c ∧ b < c := by
+  rw [← Nat.succ_le, ← Nat.succ_max_succ a b]; exact Nat.max_le
 
-protected theorem max_eq_left {a b : Nat} (h : b ≤ a) : max a b = a := by
-  rw [← Nat.max_comm b a]; exact Nat.max_eq_right h
+@[simp] protected theorem max_self (a : Nat) : max a a = a := Nat.max_eq_right (Nat.le_refl _)
 
--- Distribute succ over min
-theorem min_succ_succ (x y : Nat) : min (succ x) (succ y) = succ (min x y) := by
-  simp [Nat.min_def, succ_le_succ_iff]; split <;> rfl
+@[simp] protected theorem zero_max (a) : max 0 a = a := Nat.max_eq_right (Nat.zero_le _)
 
-theorem sub_eq_sub_min (n m : Nat) : n - m = n - min n m := by
-  rw [Nat.min_def]; split
-  · rw [Nat.sub_eq_zero_of_le ‹n ≤ m›, Nat.sub_self]
-  · rfl
+@[simp] protected theorem max_zero (a) : max a 0 = a := Nat.max_eq_left (Nat.zero_le _)
 
-@[simp] protected theorem sub_add_min_cancel (n m : Nat) : n - m + min n m = n := by
-  rw [sub_eq_sub_min, Nat.sub_add_cancel (Nat.min_le_left n m)]
+protected theorem max_assoc : ∀ (a b c : Nat), max (max a b) c = max a (max b c)
+  | 0, _, _ => by rw [Nat.zero_max, Nat.zero_max]
+  | _, 0, _ => by rw [Nat.zero_max, Nat.max_zero]
+  | _, _, 0 => by rw [Nat.max_zero, Nat.max_zero]
+  | _+1, _+1, _+1 => by simp only [Nat.succ_max_succ]; exact congrArg succ <| Nat.max_assoc ..
 
-protected theorem sub_add_eq_max {a b : Nat} : a - b + b = max a b := by
-  match a.le_total b with
+protected theorem sub_add_eq_max (a b : Nat) : a - b + b = max a b := by
+  match Nat.le_total a b with
   | .inl hl => rw [Nat.max_eq_right hl, Nat.sub_eq_zero_iff_le.mpr hl, Nat.zero_add]
   | .inr hr => rw [Nat.max_eq_left hr, Nat.sub_add_cancel hr]
 
+protected theorem sub_eq_max_sub (n m : Nat) : n - m = max n m - m := by
+  cases Nat.le_total m n with
+  | inl h => rw [Nat.max_eq_left h]
+  | inr h => rw [Nat.max_eq_right h, Nat.sub_eq_zero_of_le h, Nat.sub_self]
+
+protected theorem max_min_distrib_left : ∀ (a b c : Nat), max a (min b c) = min (max a b) (max a c)
+  | 0, _, _ => by simp only [Nat.zero_max]
+  | _, 0, _ => by
+    rw [Nat.zero_min, Nat.max_zero]
+    exact Nat.min_eq_left (Nat.le_max_left ..) |>.symm
+  | _, _, 0 => by
+    rw [Nat.min_zero, Nat.max_zero]
+    exact Nat.min_eq_right (Nat.le_max_left ..) |>.symm
+  | _+1, _+1, _+1 => by
+    simp only [Nat.succ_max_succ, Nat.succ_min_succ]
+    exact congrArg succ <| Nat.max_min_distrib_left ..
+
+protected theorem min_max_distrib_left : ∀ (a b c : Nat), min a (max b c) = max (min a b) (min a c)
+  | 0, _, _ => by simp only [Nat.zero_min]
+  | _, 0, _ => by simp only [Nat.min_zero, Nat.zero_max]
+  | _, _, 0 => by simp only [Nat.min_zero, Nat.max_zero]
+  | _+1, _+1, _+1 => by
+    simp only [Nat.succ_max_succ, Nat.succ_min_succ]
+    exact congrArg succ <| Nat.min_max_distrib_left ..
+
+protected theorem max_min_distrib_right (a b c : Nat) :
+    max (min a b) c = min (max a c) (max b c) := by
+  repeat rw [Nat.max_comm _ c]
+  exact Nat.max_min_distrib_left ..
+
+protected theorem min_max_distrib_right (a b c : Nat) :
+    min (max a b) c = max (min a c) (min b c) := by
+  repeat rw [Nat.min_comm _ c]
+  exact Nat.min_max_distrib_left ..
+
+protected theorem add_max_add_right : ∀ (a b c : Nat), max (a + c) (b + c) = max a b + c
+  | _, _, 0 => rfl
+  | _, _, _+1 => Eq.trans (Nat.succ_max_succ ..) <| congrArg _ (Nat.add_max_add_right ..)
+
+protected theorem add_min_add_right : ∀ (a b c : Nat), min (a + c) (b + c) = min a b + c
+  | _, _, 0 => rfl
+  | _, _, _+1 => Eq.trans (Nat.succ_min_succ ..) <| congrArg _ (Nat.add_min_add_right ..)
+
+protected theorem add_max_add_left (a b c : Nat) : max (a + b) (a + c) = a + max b c := by
+  repeat rw [Nat.add_comm a]
+  exact Nat.add_max_add_right ..
+
+protected theorem add_min_add_left (a b c : Nat) : min (a + b) (a + c) = a + min b c := by
+  repeat rw [Nat.add_comm a]
+  exact Nat.add_min_add_right ..
+
+protected theorem pred_min_pred : ∀ (x y), min (pred x) (pred y) = pred (min x y)
+  | 0, _ => by simp only [Nat.pred_zero, Nat.zero_min]
+  | _, 0 => by simp only [Nat.pred_zero, Nat.min_zero]
+  | _+1, _+1 => by simp only [Nat.pred_succ, Nat.succ_min_succ]
+
+protected theorem pred_max_pred : ∀ (x y), max (pred x) (pred y) = pred (max x y)
+  | 0, _ => by simp only [Nat.pred_zero, Nat.zero_max]
+  | _, 0 => by simp only [Nat.pred_zero, Nat.max_zero]
+  | _+1, _+1 => by simp only [Nat.pred_succ, Nat.succ_max_succ]
+
+protected theorem sub_min_sub_right : ∀ (a b c : Nat), min (a - c) (b - c) = min a b - c
+  | _, _, 0 => rfl
+  | _, _, _+1 => Eq.trans (Nat.pred_min_pred ..) <| congrArg _ (Nat.sub_min_sub_right ..)
+
+protected theorem sub_max_sub_right : ∀ (a b c : Nat), max (a - c) (b - c) = max a b - c
+  | _, _, 0 => rfl
+  | _, _, _+1 => Eq.trans (Nat.pred_max_pred ..) <| congrArg _ (Nat.sub_max_sub_right ..)
+
+protected theorem sub_min_sub_left (a b c : Nat) : min (a - b) (a - c) = a - max b c := by
+  induction b, c using Nat.recDiagAux with
+  | zero_left => rw [Nat.sub_zero, Nat.zero_max]; exact Nat.min_eq_right (Nat.sub_le ..)
+  | zero_right => rw [Nat.sub_zero, Nat.max_zero]; exact Nat.min_eq_left (Nat.sub_le ..)
+  | succ_succ _ _ ih => simp only [Nat.sub_succ, Nat.succ_max_succ, Nat.pred_min_pred, ih]
+
+protected theorem sub_max_sub_left (a b c : Nat) : max (a - b) (a - c) = a - min b c := by
+  induction b, c using Nat.recDiagAux with
+  | zero_left => rw [Nat.sub_zero, Nat.zero_min]; exact Nat.max_eq_left (Nat.sub_le ..)
+  | zero_right => rw [Nat.sub_zero, Nat.min_zero]; exact Nat.max_eq_right (Nat.sub_le ..)
+  | succ_succ _ _ ih => simp only [Nat.sub_succ, Nat.succ_min_succ, Nat.pred_max_pred, ih]
+
+protected theorem mul_max_mul_right (a b c : Nat) : max (a * c) (b * c) = max a b * c := by
+  induction a, b using Nat.recDiagAux with
+  | zero_left => simp only [Nat.zero_mul, Nat.zero_max]
+  | zero_right => simp only [Nat.zero_mul, Nat.max_zero]
+  | succ_succ _ _ ih => simp only [Nat.succ_mul, Nat.add_max_add_right, ih]
+
+protected theorem mul_min_mul_right (a b c : Nat) : min (a * c) (b * c) = min a b * c := by
+  induction a, b using Nat.recDiagAux with
+  | zero_left => simp only [Nat.zero_mul, Nat.zero_min]
+  | zero_right => simp only [Nat.zero_mul, Nat.min_zero]
+  | succ_succ _ _ ih => simp only [Nat.succ_mul, Nat.add_min_add_right, ih]
+
+protected theorem mul_max_mul_left (a b c : Nat) : max (a * b) (a * c) = a * max b c := by
+  repeat rw [Nat.mul_comm a]
+  exact Nat.mul_max_mul_right ..
+
+protected theorem mul_min_mul_left (a b c : Nat) : min (a * b) (a * c) = a * min b c := by
+  repeat rw [Nat.mul_comm a]
+  exact Nat.mul_min_mul_right ..
+
 /-! ## mul -/
 
 protected theorem mul_right_comm (n m k : Nat) : n * m * k = n * k * m := by